#define at_entry_1 (P1@entry_1)
#define at_crit_1  (P1@crit_1)
#define at_entry_2 (P2@entry_2)
#define at_crit_2  (P2@crit_2)

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

never {    /* !([]  ((at_entry_1  && []  ! at_entry_2 ) -> <>  at_crit_1)) */
T0_init:
	if
	:: (! ((at_crit_1)) && ! ((at_entry_2)) && (at_entry_1)) -> goto accept_S6
	:: (1) -> goto T0_init
	fi;
accept_S6:
	if
	:: (! ((at_crit_1)) && ! ((at_entry_2))) -> goto accept_S6
	fi;
}

#ifdef NOTES
Obligingness property for process P1







#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 77)
depth 42: Claim reached state 9 (line 82)
depth 94: Claim reached state 9 (line 81)
pan: acceptance cycle (at depth 88)
pan: wrote pan_in.trail
pan: reducing search depth to 135
pan: wrote pan_in.trail
pan: reducing search depth to 133
pan: wrote pan_in.trail
pan: reducing search depth to 131
pan: wrote pan_in.trail
pan: reducing search depth to 129
pan: wrote pan_in.trail
pan: reducing search depth to 125
pan: wrote pan_in.trail
pan: reducing search depth to 123
pan: wrote pan_in.trail
pan: reducing search depth to 117
pan: wrote pan_in.trail
pan: reducing search depth to 115
pan: wrote pan_in.trail
pan: reducing search depth to 113
pan: wrote pan_in.trail
pan: reducing search depth to 109
pan: wrote pan_in.trail
pan: reducing search depth to 107
pan: wrote pan_in.trail
pan: reducing search depth to 101
pan: wrote pan_in.trail
pan: reducing search depth to 99
pan: wrote pan_in.trail
pan: reducing search depth to 93
pan: wrote pan_in.trail
pan: reducing search depth to 91
(Spin Version 4.2.7 -- 23 June 2006)
	+ 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 24 byte, depth reached 135, errors: 15
     122 states, stored (207 visited)
     545 states, matched
     752 transitions (= visited+matched)
       0 atomic steps
hash conflicts: 0 (resolved)

Stats on memory usage (in Megabytes):
0.004 	equivalent memory usage for states (stored*(State-vector + overhead))
0.619 	actual memory usage for states (unsuccessful compression: 14088.07%)
	State-vector as stored = 5060 byte + 12 byte overhead
2.097 	memory used for hash table (-w19)
0.003 	memory used for DFS stack (-m91)
0.097 	memory lost to fragmentation
2.622 	total actual memory usage

unreached in proctype P1
	line 34, "pan.___", state 25, "-end-"
	(1 of 25 states)
unreached in proctype P2
	line 60, "pan.___", state 25, "-end-"
	(1 of 25 states)
unreached in proctype :never:
	line 84, "pan.___", state 11, "-end-"
	(1 of 11 states)
0.03user 0.02system 0:00.06elapsed 81%CPU (0avgtext+0avgdata 0maxresident)k
0inputs+0outputs (123major+1204minor)pagefaults 0swaps


#endif