On 11/3/21 1:18 PM, Jones Martins wrote:
Hello,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.