~/atva/Ocaml/speedtest/david_spec2 > run_tmp2.sh warning: for p.o. reduction to be valid the never claim must be stutter-invariant (never claims generated from LTL formulae are stutter-invariant) Depth= 104528 States= 1e+06 Transitions= 3.22723e+06 Memory= 151.333 Depth= 140518 States= 2e+06 Transitions= 6.77705e+06 Memory= 190.552 Depth= 140518 States= 3e+06 Transitions= 1.02171e+07 Memory= 229.259 Depth= 140518 States= 4e+06 Transitions= 1.38376e+07 Memory= 268.581 Depth= 140518 States= 5e+06 Transitions= 1.74337e+07 Memory= 308.415 Depth= 140518 States= 6e+06 Transitions= 2.12964e+07 Memory= 348.146 Depth= 140518 States= 7e+06 Transitions= 2.44278e+07 Memory= 387.365 Depth= 244031 States= 8e+06 Transitions= 2.79691e+07 Memory= 427.813 Depth= 244031 States= 9e+06 Transitions= 3.12267e+07 Memory= 466.930 Depth= 308153 States= 1e+07 Transitions= 3.43981e+07 Memory= 506.661 Depth= 386301 States= 1.1e+07 Transitions= 3.78925e+07 Memory= 546.495 Depth= 408292 States= 1.2e+07 Transitions= 4.15285e+07 Memory= 585.714 Depth= 430338 States= 1.3e+07 Transitions= 4.51753e+07 Memory= 624.626 Depth= 493008 States= 1.4e+07 Transitions= 4.8741e+07 Memory= 664.255 Depth= 549778 States= 1.5e+07 Transitions= 5.22237e+07 Memory= 703.986 Depth= 621873 States= 1.6e+07 Transitions= 5.57189e+07 Memory= 744.024 Depth= 717024 States= 1.7e+07 Transitions= 5.92984e+07 Memory= 784.370 Depth= 787105 States= 1.8e+07 Transitions= 6.29354e+07 Memory= 824.715 Depth= 804707 States= 1.9e+07 Transitions= 6.66927e+07 Memory= 864.549 Depth= 807090 States= 2e+07 Transitions= 7.06114e+07 Memory= 904.485 Depth= 807090 States= 2.1e+07 Transitions= 7.50975e+07 Memory= 944.011 Depth= 807090 States= 2.2e+07 Transitions= 7.8657e+07 Memory= 982.616 Depth= 807090 States= 2.3e+07 Transitions= 8.21063e+07 Memory= 1021.016 Depth= 807090 States= 2.4e+07 Transitions= 8.56924e+07 Memory= 1059.416 Depth= 807090 States= 2.5e+07 Transitions= 8.89199e+07 Memory= 1099.045 Depth= 807090 States= 2.6e+07 Transitions= 9.24995e+07 Memory= 1138.571 Depth= 807090 States= 2.7e+07 Transitions= 9.6151e+07 Memory= 1177.586 Depth= 807090 States= 2.8e+07 Transitions= 9.96339e+07 Memory= 1217.010 Depth= 807090 States= 2.9e+07 Transitions= 1.03128e+08 Memory= 1256.843 Depth= 807090 States= 3e+07 Transitions= 1.07041e+08 Memory= 1296.677 Depth= 807090 States= 3.1e+07 Transitions= 1.10225e+08 Memory= 1335.999 Depth= 807090 States= 3.2e+07 Transitions= 1.13466e+08 Memory= 1375.423 Depth= 807090 States= 3.3e+07 Transitions= 1.16978e+08 Memory= 1414.949 Depth= 807090 States= 3.4e+07 Transitions= 1.201e+08 Memory= 1454.475 Depth= 807090 States= 3.5e+07 Transitions= 1.2361e+08 Memory= 1494.104 Depth= 807090 States= 3.6e+07 Transitions= 1.27245e+08 Memory= 1533.323 Depth= 807090 States= 3.7e+07 Transitions= 1.30796e+08 Memory= 1572.338 Depth= 807090 States= 3.8e+07 Transitions= 1.34419e+08 Memory= 1611.864 Depth= 807090 States= 3.9e+07 Transitions= 1.37958e+08 Memory= 1651.083 Depth= 807090 States= 4e+07 Transitions= 1.41434e+08 Memory= 1690.507 Depth= 807090 States= 4.1e+07 Transitions= 1.45045e+08 Memory= 1730.341 Depth= 807090 States= 4.2e+07 Transitions= 1.48747e+08 Memory= 1770.175 Depth= 807090 States= 4.3e+07 Transitions= 1.52562e+08 Memory= 1809.906 Depth= 807090 States= 4.4e+07 Transitions= 1.56325e+08 Memory= 1849.739 Depth= 807090 States= 4.5e+07 Transitions= 1.60833e+08 Memory= 1889.266 Depth= 807090 States= 4.6e+07 Transitions= 1.64323e+08 Memory= 1927.973 Depth= 807090 States= 4.7e+07 Transitions= 1.678e+08 Memory= 1966.373 (Spin Version 4.2.9 -- 8 February 2007) + Partial Order Reduction + Compression Full statespace search for: never claim + assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled) invalid end states - (disabled by never claim) State-vector 240 byte, depth reached 807090, errors: 0 4.79521e+07 states, stored 1.23291e+08 states, matched 1.71243e+08 transitions (= stored+matched) 3.22204e+08 atomic steps hash conflicts: 4.56746e+07 (resolved) Stats on memory usage (in Megabytes): 12275.737 equivalent memory usage for states (stored*(State-vector + overhead)) 1887.640 actual memory usage for states (compression: 15.38%) State-vector as stored = 23 byte + 16 byte overhead 67.109 memory used for hash table (-w24) 44.800 memory used for DFS stack (-m1400000) 3.108 other (proc and chan stacks) 0.273 memory lost to fragmentation 2002.930 total actual memory usage nr of templates: [ globals chans procs ] collapse counts: [ 369 129 31 2067 210 4525 4251 2 5 ] real 14m25.096s user 14m20.340s sys 0m3.790s