//-*-c-*-

coordinator BStack {
  selfex { put,take }
  mutex { put,take }

  put requires (@!(count1==SIZE)@) {
  }

  take requires (@!(count1==1)@) {
  }
}