% Learning Bridge

vocabulary Messages
types Message tuple [source, dest: Nat, data: Seq[Nat]] 
end

imports Messages
automaton LearningBridge

signature
  output send(m: Message, p: Nat)
  input receive(m: Message, p: Nat)
  internal copy(p: Nat)

states
  inbuf: Array[Nat, Seq[Message]],
  outbuf: Array[Nat, Seq[Message]],
  macAddressTable: Array[Nat,Nat] := constant(0),
  ports: Set[Nat] := {1, 2, 3, 4, 5, 6}

transitions
  output send(m, p)
    pre outbuf[p] ~= {} /\ m = head(outbuf[p])
    eff outbuf := assign(outbuf, p, tail(outbuf[p]))
  
  input receive(m, p)
    eff macAddressTable := assign(macAddressTable, m.source, p);
        inbuf := assign(inbuf, p, inbuf[p] |- m)

  internal copy(p) 
    pre inbuf[p] ~= {}
    eff
      if macAddressTable[head(inbuf[p]).dest] > 0 then
            outbuf := assign(outbuf, macAddressTable[head(inbuf[p]).dest],
                   outbuf[macAddressTable[head(inbuf[p]).dest]] |- head(inbuf[p]))

      else
        for x:Nat in ports do
          if x ~= macAddressTable[head(inbuf[p]).source] then
            outbuf := assign(outbuf, x, outbuf[x] |- head(inbuf[p]))
          fi
        od
      fi;
      inbuf := assign(inbuf, p, tail(inbuf[p]))