~/atva/Ocaml/speedtest/david_spec2 > run_spin.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.38901e+07 Memory= 268.991
Depth=  140809 States=   5e+06 Transitions= 1.74571e+07 Memory= 308.517
Depth=  140809 States=   6e+06 Transitions= 2.13304e+07 Memory= 348.351
Depth=  140809 States=   7e+06 Transitions= 2.45172e+07 Memory= 387.467
Depth=  241085 States=   8e+06 Transitions= 2.76973e+07 Memory= 427.199
Depth=  244031 States=   9e+06 Transitions= 3.12877e+07 Memory= 466.725
Depth=  304222 States=   1e+07 Transitions= 3.44078e+07 Memory= 506.661
Depth=  384344 States= 1.1e+07 Transitions= 3.78961e+07 Memory= 546.495
Depth=  408292 States= 1.2e+07 Transitions= 4.15418e+07 Memory= 586.021
Depth=  453471 States= 1.3e+07 Transitions= 4.51112e+07 Memory= 625.343
Depth=  511640 States= 1.4e+07 Transitions= 4.86934e+07 Memory= 664.767
Depth=  549778 States= 1.5e+07 Transitions= 5.22502e+07 Memory= 704.191
Depth=  635827 States= 1.6e+07 Transitions= 5.57302e+07 Memory= 744.024
Depth=  737097 States= 1.7e+07 Transitions= 5.93195e+07 Memory= 784.472
Depth=  804707 States= 1.8e+07 Transitions= 6.30473e+07 Memory= 824.818
Depth=  804707 States= 1.9e+07 Transitions= 6.68504e+07 Memory= 864.651
Depth=  807090 States=   2e+07 Transitions= 7.06045e+07 Memory= 904.485
Depth=  807090 States= 2.1e+07 Transitions= 7.51e+07 Memory= 944.011
Depth=  807090 States= 2.2e+07 Transitions= 7.86087e+07 Memory= 982.719
Depth=  807090 States= 2.3e+07 Transitions= 8.21161e+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.16456e+07 states, matched
8.56217e+07 transitions (= stored+matched)
1.61045e+08 atomic steps
hash conflicts: 2.14713e+07 (resolved)

Stats on memory usage (in Megabytes):
6137.873        equivalent memory usage for states (stored*(State-vector + overhead))
943.107 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.304   other (proc and chan stacks)
0.175   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    7m8.934s
user    7m6.900s
sys     0m1.730s