#define rdy (ready[0] == true && ready[1] == true)
#define ak (ackedId[0] == ackedId[1])
#define akSn (ackedSent[0] == ackedRecd[1])
#define akRc (ackedRecd[0] == ackedSent[1])
#define akPn (ackedId[0] == pendId[1])
#define akPnSn (ackedSent[0] == ((ackedRecd[1] + pendRecd[1]) % wrap))
#define akPnRc (ackedRecd[0] == ((ackedSent[1] + pendSent[1]) % wrap))
#define pnAk (pendId[0] == ackedId[1])
#define pnAkSn (((ackedSent[0] + pendSent[0]) % wrap) == ackedRecd[1])
#define pnAkRc (((ackedRecd[0] + pendRecd[0]) % wrap) == ackedSent[1])
	/*
	 * Formula As Typed: [] (rdy -> ((ak -> (akSn && akRc)) && (akPn  -> (akPnSn && akPnRc)) && (pnAk  -> (pnAkSn && pnAkRc)) && ((ak && !akPn && !pnAk) || (!ak && akPn && !pnAk) || (!ak && !akPn && pnAk))))
	 * The Never Claim Below Corresponds
	 * To The Negated Formula !([] (rdy -> ((ak -> (akSn && akRc)) && (akPn  -> (akPnSn && akPnRc)) && (pnAk  -> (pnAkSn && pnAkRc)) && ((ak && !akPn && !pnAk) || (!ak && akPn && !pnAk) || (!ak && !akPn && pnAk)))))
	 * (formalizing violations of the original)
	 */

never {    /* !([] (rdy -> ((ak -> (akSn && akRc)) && (akPn  -> (akPnSn && akPnRc)) && (pnAk  -> (pnAkSn && pnAkRc)) && ((ak && !akPn && !pnAk) || (!ak && akPn && !pnAk) || (!ak && !akPn && pnAk))))) */
T0_init:
	if
	:: (((! ((akRc)) && (ak) && (rdy) && (((ak) && ((! ((akRc))) || (! ((akSn))))) || ((pnAk) && ((! ((pnAkRc))) || (! ((pnAkSn)))))) && (((akPn) && ((! ((akPnRc))) || (! ((akPnSn))))) || ((((ak) && ((! ((akRc))) || (! ((akSn))))) || ((pnAk) && ((! ((pnAkRc))) || (! ((pnAkSn)))))))) && ((((! ((pnAk))) || ((((ak)) || ((akPn))))) && ((! ((akPn))) || ((((ak)) || ((pnAk))))) && ((! ((ak))) || ((((akPn)) || ((pnAk)))))) || ((((akPn) && ((! ((akPnRc))) || (! ((akPnSn))))) || ((((ak) && ((! ((akRc))) || (! ((akSn))))) || ((pnAk) && ((! ((pnAkRc))) || (! ((pnAkSn))))))))))) || (((! ((akSn)) && (ak) && (rdy) && (((ak) && ((! ((akRc))) || (! ((akSn))))) || ((pnAk) && ((! ((pnAkRc))) || (! ((pnAkSn)))))) && (((akPn) && ((! ((akPnRc))) || (! ((akPnSn))))) || ((((ak) && ((! ((akRc))) || (! ((akSn))))) || ((pnAk) && ((! ((pnAkRc))) || (! ((pnAkSn)))))))) && ((((! ((pnAk))) || ((((ak)) || ((akPn))))) && ((! ((akPn))) || ((((ak)) || ((pnAk))))) && ((! ((ak))) || ((((akPn)) || ((pnAk)))))) || ((((akPn) && ((! ((akPnRc))) || (! ((akPnSn))))) || ((((ak) && ((! ((akRc))) || (! ((akSn))))) || ((pnAk) && ((! ((pnAkRc))) || (! ((pnAkSn))))))))))) || (((! ((pnAkRc)) && (pnAk) && (rdy) && (((ak) && ((! ((akRc))) || (! ((akSn))))) || ((pnAk) && ((! ((pnAkRc))) || (! ((pnAkSn)))))) && (((akPn) && ((! ((akPnRc))) || (! ((akPnSn))))) || ((((ak) && ((! ((akRc))) || (! ((akSn))))) || ((pnAk) && ((! ((pnAkRc))) || (! ((pnAkSn)))))))) && ((((! ((pnAk))) || ((((ak)) || ((akPn))))) && ((! ((akPn))) || ((((ak)) || ((pnAk))))) && ((! ((ak))) || ((((akPn)) || ((pnAk)))))) || ((((akPn) && ((! ((akPnRc))) || (! ((akPnSn))))) || ((((ak) && ((! ((akRc))) || (! ((akSn))))) || ((pnAk) && ((! ((pnAkRc))) || (! ((pnAkSn))))))))))) || (((! ((pnAkSn)) && (pnAk) && (rdy) && (((ak) && ((! ((akRc))) || (! ((akSn))))) || ((pnAk) && ((! ((pnAkRc))) || (! ((pnAkSn)))))) && (((akPn) && ((! ((akPnRc))) || (! ((akPnSn))))) || ((((ak) && ((! ((akRc))) || (! ((akSn))))) || ((pnAk) && ((! ((pnAkRc))) || (! ((pnAkSn)))))))) && ((((! ((pnAk))) || ((((ak)) || ((akPn))))) && ((! ((akPn))) || ((((ak)) || ((pnAk))))) && ((! ((ak))) || ((((akPn)) || ((pnAk)))))) || ((((akPn) && ((! ((akPnRc))) || (! ((akPnSn))))) || ((((ak) && ((! ((akRc))) || (! ((akSn))))) || ((pnAk) && ((! ((pnAkRc))) || (! ((pnAkSn))))))))))) || (((! ((ak)) && ! ((akPn)) && ! ((pnAk)) && (rdy) && ((((! ((pnAk))) || ((((ak)) || ((akPn))))) && ((! ((akPn))) || ((((ak)) || ((pnAk))))) && ((! ((ak))) || ((((akPn)) || ((pnAk)))))) || ((((akPn) && ((! ((akPnRc))) || (! ((akPnSn))))) || ((((ak) && ((! ((akRc))) || (! ((akSn))))) || ((pnAk) && ((! ((pnAkRc))) || (! ((pnAkSn))))))))))) || (((! ((akPnRc)) && (akPn) && (rdy) && (((akPn) && ((! ((akPnRc))) || (! ((akPnSn))))) || ((((ak) && ((! ((akRc))) || (! ((akSn))))) || ((pnAk) && ((! ((pnAkRc))) || (! ((pnAkSn)))))))) && ((((! ((pnAk))) || ((((ak)) || ((akPn))))) && ((! ((akPn))) || ((((ak)) || ((pnAk))))) && ((! ((ak))) || ((((akPn)) || ((pnAk)))))) || ((((akPn) && ((! ((akPnRc))) || (! ((akPnSn))))) || ((((ak) && ((! ((akRc))) || (! ((akSn))))) || ((pnAk) && ((! ((pnAkRc))) || (! ((pnAkSn))))))))))) || (((! ((akPnSn)) && (akPn) && (rdy) && (((akPn) && ((! ((akPnRc))) || (! ((akPnSn))))) || ((((ak) && ((! ((akRc))) || (! ((akSn))))) || ((pnAk) && ((! ((pnAkRc))) || (! ((pnAkSn)))))))) && ((((! ((pnAk))) || ((((ak)) || ((akPn))))) && ((! ((akPn))) || ((((ak)) || ((pnAk))))) && ((! ((ak))) || ((((akPn)) || ((pnAk)))))) || ((((akPn) && ((! ((akPnRc))) || (! ((akPnSn))))) || ((((ak) && ((! ((akRc))) || (! ((akSn))))) || ((pnAk) && ((! ((pnAkRc))) || (! ((pnAkSn))))))))))) || (((! ((ak)) && (ak) && (rdy) && ((((! ((pnAk))) || ((((ak)) || ((akPn))))) && ((! ((akPn))) || ((((ak)) || ((pnAk))))) && ((! ((ak))) || ((((akPn)) || ((pnAk)))))) || ((((akPn) && ((! ((akPnRc))) || (! ((akPnSn))))) || ((((ak) && ((! ((akRc))) || (! ((akSn))))) || ((pnAk) && ((! ((pnAkRc))) || (! ((pnAkSn))))))))))) || (((! ((akPn)) && (akPn) && (rdy) && ((((! ((pnAk))) || ((((ak)) || ((akPn))))) && ((! ((akPn))) || ((((ak)) || ((pnAk))))) && ((! ((ak))) || ((((akPn)) || ((pnAk)))))) || ((((akPn) && ((! ((akPnRc))) || (! ((akPnSn))))) || ((((ak) && ((! ((akRc))) || (! ((akSn))))) || ((pnAk) && ((! ((pnAkRc))) || (! ((pnAkSn))))))))))) || (((! ((pnAk)) && (pnAk) && (rdy) && ((((! ((pnAk))) || ((((ak)) || ((akPn))))) && ((! ((akPn))) || ((((ak)) || ((pnAk))))) && ((! ((ak))) || ((((akPn)) || ((pnAk)))))) || ((((akPn) && ((! ((akPnRc))) || (! ((akPnSn))))) || ((((ak) && ((! ((akRc))) || (! ((akSn))))) || ((pnAk) && ((! ((pnAkRc))) || (! ((pnAkSn))))))))))) || ((((ak) && (pnAk) && (rdy) && ((((! ((pnAk))) || ((((ak)) || ((akPn))))) && ((! ((akPn))) || ((((ak)) || ((pnAk))))) && ((! ((ak))) || ((((akPn)) || ((pnAk)))))) || ((((akPn) && ((! ((akPnRc))) || (! ((akPnSn))))) || ((((ak) && ((! ((akRc))) || (! ((akSn))))) || ((pnAk) && ((! ((pnAkRc))) || (! ((pnAkSn))))))))))) || ((((akPn) && (pnAk) && (rdy) && ((((! ((pnAk))) || ((((ak)) || ((akPn))))) && ((! ((akPn))) || ((((ak)) || ((pnAk))))) && ((! ((ak))) || ((((akPn)) || ((pnAk)))))) || ((((akPn) && ((! ((akPnRc))) || (! ((akPnSn))))) || ((((ak) && ((! ((akRc))) || (! ((akSn))))) || ((pnAk) && ((! ((pnAkRc))) || (! ((pnAkSn))))))))))) || ((ak) && (akPn) && (rdy) && ((((! ((pnAk))) || ((((ak)) || ((akPn))))) && ((! ((akPn))) || ((((ak)) || ((pnAk))))) && ((! ((ak))) || ((((akPn)) || ((pnAk)))))) || ((((akPn) && ((! ((akPnRc))) || (! ((akPnSn))))) || ((((ak) && ((! ((akRc))) || (! ((akSn))))) || ((pnAk) && ((! ((pnAkRc))) || (! ((pnAkSn))))))))))))))))))))))))))))))))))) -> goto accept_all
	:: (1) -> goto T0_init
	fi;
accept_all:
	skip
}

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












#endif
#ifdef RESULT

#endif