#define w1 wait[0]==1
#define w2 wait[1]==1
#define e1 (waitS==1 && len(request[0])>0)
#define x1 (sender==1)

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

never {    /* !((([]<>e1) -> ([]<>x1)) -> [](w1 -> <>!w1)) */
T0_init:
	if
	:: ((w1) && (x1)) -> goto accept_S143
	:: ((w1)) -> goto T0_S143
	:: (! ((e1)) && (w1)) -> goto accept_S219
	:: ((w1)) -> goto T0_S234
	:: (1) -> goto T0_S160
	:: (! ((e1))) -> goto T0_S223
	:: (1) -> goto T0_S214
	fi;
accept_S143:
	if
	:: ((w1)) -> goto T0_S143
	fi;
accept_S219:
	if
	:: (! ((e1)) && (w1)) -> goto accept_S219
	fi;
T0_S143:
	if
	:: ((w1) && (x1)) -> goto accept_S143
	:: ((w1)) -> goto T0_S143
	fi;
T0_S160:
	if
	:: (1) -> goto T0_S160
	:: ((w1) && (x1)) -> goto accept_S143
	:: ((w1)) -> goto T0_S143
	fi;
T0_S223:
	if
	:: (! ((e1)) && (w1)) -> goto accept_S219
	:: (! ((e1))) -> goto T0_S223
	fi;
T0_S214:
	if
	:: (! ((e1)) && (w1)) -> goto accept_S219
	:: (! ((e1))) -> goto T0_S223
	:: (1) -> goto T0_S214
	:: ((w1)) -> goto T0_S234
	fi;
T0_S234:
	if
	:: (! ((e1)) && (w1)) -> goto accept_S219
	:: ((w1)) -> goto T0_S234
	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 260: Claim reached state 37 (line 107)
depth 250: Claim reached state 29 (line 102)
depth 98: Claim reached state 23 (line 98)
(Spin Version 4.2.2 -- 12 December 2004)
	+ 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 52 byte, depth reached 637, errors: 0
    3586 states, stored (4325 visited)
    7851 states, matched
   12176 transitions (= visited+matched)
       0 atomic steps
hash conflicts: 8 (resolved)

Stats on memory usage (in Megabytes):
0.215 	equivalent memory usage for states (stored*(State-vector + overhead))
0.399 	actual memory usage for states (unsuccessful compression: 185.64%)
	State-vector as stored = 103 byte + 8 byte overhead
2.097 	memory used for hash table (-w19)
0.320 	memory used for DFS stack (-m10000)
0.136 	other (proc and chan stacks)
0.092 	memory lost to fragmentation
2.724 	total actual memory usage

unreached in proctype client
	line 24, "pan.___", state 13, "-end-"
	(1 of 13 states)
unreached in proctype server
	line 61, "pan.___", state 29, "-end-"
	(1 of 29 states)
unreached in proctype :init:
	(0 of 4 states)
unreached in proctype :never:
	line 129, "pan.___", state 61, "-end-"
	(1 of 61 states)
0.00user 0.11system 0:00.11elapsed 93%CPU (0avgtext+0avgdata 0maxresident)k
0inputs+0outputs (0major+778minor)pagefaults 0swaps

#endif