/* Broken unfair mutex */
byte progress0, progress1;
#define COUNT 2
bit mutex;
/*---------------------------------------------*/
/* A process that uses these semaphores         */
/*---------------------------------------------*/
proctype myproc(byte id)
{ do :: atomic {mutex==0; mutex=1}; 
         if :: (id == 0) -> progress0 = 1 -> progress0 = 0
            :: (id == 1) -> progress1 = 1 -> progress1 = 0
         fi;
        mutex=0;
  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
       } }
/* 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; }