// ------------------------------------------------------------
// The entry protocol has to determine the ticket of the process
// by inspecting the tickets of all other customers (processes).
// The own ticket is the maximum of the other tickets plus one.
// The the process has to wait until its ticket is the smallest
// one.
//  In a fine grained implementation, however, it can happen that
// some customers will have the same ticket number at the end.
// In this case, the customer with the lower index will first
// enter the critical section due to the definition of the
// partial order SmallerTicket.
// ------------------------------------------------------------

package Communication.MutexProtocols.Bakery2;

macro ticket_length = 16;
macro MAX(x,y) = ((x<y)?y:x);
macro SmallerTicket(ti,i,tj,j) = ((tj==0) or ((ti==tj)?(i<j):(ti<tj)));
macro NumProc = 3;

module EntryProtocol(nat{NumProc()} ?i,[NumProc()] int{ticket_length()} ticket) {
    int{ticket_length()} max_ticket;
    ticket[i] = 1;
    // ------ compute the maximum of all customer's tickets ----------
    max_ticket = ticket[0];
    for(j=1 .. (NumProc()-1)) {
       next(max_ticket) = MAX(max_ticket,ticket[j]);
       pause;
    }
    // ------ store the maximum plus one in the own ticket[i] --------
    next(ticket[i]) = max_ticket+1;
    // ------ wait until no customer has a smaller ticket ----
    for(j=0 .. (NumProc()-1)) {
       if (i!=j)
	  await(SmallerTicket(ticket[i],i,ticket[j],j));
    }
}