warning: for p.o. reduction to be valid the never claim must be stutter-closed
(never claims generated from LTL formulae are stutter-closed)
pan: claim violated! (at depth 146)
pan: wrote RW4.prom.trail
(Spin Version 3.0.9 -- 11 January 1998)
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 endstates	- (disabled by never-claim)

State-vector 344 byte, depth reached 2889, errors: 1
  235966 states, stored
  715453 states, matched
  951419 transitions (= stored+matched)
1.87259e+06 atomic steps
hash conflicts: 383865 (resolved)
(max size 2^18 states)

Stats on memory usage (in Megabytes):
83.060	equivalent memory usage for states (stored*(State-vector + overhead))
23.654	actual memory usage for states (compression: 28.48%)
	State-vector as stored = 92 byte + 8 byte overhead
1.049 	memory used for hash-table (-w18)
0.240 	memory used for DFS stack (-m10000)
25.762	total actual memory usage

warning: for p.o. reduction to be valid the never claim must be stutter-closed
(never claims generated from LTL formulae are stutter-closed)
(Spin Version 3.0.9 -- 11 January 1998)
	+ Partial Order Reduction

Full statespace search for:
	never-claim         	+
	assertion violations	+ (if within scope of claim)
	acceptance   cycles 	+ (fairness disabled)
	invalid endstates	- (disabled by never-claim)

State-vector 344 byte, depth reached 2781, errors: 0
   31517 states, stored
   31034 states, matched
   62551 transitions (= stored+matched)
  124923 atomic steps
hash conflicts: 9198 (resolved)
(max size 2^18 states)

Stats on memory usage (in Megabytes):
11.094	equivalent memory usage for states (stored*(State-vector + overhead))
3.174 	actual memory usage for states (compression: 28.61%)
	State-vector as stored = 93 byte + 8 byte overhead
1.049 	memory used for hash-table (-w18)
0.240 	memory used for DFS stack (-m10000)
5.385 	total actual memory usage

warning: for p.o. reduction to be valid the never claim must be stutter-closed
(never claims generated from LTL formulae are stutter-closed)
pan: acceptance cycle (at depth 227)
pan: wrote RW5.prom.trail
(Spin Version 3.0.9 -- 11 January 1998)
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 endstates	- (disabled by never-claim)

State-vector 344 byte, depth reached 330, errors: 1
    6355 states, stored (6461 visited)
   10114 states, matched
   16575 transitions (= visited+matched)
   94523 atomic steps
hash conflicts: 380 (resolved)
(max size 2^18 states)

Stats on memory usage (in Megabytes):
2.237 	equivalent memory usage for states (stored*(State-vector + overhead))
0.717 	actual memory usage for states (compression: 32.04%)
	State-vector as stored = 105 byte + 8 byte overhead
1.049 	memory used for hash-table (-w18)
0.240 	memory used for DFS stack (-m10000)
2.927 	total actual memory usage

warning: for p.o. reduction to be valid the never claim must be stutter-closed
(never claims generated from LTL formulae are stutter-closed)
pan: acceptance cycle (at depth 640)
pan: wrote RW5.prom.trail
(Spin Version 3.0.9 -- 11 January 1998)
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 endstates	- (disabled by never-claim)

State-vector 344 byte, depth reached 714, errors: 1
     199 states, stored (201 visited)
     122 states, matched
     323 transitions (= visited+matched)
    1907 atomic steps
hash conflicts: 0 (resolved)
(max size 2^18 states)

2.313 	memory usage (Mbyte)

warning: for p.o. reduction to be valid the never claim must be stutter-closed
(never claims generated from LTL formulae are stutter-closed)
pan: claim violated! (at depth 6125)
pan: wrote RWlist6.prom.trail
(Spin Version 3.0.9 -- 11 January 1998)
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 endstates	- (disabled by never-claim)

State-vector 380 byte, depth reached 8388, errors: 1
   16818 states, stored
   28885 states, matched
   45703 transitions (= stored+matched)
  531040 atomic steps
hash conflicts: 998 (resolved)
(max size 2^18 states)

Stats on memory usage (in Megabytes):
6.525 	equivalent memory usage for states (stored*(State-vector + overhead))
1.843 	actual memory usage for states (compression: 28.25%)
	State-vector as stored = 102 byte + 8 byte overhead
1.049 	memory used for hash-table (-w18)
0.240 	memory used for DFS stack (-m10000)
4.668 	total actual memory usage