[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] How to specify broadcasting a message

On 11/3/21 1:18 PM, Jones Martins wrote:

In a system where a broadcast is possible, how do I specify an instantaneous broadcast, where a message has been appended to all processes' inboxes?

For example:
Send(p1, p2, msg) ==
   /\ inbox' = [ inbox EXCEPT ![p2] = Append(inbox[p2], msg) ]

Broadcast(p1) ==
   /\ \A p2 \in Processes: p # p2 /\ Send(p1, p2, "Hello")

Is this correct?

Broadcast(sndr, msg) ==
 inbox' =
[ p \in Processes |-> IF p = sndr THEN inbox[p] ELSE Append(inbox[p], msg) ]

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/55332619-a838-0436-d599-bd0bbeb92f9f%40lemmster.de.