Spinroot

marc15

Member

Registered: 2019-02-07

Posts: 34

-ltl vs 2 never claims inside

when I've got 2 never claims inside a model, I can address the 2nd never claim with ''spin -run -ltl never_1 -a model.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)

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: -ltl vs 2 never claims inside

it should work, yes, but for the replay you should also give the same never claim name

marc15

Member

Registered: 2019-02-07

Posts: 34

Re: -ltl vs 2 never claims inside

perfect, this works!!
sorry for not reading :-(

./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'
?

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: -ltl vs 2 never claims inside

does spin -replay -noclaim file.pml not work?

marc15

Member

Registered: 2019-02-07

Posts: 34

Re: -ltl vs 2 never claims inside

:-) not when my mind is on the trace of -N

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??

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: -ltl vs 2 never claims inside

spinroot.com/spin/Man/promela.html  has manual pages -- check the one for np_
spin --  will give an overview of the main command-line arguments
pan -- will do the same for the executable analyzer

marc15

Member

Registered: 2019-02-07

Posts: 34

Re: -ltl vs 2 never claims inside

If the manual pages and your help were so good, I wouldn't have been at the point to ask questions.

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)