#define NPROC 3

/* variables locales a chaque site */
byte myNum[NPROC];
byte highestNum[NPROC];
bool requestCS[NPROC];
byte nba[NPROC];
chan deferred[NPROC] = [NPROC] of { byte };

/* types messages */
mtype = { request, reply };

/* les canaux */
chan ch [NPROC] = [NPROC] of { mtype, byte, byte };

/* compteur section critique */
int in_cs = 0;

active [NPROC] proctype Main() {
byte k;
byte myID = _pid;

do :: 1 ->
   printf("MSC: section non critique\n");

   atomic {
     requestCS[myID] = 1;
     myNum[myID] = highestNum[myID] + 1;
     nba[myID] = NPROC-1
   }
req:
   k = 0;
   do :: k < NPROC && k != myID -> ch[k] ! request, myID, myNum[myID]; k++
      :: k == myID -> k++
      :: k >= NPROC -> break
   od;

   (nba[myID] == 0);

 cs:  in_cs++; printf("MSC: section critique\n"); in_cs--;

   requestCS[myID] = false;

   do :: empty(deferred[myID]) -> break
      :: deferred[myID] ? k -> ch[k] ! reply, 0, 0
   od
od
}

active [NPROC] proctype Receive() {
byte reqNum, source;
byte myID = _pid - NPROC;

do :: ch[myID] ?? request, source, reqNum -> 
      highestNum[myID] = 
      	((reqNum > highestNum[myID]) -> reqNum : highestNum[myID]);

      atomic {
        if :: requestCS[myID] &&
                ( (myNum[myID] < reqNum) ||
                  ( (myNum[myID] == reqNum) && (myID < source) )
                )
              -> deferred[myID] ! source

	   :: else -> ch[source] ! reply, 0, 0
         fi
      }

  :: ch[myID] ?? reply, _, _ -> nba[myID]--

od
}