------------------------------------------ 3 Threads -----------------------------------------------------

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 86)
pan: claim violated! (at depth 423)
pan: wrote pan_in.trail

(Spin Version 5.1.4 -- 27 January 2008)
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 108 byte, depth reached 495, errors: 1
     3065 states, stored
     1930 states, matched
     4995 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         3 (resolved)

Stats on memory usage (in Megabytes):
    0.362	equivalent memory usage for states (stored*(State-vector + overhead))
    0.569	actual memory usage for states (unsuccessful compression: 157.06%)
         	state-vector as stored = 179 byte + 16 byte overhead
    2.000	memory used for hash table (-w19)
   30.518	memory used for DFS stack (-m1000000)
   33.006	total actual memory usage
unreached in proctype main
	(0 of 84 states)
unreached in proctype :never:
	line 91, "pan.___", state 8, "-end-"
	(1 of 8 states)

pan: elapsed time 0.031 seconds
pan: rate 98870.968 states/second
pan: avg transition delay 6.2062e-06 usec


------------------------------------------ 4 Threads -----------------------------------------------------

depth 0: Claim reached state 5 (line 88)
pan: claim violated! (at depth 545)
pan: wrote pan_in.trail

(Spin Version 5.1.4 -- 27 January 2008)
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 140 byte, depth reached 633, errors: 1
    12766 states, stored
    13370 states, matched
    26136 transitions (= stored+matched)
        0 atomic steps
hash conflicts:        81 (resolved)

Stats on memory usage (in Megabytes):
    1.899	equivalent memory usage for states (stored*(State-vector + overhead))
    2.029	actual memory usage for states (unsuccessful compression: 106.83%)
         	state-vector as stored = 151 byte + 16 byte overhead
    2.000	memory used for hash table (-w19)
   30.518	memory used for DFS stack (-m1000000)
   34.471	total actual memory usage
unreached in proctype main
	(0 of 99 states)
unreached in proctype :never:
	line 93, "pan.___", state 8, "-end-"
	(1 of 8 states)

pan: elapsed time 0.093 seconds
pan: rate 137268.82 states/second
pan: avg transition delay 3.5583e-06 usec


------------------------------------------ 5 Threads -----------------------------------------------------

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 88)
pan: claim violated! (at depth 667)
pan: wrote pan_in.trail

(Spin Version 5.1.4 -- 27 January 2008)
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 168 byte, depth reached 771, errors: 1
    56067 states, stored
    85110 states, matched
   141177 transitions (= stored+matched)
        0 atomic steps
hash conflicts:      2566 (resolved)

Stats on memory usage (in Megabytes):
    9.838	equivalent memory usage for states (stored*(State-vector + overhead))
    9.453	actual memory usage for states (compression: 96.08%)
         	state-vector as stored = 161 byte + 16 byte overhead
    2.000	memory used for hash table (-w19)
   30.518	memory used for DFS stack (-m1000000)
   41.893	total actual memory usage
unreached in proctype main
	(0 of 114 states)
unreached in proctype :never:
	line 93, "pan.___", state 8, "-end-"
	(1 of 8 states)

pan: elapsed time 0.5 seconds
pan: rate    112134 states/second
pan: avg transition delay 3.5417e-06 usec

------------------------------------------ 6 Threads -----------------------------------------------------

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 87)
pan: claim violated! (at depth 789)
pan: wrote pan_in.trail

(Spin Version 5.1.4 -- 27 January 2008)
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 200 byte, depth reached 909, errors: 1
   244478 states, stored
   496330 states, matched
   740808 transitions (= stored+matched)
        0 atomic steps
hash conflicts:     70429 (resolved)

Stats on memory usage (in Megabytes):
   50.361	equivalent memory usage for states (stored*(State-vector + overhead))
   47.843	actual memory usage for states (compression: 95.00%)
         	state-vector as stored = 189 byte + 16 byte overhead
    2.000	memory used for hash table (-w19)
   30.518	memory used for DFS stack (-m1000000)
   80.272	total actual memory usage
unreached in proctype main
	(0 of 129 states)
unreached in proctype :never:
	line 92, "pan.___", state 8, "-end-"
	(1 of 8 states)

pan: elapsed time 2.92 seconds
pan: rate 83696.679 states/second
pan: avg transition delay 3.943e-06 usec



------------------------------------------ 7 Threads -----------------------------------------------------
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 87)
Depth=    1047 States=    1e+06 Transitions= 3.57e+06 Memory=   254.490	t=   16.4 R=   6e+04
pan: claim violated! (at depth 911)
pan: wrote pan_in.trail

(Spin Version 5.1.4 -- 27 January 2008)
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 228 byte, depth reached 1047, errors: 1
  1046989 states, stored
  2718530 states, matched
  3765519 transitions (= stored+matched)
        0 atomic steps
hash conflicts:   1767172 (resolved)

Stats on memory usage (in Megabytes):
  243.631	equivalent memory usage for states (stored*(State-vector + overhead))
  232.998	actual memory usage for states (compression: 95.64%)
         	state-vector as stored = 217 byte + 16 byte overhead
    2.000	memory used for hash table (-w19)
   30.518	memory used for DFS stack (-m1000000)
  265.037	total actual memory usage
unreached in proctype main
	(0 of 144 states)
unreached in proctype :never:
	line 92, "pan.___", state 8, "-end-"
	(1 of 8 states)

pan: elapsed time 17.4 seconds
pan: rate  60151.04 states/second
pan: avg transition delay 4.6225e-06 usec


------------------------------------------ 8 Threads -----------------------------------------------------
Got out of memory!