Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- ------------------------------ 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 *)
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement