~/atva/Ocaml/speedtest/david_spec2 > runspin.sh 2 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.0182e+07 Memory= 229.259 Depth= 140518 States= 4e+06 Transitions= 1.36229e+07 Memory= 268.888 Depth= 140809 States= 5e+06 Transitions= 1.72764e+07 Memory= 308.312 Depth= 140809 States= 6e+06 Transitions= 2.07115e+07 Memory= 347.122 Depth= 140809 States= 7e+06 Transitions= 2.43342e+07 Memory= 386.751 Depth= 140809 States= 8e+06 Transitions= 2.79161e+07 Memory= 426.584 Depth= 140809 States= 9e+06 Transitions= 3.15813e+07 Memory= 466.111 Depth= 227810 States= 1e+07 Transitions= 3.44736e+07 Memory= 505.944 Depth= 244031 States= 1.1e+07 Transitions= 3.83975e+07 Memory= 545.880 Depth= 244031 States= 1.2e+07 Transitions= 4.1658e+07 Memory= 585.099 Depth= 347431 States= 1.3e+07 Transitions= 4.4789e+07 Memory= 625.035 Depth= 392045 States= 1.4e+07 Transitions= 4.83787e+07 Memory= 664.459 Depth= 422042 States= 1.5e+07 Transitions= 5.19352e+07 Memory= 703.679 Depth= 439138 States= 1.6e+07 Transitions= 5.56031e+07 Memory= 742.693 Depth= 509641 States= 1.7e+07 Transitions= 5.91372e+07 Memory= 782.527 Depth= 565784 States= 1.8e+07 Transitions= 6.26099e+07 Memory= 822.053 Depth= 664247 States= 1.9e+07 Transitions= 6.61056e+07 Memory= 862.296 Depth= 741728 States= 2e+07 Transitions= 6.9709e+07 Memory= 902.744 Depth= 803567 States= 2.1e+07 Transitions= 7.33266e+07 Memory= 942.987 Depth= 804707 States= 2.2e+07 Transitions= 7.71961e+07 Memory= 982.719 Depth= 807090 States= 2.3e+07 Transitions= 8.12542e+07 Memory= 1022.450 Depth= 807090 States= 2.4e+07 Transitions= 8.565e+07 Memory= 1061.976 Depth= 807090 States= 2.5e+07 Transitions= 8.90267e+07 Memory= 1100.376 Depth= 807090 States= 2.6e+07 Transitions= 9.25097e+07 Memory= 1138.776 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: 6.24601e+07 (resolved) Stats on memory usage (in Megabytes): 12275.737 equivalent memory usage for states (stored*(State-vector + overhead)) 1887.629 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.130 other (proc and chan stacks) 0.261 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 17m57.181s user 14m41.110s sys 0m5.800s