// ================================================================ // 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]); // ============================================================ }