//-*-c-*-

coordinator BStack {
  selfex { put,take }
//  mutex { put,take }
  boolean full = (@false@), empty = (@true@);
  int count = (@0@);

  put requires (@!full@) {
    on entry (@
      empty=false;
      count++;
      if(count==SIZE) full=true;
    @)
  }

  take requires (@!empty@) {
    on entry (@
      full=false;
      count--;
      if(count==0) empty=true;
    @)
  }
}