#define w1 client[1]@W
#define w2 client[2]@W
#define r1 (server@R && len(request[0])>0)
#define r2 (server@R && len(request[1])>0)
#define s1 server@S1
#define s2 server@S2

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

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

#ifdef NOTES
Use Load to open a file or a template.


#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 9 (line 72)
depth 0: Claim reached state 9 (line 73)
depth 0: Claim reached state 9 (line 74)
depth 46: Claim reached state 15 (line 79)
depth 46: Claim reached state 15 (line 80)
depth 48: Claim reached state 35 (line 94)
depth 52: Claim reached state 27 (line 89)
depth 68: Claim reached state 27 (line 90)
depth 66: Claim reached state 27 (line 88)
depth 68: Claim reached state 35 (line 95)
depth 68: Claim reached state 35 (line 96)
depth 66: Claim reached state 35 (line 93)
depth 50: Claim reached state 21 (line 84)
depth 50: Claim reached state 21 (line 85)
depth 48: Claim reached state 47 (line 100)
depth 48: Claim reached state 47 (line 101)
depth 170: Claim reached state 47 (line 103)
depth 170: Claim reached state 47 (line 104)
(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 disabled)
	invalid end states	- (disabled by never claim)

State-vector 48 byte, depth reached 301, errors: 0
     683 states, stored (969 visited)
    1547 states, matched
    2516 transitions (= visited+matched)
       0 atomic steps
hash conflicts: 0 (resolved)

Stats on memory usage (in Megabytes):
0.041 	equivalent memory usage for states (stored*(State-vector + overhead))
0.298 	actual memory usage for states (unsuccessful compression: 727.92%)
	State-vector as stored = 425 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 client
	line 14, "pan.___", state 9, "-end-"
	(1 of 9 states)
unreached in proctype server
	line 46, "pan.___", state 27, "-end-"
	(1 of 27 states)
unreached in proctype :init:
	(0 of 4 states)
unreached in proctype :never:
	line 106, "pan.___", state 49, "-end-"
	(1 of 49 states)
0.00user 0.00system 0:00.01elapsed 120%CPU (0avgtext+0avgdata 0maxresident)k
0inputs+0outputs (0major+768minor)pagefaults 0swaps

#endif