DATA = {0,1}
N = 2

channel left, right : DATA
channel produce,consume  : DATA

BUFF_4(s) = (#s==0) & (left?x -> BUFF_4(<x>))
	    []
	    (#s==4) & (right.head(s) -> BUFF_4(tail(s)))
	    []
	    (#s<4 and #s>0) & 
		((left?x -> BUFF_4(s^<x>) |~| STOP)
		 []
		 right.head(s) -> BUFF_4(tail(s)))

PROD_INIT = produce.0 -> PROD(0)
PROD(x) = left.x -> PROD((x+1)%N)

CONS = right?x -> consume.x -> CONS

SYS = ((PROD_INIT ||| CONS)
       [| {| left,right |} |]
       BUFF_4(<>)) \ {| left,right |}