never { /* ! ( (((! g1) U (u1 || [] ! g1)) && []( o1 -> ((! g1) U (u1 || [] ! g1)))) && (((! g2) U (u2 || [] ! g2)) && []( o2 -> ((! g2) U (u2 || [] ! g2)))) )
 */
T0_init:
	if
	:: (1) -> goto T3_S1
	:: (!u2) -> goto T2_S2
	:: (!u2 && g2) || (!u1 && g1) -> goto accept_all
	:: (!u1) -> goto T0_S5
	:: (1) -> goto T1_S4
	fi;
T3_S1:
	if
	:: (1) -> goto T3_S1
	:: (!u2 && o2) -> goto T2_S2
	:: (!u2 && g2 && o2) -> goto accept_all
	fi;
T2_S2:
	if
	:: (!u2) -> goto T2_S2
	:: (!u2 && g2) -> goto accept_all
	fi;
T1_S4:
	if
	:: (1) -> goto T1_S4
	:: (!u1 && o1) -> goto T0_S5
	:: (!u1 && g1 && o1) -> goto accept_all
	fi;
T0_S5:
	if
	:: (!u1) -> goto T0_S5
	:: (!u1 && g1) -> goto accept_all
	fi;
accept_all:
	skip
}