~/atva/Ocaml/speedtest/giop > runspin.sh 1 -DCOLLAPSE
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=     456 States=   1e+06 Transitions= 1.64763e+06 Memory= 157.067
Depth=     456 States=   2e+06 Transitions= 3.2975e+06 Memory= 204.376
Depth=     512 States=   3e+06 Transitions= 4.9479e+06 Memory= 253.119
Depth=     512 States=   4e+06 Transitions= 6.58797e+06 Memory= 304.216
Depth=     512 States=   5e+06 Transitions= 8.22601e+06 Memory= 356.747
Depth=     512 States=   6e+06 Transitions= 9.88628e+06 Memory= 408.767
Depth=     512 States=   7e+06 Transitions= 1.15226e+07 Memory= 460.786
Depth=     512 States=   8e+06 Transitions= 1.31389e+07 Memory= 512.600
Depth=     512 States=   9e+06 Transitions= 1.48158e+07 Memory= 564.415
Depth=     512 States=   1e+07 Transitions= 1.64627e+07 Memory= 616.639
Depth=     542 States= 1.1e+07 Transitions= 1.80975e+07 Memory= 668.351
Depth=     542 States= 1.2e+07 Transitions= 1.97618e+07 Memory= 720.370
Depth=     542 States= 1.3e+07 Transitions= 2.14129e+07 Memory= 772.287
Depth=     542 States= 1.4e+07 Transitions= 2.30371e+07 Memory= 823.896
Depth=     542 States= 1.5e+07 Transitions= 2.4668e+07 Memory= 874.994
Depth=     542 States= 1.6e+07 Transitions= 2.63317e+07 Memory= 926.808
Depth=     542 States= 1.7e+07 Transitions= 2.79721e+07 Memory= 978.827
Depth=     542 States= 1.8e+07 Transitions= 2.95987e+07 Memory= 1029.823
Depth=     542 States= 1.9e+07 Transitions= 3.12758e+07 Memory= 1081.637
Depth=     542 States=   2e+07 Transitions= 3.29001e+07 Memory= 1132.018
Depth=     542 States= 2.1e+07 Transitions= 3.45056e+07 Memory= 1183.525
Depth=     542 States= 2.2e+07 Transitions= 3.61534e+07 Memory= 1235.237
Depth=     542 States= 2.3e+07 Transitions= 3.77796e+07 Memory= 1287.051
Depth=     542 States= 2.4e+07 Transitions= 3.94019e+07 Memory= 1338.763
Depth=     542 States= 2.5e+07 Transitions= 4.1052e+07 Memory= 1391.295
Depth=     542 States= 2.6e+07 Transitions= 4.26866e+07 Memory= 1443.519
Depth=     542 States= 2.7e+07 Transitions= 4.43181e+07 Memory= 1494.616
Depth=     542 States= 2.8e+07 Transitions= 4.59859e+07 Memory= 1546.533
Depth=     542 States= 2.9e+07 Transitions= 4.76338e+07 Memory= 1598.552
Depth=     542 States=   3e+07 Transitions= 4.9242e+07 Memory= 1650.571
Depth=     542 States= 3.1e+07 Transitions= 5.08638e+07 Memory= 1700.440
Depth=     542 States= 3.2e+07 Transitions= 5.24969e+07 Memory= 1751.640
Depth=     542 States= 3.3e+07 Transitions= 5.41341e+07 Memory= 1803.762
Depth=     542 States= 3.4e+07 Transitions= 5.57495e+07 Memory= 1856.395
Depth=     542 States= 3.5e+07 Transitions= 5.73914e+07 Memory= 1908.619
Depth=     542 States= 3.6e+07 Transitions= 5.90249e+07 Memory= 1961.048
Depth=     542 States= 3.7e+07 Transitions= 6.0659e+07 Memory= 2012.555
Depth=     542 States= 3.8e+07 Transitions= 6.23036e+07 Memory= 2065.087
Depth=     542 States= 3.9e+07 Transitions= 6.3964e+07 Memory= 2114.443
Depth=     542 States=   4e+07 Transitions= 6.5594e+07 Memory= 2164.517
Depth=     542 States= 4.1e+07 Transitions= 6.7288e+07 Memory= 2215.922
Depth=     542 States= 4.2e+07 Transitions= 6.89111e+07 Memory= 2267.941
Depth=     542 States= 4.3e+07 Transitions= 7.05942e+07 Memory= 2319.039
Depth=     542 States= 4.4e+07 Transitions= 7.22497e+07 Memory= 2370.648
Depth=     542 States= 4.5e+07 Transitions= 7.39238e+07 Memory= 2422.565
Depth=     542 States= 4.6e+07 Transitions= 7.55778e+07 Memory= 2474.789
Depth=     542 States= 4.7e+07 Transitions= 7.72751e+07 Memory= 2526.603
Depth=     542 States= 4.8e+07 Transitions= 7.89392e+07 Memory= 2577.496
Depth=     542 States= 4.9e+07 Transitions= 8.06222e+07 Memory= 2629.618
Depth=     542 States=   5e+07 Transitions= 8.23015e+07 Memory= 2681.330
Depth=     542 States= 5.1e+07 Transitions= 8.39859e+07 Memory= 2733.247
Depth=     542 States= 5.2e+07 Transitions= 8.56752e+07 Memory= 2785.266
Depth=     542 States= 5.3e+07 Transitions= 8.73573e+07 Memory= 2836.978
Depth=     542 States= 5.4e+07 Transitions= 8.90469e+07 Memory= 2887.973
Depth=     542 States= 5.5e+07 Transitions= 9.06863e+07 Memory= 2939.583
Depth=     542 States= 5.6e+07 Transitions= 9.23405e+07 Memory= 2991.192
Depth=     542 States= 5.7e+07 Transitions= 9.4034e+07 Memory= 3041.983
pan: out of memory
hint: to reduce memory, recompile with
  -DMA=656   # better/slower compression, or
  -DBITSTATE # supertrace, approximation
(Spin Version 4.2.9 -- 8 February 2007)
Warning: Search not completed
        + 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 656 byte, depth reached 542, errors: 0
5.74468e+07 states, stored
3.73343e+07 states, matched
9.47811e+07 transitions (= stored+matched)
  500881 atomic steps
hash conflicts: 7.02097e+07 (resolved)

Stats on memory usage (in Megabytes):
38604.229       equivalent memory usage for states (stored*(State-vector + overhead))
2953.809        actual memory usage for states (compression: 7.65%)
        State-vector as stored = 35 byte + 16 byte overhead
67.109  memory used for hash table (-w24)
44.800  memory used for DFS stack (-m1400000)
0.616   memory lost to fragmentation
3065.125        total actual memory usage

nr of templates: [ globals chans procs ]
collapse counts: [ 281954 33 2457 102 1385 1907 2 2 ]

real    10m57.289s
user    10m50.300s
sys     0m6.150s