never { /* ! ( (((! g1) U (u1 || [] ! g1)) && []( o1 -> ((! g1) U (u1 || [] ! g1)))) )
 */
T0_init:
	if
	:: (!u1) -> goto T0_S3
	:: (!u1 && g1) -> goto accept_all
	:: (1) -> goto T1_S2
	fi;
T1_S2:
	if
	:: (1) -> goto T1_S2
	:: (!u1 && o1) -> goto T0_S3
	:: (!u1 && g1 && o1) -> goto accept_all
	fi;
T0_S3:
	if
	:: (!u1) -> goto T0_S3
	:: (!u1 && g1) -> goto accept_all
	fi;
accept_all:
	skip
}