Spinroot

A forum for Spin users

You are not logged in.

#1 2019-07-08 05:06:04

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)

Offline

#2 2019-07-08 16:45:32

spinroot
forum
Registered: 2010-11-18
Posts: 695
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

Offline

#3 2019-07-09 08:54:22

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

Offline

#4 2019-07-09 18:28:41

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: -ltl vs 2 never claims inside

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

Offline

#5 2019-07-10 03:27:45

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

Offline

#6 2019-07-10 16:15:28

spinroot
forum
Registered: 2010-11-18
Posts: 695
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

Offline

#7 2019-07-12 04:44:25

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)

Offline

Board footer

Powered by FluxBB