| You will have to explicitly model your communication medium. In case of duplicate delivery and reordering, it is probably best to model your network as a set of messages. Sending a message consists in adding a message to the set, you can use a macro like macro Send(msg) { network := network \cup {msg} } where `network' is the variable representing the network. For receiving a message, you act on some message that is present without removing it (so that it can be received as a duplicate later) like so: with (msg \in network) { \* handle message msg } A possibly more convenient variant is to model the network as an array mapping each process to the set of messages that have been sent to it, in which case the above become macro Send(msg, dest) { network[dest] := @ \cup {msg} } with (msg \in network[self]) { \* handle the message } Hope this helps, Stephan
You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/A79834EA-3604-453F-972E-0F4E91DB6EC1%40gmail.com. |