how to use tlaplus express duplicated and reordered message

[陈云星]

I want use plusCal to specify my distributed database system.

but how to express duplicated message and reordered message ?

is there some standard practice ? 

thanks your reply :)

[Stephan Merz]

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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/23a2f254-0811-4d5d-aaf0-69ba53a2c451n%40googlegroups.com.