// --------------------------------------------------------------------	
// This file implements the Bakery protocol which is a refinement of
// the Ticket protocol. According to Andrew's book, this protocol has
// the advantage that it is fair and does not require any special
// hardware assistance.
//  The protocol works similar to the Ticket protocol, however, there
// is no shared ticket dispenser. Instead, customers that enter the
// shop (to retain the notation used in the Ticket protocol) inspect
// all the other customers in the store and set their local ticket
// number to one larger than any other it can see. As in the Ticket
// protocol, the customer with the smallest number is the one that
// gets serviced next.
//  One problem with the bakery protocol is that it has to compute the
// maximum value of an array in one step. Another problem is that
// the values of the ticket numbers can get arbitrarily large. Hence,
// the example does not work with bitvetors of finite bitwidth.
//
//  References:
//	G.R. Andrews' book, Concurrent Programming, chapter 3.4, 1991
// --------------------------------------------------------------------	

package Communication.MutexProtocols.Bakery2;

macro ticket_length = 16;
macro NumProc = 3;

module BakeryProtocol(
   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()] int{ticket_length()} ticket)		// tickets already drawn by customers
{
   for(i=0 .. (NumProc()-1)) do ||
      suspend
         loop {
	    pause;
	    EntryProtocol(i,ticket);
	    CriticalSection(leave_cs,crit_var);
	    ExitProtocol(i,ticket);
         }
      when(go!=i);
}satisfies {
   // ============================================================
   MutualExclusive:
   // ------------------------------------------------------------
   // at most one process can enter critical section
   // ------------------------------------------------------------
	assert A G (crit_var<=1);
   // ============================================================
   NotAllDeadlock:
   // ------------------------------------------------------------
   // at least one process enters the critical section
   // ------------------------------------------------------------
	assert A (
	   (G forall(i=0 .. (NumProc()-1))
                 F(go==i))
	   ->
	   G F (crit_var==1)
	  );
   // ============================================================
}