[tlaplus] How to Specify a Broadcast Channel

[Earnshaw <dongluming77@xxxxxxxxx>]

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