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

never { /* ! ( [] ( ! t -> ( ( ! p U t )  || [] ! p ) ) )
 */
T1_init:
	if
	:: (1) -> goto T1_init
	:: (!t && p) -> goto accept_all
	:: (!t) -> goto T0_S2
	fi;
T0_S2:
	if
	:: (!t) -> goto T0_S2
	:: (!t && p) -> goto accept_all
	fi;
accept_all:
	skip
}