~/atva/Ocaml/speedtest/giop > 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=     579 States=   1e+06 Transitions= 2.3739e+06 Memory= 634.559
pan: claim violated! (at depth 407)
pan: wrote giop3.pr.trail
(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 579, errors: 1
1.0565e+06 states, stored
1.45456e+06 states, matched
2.51106e+06 transitions (= stored+matched)
      20 atomic steps
hash conflicts: 23525 (resolved)

Stats on memory usage (in Megabytes):
705.743 equivalent memory usage for states (stored*(State-vector + overhead))
554.780 actual memory usage for states (compression: 78.61%)
        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)
2.663   memory lost to fragmentation
664.050 total actual memory usage


real    0m12.589s
user    0m11.400s
sys     0m1.170s