// ------------------------------------------------------------ // 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); }