[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] How to Specify a Broadcast Channel

 Can you please be more specific about what you find complicated? Doesn'tbroadcast(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)?StephanOn 11 Jun 2020, at 06:37, Earnshaw 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 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. -- 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/04097AE5-8CDB-4884-B6CC-930AC837E825%40gmail.com.