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

never{
t0_init:
	if
	:: (((!(p)) && (!(t))) || ((!(p)) && (t))) || ((p) && (t)) -> goto t4
	:: (!(p)) && (!(t)) -> goto t2
	:: (p) && (!(t)) -> goto accept_t3
	fi;
t1:
	if
	:: (((!(p)) && (!(t))) || ((!(p)) && (t))) || ((p) && (t)) -> goto t1
	:: (!(p)) && (!(t)) -> goto t2
	:: (p) && (!(t)) -> goto accept_t3
	fi;
t2:
	if
	:: (!(p)) && (!(t)) -> goto t2
	:: (p) && (!(t)) -> goto accept_t3
	fi;
accept_t3:
	skip;
t4:
	if
	:: (((!(p)) && (!(t))) || ((!(p)) && (t))) || ((p) && (t)) -> goto t5
	:: (!(p)) && (!(t)) -> goto t2
	:: (p) && (!(t)) -> goto accept_t3
	fi;
t5:
	if
	:: (((!(p)) && (!(t))) || ((!(p)) && (t))) || ((p) && (t)) -> goto t1
	:: (!(p)) && (!(t)) -> goto t2
	:: (p) && (!(t)) -> goto accept_t3
	fi;
}