// ------------------------------------------------------------
// Peterson's EntryProtocol consists of several stages where
// a two process solution of Peterson's protocol is implemented
// to determine which processes get the advance to the next
// stage.
// ------------------------------------------------------------

package Communication.MutexProtocols.Peterson;

// number of processes
macro NumProc = 3;

module EntryProtocol(nat{NumProc()} ?i, [NumProc()] nat{NumProc()} prev, level) {
   for(j=0 .. (NumProc()-2)) {
      next(level[i]) = j;
      next(prev[j])  = i;
      pause;
      for(k=0 .. (NumProc()-1)) {
         if(i!=k)
	    // wait if process k is in higher numbered stage
	    // and process i was the last to enter this stage
	    await ((level[k] < level[i]) or (prev[j]!=i) );
      }
    }
}