Re: [tlaplus] How to specify broadcasting a message
25 views
Skip to first unread message
Markus Kuppe
Nov 3, 2021, 4:35:14 PM11/3/21
to tla...@googlegroups.com
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) ]
> 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) ]
Jones Martins
Nov 3, 2021, 5:00:56 PM11/3/21
to tlaplus
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
Reply all
Reply to author
Forward
0 new messages