A forum for Spin users
You are not logged in.
a model with
bit a,b,c,d,e,f,g
what is the best LTL way to express and test, if c,d,e are getting true in sequence AND
not "being interrupted" by an event with setting a,b,f or g true?
so the combination of a,b,f,g before c = 1
d=1
e=1
should be the same as behind e = 1
Thank you very much!!
the manual states
"The two statement separators are equivalent."
http://spinroot.com/spin/Man/Manual.html
is there really no exception? I ask because I'd like to prefer ; but I don't want to write a wrong recommendation :-)
So I can say, "->" can always be replaced by ";"?
http://spinroot.com/fluxbb/viewtopic.php?id=857
was read
ok, thank you!!
Best, didn't know that, thank you!!
but remoterefs are only accessible inside of never claims, aren't they?
I have to model subprocesses and I want process A to check if process B and other processes are in a valid end state. If and only if B and n processes are in end-states, go on with A.
I've got a workaround now, but it's work. Is there no easy way for doing so?
sorry, now I've found it:
http://spinroot.com/spin/Man/end.html
although, "-q require empty chans in valid end states"
is missing in
"SPIN --"
so, "spin -run -q file.pml" does the job
I'm not sure but I think once I've read SPIN checks emptiness of all channels at the end, is this correct?
Or do I have to check the emptiness with a never claim on my own?
[CODE]
never { /* []!(<>[](empty(c0) && empty(c1) && empty(c2) && empty(c3) && empty(c4))) */
T0_init:
do
:: ( ((nempty(c0) || nempty(c1) || nempty(c2) || nempty(c3) || nempty(c4)))) -> goto accept_S9
:: (1) -> goto T0_init
od;
accept_S9:
do
:: (1) -> goto T0_init
od;
}
[/CODE]