// ------------------------------------------------------------ // Here is a piece of code to be used for the critical section. // In particular, we count the number of states in the cs, // which should be at most 1. // ------------------------------------------------------------ package Communication.MutexProtocols.TicketMu; // number of processes macro NumProc = 4; module CriticalSection(event ?leave_cs, nat{4} crit_var) { next(crit_var) = crit_var+1; await(leave_cs); next(crit_var) = crit_var-1; }