// --------------------------------------------------------------------	
// This file implements Peterson's Mutex protocol that is also known
// as the Tie-Breaker algorithm. In contrast to SpinLocks, Peterson's
// protocol is fair, provided that all processes eventually leave the
// critical section after they entered it, and provided that the
// scheduler enables every process infinitely often.
//				
//  References:
// 	G.R. Andrews' book, Concurrent Programming, Chapter 3.2, 1991
// --------------------------------------------------------------------	

package Communication.MutexProtocols.Peterson;

// number of processes
macro NumProc = 3;

module PetersonMutexProtocol
   (event ?leave_cs,		  	// instructs to leave the critical section
    nat{NumProc()} ?go,	  	// used to control interleaved execution
    nat{4} crit_var,			// shared variable used in critic section
    [NumProc()] bool done,		// to check successful termination
    [NumProc()] nat{NumProc()} prev,
    [NumProc()] nat{NumProc()} level)
{
   crit_var = 0;
   for(i=0 .. (NumProc()-1)) do ||
      suspend
         loop {
	    EntryProtocol(i,prev,level);
	    CriticalSection(leave_cs,crit_var);
	    ExitProtocol(done[i],level[i]);
         }
      when(go!=i);
}satisfies {
   // ============================================================
   Reactive:
   // ------------------------------------------------------------
   // all initial states have at least one infinite path
   // ------------------------------------------------------------
	assert nu z. <> z;
   // ============================================================
   MutualExclusive:
   // ------------------------------------------------------------
   // at most one process can enter critical section
   // ------------------------------------------------------------
	assert A G (crit_var<=1);
   // ============================================================
   EventualEntry:
   // ------------------------------------------------------------
   // fairness is very hard to achieve: it only holds if the
   // scheduler does not always choose the same process out of
   // the processes that are applying for the critical section
   // ------------------------------------------------------------
	assert A (
	   (G forall(i=0 .. (NumProc()-1))
                 F((level[i]>0) & (go==i)))
	   ->
	   G forall(i=0 .. (NumProc()-1))
		 F done[i]
	  );
   // ============================================================
}