#define point1Act Endpoint[1]@ACTIVE
#define point2Act Endpoint[2]@ACTIVE
	/*
	 * Formula As Typed: ([] <> point1Act) && ([] <> point2Act)
	 * The Never Claim Below Corresponds
	 * To The Negated Formula !(([] <> point1Act) && ([] <> point2Act))
	 * (formalizing violations of the original)
	 */

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

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












#endif
#ifdef RESULT

#endif