never {
q1:
	if
	:: ((! (p0) && ! (p0)) || (! (p0) && (p0)) || ((p0) && ! (p0))) -> goto q1
	:: (((p0) && (p0))) -> goto q3
	fi;
accept_q2:
q2:
	if
	:: ((! (p0) && ! (p0)) || (! (p0) && (p0)) || ((p0) && ! (p0)) || ((p0) && (p0))) -> goto q2
	fi;
q3:
	if
	:: ((! (p0) && ! (p0)) || (! (p0) && (p0))) -> goto q1
	:: (((p0) && ! (p0))) -> goto q2
	:: (((p0) && (p0))) -> goto q3
	fi;
}