Re: [tlaplus] How to Specify a Broadcast Channel

Thanks a lot, dear Stephan, this really works, but what I previously mean is how to think a way to reduce the computing rerourses by defining just one sharing message queue instead of the N*N matrix.

For example, each message strucure has a bitmap identifying each consumer, when the last consumer recieve and clear the bitmap, the message can be removed from the tail of the queue.

在 2020年6月11日星期四 UTC+8下午2:37:11，Stephan Merz写道：

Can you please be more specific about what you find complicated? Doesn't

broadcast(sndr, msg) ==
[n \in Node |-> IF n = sndr
THEN [m \in Node |-> Append(chan[n], msg)]
ELSE chan[n]]

do what you want (where "chan" is the variable that represents the N*N matrix of channels)?

Stephan

On 11 Jun 2020, at 06:37, Earnshaw <donglu...@xxxxxxxxx> wrote:

Dear All:

I am now specifying a distributed system consists of a group of nodes as a cluster.

Some control signals are syncronized to all the members in the cluster by broadcast message. So I must specify the message queue between each consumer and producer.

Now I split the message bus mechanism to a N * N unicast Queue as below:

NodeCtrlChannel = [n \in Node |-> [m \in Node |-> <<>>]]

But it is a little complicated, is there any simplified method to specify it?

--
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 tla...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/38ae9985-8b69-4060-99e5-7dfe6f5d130eo%40googlegroups.com.