// ================================================================
// This file implements an arbiter that handles requests of N
// components that want to access a shared resource for one point
// of time. The arbiter is fair and guarantees mutually exclusive
// access to the shared resource for one point of time.
//  The arbiter makes use of a round robin schema (daisy chain),
// i.e., a token is passed around in a ring of N FlipFlops (token[i]).
// At each point of time, only the component with the token can have
// access to the shared ressource.
// ================================================================

package Communication.MutexProtocols.RoundRobin;

macro NumProc = 6;

module RoundRobinArbiter([NumProc()] bool ?req, !ack)
{
  [NumProc()] bool token;
  token[0] = true;
  loop {
    next(token[0]) = token[(NumProc()-1)];
    ack[0] = req[0] & token[0] ;
    for(i=1 .. (NumProc()-1)) {
	next(token[i]) = token[i-1];
	ack[i] = req[i] & token[i] ;
    }
    pause;
  }
}satisfies {
   // ============================================================
   MutualExclusive:
   // ------------------------------------------------------------
   // at most one process is given an acknowledge
   // ------------------------------------------------------------
	assert A G forall(i=0 .. (NumProc()-2))
               forall(j=i+1 .. (NumProc()-1))
                   (ack[i] -> !ack[j]);
   // ============================================================
   AcknowledgeOnlyByRequest:
   // ------------------------------------------------------------
   // acknowledge is only given if component requests for access
   // ------------------------------------------------------------
	assert A G forall(i=0 .. (NumProc()-1))
		(ack[i] -> req[i]);
   // ============================================================
   Fairness:
   // ------------------------------------------------------------
   // at most one process is given an acknowledge
   // ------------------------------------------------------------
	 assert forall(i=0 .. (NumProc()-1))
	    !E F E G (req[i] & !ack[i]);
   // ============================================================
}