yes, of course, the manual helps and it helps to know there is the answer;
so for me it's to name the claim
never npc { /* <>[] np_ */
do
:: true
:: np_ -> break
od;
accept: do
:: np_
od
}
spin -run -ltl npc file.pml
./pan -r -v -N npc
(otherwise the spin output 'the model contains ...' doesn't contain a name for the np_ claim)
]]>yes, of course, this works, Thank you!!
but lost again, cannot find the name for np_
how can I address non-progress cycles,
'spin -t -k file.pml.trail -r -s file.pml' would work, but I like more the trail with './pan -r -v'
./pan -r -v -N ??non-progress cycles??
]]>./pan -r -v -N ltl_or_never_claim_name [or e.g. never_0]
but how can I address the counterexample for invalid end states
after
'spin -run -noclaim file.pml'
?
But if there should be a counterexample, I'm getting in trouble.
Therefore my question, should this work with 2 never claims inside?
(with ltl-formulae it works)