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 ifs have been changed into dos, 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.