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

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