% Learning bridge: smart forwarding

% For use with an reliable channel

vocabulary Messages
	types Message tuple [data:Seq[Nat], src:Nat, dst:Nat]
end

imports Messages
automaton LearningBridge(numPorts:Nat)

signature	       
	input  receive(m: Message, i:Nat)
	output send(m: Message, i:Nat)
	
	
states
	portQueue:Array[Nat,Seq[Message]] := constant({}),
	addressTable:Array[Nat,Int] := constant(0)
	
transitions
	input receive(m, port; local s:Set[Nat]) where port <= numPorts
	eff
		if addressTable[m.dst] ~= 0 then
			portQueue[m.dst] := portQueue[m.dst] |- m
		else
			s := {1, 2, 3, 4, 5};
			for i:Nat in s do %1..numPorts do
				if (i ~= port) then 
					portQueue[i] := portQueue[i] |- m
				fi
			od;
		fi;
		addressTable[m.src] := port
		
	
	output send(m, port) where port <= numPorts
	pre
		portQueue[port] ~= {} /\ m = head(portQueue[port])
	eff
		portQueue[port] := tail(portQueue[port])