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

module CriticalSection(event ?leave_cs, nat{4} crit_var) {
   next(crit_var) = crit_var+1;
   await(leave_cs);
   next(crit_var) = crit_var-1;
}