automaton CommunicationChannel(M: type)
assumes PortSpec
signature
  input send (m: M, p: Ports),
        disconnect(p: Ports)
  output receive (m: M, p: Ports)
states
  buffer : Array[Ports, Seq[M]] := constant({}),
  connected : Array[Ports, Bool] := constant(true)
transitions
  input send (m, p)
    eff if connected[p] then buffer[p] := buffer[p] |- m fi

  input disconnect(p)
    eff connected[p] := false

  output receive (m, p)
    pre connected[p] /\ buffer[succ(p)] ~= {} /\ m = head(buffer[succ(p)])
    eff buffer[succ(p)] := tail(buffer[succ(p)])