// --------------------------------------------------------------------	
// This file implements a simple Mutex protocol that is implemented in
// many stores as well. Upon entering the store, a customer draws a
// number that is one larger than the number held by any other customer
// currently waiting in the shop. The customer then waits until all
// customers holding smaller numbers have been serviced.
//  A problem for the implementation of the protocol on an uniprocessor
// is that it requires an atomic Fetch-And-Increment operation in order
// to load the value of next_ticket and incrementing it at the same time.
//
//  References:
//	G.R. Andrews' book, Concurrent Programming, chapter 3.3, 1991
// --------------------------------------------------------------------	

package Communication.MutexProtocols.Ticket;

// number of processes
macro NumProc = 4;


module TicketProtocol
   (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
    int{NumProc()} next_ticket,		// ticket to be drawn by next customer
    int{NumProc()} served_ticket,	// ticket number of currently served customer
    [NumProc()] int{NumProc()} ticket,	// tickets already drawn by customers
    [NumProc()] bool !done)		// to check successful termination
{
   for(i=0 .. (NumProc()-1)) do ||
      suspend
         loop {
	    pause;
	    EntryProtocol(served_ticket,ticket[i],next_ticket);
	    CriticalSection(leave_cs,crit_var);
	    ExitProtocol(served_ticket,done[i]);
         }
      when(go!=i);
}