add option to output neverclaims in spin 6.2.4's format
In 2013 Spin 6.2.4 changed the way it outputs neverclaim. The current parser can read both styles, but so far we only output the old style.
Compare:
% spin-6.2.2 -f '<>a || []b'
never { /* <>a || []b */
T0_init:
if
:: ((b)) -> goto accept_S2
:: ((a)) -> goto accept_all
:: (1) -> goto T0_S5
fi;
accept_S2:
if
:: ((b)) -> goto accept_S2
fi;
T0_S5:
if
:: ((a)) -> goto accept_all
:: (1) -> goto T0_S5
fi;
accept_all:
skip
}
% spin-6.4.3 -f '<>a || []b'
never { /* <>a || []b */
T0_init:
do
:: ((b)) -> goto accept_S2
:: atomic { ((a)) -> assert(!((a))) }
:: (1) -> goto T0_S5
od;
accept_S2:
do
:: ((b)) -> goto accept_S2
od;
T0_S5:
do
:: atomic { ((a)) -> assert(!((a))) }
:: (1) -> goto T0_S5
od;
accept_all:
skip
}
So if
s have been changed into do
s, and transitions to accept_all:
have been replaced by these atomic
/assert
combinations. IIRC Holzmann said this improves counterexamples. I do not know if the accept_all:
state is necessary in the new format.