warning: for p.o. reduction to be valid the never claim must be stutter-closed
(never claims generated from LTL formulae are stutter-closed)
(Spin Version 3.4.13 -- 31 January 2002)
        + Partial Order Reduction

Full statespace search for:
        never-claim             +
        assertion violations    + (if within scope of claim)
        acceptance   cycles     + (fairness disabled)
        invalid endstates       - (disabled by never-claim)

State-vector 76 byte, depth reached 43, errors: 0
    7179 states, stored
   24911 states, matched
   32090 transitions (= stored+matched)
   70520 atomic steps
hash conflicts: 5809 (resolved)
(max size 2^19 states)

Stats on memory usage (in Megabytes):
0.603   equivalent memory usage for states (stored*(State-vector + overhead))
0.584   actual memory usage for states (compression: 96.77%)
        State-vector as stored = 73 byte + 8 byte overhead
2.097   memory used for hash-table (-w19)
0.240   memory used for DFS stack (-m10000)
2.849   total actual memory usage

unreached in proctype PIni
        (0 of 22 states)
unreached in proctype PRes
        (0 of 22 states)
unreached in proctype PI
        line 293, state 214, "-end-"
        (28 of 214 states)
unreached in proctype :init:
        (0 of 12 states)

real       10.8
user       10.7
sys         0.0