#define t       (srequested[0] == TRUE)
#define p       ((GIOPAgent[mypid[4]]@SReplyReceived  || GIOPAgent[mypid[5]]@SReplyReceived) && (sreply_reqId == 0))

never{ 
T2_init:
	if
	:: (p && (! t)) -> goto accept_all
	:: (1) -> goto T2_init
	fi;
accept_all:
	skip
}