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 0: Claim reached state 5 (line 321)
Depth=     201 States=    1e+06 Transitions= 3.11e+06 Memory=    79.063	t=   25.4 R=   4e+04
Depth=     201 States=    2e+06 Transitions= 6.44e+06 Memory=   156.895	t=   46.1 R=   4e+04
pan: resizing hashtable to -w21..  done

(Spin Version 5.1.6 -- 9 May 2008)
	+ 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 100 byte, depth reached 203, errors: 0
  2590821 states, stored
  5924281 states, matched
  8515102 transitions (= stored+matched)
  9636364 atomic steps
hash conflicts:   6260639 (resolved)

Stats on memory usage (in Megabytes):
  286.613	equivalent memory usage for states (stored*(State-vector + overhead))
  202.768	actual memory usage for states (compression: 70.75%)
         	state-vector as stored = 66 byte + 16 byte overhead
    8.000	memory used for hash table (-w21)
    0.305	memory used for DFS stack (-m10000)
  210.891	total actual memory usage

unreached in proctype switcher
	(0 of 31 states)
unreached in proctype tracer
	(0 of 51 states)
unreached in proctype reader
	(0 of 29 states)
unreached in proctype cleaner
	(0 of 9 states)
unreached in proctype :init:
	(0 of 47 states)
unreached in proctype :never:
	line 326, "pan.___", state 8, "-end-"
	(1 of 8 states)

pan: elapsed time 56.4 seconds
pan: rate  45960.99 states/second
pan: avg transition delay 6.62e-06 usec
23.05user 0.18system 0:56.38elapsed 41%CPU (0avgtext+0avgdata 0maxresident)k
0inputs+0outputs (0major+54128minor)pagefaults 0swaps