// ------------------------------------------------------------
// Fischer's EntryProtocol consists of waiting until the lock
// variable holds no process id. Then, the process id of the
// own process is assigned. If after the assignment lock has
// still this value, the process can enter the critical section,
// otherwise another process wrote its process id in the lock
// after this process has done this and before this process has
// left the EntryProtocol.
// ------------------------------------------------------------

package Communication.MutexProtocols.Fischer;

macro NumProc = 5;

module EntryProtocol(nat{NumProc()} ?process_id, lock) {
   do {
      await(lock==0);
      next(lock) = process_id;
      pause;
   } while(lock != process_id);
}