Spinroot

A forum for Spin users

You are not logged in.

#1 2019-02-11 18:35:18

marc15
Member
Registered: 2019-02-07
Posts: 34

final check if all channels are empty

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]

Offline

#2 2019-02-11 18:54:53

marc15
Member
Registered: 2019-02-07
Posts: 34

Re: final check if all channels are empty

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

Offline

#3 2019-02-11 20:15:54

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

Re: final check if all channels are empty

good point, but most runtime flags aren't mentioned in spin -- (since that's focused on spin flags proper.  the runtime flags can be seen with ./pan --, and the explanation of -q appears there)

Offline

#4 2019-02-11 22:43:52

marc15
Member
Registered: 2019-02-07
Posts: 34

Re: final check if all channels are empty

Best, didn't know that, thank you!!

Offline

Board footer

Powered by FluxBB