~/atva/Ocaml/speedtest/david_spec2 > run_modella.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= 98519 States= 1e+06 Transitions= 3.63445e+06 Memory= 151.026 Depth= 98809 States= 2e+06 Transitions= 7.25559e+06 Memory= 190.552 Depth= 105236 States= 3e+06 Transitions= 1.05017e+07 Memory= 229.669 Depth= 141226 States= 4e+06 Transitions= 1.40871e+07 Memory= 269.195 Depth= 141226 States= 5e+06 Transitions= 1.78441e+07 Memory= 308.722 Depth= 141226 States= 6e+06 Transitions= 2.1079e+07 Memory= 348.453 Depth= 241085 States= 7e+06 Transitions= 2.43491e+07 Memory= 388.184 Depth= 244051 States= 8e+06 Transitions= 2.79836e+07 Memory= 427.813 Depth= 244051 States= 9e+06 Transitions= 3.11685e+07 Memory= 467.442 Depth= 357498 States= 1e+07 Transitions= 3.44535e+07 Memory= 507.787 Depth= 408356 States= 1.1e+07 Transitions= 3.79537e+07 Memory= 547.314 Depth= 434090 States= 1.2e+07 Transitions= 4.15753e+07 Memory= 586.738 Depth= 495995 States= 1.3e+07 Transitions= 4.51485e+07 Memory= 626.367 Depth= 552240 States= 1.4e+07 Transitions= 4.86516e+07 Memory= 666.200 Depth= 581747 States= 1.5e+07 Transitions= 5.22799e+07 Memory= 705.727 Depth= 673942 States= 1.6e+07 Transitions= 5.5853e+07 Memory= 746.072 Depth= 752999 States= 1.7e+07 Transitions= 5.94855e+07 Memory= 786.315 Depth= 804707 States= 1.8e+07 Transitions= 6.29974e+07 Memory= 826.251 Depth= 804707 States= 1.9e+07 Transitions= 6.69891e+07 Memory= 865.880 Depth= 807146 States= 2e+07 Transitions= 7.11137e+07 Memory= 905.611 Depth= 807146 States= 2.1e+07 Transitions= 7.52266e+07 Memory= 945.035 Depth= 807146 States= 2.2e+07 Transitions= 7.86589e+07 Memory= 983.231 Depth= 807146 States= 2.3e+07 Transitions= 8.21104e+07 Memory= 1021.528 Depth= 807146 States= 2.4e+07 Transitions= 8.56507e+07 Memory= 1060.031 Depth= 807146 States= 2.5e+07 Transitions= 8.92584e+07 Memory= 1098.635 Depth= 807146 States= 2.6e+07 Transitions= 9.25801e+07 Memory= 1138.264 Depth= 807146 States= 2.7e+07 Transitions= 9.62744e+07 Memory= 1177.893 Depth= 807146 States= 2.8e+07 Transitions= 9.98126e+07 Memory= 1217.317 Depth= 807146 States= 2.9e+07 Transitions= 1.0336e+08 Memory= 1256.843 Depth= 807146 States= 3e+07 Transitions= 1.06921e+08 Memory= 1296.677 Depth= 807146 States= 3.1e+07 Transitions= 1.10074e+08 Memory= 1336.101 Depth= 807146 States= 3.2e+07 Transitions= 1.13601e+08 Memory= 1375.627 Depth= 807146 States= 3.3e+07 Transitions= 1.16876e+08 Memory= 1415.154 Depth= 807146 States= 3.4e+07 Transitions= 1.20159e+08 Memory= 1454.783 Depth= 807146 States= 3.5e+07 Transitions= 1.23665e+08 Memory= 1494.104 Depth= 807146 States= 3.6e+07 Transitions= 1.27309e+08 Memory= 1533.528 Depth= 807146 States= 3.7e+07 Transitions= 1.3086e+08 Memory= 1572.850 Depth= 807146 States= 3.8e+07 Transitions= 1.34435e+08 Memory= 1612.581 Depth= 807146 States= 3.9e+07 Transitions= 1.38001e+08 Memory= 1652.005 Depth= 807146 States= 4e+07 Transitions= 1.41605e+08 Memory= 1691.736 Depth= 807146 States= 4.1e+07 Transitions= 1.45255e+08 Memory= 1731.467 Depth= 807146 States= 4.2e+07 Transitions= 1.48942e+08 Memory= 1771.096 Depth= 807146 States= 4.3e+07 Transitions= 1.52729e+08 Memory= 1810.725 Depth= 807146 States= 4.4e+07 Transitions= 1.56838e+08 Memory= 1850.354 Depth= 807146 States= 4.5e+07 Transitions= 1.60911e+08 Memory= 1889.778 Depth= 807146 States= 4.6e+07 Transitions= 1.64335e+08 Memory= 1928.178 Depth= 807146 States= 4.7e+07 Transitions= 1.67819e+08 Memory= 1966.475 (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 807146, errors: 0 4.79518e+07 states, stored 1.23289e+08 states, matched 1.71241e+08 transitions (= stored+matched) 3.22199e+08 atomic steps hash conflicts: 5.94433e+07 (resolved) Stats on memory usage (in Megabytes): 12275.669 equivalent memory usage for states (stored*(State-vector + overhead)) 1887.790 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.216 other (proc and chan stacks) 0.219 memory lost to fragmentation 2003.135 total actual memory usage nr of templates: [ globals chans procs ] collapse counts: [ 406 129 31 2067 210 4525 4251 2 7 ] real 14m9.425s user 14m5.070s sys 0m3.510s