/* Verification of the Semaphore Implementation of */
/* Hoare's Bounded Buffer Monitor                  */
#define n 2
byte count = 0, urgentcount, nonfullcount, nonemptycount;
byte mutex = 1, urgent, nonfull, nonempty;
inline wait(sem) {
      atomic{ sem >= 1; sem--;}
 }
inline signal(sem){
          atomic{sem++;}
 }
proctype producer(byte i)
{
  wait(mutex);
  if
  :: (count==n) ->
        nonfullcount++;
         if
         :: (urgentcount>0) -> signal(urgent);
         :: else -> signal(mutex);
            wait(nonfull);  nonfullcount--;        
         fi;
  :: else-> skip;
  fi;
    count++;
/* code for append*/
  urgentcount++;
  if
  :: (nonemptycount > 0) ->
              signal(nonempty);  wait(urgent);
  :: else -> skip;
  fi;
  urgentcount--;
  if
  :: (urgentcount>0) -> signal(urgent);
  :: else -> signal(mutex);
  fi;
}
proctype consumer(byte i)
{
  wait(mutex);
  
  if
  :: (count==0) ->  nonemptycount++;
          if
          :: (urgentcount>0) -> signal(urgent);
          :: else signal(mutex);
          fi;
          wait(nonempty);
          nonemptycount--;
  :: else -> skip;
  fi;

/* code for consume */
  count--;
  urgentcount++;
  if 
  :: (nonfullcount > 0) ->
            signal(nonfull); wait(urgent);
  :: else -> skip;
  fi;
  urgentcount--;
  if
  :: (urgentcount>0) -> signal(urgent);
  :: else -> signal(mutex);
  fi;
}

active proctype invariant()
{  assert(0<=count<=n);
}
init
{ run producer(1); run producer(2); run producer(3);
  run consumer(1); run consumer(2); run consumer(3);
}