never{
T0_init:
	if
	:: true -> goto T1
	:: (p0) && (p1) -> goto T2
	fi;
T1:
	if
	:: true -> goto T1
	:: (p0) && (p1) -> goto T2
	fi;
T2:
	if
	:: (p0) && (p1) -> goto T2
	:: (!(p0)) && (p1) -> goto accept_T3
	fi;
accept_T3:
	skip;
}