never {    /* ! ( (((! g1) U (u1 || [] ! g1)) && []( o1 -> ((! g1) U (u1 || [] ! g1)))) && (((! g2) U (u2 || [] ! g2)) && []( o2 -> ((! g2) U (u2 || [] ! g2)))) ) */
T0_init:
	if
	:: (! ((u2)) && (g2)) -> goto accept_S76
	:: (((! ((u1)) && (g1)) || (! ((u2)) && (g2)))) -> goto accept_all
	:: (! ((u2)) && (g2)) -> goto accept_S89
	:: (! ((u2))) -> goto T0_S76
	:: (! ((u1)) && (g1)) -> goto accept_S104
	:: (! ((u1)) && (g1)) -> goto accept_S117
	:: (! ((u1))) -> goto T0_S104
	:: (1) -> goto T0_S93
	:: (1) -> goto T0_S102
	fi;
accept_S76:
	if
	:: (! ((u2))) -> goto T0_S76
	:: (! ((u2)) && (g2)) -> goto accept_all
	:: (! ((u2)) && (g2)) -> goto T0_S89
	fi;
accept_S89:
	if
	:: ((g2)) -> goto accept_all
	:: (1) -> goto T0_S89
	fi;
accept_S104:
	if
	:: (! ((u1))) -> goto T0_S104
	:: (! ((u1)) && (g1)) -> goto accept_all
	:: (! ((u1)) && (g1)) -> goto T0_S117
	fi;
accept_S117:
	if
	:: ((g1)) -> goto accept_all
	:: (1) -> goto T0_S117
	fi;
T0_S76:
	if
	:: (! ((u2)) && (g2)) -> goto accept_S76
	:: (! ((u2))) -> goto T0_S76
	:: (! ((u2)) && (g2)) -> goto accept_all
	:: (! ((u2)) && (g2)) -> goto accept_S89
	fi;
T0_S89:
	if
	:: ((g2)) -> goto accept_all
	:: (1) -> goto T0_S89
	fi;
T0_S93:
	if
	:: (! ((u2)) && (g2) && (o2)) -> goto accept_S76
	:: (! ((u2)) && (o2)) -> goto T0_S76
	:: (! ((u2)) && (g2) && (o2)) -> goto accept_all
	:: (! ((u2)) && (g2) && (o2)) -> goto accept_S89
	:: (1) -> goto T0_S93
	fi;
T0_S104:
	if
	:: (! ((u1)) && (g1)) -> goto accept_S104
	:: (! ((u1))) -> goto T0_S104
	:: (! ((u1)) && (g1)) -> goto accept_all
	:: (! ((u1)) && (g1)) -> goto accept_S117
	fi;
T0_S117:
	if
	:: ((g1)) -> goto accept_all
	:: (1) -> goto T0_S117
	fi;
T0_S102:
	if
	:: (! ((u1)) && (g1) && (o1)) -> goto accept_S104
	:: (! ((u1)) && (o1)) -> goto T0_S104
	:: (! ((u1)) && (g1) && (o1)) -> goto accept_all
	:: (! ((u1)) && (g1) && (o1)) -> goto accept_S117
	:: (1) -> goto T0_S102
	fi;
accept_all:
	skip
}