~/atva/Ocaml/speedtest/david_spec2 > run_ltl2ba.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= 104679 States= 1e+06 Transitions= 3.22664e+06 Memory= 151.333 Depth= 140809 States= 2e+06 Transitions= 6.7766e+06 Memory= 190.552 Depth= 140809 States= 3e+06 Transitions= 1.04066e+07 Memory= 229.362 Depth= 140809 States= 4e+06 Transitions= 1.38929e+07 Memory= 268.991 Depth= 140809 States= 5e+06 Transitions= 1.74312e+07 Memory= 308.517 Depth= 140809 States= 6e+06 Transitions= 2.13275e+07 Memory= 348.351 Depth= 140809 States= 7e+06 Transitions= 2.45233e+07 Memory= 387.467 Depth= 241085 States= 8e+06 Transitions= 2.77499e+07 Memory= 427.199 Depth= 244031 States= 9e+06 Transitions= 3.12774e+07 Memory= 466.725 Depth= 309189 States= 1e+07 Transitions= 3.43929e+07 Memory= 506.661 Depth= 386555 States= 1.1e+07 Transitions= 3.79061e+07 Memory= 546.802 Depth= 429196 States= 1.2e+07 Transitions= 4.14622e+07 Memory= 586.328 Depth= 458817 States= 1.3e+07 Transitions= 4.50874e+07 Memory= 625.343 Depth= 522323 States= 1.4e+07 Transitions= 4.86144e+07 Memory= 665.176 Depth= 552240 States= 1.5e+07 Transitions= 5.22599e+07 Memory= 704.191 Depth= 638393 States= 1.6e+07 Transitions= 5.57342e+07 Memory= 744.024 Depth= 737097 States= 1.7e+07 Transitions= 5.9339e+07 Memory= 784.472 Depth= 804707 States= 1.8e+07 Transitions= 6.30346e+07 Memory= 824.818 Depth= 804707 States= 1.9e+07 Transitions= 6.68445e+07 Memory= 864.651 Depth= 807090 States= 2e+07 Transitions= 7.06026e+07 Memory= 904.485 Depth= 807090 States= 2.1e+07 Transitions= 7.50976e+07 Memory= 944.011 Depth= 807090 States= 2.2e+07 Transitions= 7.86085e+07 Memory= 982.719 Depth= 807090 States= 2.3e+07 Transitions= 8.21118e+07 Memory= 1021.016 (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.39761e+07 states, stored 6.16455e+07 states, matched 8.56215e+07 transitions (= stored+matched) 1.61044e+08 atomic steps hash conflicts: 2.16712e+07 (resolved) Stats on memory usage (in Megabytes): 6137.873 equivalent memory usage for states (stored*(State-vector + overhead)) 943.115 actual memory usage for states (compression: 15.37%) 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.289 other (proc and chan stacks) 0.182 memory lost to fragmentation 1058.495 total actual memory usage nr of templates: [ globals chans procs ] collapse counts: [ 371 129 31 2067 210 4525 4251 2 3 ] real 7m7.626s user 7m4.710s sys 0m2.190s