/* Courtesy of Salman Pervez, 2005.. */
/* ..based on the Fair Mutex idea of Ratan Nalumasu, 1995 */
/*----------------------------*/
/* Macros for P and V          */
/*----------------------------*/
#define P(CH)       CH!reply; reply?0
#define V(CH)       reply?0
/*----------------------------*/
/* This makes semaphores fair */
/*----------------------------*/
byte progress0, progress1;

#define COUNT 2

proctype fifo(chan X)
{    chan R;
     /* Reply to the senders in a fifo order */
     do
         :: X ? R ->
                     R ! 0; /* Matches first ? query of P() */
                     R!0     /* Matches only ? query of V() */
     od
}
/*---------------------------------------------*/
/* Need this much capacity to work properly... */
/*---------------------------------------------*/
chan mutex = [COUNT] of { chan };
/*---------------------------------------------*/
/* A process that uses these semaphores         */
/*---------------------------------------------*/
proctype myproc(byte id)
{
  chan reply = [0] of {bit};
  do :: P(mutex);
         if
          :: (id == 0) -> progress0 = 1 -> progress0 = 0
          :: (id == 1) -> progress1 = 1 -> progress1 = 0
         fi;
        V(mutex)
  od
}

/*---------------------------------------------*/
/* COUNT number of myproc are spawned          */
/*---------------------------------------------*/
init {
    byte cnt = 0;
         atomic {
         do
         :: (cnt == COUNT) -> break
         :: (cnt < COUNT) -> run myproc(cnt);
                              cnt = cnt + 1
         od;
         run fifo(mutex)
       }
}

/*
never {

    do
    :: skip
    :: (!progress0 && !progress1) -> goto accept
    od;

    accept: (!progress0 && !progress1) -> goto accept
}
*/

never {

   do
    :: skip
    :: (!progress0) -> goto accept0;
    :: (!progress1) -> goto accept1;
   od;
   accept0: (!progress0) -> goto accept0;
   accept1: (!progress1) -> goto accept1;
}