#define inAct Initiator@ACTIVE
#define ninAct Noninitiator@ACTIVE
	/*
	 * Formula As Typed: ([] <> inAct) && ([] <> ninAct)
	 * The Never Claim Below Corresponds
	 * To The Negated Formula !(([] <> inAct) && ([] <> ninAct))
	 * (formalizing violations of the original)
	 */

never {    /* !(([] <> inAct) && ([] <> ninAct)) */
T0_init:
	if
	:: (! ((ninAct))) -> goto accept_S5
	:: (! ((inAct))) -> goto accept_S10
	:: (1) -> goto T0_init
	fi;
accept_S5:
	if
	:: (! ((ninAct))) -> goto accept_S5
	fi;
accept_S10:
	if
	:: (! ((inAct))) -> goto accept_S10
	fi;
}

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











#endif
#ifdef RESULT

#endif