never{ 
T2_init:
	if
	:: (g1 && (! u1)) || (g2 && (! u2)) -> goto accept_all
	:: ((! u2)) -> goto T5
	:: (1) -> goto T4
	:: ((! u1)) -> goto T3
	:: (1) -> goto T1
	fi;
T3:
	if
	:: (g1 && (! u1)) -> goto accept_all
	:: ((! u1)) -> goto T3
	fi;
T1:
	if
	:: (g1 && (! u1) && o1) -> goto accept_all
	:: ((! u1) && o1) -> goto T3
	:: (1) -> goto T1
	fi;
T4:
	if
	:: (g2 && (! u2) && o2) -> goto accept_all
	:: ((! u2) && o2) -> goto T5
	:: (1) -> goto T4
	fi;
T5:
	if
	:: (g2 && (! u2)) -> goto accept_all
	:: ((! u2)) -> goto T5
	fi;
accept_all:
	skip
}