~/atva/Ocaml/speedtest/david_spec2 > runspinalt.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.56915e+07 Memory= 1060.031
Depth=  807146 States= 2.5e+07 Transitions= 8.89195e+07 Memory= 1099.659
Depth=  807146 States= 2.6e+07 Transitions= 9.24996e+07 Memory= 1139.288
Depth=  807146 States= 2.7e+07 Transitions= 9.61502e+07 Memory= 1177.893
Depth=  807146 States= 2.8e+07 Transitions= 9.96391e+07 Memory= 1216.805
Depth=  807146 States= 2.9e+07 Transitions= 1.03117e+08 Memory= 1256.331
Depth=  807146 States=   3e+07 Transitions= 1.07041e+08 Memory= 1295.960
Depth=  807146 States= 3.1e+07 Transitions= 1.10227e+08 Memory= 1335.589
Depth=  807146 States= 3.2e+07 Transitions= 1.13452e+08 Memory= 1375.013
Depth=  807146 States= 3.3e+07 Transitions= 1.16964e+08 Memory= 1414.642
Depth=  807146 States= 3.4e+07 Transitions= 1.20093e+08 Memory= 1454.168
Depth=  807146 States= 3.5e+07 Transitions= 1.23624e+08 Memory= 1493.490
Depth=  807146 States= 3.6e+07 Transitions= 1.2718e+08 Memory= 1532.811
Depth=  807146 States= 3.7e+07 Transitions= 1.30791e+08 Memory= 1572.440
Depth=  807146 States= 3.8e+07 Transitions= 1.34326e+08 Memory= 1611.762
Depth=  807146 States= 3.9e+07 Transitions= 1.3796e+08 Memory= 1651.391
Depth=  807146 States=   4e+07 Transitions= 1.41448e+08 Memory= 1690.917
Depth=  807146 States= 4.1e+07 Transitions= 1.45035e+08 Memory= 1730.751
Depth=  807146 States= 4.2e+07 Transitions= 1.48736e+08 Memory= 1770.482
Depth=  807146 States= 4.3e+07 Transitions= 1.52564e+08 Memory= 1810.111
Depth=  807146 States= 4.4e+07 Transitions= 1.56318e+08 Memory= 1849.739
Depth=  807146 States= 4.5e+07 Transitions= 1.60833e+08 Memory= 1889.368
Depth=  807146 States= 4.6e+07 Transitions= 1.64323e+08 Memory= 1928.075
Depth=  807146 States= 4.7e+07 Transitions= 1.67815e+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.7952e+07 states, stored
1.2329e+08 states, matched
1.71242e+08 transitions (= stored+matched)
3.22201e+08 atomic steps
hash conflicts: 5.24706e+07 (resolved)

Stats on memory usage (in Megabytes):
12275.703       equivalent memory usage for states (stored*(State-vector + overhead))
1887.834        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.128   other (proc and chan stacks)
0.263   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 5 ]

real    14m22.982s
user    14m18.210s
sys     0m3.900s