never t {    /* !((((<> (eating[0])) && (<> (eating[1]))) && (<> (eating[2]))) && (<> (eating[3]))) */
accept_init:
T0_init:
	do
	:: (! ((eating[3]))) -> goto accept_S6
	:: (! ((eating[2]))) -> goto accept_S11
	:: (! ((eating[1]))) -> goto accept_S14
	:: (! ((eating[0]))) -> goto accept_S17
	od;
accept_S6:
T0_S6:
	do
	:: (! ((eating[3]))) -> goto accept_S6
	od;
accept_S11:
T0_S11:
	do
	:: (! ((eating[2]))) -> goto accept_S11
	od;
accept_S14:
T0_S14:
	do
	:: (! ((eating[1]))) -> goto accept_S14
	od;
accept_S17:
T0_S17:
	do
	:: (! ((eating[0]))) -> goto accept_S17
	od;
}