#define oneLeader	(leader[0] + leader[1] + leader[2]+ leader[3] + leader[4]== 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 125)
(Spin Version 4.3.0 -- 22 June 2007)
	+ 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 248 byte, depth reached 322, errors: 0
     558 states, stored (14791 visited)
   78183 states, matched
   92974 transitions (= visited+matched)
   17476 atomic steps
hash conflicts: 0 (resolved)

Stats on memory usage (in Megabytes):
0.145 	equivalent memory usage for states (stored*(State-vector + overhead))
0.298 	actual memory usage for states (unsuccessful compression: 205.41%)
	State-vector as stored = 522 byte + 12 byte overhead
2.097 	memory used for hash table (-w19)
0.320 	memory used for DFS stack (-m10000)
0.093 	memory lost to fragmentation
2.622 	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 46 states)
unreached in proctype :never:
	line 132, "pan.___", state 11, "-end-"
	(1 of 11 states)
0.42user 0.00system 0:00.42elapsed 100%CPU (0avgtext+0avgdata 0maxresident)k
0inputs+0outputs (0major+788minor)pagefaults 0swaps

#endif
