// ------------------------------------------------------------
// 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.Bakery;

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, mticket) {
    ticket[i] = 1;
    // ------ compute the maximum of all customer's tickets ----------
    mticket[0] = ticket[0];
    for(j=1 .. (NumProc()-1)) {
       mticket[j] = ((mticket[j-1]<ticket[j])
			? ticket[j]
			: mticket[j-1]);
    }
    // ------ store the maximum plus one in the own ticket[i] --------
    next(ticket[i]) = mticket[(NumProc()-1)]+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));
    }
}