    SPECIFICATION producer_consumer (delay: number) : NOEXIT

    TYPE Integers

    BEHAVIOUR
      HIDE send, recv IN
          (   producer [send] (one)
            |[]|
              consumer [recv]
          )
        |[send, recv]|
          ( HIDE chan IN
                fast_buffer [send, chan]
              |[chan]|
                slow_buffer [chan, recv] (delay)
          )
      WHERE
        PROCESS producer [send] (n: number) : NOEXIT
        PROCESS consumer [recv] : NOEXIT
        PROCESS fast_buffer [get, put] : NOEXIT
        PROCESS slow_buffer [get, put] (delay: number) : NOEXIT
    ENDSPEC