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.70547e+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.70678e+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= 21 States= 1e+06 Transitions= 1.04189e+06 Memory= 384.654 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= 21 States= 1e+06 Transitions= 1.03686e+06 Memory= 0.000 cpu1: Depth= 27 States= 2e+06 Transitions= 3.4118e+06 Memory= 0.000 cpu3: Depth= 27 States= 2e+06 Transitions= 3.38686e+06 Memory= 0.000 cpu1: Depth= 27 States= 3e+06 Transitions= 5.04729e+06 Memory= 0.000 cpu3: Depth= 27 States= 3e+06 Transitions= 5.05868e+06 Memory= 0.000 cpu0: Depth= 21 States= 2e+06 Transitions= 2.07658e+06 Memory= 384.654 cpu2: Depth= 21 States= 2e+06 Transitions= 2.08167e+06 Memory= 0.000 cpu1: Depth= 27 States= 4e+06 Transitions= 6.72021e+06 Memory= 0.000 cpu3: Depth= 27 States= 4e+06 Transitions= 6.68241e+06 Memory= 0.000 cpu0: Depth= 21 States= 3e+06 Transitions= 3.1438e+06 Memory= 384.654 cpu2: Depth= 21 States= 3e+06 Transitions= 3.11795e+06 Memory= 0.000 cpu1: Depth= 27 States= 5e+06 Transitions= 8.34406e+06 Memory= 0.000 cpu3: Depth= 27 States= 5e+06 Transitions= 8.29819e+06 Memory= 0.000 cpu2: Depth= 27 States= 4e+06 Transitions= 4.19288e+06 Memory= 0.000 cpu0: Depth= 21 States= 4e+06 Transitions= 4.18911e+06 Memory= 384.654 cpu1: Depth= 27 States= 6e+06 Transitions= 9.93911e+06 Memory= 0.000 cpu3: Depth= 27 States= 6e+06 Transitions= 9.9099e+06 Memory= 0.000 cpu2: Depth= 27 States= 5e+06 Transitions= 5.2329e+06 Memory= 0.000 cpu0: Depth= 21 States= 5e+06 Transitions= 5.22121e+06 Memory= 384.654 cpu1: Depth= 27 States= 7e+06 Transitions= 1.14827e+07 Memory= 0.000 cpu3: Depth= 27 States= 7e+06 Transitions= 1.14651e+07 Memory= 0.000 cpu0: Depth= 21 States= 6e+06 Transitions= 6.2523e+06 Memory= 384.654 cpu2: Depth= 27 States= 6e+06 Transitions= 6.28373e+06 Memory= 0.000 cpu1: Depth= 27 States= 8e+06 Transitions= 1.3102e+07 Memory= 0.000 cpu3: Depth= 27 States= 8e+06 Transitions= 1.30602e+07 Memory= 0.000 cpu0: Depth= 27 States= 7e+06 Transitions= 7.33387e+06 Memory= 384.654 cpu2: Depth= 27 States= 7e+06 Transitions= 7.31892e+06 Memory= 0.000 cpu1: Depth= 27 States= 9e+06 Transitions= 1.46491e+07 Memory= 0.000 cpu3: Depth= 27 States= 9e+06 Transitions= 1.45153e+07 Memory= 0.000 cpu0: Depth= 27 States= 8e+06 Transitions= 8.38669e+06 Memory= 384.654 cpu2: Depth= 27 States= 8e+06 Transitions= 8.35645e+06 Memory= 0.000 cpu1: Depth= 27 States= 1e+07 Transitions= 1.61557e+07 Memory= 0.000 cpu3: Depth= 27 States= 1e+07 Transitions= 1.60524e+07 Memory= 0.000 cpu0: Depth= 27 States= 9e+06 Transitions= 9.42516e+06 Memory= 384.654 cpu2: Depth= 27 States= 9e+06 Transitions= 9.38824e+06 Memory= 0.000 cpu1: Depth= 27 States= 1.1e+07 Transitions= 1.77041e+07 Memory= 0.000 cpu3: Depth= 27 States= 1.1e+07 Transitions= 1.76059e+07 Memory= 0.000 cpu2: Depth= 27 States= 1e+07 Transitions= 1.04704e+07 Memory= 0.000 cpu0: Depth= 27 States= 1e+07 Transitions= 1.04655e+07 Memory= 384.654 cpu1: Depth= 27 States= 1.2e+07 Transitions= 1.91332e+07 Memory= 0.000 cpu2: Depth= 27 States= 1.1e+07 Transitions= 1.15104e+07 Memory= 0.000 cpu0: Depth= 27 States= 1.1e+07 Transitions= 1.14939e+07 Memory= 384.654 cpu3: Depth= 27 States= 1.2e+07 Transitions= 1.90538e+07 Memory= 0.000 cpu2: Depth= 27 States= 1.2e+07 Transitions= 1.25564e+07 Memory= 0.000 cpu0: Depth= 27 States= 1.2e+07 Transitions= 1.2535e+07 Memory= 384.654 cpu1: Depth= 27 States= 1.3e+07 Transitions= 2.05878e+07 Memory= 0.000 cpu3: Depth= 27 States= 1.3e+07 Transitions= 2.05268e+07 Memory= 0.000 cpu0: Depth= 27 States= 1.3e+07 Transitions= 1.35718e+07 Memory= 384.654 cpu2: Depth= 27 States= 1.3e+07 Transitions= 1.36044e+07 Memory= 0.000 cpu1: Depth= 27 States= 1.4e+07 Transitions= 2.20897e+07 Memory= 0.000 cpu3: Depth= 27 States= 1.4e+07 Transitions= 2.20259e+07 Memory= 0.000 cpu2: Depth= 27 States= 1.4e+07 Transitions= 1.46408e+07 Memory= 0.000 cpu0: Depth= 27 States= 1.4e+07 Transitions= 1.46206e+07 Memory= 384.654 cpu1: Depth= 27 States= 1.5e+07 Transitions= 2.35369e+07 Memory= 0.000 cpu2: Depth= 27 States= 1.5e+07 Transitions= 1.56744e+07 Memory= 0.000 cpu0: Depth= 27 States= 1.5e+07 Transitions= 1.56831e+07 Memory= 384.654 cpu3: Depth= 27 States= 1.5e+07 Transitions= 2.34285e+07 Memory= 0.000 cpu2: Depth= 27 States= 1.6e+07 Transitions= 1.67123e+07 Memory= 0.000 cpu0: Depth= 27 States= 1.6e+07 Transitions= 1.67373e+07 Memory= 384.654 cpu1: Depth= 27 States= 1.6e+07 Transitions= 2.49493e+07 Memory= 0.000 cpu3: Depth= 27 States= 1.6e+07 Transitions= 2.485e+07 Memory= 0.000 cpu2: Depth= 27 States= 1.7e+07 Transitions= 1.77532e+07 Memory= 0.000 cpu0: Depth= 27 States= 1.7e+07 Transitions= 1.77768e+07 Memory= 384.654 cpu1: Depth= 27 States= 1.7e+07 Transitions= 2.63559e+07 Memory= 0.000 cpu2: Depth= 27 States= 1.8e+07 Transitions= 1.87978e+07 Memory= 0.000 cpu3: Depth= 27 States= 1.7e+07 Transitions= 2.62783e+07 Memory= 0.000 cpu0: Depth= 27 States= 1.8e+07 Transitions= 1.88288e+07 Memory= 384.654 cpu1: Depth= 27 States= 1.8e+07 Transitions= 2.77957e+07 Memory= 0.000 cpu2: Depth= 27 States= 1.9e+07 Transitions= 1.98395e+07 Memory= 0.000 cpu0: Depth= 27 States= 1.9e+07 Transitions= 1.98687e+07 Memory= 384.654 cpu3: Depth= 27 States= 1.8e+07 Transitions= 2.77279e+07 Memory= 0.000 cpu2: Depth= 27 States= 2e+07 Transitions= 2.09208e+07 Memory= 0.000 cpu0: Depth= 27 States= 2e+07 Transitions= 2.0909e+07 Memory= 384.654 cpu1: Depth= 27 States= 1.9e+07 Transitions= 2.91595e+07 Memory= 0.000 cpu3: Depth= 27 States= 1.9e+07 Transitions= 2.91119e+07 Memory= 0.000 cpu2: Depth= 27 States= 2.1e+07 Transitions= 2.19802e+07 Memory= 0.000 cpu0: Depth= 27 States= 2.1e+07 Transitions= 2.195e+07 Memory= 384.654 cpu1: Depth= 27 States= 2e+07 Transitions= 3.055e+07 Memory= 0.000 cpu2: Depth= 27 States= 2.2e+07 Transitions= 2.30251e+07 Memory= 0.000 cpu0: Depth= 27 States= 2.2e+07 Transitions= 2.29955e+07 Memory= 384.654 cpu3: Depth= 27 States= 2e+07 Transitions= 3.04698e+07 Memory= 0.000 cpu2: Depth= 27 States= 2.3e+07 Transitions= 2.40741e+07 Memory= 0.000 cpu0: Depth= 27 States= 2.3e+07 Transitions= 2.40409e+07 Memory= 384.654 cpu1: Depth= 27 States= 2.1e+07 Transitions= 3.19363e+07 Memory= 0.000 cpu3: Depth= 27 States= 2.1e+07 Transitions= 3.18508e+07 Memory= 0.000 cpu2: Depth= 27 States= 2.4e+07 Transitions= 2.51283e+07 Memory= 0.000 cpu0: Depth= 27 States= 2.4e+07 Transitions= 2.50882e+07 Memory= 384.654 cpu1: Depth= 27 States= 2.2e+07 Transitions= 3.3338e+07 Memory= 0.000 cpu2: Depth= 27 States= 2.5e+07 Transitions= 2.61744e+07 Memory= 0.000 cpu0: Depth= 27 States= 2.5e+07 Transitions= 2.61342e+07 Memory= 384.654 cpu3: Depth= 27 States= 2.2e+07 Transitions= 3.32278e+07 Memory= 0.000 cpu2: Depth= 27 States= 2.6e+07 Transitions= 2.7215e+07 Memory= 0.000 cpu0: Depth= 27 States= 2.6e+07 Transitions= 2.71972e+07 Memory= 384.654 cpu1: Depth= 27 States= 2.3e+07 Transitions= 3.47119e+07 Memory= 0.000 cpu3: Depth= 27 States= 2.3e+07 Transitions= 3.45609e+07 Memory= 0.000 cpu2: Depth= 27 States= 2.7e+07 Transitions= 2.82644e+07 Memory= 0.000 cpu0: Depth= 27 States= 2.7e+07 Transitions= 2.82623e+07 Memory= 384.654 cpu1: Depth= 27 States= 2.4e+07 Transitions= 3.60652e+07 Memory= 0.000 cpu2: Depth= 27 States= 2.8e+07 Transitions= 2.93178e+07 Memory= 0.000 cpu0: Depth= 27 States= 2.8e+07 Transitions= 2.93184e+07 Memory= 384.654 cpu3: Depth= 27 States= 2.4e+07 Transitions= 3.59105e+07 Memory= 0.000 cpu2: Depth= 27 States= 2.9e+07 Transitions= 3.03693e+07 Memory= 0.000 cpu0: Depth= 27 States= 2.9e+07 Transitions= 3.03738e+07 Memory= 384.654 cpu1: Depth= 27 States= 2.5e+07 Transitions= 3.74047e+07 Memory= 0.000 cpu3: Depth= 27 States= 2.5e+07 Transitions= 3.72738e+07 Memory= 0.000 cpu2: Depth= 27 States= 3e+07 Transitions= 3.14265e+07 Memory= 0.000 cpu0: Depth= 27 States= 3e+07 Transitions= 3.14386e+07 Memory= 384.654 cpu1: Depth= 27 States= 2.6e+07 Transitions= 3.87482e+07 Memory= 0.000 cpu2: Depth= 27 States= 3.1e+07 Transitions= 3.24819e+07 Memory= 0.000 cpu0: Depth= 27 States= 3.1e+07 Transitions= 3.24955e+07 Memory= 384.654 cpu3: Depth= 27 States= 2.6e+07 Transitions= 3.86412e+07 Memory= 0.000 cpu2: Depth= 27 States= 3.2e+07 Transitions= 3.35511e+07 Memory= 0.000 cpu0: Depth= 27 States= 3.2e+07 Transitions= 3.35493e+07 Memory= 384.654 cpu1: Depth= 27 States= 2.7e+07 Transitions= 4.00712e+07 Memory= 0.000 cpu3: Depth= 27 States= 2.7e+07 Transitions= 3.99997e+07 Memory= 0.000 cpu2: Depth= 27 States= 3.3e+07 Transitions= 3.46293e+07 Memory= 0.000 cpu0: Depth= 27 States= 3.3e+07 Transitions= 3.46081e+07 Memory= 384.654 cpu1: Depth= 27 States= 2.8e+07 Transitions= 4.14181e+07 Memory= 0.000 cpu0: Depth= 27 States= 3.4e+07 Transitions= 3.56736e+07 Memory= 384.654 cpu2: Depth= 27 States= 3.4e+07 Transitions= 3.56972e+07 Memory= 0.000 cpu3: Depth= 27 States= 2.8e+07 Transitions= 4.13291e+07 Memory= 0.000 cpu0: Depth= 27 States= 3.5e+07 Transitions= 3.67383e+07 Memory= 384.654 cpu1: Depth= 27 States= 2.9e+07 Transitions= 4.27402e+07 Memory= 0.000 cpu2: Depth= 27 States= 3.5e+07 Transitions= 3.67696e+07 Memory= 0.000 cpu3: Depth= 27 States= 2.9e+07 Transitions= 4.26539e+07 Memory= 0.000 cpu0: Depth= 27 States= 3.6e+07 Transitions= 3.78062e+07 Memory= 384.654 cpu2: Depth= 27 States= 3.6e+07 Transitions= 3.78484e+07 Memory= 0.000 cpu1: Depth= 27 States= 3e+07 Transitions= 4.40994e+07 Memory= 0.000 cpu3: Depth= 27 States= 3e+07 Transitions= 4.39878e+07 Memory= 0.000 cpu0: Depth= 27 States= 3.7e+07 Transitions= 3.88743e+07 Memory= 384.654 cpu2: Depth= 27 States= 3.7e+07 Transitions= 3.89186e+07 Memory= 0.000 cpu1: Depth= 27 States= 3.1e+07 Transitions= 4.54456e+07 Memory= 0.000 cpu0: Depth= 27 States= 3.8e+07 Transitions= 3.99648e+07 Memory= 384.654 cpu2: Depth= 27 States= 3.8e+07 Transitions= 3.9985e+07 Memory= 0.000 cpu3: Depth= 27 States= 3.1e+07 Transitions= 4.53293e+07 Memory= 0.000 cpu1: Depth= 27 States= 3.2e+07 Transitions= 4.67872e+07 Memory= 0.000 cpu2: Depth= 27 States= 3.9e+07 Transitions= 4.10679e+07 Memory= 0.000 cpu0: Depth= 27 States= 3.9e+07 Transitions= 4.10633e+07 Memory= 384.654 cpu3: Depth= 27 States= 3.2e+07 Transitions= 4.66878e+07 Memory= 0.000 cpu2: Depth= 27 States= 4e+07 Transitions= 4.21455e+07 Memory= 0.000 cpu1: Depth= 27 States= 3.3e+07 Transitions= 4.80987e+07 Memory= 0.000 cpu0: Depth= 27 States= 4e+07 Transitions= 4.21514e+07 Memory= 384.654 cpu3: Depth= 27 States= 3.3e+07 Transitions= 4.80235e+07 Memory= 0.000 cpu2: Depth= 27 States= 4.1e+07 Transitions= 4.32313e+07 Memory= 0.000 cpu1: Depth= 27 States= 3.4e+07 Transitions= 4.94415e+07 Memory= 0.000 cpu0: Depth= 27 States= 4.1e+07 Transitions= 4.32459e+07 Memory= 384.654 cpu3: Depth= 27 States= 3.4e+07 Transitions= 4.93919e+07 Memory= 0.000 cpu2: Depth= 27 States= 4.2e+07 Transitions= 4.43138e+07 Memory= 0.000 cpu0: Depth= 27 States= 4.2e+07 Transitions= 4.4326e+07 Memory= 384.654 cpu1: Depth= 27 States= 3.5e+07 Transitions= 5.07714e+07 Memory= 0.000 cpu3: Depth= 27 States= 3.5e+07 Transitions= 5.07376e+07 Memory= 0.000 cpu2: Depth= 27 States= 4.3e+07 Transitions= 4.54457e+07 Memory= 0.000 cpu0: Depth= 27 States= 4.3e+07 Transitions= 4.54264e+07 Memory= 384.654 cpu1: Depth= 27 States= 3.6e+07 Transitions= 5.21826e+07 Memory= 0.000 cpu3: Depth= 27 States= 3.6e+07 Transitions= 5.20926e+07 Memory= 0.000 cpu2: Depth= 27 States= 4.4e+07 Transitions= 4.65528e+07 Memory= 0.000 cpu0: Depth= 27 States= 4.4e+07 Transitions= 4.65196e+07 Memory= 384.654 cpu1: Depth= 27 States= 3.7e+07 Transitions= 5.3545e+07 Memory= 0.000 cpu3: Depth= 27 States= 3.7e+07 Transitions= 5.34368e+07 Memory= 0.000 cpu0: Depth= 27 States= 4.5e+07 Transitions= 4.76261e+07 Memory= 384.654 cpu1: Depth= 27 States= 3.8e+07 Transitions= 5.49299e+07 Memory= 0.000 cpu2: Depth= 27 States= 4.5e+07 Transitions= 4.76677e+07 Memory= 0.000 cpu3: Depth= 27 States= 3.8e+07 Transitions= 5.48117e+07 Memory= 0.000 cpu1: Depth= 27 States= 3.9e+07 Transitions= 5.6357e+07 Memory= 0.000 cpu0: Depth= 27 States= 4.6e+07 Transitions= 4.87563e+07 Memory= 384.654 cpu2: Depth= 27 States= 4.6e+07 Transitions= 4.87833e+07 Memory= 0.000 cpu3: Depth= 27 States= 3.9e+07 Transitions= 5.62575e+07 Memory= 0.000 cpu1: Depth= 27 States= 4e+07 Transitions= 5.77043e+07 Memory= 0.000 cpu3: Depth= 27 States= 4e+07 Transitions= 5.76889e+07 Memory= 0.000 cpu2: Depth= 27 States= 4.7e+07 Transitions= 4.98956e+07 Memory= 0.000 cpu0: Depth= 27 States= 4.7e+07 Transitions= 4.98907e+07 Memory= 384.654 cpu1: Depth= 27 States= 4.1e+07 Transitions= 5.9123e+07 Memory= 0.000 cpu3: Depth= 27 States= 4.1e+07 Transitions= 5.91096e+07 Memory= 0.000 cpu2: Depth= 27 States= 4.8e+07 Transitions= 5.1037e+07 Memory= 0.000 cpu1: Depth= 27 States= 4.2e+07 Transitions= 6.0586e+07 Memory= 0.000 cpu0: Depth= 27 States= 4.8e+07 Transitions= 5.10196e+07 Memory= 384.654 cpu3: Depth= 27 States= 4.2e+07 Transitions= 6.05794e+07 Memory= 0.000 cpu1: Depth= 27 States= 4.3e+07 Transitions= 6.20797e+07 Memory= 0.000 cpu3: Depth= 27 States= 4.3e+07 Transitions= 6.20363e+07 Memory= 0.000 cpu2: Depth= 27 States= 4.9e+07 Transitions= 5.21813e+07 Memory= 0.000 cpu0: Depth= 27 States= 4.9e+07 Transitions= 5.21586e+07 Memory= 384.654 cpu1: Depth= 27 States= 4.4e+07 Transitions= 6.35935e+07 Memory= 0.000 cpu3: Depth= 27 States= 4.4e+07 Transitions= 6.3549e+07 Memory= 0.000 cpu1: Depth= 27 States= 4.5e+07 Transitions= 6.51233e+07 Memory= 0.000 cpu3: Depth= 27 States= 4.5e+07 Transitions= 6.50702e+07 Memory= 0.000 cpu1: Depth= 27 States= 4.6e+07 Transitions= 6.67225e+07 Memory= 0.000 cpu2: Depth= 27 States= 5e+07 Transitions= 5.33465e+07 Memory= 0.000 cpu0: Depth= 27 States= 5e+07 Transitions= 5.33214e+07 Memory= 384.654 cpu3: Depth= 27 States= 4.6e+07 Transitions= 6.66648e+07 Memory= 0.000 cpu1: Depth= 27 States= 4.7e+07 Transitions= 6.83304e+07 Memory= 0.000 cpu3: Depth= 27 States= 4.7e+07 Transitions= 6.83212e+07 Memory= 0.000 cpu1: Depth= 27 States= 4.8e+07 Transitions= 6.99892e+07 Memory= 0.000 cpu3: Depth= 27 States= 4.8e+07 Transitions= 7.00084e+07 Memory= 0.000 cpu1: done -- local memcnt 0 Mb cpu1: states stored 48933195 matched 22659139 cpu2: done -- local memcnt 0 Mb cpu1: locks: global 0 other 78784 cpu1: waits: states 6510593 slots 0 cpu2: states stored 50835507 matched 3562777 cpu3: cpu2: locks: global 32 other 103826 cpu2: waits: states 3.6509276e+09 slots 0 done -- local memcnt 0 Mb cpu3: states stored 48443318 matched 22331563 cpu0: done -- local memcnt 384.654 Mb cpu0: states stored 50741761 matched 3532468 cpu0: locks: global 0 other 126548 cpu0: waits: states 3.7379326e+09 slots 0 (Spin Version 5.0.0 -- 8 May 2007) + Multi-Core (NCORE=4 -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 cpu3: locks: global 189 other 50256 cpu3: waits: states 10394425 slots 0 1.9895378e+08 states, stored 52085947 states, matched 2.5103973e+08 transitions (= stored+matched) 79999524 atomic steps hash factor: 5.39694 (best if > 100.) bits set per state: 3 (-k3) Stats on memory usage (in Megabytes): 39465.319 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) 256.000 memory used for shared work-queues 256.071 other (proc and chan stacks) 0.049 memory lost to fragmentation 384.654 total actual memory usage Successor counts: 0 575053 (0.5666 % of total) 1 97701977 (96.27 % of total) 2 2391610 (2.357 % of total) 4 599903 (0.5911 % of total) 14 55051 (0.05424 % of total) 16 164955 (0.1625 % of total) mean 1.067 (without 0: 1.073) cpu0: elapsed time 184 seconds (1.98954e+08 states) cpu0: rate 1.07933e+06 states/second