1 warning: for p.o. reduction to be valid the never claim must be stutter-invariant
2 (never claims generated from LTL formulae are stutter-invariant)
3 depth 0: Claim reached state 5 (line 321)
4 Depth= 201 States= 1e+06 Transitions= 3.11e+06 Memory= 79.063 t= 25.4 R= 4e+04
5 Depth= 201 States= 2e+06 Transitions= 6.44e+06 Memory= 156.895 t= 46.1 R= 4e+04
6 pan: resizing hashtable to -w21.. done
8 (Spin Version 5.1.6 -- 9 May 2008)
9 + Partial Order Reduction
11 Full statespace search for:
13 assertion violations + (if within scope of claim)
14 acceptance cycles + (fairness disabled)
15 invalid end states - (disabled by never claim)
17 State-vector 100 byte, depth reached 203, errors: 0
18 2590821 states, stored
19 5924281 states, matched
20 8515102 transitions (= stored+matched)
22 hash conflicts: 6260639 (resolved)
24 Stats on memory usage (in Megabytes):
25 286.613 equivalent memory usage for states (stored*(State-vector + overhead))
26 202.768 actual memory usage for states (compression: 70.75%)
27 state-vector as stored = 66 byte + 16 byte overhead
28 8.000 memory used for hash table (-w21)
29 0.305 memory used for DFS stack (-m10000)
30 210.891 total actual memory usage
32 unreached in proctype switcher
34 unreached in proctype tracer
36 unreached in proctype reader
38 unreached in proctype cleaner
40 unreached in proctype :init:
42 unreached in proctype :never:
43 line 326, "pan.___", state 8, "-end-"
46 pan: elapsed time 56.4 seconds
47 pan: rate 45960.99 states/second
48 pan: avg transition delay 6.62e-06 usec
49 23.05user 0.18system 0:56.38elapsed 41%CPU (0avgtext+0avgdata 0maxresident)k
50 0inputs+0outputs (0major+54128minor)pagefaults 0swaps