#define p	gateway_authOK
#define q	shipper_shipOrder


	/*
	 * 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
if 'p' is true in at least one state,
then sometime thereafter 'q' must also
become true at least once.

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

#endif
#ifdef RESULT


#endif