% Observer module implementing the temporal property
% "always ( i =/= j ==> not(Ack_i and Ack_j) )"
% expressing there is at most one acknowledge
module AtMostOneAck4:
input AckA, AckB, AckC, AckD;
output AT_MOST_ONE_ACK_VIOLATED;

loop
   present [(AckA and AckB) or (AckA and AckC) or (AckA and AckD) or
	    (AckB and AckC) or (AckB and AckD) or
	    (AckC and AckD)] then
      emit AT_MOST_ONE_ACK_VIOLATED
   end;
   await tick
end.

% Observer module implementing the temporal property
% "always ( Requ_i ==> exists j, Ack_j)"
% expressing there is at least one ack in case of request.
module AtLeastOneAck4:
input ReqA, ReqB, ReqC, ReqD, AckA, AckB, AckC, AckD;
output AT_LEAST_ONE_ACK_VIOLATED;

loop
   await immediate [ReqA or ReqB or ReqC or ReqD];
   present [AckA or AckB or AckC or AckD]
   else
      emit AT_LEAST_ONE_ACK_VIOLATED;
   end;
   await tick
end.

% Observer module implementing the temporal property
% "always eventually ( Ack_i or (not Requ_i))"
% expressing someone constantly requesting will eventually be ackwoledged.
module WeakFairness4:
input ReqA, ReqB, ReqC, AckD;
output WEAK_FAIR;

await immediate [ReqA and ReqB and ReqC and AckD];
emit WEAK_FAIR
.

% Observer module implementing the temporal property
% "always  (always Requ_i implies eventually Ack_i )"
% under the knowledge that a constant request must be statisfied in 4 cycles
% (4 being the number of Cell processes in the ring). It expresses
% someone constantly requesting will eventually be ackwoledged in 4 cycles.
module Fairness:
input RequestIn, AckOut;
output Fairness_FAIL;

loop
   trap SUCCESS in
      loop
	 trap RESET in
	    loop
	       present RequestIn then
		  present AckOut then
		     exit SUCCESS;
		  end present;
	       else 
		  exit RESET;
	       end present;
	    each tick
	 ||
	    [
	     % await 4 tick (4 = number of Cells in the ring)
	     await tick; await tick; await tick; await tick;
	     emit Fairness_FAIL
	     ]
	 handle RESET do await tick;
	 end trap; % RESET
      end loop;
   handle SUCCESS do await tick;
   end trap; % SUCCESS
end loop
end module


module ObsArbitrer4:
input RequestIn1, RequestIn2, RequestIn3, RequestIn4;
output AT_MOST_ONE_ACK_VIOLATED, AT_LEAST_ONE_ACK_VIOLATED,
       WEAK_FAIR, Fairness_FAIL1, Fairness_FAIL2, Fairness_FAIL3,
       Fairness_FAIL4;

signal AckOut1, AckOut2, AckOut3, AckOut4 in
   run Arbiter4

|| run WeakFairness4[signal RequestIn1/ReqA, RequestIn2/ReqB,
			    RequestIn3/ReqC, AckOut4/AckD]

|| run AtLeastOneAck4[signal RequestIn1/ReqA, RequestIn2/ReqB,
			     RequestIn3/ReqC, RequestIn4/ReqD,
			     AckOut1/AckA, AckOut2/AckB,
			     AckOut3/AckC,AckOut4/AckD]

|| run AtMostOneAck4[signal AckOut1/AckA, AckOut2/AckB,
			    AckOut3/AckC,AckOut4/AckD]

|| run Fairness[signal AckOut1/AckOut, RequestIn1/RequestIn,
		       Fairness_FAIL1/Fairness_FAIL]

|| run Fairness[signal AckOut2/AckOut, RequestIn2/RequestIn,
		       Fairness_FAIL2/Fairness_FAIL]

|| run Fairness[signal AckOut3/AckOut, RequestIn3/RequestIn,
		       Fairness_FAIL3/Fairness_FAIL]

|| run Fairness[signal AckOut4/AckOut, RequestIn4/RequestIn,
		       Fairness_FAIL4/Fairness_FAIL]
end.
