tlrouter.tla

------------------------------ MODULE tlrouter ------------------------------
EXTENDS TLC, Sequences, Integers
(* --algorithm tlrouter
variables  
    input_stream = << [dest |-> "a", id |-> 1], [id |-> 1]>>,
    routing_table = <<>>, 

    output_streams = <<>>,
    dead_messages = {},
    msg;
begin

while input_stream /= <<>> do
    \* consume the next msg
    msg := Head(input_stream);
  
    input_stream := Tail(input_stream);
    
     \* try to learn an output channel
    if "dest" \in DOMAIN msg then
        routing_table[msg.id] := routing_table[msg.id] \union {msg.dest};
    else
        skip;
    end if;
    
    \* have we learned an output channel? otherwise its dead
    if msg.id \in DOMAIN routing_table then
        output_streams[msg.id] := output_streams[msg.id] \union {msg}
    else
        dead_messages := dead_messages \union {msg}
    end if; 
end while;
assert dead_messages = {};
end algorithm *)