Re: [tlaplus] How to specify broadcasting a message

[Jones Martins <jonesmvc@xxxxxxxxx>]

Hello, Markus!

I deleted my message because I had found the solution on the TLA Examples Github page a minute after sending my question.

Thank you anyway. :)

Jones

On Wednesday, 3 November 2021 at 17:35:14 UTC-3 Markus Alexander Kuppe wrote:

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/d4fa4b1b-c244-45e4-a208-150df9256dc8n%40googlegroups.com.