A forum for Spin users
You are not logged in.
Pages: 1
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
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
Best, didn't know that, thank you!!
Offline
Pages: 1