resource bounded_buffer
   op deposit(item : real)
   op fetch() returns item : real
body bounded_buffer(size : int)
   write("bounded buffer resource with", size, "slots is alive")
   var buf[0:size-1] : real
   var count := 0
   var take_out := 0
   var put_in := 0

   process bb
      do true ->
         in deposit(item) st count < size ->
            buf[put_in] := item
            put_in := (put_in + 1) % size
            count++
         [] fetch() returns item st count > 0 ->
            item := buf[take_out]
            take_out := (take_out + 1) % size
            count--
         ni
      od
   end bb
end bounded_buffer