never{ 
T2_init:
	if
	:: (1) -> goto T2_init
	:: (p1 && p0) -> goto T1
	fi;
T1:
	if
	:: (p1 && (! p0)) -> goto accept_all
	:: (p1) -> goto T1
	fi;
accept_all:
	skip
}