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