#define p0c	proc0InCrit == true
#define p1c	proc1InCrit == true

	/*
	 * Formula As Typed: []   (! (p0c && p1c))
	 * The Never Claim Below Corresponds
	 * To The Negated Formula !([]   (! (p0c && p1c)))
	 * (formalizing violations of the original)
	 */

never {    /* !([]   (! (p0c && p1c))) */
T0_init:
	if
	:: ((p0c) && (p1c)) -> goto accept_all
	:: (1) -> goto T0_init
	fi;
accept_all:
	skip
}

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











#endif
#ifdef RESULT

#endif