#define oneLeader	(leader[0] + leader[1] + leader[2] + leader[3] + leader[4] + leader[5]+ leader[6]+ leader[7]== 1)
#define correct		(detectorcorrect == 1)

	/*
	 * Formula As Typed: <>  []  oneLeader
	 * The Never Claim Below Corresponds
	 * To The Negated Formula !(<>  []  oneLeader)
	 * (formalizing violations of the original)
	 */

never {    /* !(<>  []  oneLeader) */
T0_init:
	if
	:: (! ((oneLeader))) -> goto accept_S9
	:: (1) -> goto T0_init
	fi;
accept_S9:
	if
	:: (1) -> goto T0_init
	fi;
}

#ifdef NOTES







#endif
#ifdef RESULT
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 297)
Depth=   18718 States=    1e+06 Transitions= 5.94e+07 Memory=    18.724	t= 1.73e+03 R=   6e+02
Depth=   18718 States=    2e+06 Transitions= 1.18e+08 Memory=    18.724	t= 3.47e+03 R=   6e+02
pan: resizing hashtable to -w21..  done
Depth=   18718 States=    3e+06 Transitions= 1.74e+08 Memory=    30.630	t= 5.13e+03 R=   6e+02
Depth=   18718 States=    4e+06 Transitions= 1.84e+08 Memory=    36.099	t= 5.38e+03 R=   7e+02
Depth=   18718 States=    5e+06 Transitions= 1.85e+08 Memory=    42.349	t= 5.42e+03 R=   9e+02
pan: resizing hashtable to -w23..  done
Depth=   18718 States=    6e+06 Transitions= 1.87e+08 Memory=    77.864	t= 5.45e+03 R=   1e+03
Depth=   18718 States=    7e+06 Transitions= 1.88e+08 Memory=    84.114	t= 5.48e+03 R=   1e+03
Depth=   18718 States=    8e+06 Transitions=  1.9e+08 Memory=    89.974	t= 5.51e+03 R=   1e+03
Depth=   18718 States=    9e+06 Transitions= 1.91e+08 Memory=    95.833	t= 5.54e+03 R=   2e+03
Depth=   18718 States=    1e+07 Transitions= 1.93e+08 Memory=   101.302	t= 5.57e+03 R=   2e+03
Depth=   18718 States=  1.1e+07 Transitions= 1.94e+08 Memory=   107.161	t= 5.61e+03 R=   2e+03
Depth=   18718 States=  1.2e+07 Transitions= 1.96e+08 Memory=   113.021	t= 5.64e+03 R=   2e+03
Depth=   18718 States=  1.3e+07 Transitions= 1.97e+08 Memory=   118.489	t= 5.67e+03 R=   2e+03
Depth=   18718 States=  1.4e+07 Transitions= 1.99e+08 Memory=   124.349	t= 5.7e+03 R=   2e+03
pan: out of memory
	1.34075e+08 bytes used
	409600 bytes more needed
	1.34218e+08 bytes limit
hint: to reduce memory, recompile with
  -DCOLLAPSE # good, fast compression, or
  -DMA=2096   # better/slower compression, or
  -DHC # hash-compaction, approximation
  -DBITSTATE # supertrace, approximation

(Spin Version 5.1.6 -- 9 May 2008)
Warning: Search not completed
	+ Partial Order Reduction

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

State-vector 2096 byte, depth reached 18718, errors: 0
    80483 states, stored (1.46409e+07 visited)
1.8528198e+08 states, matched
1.9992284e+08 transitions (= visited+matched)
 72776012 atomic steps
hash conflicts:    651077 (resolved)

Stats on memory usage (in Megabytes):
  162.106	equivalent memory usage for states (stored*(State-vector + overhead))
   93.778	actual memory usage for states (compression: 57.85%)
         	state-vector as stored = 1206 byte + 16 byte overhead
   32.000	memory used for hash table (-w23)
    3.052	memory used for DFS stack (-m100000)
  127.864	total actual memory usage

unreached in proctype Rule1
	line 22, "pan.___", state 7, "-end-"
	(1 of 7 states)
unreached in proctype Rule2
	line 33, "pan.___", state 7, "-end-"
	(1 of 7 states)
unreached in proctype Rule3
	line 44, "pan.___", state 7, "-end-"
	(1 of 7 states)
unreached in proctype DetectorCorrect
	line 54, "pan.___", state 6, "-end-"
	(1 of 6 states)
unreached in proctype RandomDetector
	line 61, "pan.___", state 8, "-end-"
	(1 of 8 states)
unreached in proctype :init:
	(0 of 236 states)
unreached in proctype :never:
	line 304, "pan.___", state 11, "-end-"
	(1 of 11 states)

pan: elapsed time 5.72e+03 seconds
pan: rate 2559.5406 states/second
pan: avg transition delay 2.8612e-05 usec

#endif
