~/atva/Ocaml/speedtest/david_spec2 > run_modella.sh 1 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= 98277 States= 1e+06 Transitions= 3.57832e+06 Memory= 151.231 Depth= 104646 States= 2e+06 Transitions= 6.88141e+06 Memory= 190.962 Depth= 140776 States= 3e+06 Transitions= 1.05388e+07 Memory= 230.898 Depth= 140776 States= 4e+06 Transitions= 1.40607e+07 Memory= 270.424 Depth= 140776 States= 5e+06 Transitions= 1.76151e+07 Memory= 309.951 Depth= 140776 States= 6e+06 Transitions= 2.12299e+07 Memory= 349.784 Depth= 140776 States= 7e+06 Transitions= 2.43703e+07 Memory= 389.208 Depth= 244031 States= 8e+06 Transitions= 2.79037e+07 Memory= 429.144 Depth= 244031 States= 9e+06 Transitions= 3.11822e+07 Memory= 468.773 Depth= 357459 States= 1e+07 Transitions= 3.44642e+07 Memory= 509.221 Depth= 408356 States= 1.1e+07 Transitions= 3.79641e+07 Memory= 548.850 Depth= 436895 States= 1.2e+07 Transitions= 4.15928e+07 Memory= 588.479 Depth= 495069 States= 1.3e+07 Transitions= 4.5161e+07 Memory= 628.107 Depth= 529438 States= 1.4e+07 Transitions= 4.87362e+07 Memory= 668.043 Depth= 581747 States= 1.5e+07 Transitions= 5.22958e+07 Memory= 707.775 Depth= 684525 States= 1.6e+07 Transitions= 5.59039e+07 Memory= 748.120 Depth= 776554 States= 1.7e+07 Transitions= 5.95456e+07 Memory= 788.466 Depth= 804707 States= 1.8e+07 Transitions= 6.32146e+07 Memory= 828.402 Depth= 804707 States= 1.9e+07 Transitions= 6.70322e+07 Memory= 868.031 Depth= 807090 States= 2e+07 Transitions= 7.11106e+07 Memory= 907.762 Depth= 807090 States= 2.1e+07 Transitions= 7.52021e+07 Memory= 947.083 Depth= 807090 States= 2.2e+07 Transitions= 7.86108e+07 Memory= 985.483 Depth= 807090 States= 2.3e+07 Transitions= 8.21196e+07 Memory= 1023.883 (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 2.39759e+07 states, stored 6.16448e+07 states, matched 8.56207e+07 transitions (= stored+matched) 1.61042e+08 atomic steps hash conflicts: 2.75133e+07 (resolved) Stats on memory usage (in Megabytes): 6137.839 equivalent memory usage for states (stored*(State-vector + overhead)) 946.070 actual memory usage for states (compression: 15.41%) 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.318 other (proc and chan stacks) 0.168 memory lost to fragmentation 1061.464 total actual memory usage nr of templates: [ globals chans procs ] collapse counts: [ 406 129 31 2067 210 4525 4251 2 3 ] real 7m10.661s user 7m8.330s sys 0m1.950s