#define p	cc_goods
#define q	cc_pay


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

never {    /* !([] ((p) -> (<> (q)))) */
T0_init:
	if
	:: (! ((q)) && (p)) -> goto accept_S4
	:: (1) -> goto T0_init
	fi;
accept_S4:
	if
	:: (! ((q))) -> goto accept_S4
	fi;
}


#ifdef NOTES

Here we are check the property that the shipment of goods, will eventualy lead to the payments of the goods.

#endif
#ifdef RESULT


#endif