---------------------------------------------------------
-- COMMUNICATION RULES --
---------------------------------------------------------

INTER(P,Q) = P ||| Q
COMM(P,Q,c1,c2) = (P ||| Q) [| {| c1,c2 |} |] BFIO(c1,c2)
FEED(P,c1,c2) = P[| {| c1,c2 |} |] BFIO(c1,c2)
REF(P,c1,c2) =  P[| {| c1,c2 |} |] BFIO(c1,c2)

-- BUFFERS
BUFFER(ci,co, n) =
  let
    B(<>) = ci?x -> B(<x>)
    B(s)  =    (co!head(s) -> B(tail(s)))
              [] (#s<n & ci?x -> B(s^<x>))
  within B(<>)
BFIO(c1,c2) = BUFFER(c1.req, c2.req,1) ||| BUFFER(c2.ack, c1.ack,1)