DATA = {0,1}
N = {1,2,3,4}

channel left, right : N.DATA
channel mux, dmux, mess : N.DATA
channel amux, admx, ack : N

X = {| mux, admx |}
Y = {| amux, dmux |}
Z = {| mess, ack |}

COPY(i) = left.i?x -> right.i.x-> COPY(i) 
SPEC = |||i:N @ COPY(i) 

 
LHS = ((|||i:N @ T(i)) [| X |] (SM|||RA)) \ X 
RHS = ((|||i:N @ R(i)) [| Y |] (RM|||SA)) \ Y 
SYS = (LHS [| Z |] RHS) \ Z

T(i) = left.i?x -> mux.i.x -> admx.i -> T(i) 
R(i) = dmux.i?x -> right.i.x -> amux.i ->R(i) 
SM = mux?i.x -> mess.i.x -> SM 
RM = mess?i.x -> dmux.i.x -> RM 
SA = amux?i -> ack.i ->SA 
RA = ack?i -> admx.i ->RA

assert SPEC [T= SYS
assert SYS [T= SPEC