#define correct		(detectorcorrect == 1)
#define oneLeader	(token[0] + token[1] + token[2] + token[3] + token[4] == 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
Use Load to open a file or a template.





#endif
#ifdef RESULT
warning: -i or -I work for safety properties only
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 189)
pan: acceptance cycle (at depth 108)
pan: wrote pan_in.trail
pan: reducing search depth to 225
pan: wrote pan_in.trail
pan: reducing search depth to 223
pan: wrote pan_in.trail
pan: reducing search depth to 221
pan: wrote pan_in.trail
pan: reducing search depth to 219
pan: wrote pan_in.trail
pan: reducing search depth to 157
pan: wrote pan_in.trail
pan: reducing search depth to 149
pan: wrote pan_in.trail
pan: reducing search depth to 145
(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 212 byte, depth reached 295, errors: 7
   14427 states, stored (143751 visited)
  179203 states, matched
  322954 transitions (= visited+matched)
    1020 atomic steps
hash conflicts: 503 (resolved)

Stats on memory usage (in Megabytes):
3.232 	equivalent memory usage for states (stored*(State-vector + overhead))
2.243 	actual memory usage for states (compression: 69.42%)
	State-vector as stored = 143 byte + 12 byte overhead
2.097 	memory used for hash table (-w19)
0.005 	memory used for DFS stack (-m145)
0.085 	memory lost to fragmentation
4.260 	total actual memory usage

unreached in proctype Rule1
	line 26, "pan.___", state 10, "-end-"
	(1 of 10 states)
unreached in proctype Rule2
	line 38, "pan.___", state 11, "-end-"
	(1 of 11 states)
unreached in proctype Rule3
	line 50, "pan.___", state 12, "-end-"
	(1 of 12 states)
unreached in proctype Rule4
	line 62, "pan.___", state 11, "-end-"
	(1 of 11 states)
unreached in proctype Rule5
	line 74, "pan.___", state 11, "-end-"
	(1 of 11 states)
unreached in proctype DetectorCorrect
	line 81, "pan.___", state 2, "detectorcorrect = 1"
	line 79, "pan.___", state 3, "((detectorcorrect==0))"
	line 83, "pan.___", state 6, "-end-"
	(3 of 6 states)
unreached in proctype RandomDetector
	line 86, "pan.___", state 7, "((detectorcorrect==0))"
	line 86, "pan.___", state 7, "((detectorcorrect==0))"
	line 90, "pan.___", state 10, "-end-"
	(2 of 10 states)
unreached in proctype :init:
	(0 of 91 states)
unreached in proctype :never:
	line 196, "pan.___", state 11, "-end-"
	(1 of 11 states)
1.42user 0.01system 0:01.43elapsed 100%CPU (0avgtext+0avgdata 0maxresident)k
0inputs+0outputs (0major+1187minor)pagefaults 0swaps

#endif
