#define x2		(x == 2)
#define ready0  (flag[0] == 1)
#define ready1  (flag[1] == 1)
#define ready2  (flag[2] == 1)

	/*
	 * Formula As Typed:  [] ((ready0 && ready1 && ready2)  -> !x2)
	 * The Never Claim Below Corresponds
	 * To The Negated Formula !( [] ((ready0 && ready1 && ready2)  -> !x2))
	 * (formalizing violations of the original)
	 */

never {    /* !( [] ((ready0 && ready1 && ready2)  -> !x2)) */
T0_init:
	if
	:: ((ready0) && (ready1) && (ready2) && (x2)) -> goto accept_all
	:: (1) -> goto T0_init
	fi;
accept_all:
	skip
}


#ifdef NOTES









#endif
#ifdef RESULT

#endif