~/atva/Ocaml/speedtest/giop > run_modella.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=     579 States=   1e+06 Transitions= 2.3739e+06 Memory= 634.559
Depth=     579 States=   2e+06 Transitions= 4.68475e+06 Memory= 1072.831
Depth=     579 States=   3e+06 Transitions= 7.00122e+06 Memory= 1595.275
Depth=     579 States=   4e+06 Transitions= 9.38044e+06 Memory= 2006.207
Depth=     580 States=   5e+06 Transitions= 1.17548e+07 Memory= 2472.946
Depth=     580 States=   6e+06 Transitions= 1.41642e+07 Memory= 2995.391
pan: out of memory
hint: to reduce memory, recompile with
  -DCOLLAPSE # good, fast compression, or
  -DMA=656   # better/slower compression, or
  -DHC # hash-compaction, approximation
  -DBITSTATE # supertrace, approximation
(Spin Version 4.2.9 -- 8 February 2007)
Warning: Search not completed
        + Partial Order Reduction

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 580, errors: 0
5.64691e+06 states, stored (6.12812e+06 visited)
8.34468e+06 states, matched
1.44728e+07 transitions (= visited+matched)
      23 atomic steps
hash conflicts: 870339 (resolved)

Stats on memory usage (in Megabytes):
3772.135        equivalent memory usage for states (stored*(State-vector + overhead))
2964.225        actual memory usage for states (compression: 78.58%)
        State-vector as stored = 513 byte + 12 byte overhead
67.109  memory used for hash table (-w24)
44.800  memory used for DFS stack (-m1400000)
13.899  memory lost to fragmentation
3062.258        total actual memory usage


real    1m11.883s
user    1m2.590s
sys     0m6.590s