never {
q1:
	if
	:: ((! (o1) && ! (u1) && ! (g1)) || ((o1) && ! (u1) && ! (g1))) -> goto q1
	:: ((! (o1) && ! (u1) && (g1)) || ((o1) && ! (u1) && (g1))) -> goto q2
	:: ((! (o1) && (u1) && ! (g1)) || (! (o1) && (u1) && (g1)) || ((o1) && (u1) && ! (g1)) || ((o1) && (u1) && (g1))) -> goto q3
	fi;
accept_q2:
q2:
	if
	:: ((! (o1) && ! (u1) && ! (g1)) || (! (o1) && ! (u1) && (g1)) || (! (o1) && (u1) && ! (g1)) || (! (o1) && (u1) && (g1)) || ((o1) && ! (u1) && ! (g1)) || ((o1) && ! (u1) && (g1)) || ((o1) && (u1) && ! (g1)) || ((o1) && (u1) && (g1))) -> goto q2
	fi;
q3:
	if
	:: (((o1) && ! (u1) && ! (g1))) -> goto q1
	:: (((o1) && ! (u1) && (g1))) -> goto q2
	:: ((! (o1) && ! (u1) && ! (g1)) || (! (o1) && ! (u1) && (g1)) || (! (o1) && (u1) && ! (g1)) || (! (o1) && (u1) && (g1)) || ((o1) && (u1) && ! (g1)) || ((o1) && (u1) && (g1))) -> goto q3
	fi;
}
/* type, BA, WDBA, minWDBA:  obligation+guarantee, 4, 3, 5, 3 */