#define p	cc[1].state==cc_idle  || cc[1].state==cc_discharged
#define q	cc[2].state==cc_idle  || cc[2].state==cc_discharged

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

never {    /* !(<>   (p && q) ) */
accept_init:
T0_init:
	if
	:: (((! ((p))) || (! ((q))))) -> goto T0_init
	fi;
}

#ifdef NOTES
Here it verifies that all commitment will eventually be come either idle or discharged.


#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 3 (line 559)
Depth=     130 States=   1e+06 Transitions= 2.49245e+06 Memory= 34.514

#endif