[tlaplus] How to specify broadcasting a message

[Jones Martins <jonesmvc@xxxxxxxxx>]

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?

Thanks,

Jones

 

-- 
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/cc593d7d-c974-408d-8a63-824d61b52f99n%40googlegroups.com.