// --------------------------------------------------------------------	//
// This file implements Fischer's protocol which is used to control 	//
// mutual exclusive access of NumProc processes to a shared ressource.	//
// In the Quartz module below, we use a shared variable crit_var that 	//
// is incremented and afterwards decremented during such an access of	//
// one process. Hence, the variable should be invariantly zero or one.	//
//   The protocol goes back to Lamport and Fischer, and works as 	//
// follows: Each thread has a unique process identifier i, which is a 	//
// positive number. The access to the critical section is controlled 	//
// via a lock variable that either holds an id of a process or is zero. //
// The former is the case if a process has obtained access to the 	//
// shared resource.							//
// --------------------------------------------------------------------	//

package Communication.MutexProtocols.Fischer;

macro NumProc = 5;

module FischerMutex
   (event ?leave_cs,		  	// instructs to leave the critical section
    nat{NumProc()} ?go,	  		// used to control interleaved execution
    nat{NumProc()} lock,	  	// lock variable holding process ids
    nat{4} crit_var,			// shared variable used in critic section
    [NumProc()] bool done)		// to check successful termination
{
   for(i=1 .. (NumProc()-1))
      suspend
         loop {
	    EntryProtocol(i,lock);
	    CriticalSection(leave_cs,crit_var);
	    ExitProtocol(done[i],lock);
         }
      when(go!=i);
} satisfies {
   // ============================================================
   MutualExclusive:
   // ------------------------------------------------------------
   // at most one process can enter critical section
   // ------------------------------------------------------------
	assert A G (crit_var<=1);
   // ============================================================
   EventualEntry:
   // ------------------------------------------------------------
   // fairness is very hard to achieve in Fischer's protocol;
   // as the specification below shows, it may even happen
   // that none of the processes will eventually enter the
   // critical section, which makes the protocol impractical
   // ------------------------------------------------------------
	assert E G
	   forall(i=0 .. (NumProc()-1))
              !done[i];
   // ============================================================
}