// ================================================================
// see comments for DMA-Arbiter.qrz. The only difference is here
// that the the decision to use static priorities is not stored
// in a local variable, but abbreviated in a let-expression.
// This gives different runtimes for model checking...
// ================================================================

package Communication.MutexProtocols.DMA_Arbiter2;

macro NumProc = 5;

module DMA_Arbiter([NumProc()] bool ?req, ack)
{
  [NumProc()] bool token, persreq;
  token[0] = true;
  loop {
    // ----------------------------------------------------
    // use static priorities if that component that currently
    // has the token has no outstanding persistent request
    // ----------------------------------------------------
    let (static = !exists(i=1 .. (NumProc()-1)) (persreq[i] & token[i])) {
       next(persreq[0]) = req[0] & (persreq[0] | token[0]);
	  next(token[0]) = token[NumProc()-1];
	  ack[0] = req[0] & persreq[0] & token[0] 
                 | req[0] & static;
		   
       for(i=1 .. (NumProc()-1)) {
	  next(persreq[i]) = req[i] & (persreq[i] | token[i]);
	  next(token[i]) = token[i-1];
	  ack[i] = req[i] & persreq[i] & token[i] 
                 | req[i] & static &
  	  	   (forall(j=0 .. (i-1)) !req[j]);
       }
    }
    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]);
   // ============================================================
}