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

never {
q1:
	if
	:: ((! (p) && ! (t)) || (! (p) && (t)) || ((p) && (t))) -> goto q1
	:: (((p) && ! (t))) -> goto q2
	fi;
accept_q2:
q2:
	if
	:: ((! (p) && ! (t)) || (! (p) && (t)) || ((p) && ! (t)) || ((p) && (t))) -> goto q2
	fi;
}
/* type, nba, -nba, wdba, min:  guarantee, 6, 8, 7, 2 */