never{ 
T3_init:
	if
	:: (g1 && (! u1)) -> goto accept_all
	:: ((! u1)) -> goto T2
	:: (1) -> goto T1
	fi;
T2:
	if
	:: (g1 && (! u1)) -> goto accept_all
	:: ((! u1)) -> goto T2
	fi;
T1:
	if
	:: (g1 && (! u1) && o1) -> goto accept_all
	:: ((! u1) && o1) -> goto T2
	:: (1) -> goto T1
	fi;
accept_all:
	skip
}