[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
Send(p1, p2, msg) ==
/\ inbox' = [ inbox EXCEPT ![p2] = Append(inbox[p2], msg) ]
/\ \A p2 \in Processes: p # p2 /\ Send(p1, p2, "Hello")
Is this correct?
Broadcast(sndr, msg) ==
[ p \in Processes |-> IF p = sndr THEN inbox[p] ELSE Append(inbox[p],
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.