~/atva/Ocaml/speedtest/david_spec2 > run_wdba.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=   98277 States=   1e+06 Transitions= 3.4492e+06 Memory= 151.128
Depth=   98996 States=   2e+06 Transitions= 7.08086e+06 Memory= 190.757
Depth=  103809 States=   3e+06 Transitions= 1.09929e+07 Memory= 230.386
Depth=  231814 States=   4e+06 Transitions= 1.38877e+07 Memory= 270.527
Depth=  244062 States=   5e+06 Transitions= 1.77259e+07 Memory= 310.258
Depth=  332299 States=   6e+06 Transitions= 2.08647e+07 Memory= 350.399
Depth=  374980 States=   7e+06 Transitions= 2.44304e+07 Memory= 390.027
Depth=  425576 States=   8e+06 Transitions= 2.79288e+07 Memory= 429.656
Depth=  499122 States=   9e+06 Transitions= 3.14651e+07 Memory= 469.490
Depth=  549506 States=   1e+07 Transitions= 3.50619e+07 Memory= 509.426
Depth=  635585 States= 1.1e+07 Transitions= 3.87076e+07 Memory= 549.567
Depth=  676534 States= 1.2e+07 Transitions= 4.23316e+07 Memory= 589.503
Depth=  685520 States= 1.3e+07 Transitions= 4.61221e+07 Memory= 629.234
Depth=  685520 States= 1.4e+07 Transitions= 5.0024e+07 Memory= 668.863
Depth=  685520 States= 1.5e+07 Transitions= 5.40598e+07 Memory= 708.389
Depth=  685520 States= 1.6e+07 Transitions= 5.74388e+07 Memory= 746.687
(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 685520, errors: 0
1.68302e+07 states, stored
4.36242e+07 states, matched
6.04544e+07 transitions (= stored+matched)
1.13966e+08 atomic steps
hash conflicts: 1.43004e+07 (resolved)

Stats on memory usage (in Megabytes):
4308.532        equivalent memory usage for states (stored*(State-vector + overhead))
663.889 actual memory usage for states (compression: 15.41%)
        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)
2.702   other (proc and chan stacks)
0.135   memory lost to fragmentation
778.635 total actual memory usage

nr of templates: [ globals chans procs ]
collapse counts: [ 406 129 31 2067 210 4525 4251 2 2 ]

real    4m55.339s
user    4m53.650s
sys     0m1.130s