// ------------------------------------------------------------
// The entry protocol is simple:the customer draws a ticket;
// thus the next ticket must be incremented, and then (s)he
// has to wait until the served_ticket is the drawn ticket.
// ------------------------------------------------------------

package Communication.MutexProtocols.Ticket;

// number of processes
macro NumProc = 4;

module EntryProtocol(int{NumProc()} ?served_ticket, ticket, next_ticket) {
   ticket = next_ticket;
   next(next_ticket) = next_ticket+1;
   await(ticket == served_ticket);
}