warning: for p.o. reduction to be valid the never claim must be stutter-invariant (never claims generated from LTL formulae are stutter-invariant) Changing debug level from 0 to -1 Using 1015 state memory Using 12 stats memory cpu2: Depth= 27 States= 1e+06 Transitions= 1.59882e+06 Memory= 0.000 warning: for p.o. reduction to be valid the never claim must be stutter-invariant (never claims generated from LTL formulae are stutter-invariant) Changing debug level from 0 to -1 Using 1015 state memory Using 12 stats memory cpu4: Depth= 27 States= 1e+06 Transitions= 1.65873e+06 Memory= 0.000 warning: for p.o. reduction to be valid the never claim must be stutter-invariant (never claims generated from LTL formulae are stutter-invariant) Changing debug level from 0 to -1 Using 1015 state memory Using 12 stats memory cpu1: Depth= 27 States= 1e+06 Transitions= 1.57518e+06 Memory= 0.000 warning: for p.o. reduction to be valid the never claim must be stutter-invariant (never claims generated from LTL formulae are stutter-invariant) Changing debug level from 0 to -1 Using 1015 state memory Using 12 stats memory cpu3: Depth= 27 States= 1e+06 Transitions= 1.41586e+06 Memory= 0.000 warning: for p.o. reduction to be valid the never claim must be stutter-invariant (never claims generated from LTL formulae are stutter-invariant) Changing debug level from 0 to -1 Using 1015 state memory Using 12 stats memory cpu0: Depth= 27 States= 1e+06 Transitions= 1.28591e+06 Memory= 448.654 cpu1: Depth= 27 States= 2e+06 Transitions= 3.2825e+06 Memory= 0.000 cpu4: Depth= 27 States= 2e+06 Transitions= 3.17265e+06 Memory= 0.000 cpu2: Depth= 27 States= 2e+06 Transitions= 2.64274e+06 Memory= 0.000 cpu0: Depth= 27 States= 2e+06 Transitions= 2.84474e+06 Memory= 448.654 cpu3: Depth= 27 States= 2e+06 Transitions= 3.08566e+06 Memory= 0.000 cpu1: Depth= 27 States= 3e+06 Transitions= 4.9711e+06 Memory= 0.000 cpu0: Depth= 27 States= 3e+06 Transitions= 4.50224e+06 Memory= 448.654 cpu2: Depth= 27 States= 3e+06 Transitions= 4.01244e+06 Memory= 0.000 cpu4: Depth= 27 States= 3e+06 Transitions= 4.21485e+06 Memory= 0.000 cpu1: Depth= 27 States= 4e+06 Transitions= 6.11682e+06 Memory= 0.000 cpu3: Depth= 27 States= 3e+06 Transitions= 4.76097e+06 Memory= 0.000 cpu0: Depth= 27 States= 4e+06 Transitions= 6.18095e+06 Memory= 448.654 cpu2: Depth= 27 States= 4e+06 Transitions= 5.62245e+06 Memory= 0.000 cpu4: Depth= 27 States= 4e+06 Transitions= 5.24867e+06 Memory= 0.000 cpu1: Depth= 27 States= 5e+06 Transitions= 7.15512e+06 Memory= 0.000 cpu3: Depth= 27 States= 4e+06 Transitions= 6.38384e+06 Memory= 0.000 cpu0: Depth= 27 States= 5e+06 Transitions= 7.84476e+06 Memory= 448.654 cpu2: Depth= 27 States= 5e+06 Transitions= 7.24468e+06 Memory= 0.000 cpu4: Depth= 27 States= 5e+06 Transitions= 6.61614e+06 Memory= 0.000 cpu3: Depth= 27 States= 5e+06 Transitions= 7.58838e+06 Memory= 0.000 cpu0: Depth= 27 States= 6e+06 Transitions= 9.48852e+06 Memory= 448.654 cpu1: Depth= 27 States= 6e+06 Transitions= 8.19484e+06 Memory= 0.000 cpu2: Depth= 27 States= 6e+06 Transitions= 8.89583e+06 Memory= 0.000 cpu4: Depth= 27 States= 6e+06 Transitions= 8.09829e+06 Memory= 0.000 cpu3: Depth= 27 States= 6e+06 Transitions= 8.63074e+06 Memory= 0.000 cpu0: Depth= 27 States= 7e+06 Transitions= 1.10874e+07 Memory= 448.654 cpu1: Depth= 27 States= 7e+06 Transitions= 9.21639e+06 Memory= 0.000 cpu2: Depth= 27 States= 7e+06 Transitions= 1.04928e+07 Memory= 0.000 cpu0: Depth= 27 States= 8e+06 Transitions= 1.23263e+07 Memory= 448.654 cpu4: Depth= 27 States= 7e+06 Transitions= 9.74121e+06 Memory= 0.000 cpu1: Depth= 27 States= 8e+06 Transitions= 1.05906e+07 Memory= 0.000 cpu3: Depth= 27 States= 7e+06 Transitions= 9.66743e+06 Memory= 0.000 cpu2: Depth= 27 States= 8e+06 Transitions= 1.21224e+07 Memory= 0.000 cpu0: Depth= 27 States= 9e+06 Transitions= 1.33662e+07 Memory= 448.654 cpu4: Depth= 27 States= 8e+06 Transitions= 1.12846e+07 Memory= 0.000 cpu1: Depth= 27 States= 9e+06 Transitions= 1.20747e+07 Memory= 0.000 cpu3: Depth= 27 States= 8e+06 Transitions= 1.06937e+07 Memory= 0.000 cpu2: Depth= 27 States= 9e+06 Transitions= 1.36504e+07 Memory= 0.000 cpu0: Depth= 27 States= 1e+07 Transitions= 1.44037e+07 Memory= 448.654 cpu4: Depth= 27 States= 9e+06 Transitions= 1.29188e+07 Memory= 0.000 cpu1: Depth= 27 States= 1e+07 Transitions= 1.36336e+07 Memory= 0.000 cpu2: Depth= 27 States= 1e+07 Transitions= 1.5065e+07 Memory= 0.000 cpu3: Depth= 27 States= 9e+06 Transitions= 1.17645e+07 Memory= 0.000 cpu0: Depth= 27 States= 1.1e+07 Transitions= 1.54464e+07 Memory= 448.654 cpu2: Depth= 27 States= 1.1e+07 Transitions= 1.6105e+07 Memory= 0.000 cpu4: Depth= 27 States= 1e+07 Transitions= 1.44837e+07 Memory= 0.000 cpu1: Depth= 27 States= 1.1e+07 Transitions= 1.51721e+07 Memory= 0.000 cpu3: Depth= 27 States= 1e+07 Transitions= 1.31179e+07 Memory= 0.000 cpu0: Depth= 27 States= 1.2e+07 Transitions= 1.64813e+07 Memory= 448.654 cpu2: Depth= 27 States= 1.2e+07 Transitions= 1.71387e+07 Memory= 0.000 cpu4: Depth= 27 States= 1.1e+07 Transitions= 1.59801e+07 Memory= 0.000 cpu1: Depth= 27 States= 1.2e+07 Transitions= 1.67411e+07 Memory= 0.000 cpu0: Depth= 27 States= 1.3e+07 Transitions= 1.7507e+07 Memory= 448.654 cpu2: Depth= 27 States= 1.3e+07 Transitions= 1.81782e+07 Memory= 0.000 cpu3: Depth= 27 States= 1.1e+07 Transitions= 1.46352e+07 Memory= 0.000 cpu4: Depth= 27 States= 1.2e+07 Transitions= 1.75142e+07 Memory= 0.000 cpu1: Depth= 27 States= 1.3e+07 Transitions= 1.82604e+07 Memory= 0.000 cpu0: Depth= 27 States= 1.4e+07 Transitions= 1.86129e+07 Memory= 448.654 cpu2: Depth= 27 States= 1.4e+07 Transitions= 1.92208e+07 Memory= 0.000 cpu3: Depth= 27 States= 1.2e+07 Transitions= 1.61076e+07 Memory= 0.000 cpu4: Depth= 27 States= 1.3e+07 Transitions= 1.86838e+07 Memory= 0.000 cpu1: Depth= 27 States= 1.4e+07 Transitions= 1.97597e+07 Memory= 0.000 cpu0: Depth= 27 States= 1.5e+07 Transitions= 1.99508e+07 Memory= 448.654 cpu2: Depth= 27 States= 1.5e+07 Transitions= 2.02615e+07 Memory= 0.000 cpu4: Depth= 27 States= 1.4e+07 Transitions= 1.97178e+07 Memory= 0.000 cpu3: Depth= 27 States= 1.3e+07 Transitions= 1.75737e+07 Memory= 0.000 cpu1: Depth= 27 States= 1.5e+07 Transitions= 2.12832e+07 Memory= 0.000 cpu0: Depth= 27 States= 1.6e+07 Transitions= 2.14006e+07 Memory= 448.654 cpu2: Depth= 27 States= 1.6e+07 Transitions= 2.12885e+07 Memory= 0.000 cpu4: Depth= 27 States= 1.5e+07 Transitions= 2.07675e+07 Memory= 0.000 cpu3: Depth= 27 States= 1.4e+07 Transitions= 1.9088e+07 Memory= 0.000 cpu2: Depth= 27 States= 1.7e+07 Transitions= 2.23301e+07 Memory= 0.000 cpu0: Depth= 27 States= 1.7e+07 Transitions= 2.29282e+07 Memory= 448.654 cpu1: Depth= 27 States= 1.6e+07 Transitions= 2.27701e+07 Memory= 0.000 cpu4: Depth= 27 States= 1.6e+07 Transitions= 2.18092e+07 Memory= 0.000 cpu2: Depth= 27 States= 1.8e+07 Transitions= 2.35403e+07 Memory= 0.000 cpu1: Depth= 27 States= 1.7e+07 Transitions= 2.39219e+07 Memory= 0.000 cpu0: Depth= 27 States= 1.8e+07 Transitions= 2.43912e+07 Memory= 448.654 cpu3: Depth= 27 States= 1.5e+07 Transitions= 2.05286e+07 Memory= 0.000 cpu4: Depth= 27 States= 1.7e+07 Transitions= 2.28535e+07 Memory= 0.000 cpu1: Depth= 27 States= 1.8e+07 Transitions= 2.49801e+07 Memory= 0.000 cpu2: Depth= 27 States= 1.9e+07 Transitions= 2.48808e+07 Memory= 0.000 cpu0: Depth= 27 States= 1.9e+07 Transitions= 2.59433e+07 Memory= 448.654 cpu4: Depth= 27 States= 1.8e+07 Transitions= 2.38972e+07 Memory= 0.000 cpu3: Depth= 27 States= 1.6e+07 Transitions= 2.19851e+07 Memory= 0.000 cpu1: Depth= 27 States= 1.9e+07 Transitions= 2.60283e+07 Memory= 0.000 cpu2: Depth= 27 States= 2e+07 Transitions= 2.63467e+07 Memory= 0.000 cpu4: Depth= 27 States= 1.9e+07 Transitions= 2.49413e+07 Memory= 0.000 cpu0: Depth= 27 States= 2e+07 Transitions= 2.74325e+07 Memory= 448.654 cpu3: Depth= 27 States= 1.7e+07 Transitions= 2.343e+07 Memory= 0.000 cpu1: Depth= 27 States= 2e+07 Transitions= 2.7075e+07 Memory= 0.000 cpu2: Depth= 27 States= 2.1e+07 Transitions= 2.78617e+07 Memory= 0.000 cpu4: Depth= 27 States= 2e+07 Transitions= 2.5993e+07 Memory= 0.000 cpu0: Depth= 27 States= 2.1e+07 Transitions= 2.88978e+07 Memory= 448.654 cpu1: Depth= 27 States= 2.1e+07 Transitions= 2.81245e+07 Memory= 0.000 cpu3: Depth= 27 States= 1.8e+07 Transitions= 2.47793e+07 Memory= 0.000 cpu2: Depth= 27 States= 2.2e+07 Transitions= 2.9388e+07 Memory= 0.000 cpu4: Depth= 27 States= 2.1e+07 Transitions= 2.72191e+07 Memory= 0.000 cpu0: Depth= 27 States= 2.2e+07 Transitions= 3.0408e+07 Memory= 448.654 cpu3: Depth= 27 States= 1.9e+07 Transitions= 2.58379e+07 Memory= 0.000 cpu1: Depth= 27 States= 2.2e+07 Transitions= 2.9178e+07 Memory= 0.000 cpu2: Depth= 27 States= 2.3e+07 Transitions= 3.0895e+07 Memory= 0.000 cpu4: Depth= 27 States= 2.2e+07 Transitions= 2.85596e+07 Memory= 0.000 cpu0: Depth= 27 States= 2.3e+07 Transitions= 3.18689e+07 Memory= 448.654 cpu1: Depth= 27 States= 2.3e+07 Transitions= 3.02299e+07 Memory= 0.000 cpu3: Depth= 27 States= 2e+07 Transitions= 2.68859e+07 Memory= 0.000 cpu2: Depth= 27 States= 2.4e+07 Transitions= 3.23435e+07 Memory= 0.000 cpu4: Depth= 27 States= 2.3e+07 Transitions= 3.00213e+07 Memory= 0.000 cpu1: Depth= 27 States= 2.4e+07 Transitions= 3.1292e+07 Memory= 0.000 cpu3: Depth= 27 States= 2.1e+07 Transitions= 2.79452e+07 Memory= 0.000 cpu0: Depth= 27 States= 2.4e+07 Transitions= 3.33078e+07 Memory= 448.654 cpu2: Depth= 27 States= 2.5e+07 Transitions= 3.38366e+07 Memory= 0.000 cpu4: Depth= 27 States= 2.4e+07 Transitions= 3.15269e+07 Memory= 0.000 cpu0: Depth= 27 States= 2.5e+07 Transitions= 3.45089e+07 Memory= 448.654 cpu1: Depth= 27 States= 2.5e+07 Transitions= 3.25309e+07 Memory= 0.000 cpu3: Depth= 27 States= 2.2e+07 Transitions= 2.90045e+07 Memory= 0.000 cpu2: Depth= 27 States= 2.6e+07 Transitions= 3.52986e+07 Memory= 0.000 cpu4: Depth= 27 States= 2.5e+07 Transitions= 3.30199e+07 Memory= 0.000 cpu0: Depth= 27 States= 2.6e+07 Transitions= 3.55698e+07 Memory= 448.654 cpu3: Depth= 27 States= 2.3e+07 Transitions= 3.00687e+07 Memory= 0.000 cpu1: Depth= 27 States= 2.6e+07 Transitions= 3.38437e+07 Memory= 0.000 cpu3: Depth= 27 States= 2.4e+07 Transitions= 3.11316e+07 Memory= 0.000 cpu2: Depth= 27 States= 2.7e+07 Transitions= 3.67146e+07 Memory= 0.000 cpu4: Depth= 27 States= 2.6e+07 Transitions= 3.45133e+07 Memory= 0.000 cpu0: Depth= 27 States= 2.7e+07 Transitions= 3.66314e+07 Memory= 448.654 cpu1: Depth= 27 States= 2.7e+07 Transitions= 3.53424e+07 Memory= 0.000 cpu2: Depth= 27 States= 2.8e+07 Transitions= 3.8127e+07 Memory= 0.000 cpu3: Depth= 27 States= 2.5e+07 Transitions= 3.22659e+07 Memory= 0.000 cpu4: Depth= 27 States= 2.7e+07 Transitions= 3.60081e+07 Memory= 0.000 cpu1: Depth= 27 States= 2.8e+07 Transitions= 3.68795e+07 Memory= 0.000 cpu0: Depth= 27 States= 2.8e+07 Transitions= 3.77129e+07 Memory= 448.654 cpu2: Depth= 27 States= 2.9e+07 Transitions= 3.92043e+07 Memory= 0.000 cpu1: Depth= 27 States= 2.9e+07 Transitions= 3.83922e+07 Memory= 0.000 cpu4: Depth= 27 States= 2.8e+07 Transitions= 3.74909e+07 Memory= 0.000 cpu0: Depth= 27 States= 2.9e+07 Transitions= 3.87895e+07 Memory= 448.654 cpu3: Depth= 27 States= 2.6e+07 Transitions= 3.3586e+07 Memory= 0.000 cpu1: Depth= 27 States= 3e+07 Transitions= 3.99264e+07 Memory= 0.000 cpu4: Depth= 27 States= 2.9e+07 Transitions= 3.89168e+07 Memory= 0.000 cpu2: Depth= 27 States= 3e+07 Transitions= 4.0292e+07 Memory= 0.000 cpu0: Depth= 27 States= 3e+07 Transitions= 3.98685e+07 Memory= 448.654 cpu3: Depth= 27 States= 2.7e+07 Transitions= 3.50825e+07 Memory= 0.000 cpu1: Depth= 27 States= 3.1e+07 Transitions= 4.14306e+07 Memory= 0.000 cpu4: Depth= 27 States= 3e+07 Transitions= 4.03472e+07 Memory= 0.000 cpu0: Depth= 27 States= 3.1e+07 Transitions= 4.10796e+07 Memory= 448.654 cpu2: Depth= 27 States= 3.1e+07 Transitions= 4.13862e+07 Memory= 0.000 cpu3: Depth= 27 States= 2.8e+07 Transitions= 3.65907e+07 Memory= 0.000 cpu1: Depth= 27 States= 3.2e+07 Transitions= 4.29523e+07 Memory= 0.000 cpu0: Depth= 27 States= 3.2e+07 Transitions= 4.25572e+07 Memory= 448.654 cpu4: Depth= 27 States= 3.1e+07 Transitions= 4.14557e+07 Memory= 0.000 cpu1: Depth= 27 States= 3.3e+07 Transitions= 4.44626e+07 Memory= 0.000 cpu2: Depth= 27 States= 3.2e+07 Transitions= 4.24867e+07 Memory= 0.000 cpu0: Depth= 27 States= 3.3e+07 Transitions= 4.41985e+07 Memory= 448.654 cpu3: Depth= 27 States= 2.9e+07 Transitions= 3.81667e+07 Memory= 0.000 cpu0: Depth= 27 States= 3.4e+07 Transitions= 4.58611e+07 Memory= 448.654 cpu2: Depth= 27 States= 3.3e+07 Transitions= 4.38396e+07 Memory= 0.000 cpu1: Depth= 27 States= 3.4e+07 Transitions= 4.57549e+07 Memory= 0.000 cpu3: Depth= 27 States= 3e+07 Transitions= 3.97103e+07 Memory= 0.000 cpu0: Depth= 27 States= 3.5e+07 Transitions= 4.75397e+07 Memory= 448.654 cpu4: Depth= 27 States= 3.2e+07 Transitions= 4.25609e+07 Memory= 0.000 cpu2: Depth= 27 States= 3.4e+07 Transitions= 4.55532e+07 Memory= 0.000 cpu3: Depth= 27 States= 3.1e+07 Transitions= 4.12503e+07 Memory= 0.000 cpu0: Depth= 27 States= 3.6e+07 Transitions= 4.91782e+07 Memory= 448.654 cpu2: Depth= 27 States= 3.5e+07 Transitions= 4.72782e+07 Memory= 0.000 cpu4: Depth= 27 States= 3.3e+07 Transitions= 4.38821e+07 Memory= 0.000 cpu0: Depth= 27 States= 3.7e+07 Transitions= 5.08595e+07 Memory= 448.654 cpu2: Depth= 27 States= 3.6e+07 Transitions= 4.89961e+07 Memory= 0.000 cpu1: Depth= 27 States= 3.5e+07 Transitions= 4.69049e+07 Memory= 0.000 cpu3: Depth= 27 States= 3.2e+07 Transitions= 4.26278e+07 Memory= 0.000 cpu4: Depth= 27 States= 3.4e+07 Transitions= 4.55883e+07 Memory= 0.000 cpu1: done -- local memcnt 0 Mb cpu1: states stored 35600055 matched 12251130 cpu2: done -- local memcnt 0 Mb cpu2: cpu1: locks: global 0 other 776643 cpu1: waits: states 1.3620639e+09 slots 0 states stored 36955569 matched 13603942 cpu3: done -- local memcnt 0 Mb cpu3: cpu2: locks: global 15 other 897958 cpu2: waits: states 1.3147573e+09 slots 0 states stored 32304057 matched 10856014 cpu4: done -- local memcnt 0 Mb cpu4: states stored 34002531 matched 11590576 cpu3: locks: global 23 other 106231 cpu3: waits: states 4.0767257e+08 slots 0 cpu0: cpu4: locks: global 5 other 748504 cpu4: waits: states 1.7199419e+09 slots 0 done -- local memcnt 448.654 Mb cpu0: states stored 37814772 matched 14311892 cpu0: locks: global 1357 other 911968 cpu0: waits: states 1.1390748e+09 slots 0 (Spin Version 5.0.0 -- 8 May 2007) + Multi-Core (NCORE=5 -z20) + Partial Order Reduction Bit statespace search for: never claim + assertion violations + (if within scope of claim) cycle checks - (disabled by -DSAFETY) invalid end states - (disabled by never claim) State-vector 180 byte, depth reached 27, errors: 0 1.7667698e+08 states, stored 62613554 states, matched 2.3929054e+08 transitions (= stored+matched) 69489342 atomic steps hash factor: 6.07743 (best if > 100.) bits set per state: 3 (-k3) Stats on memory usage (in Megabytes): 35046.399 equivalent memory usage for states (stored*(State-vector + overhead)) 128.000 memory used for hash array (-w30) 0.076 memory used for bit stack 0.458 memory used for DFS stack (-m10000) 320.000 memory used for shared work-queues 320.071 other (proc and chan stacks) 0.049 memory lost to fragmentation 448.654 total actual memory usage Successor counts: 0 120185 (0.1342 % of total) 1 86970770 (97.13 % of total) 2 882558 (0.9857 % of total) 4 532298 (0.5945 % of total) 14 256025 (0.2859 % of total) 16 775697 (0.8663 % of total) mean 1.193 (without 0: 1.195) cpu0: elapsed time 145 seconds (1.76677e+08 states) cpu0: rate 1.21436e+06 states/second