#define p	buyer_rejectQuote
#define q gateway_captured

	/*
	 * 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
	:: ((p) && (q)) -> goto accept_all
	:: (1) -> goto T0_init
	fi;
accept_all:
	skip
}

#ifdef NOTES
It that always true that when buyer reject a Quote, it should not be obliged to pay.
#endif
#ifdef RESULT
warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)
depth 0: Claim reached state 5 (line 558)
Depth=     463 States=   1e+06 Transitions= 2.108e+06 Memory= 12.805
Depth=     463 States=   2e+06 Transitions= 4.20214e+06 Memory= 14.136

#endif