#define p	in?[red]
#define q	out?[red]
#define r		(BS[a_id]@progress || BS[p_id]@progress)

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

never {    /* !((![]<>(r)) -> [](<>p -> <>q)) */
T0_init:
	if
	:: (! ((q)) && ! ((r)) && (p)) -> goto accept_S8
	:: (! ((q)) && ! ((r))) -> goto T0_S17
	:: (! ((q)) && (p)) -> goto T0_S44
	:: (! ((q))) -> goto T0_S58
	:: (! ((r))) -> goto T0_S91
	:: (1) -> goto T0_init
	fi;
accept_S8:
	if
	:: (! ((q)) && ! ((r))) -> goto accept_S8
	fi;
T0_S17:
	if
	:: (! ((q)) && ! ((r)) && (p)) -> goto accept_S8
	:: (! ((q)) && ! ((r))) -> goto T0_S17
	fi;
T0_S44:
	if
	:: (! ((q)) && ! ((r))) -> goto accept_S8
	:: (! ((q))) -> goto T0_S44
	fi;
T0_S58:
	if
	:: (! ((q)) && ! ((r)) && (p)) -> goto accept_S8
	:: (! ((q)) && ! ((r))) -> goto T0_S17
	:: (! ((q)) && (p)) -> goto T0_S44
	:: (! ((q))) -> goto T0_S58
	fi;
T0_S91:
	if
	:: (! ((q)) && ! ((r)) && (p)) -> goto accept_S8
	:: (! ((q)) && ! ((r))) -> goto T0_S17
	:: (! ((r))) -> goto T0_S91
	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-closed
(never claims generated from LTL formulae are stutter-closed)
(Spin Version 3.4.0 -- 7 August 2000)
	+ Partial Order Reduction

Full statespace search for:
	never-claim         	+
	assertion violations	+ (if within scope of claim)
	acceptance   cycles 	+ (fairness disabled)
	invalid endstates	- (disabled by never-claim)

State-vector 128 byte, depth reached 1833, errors: 0
   44455 states, stored (48719 visited)
  137737 states, matched
  186456 transitions (= visited+matched)
     241 atomic steps
hash conflicts: 8962 (resolved)
(max size 2^19 states)

Stats on memory usage (in Megabytes):
6.046 	equivalent memory usage for states (stored*(State-vector + overhead))
3.379 	actual memory usage for states (compression: 55.89%)
	State-vector as stored = 68 byte + 8 byte overhead
2.097 	memory used for hash-table (-w19)
0.240 	memory used for DFS stack (-m10000)
5.819 	total actual memory usage

unreached in proctype CC
	line 49, state 25, "-end-"
	(1 of 25 states)
unreached in proctype HC
	line 56, state 6, "-end-"
	(1 of 6 states)
unreached in proctype MSC
	(0 of 4 states)
unreached in proctype BS
	line 95, state 31, "-end-"
	(1 of 31 states)
unreached in proctype MS
	line 108, state 14, "-end-"
	(1 of 14 states)
unreached in proctype P
	(0 of 4 states)
unreached in proctype Q
	(0 of 4 states)
unreached in proctype System
	(0 of 4 states)
unreached in proctype top
	line 143, state 7, "-end-"
	(1 of 7 states)
unreached in proctype bot
	line 149, state 7, "-end-"
	(1 of 7 states)
5.1u 0.1s 5r 	 ./pan -X -m10000 -w19 -a ...

#endif