How do you broadcast a message in PROMELA?

Question

So what I want is process A to broadcast a message to say processes B to D. How can this be done? The right way of doing so seems like to have channels between A and processes B to D and then to just send the same message to each of the process from B to D, as follows.

chanA2B ! message
chanA2C ! message
chanA2D ! message

Is this the right way to mimic broadcasting in PROMELA, or is there a proper operator for doing so?

Answer 1

There is no 'broadcast' in Promela; all channels are point-to-point.

You'd want the broadcast to be atomic but if you just wrapped three message sends in an atomic, as such:

 atomic { a2b ! msg; a2c ! msg; a2d ! msg }

then the a proctype could block between any two sends. You might try:

atomic { !nfull(a2b) && !nfull(a2b) && !nfull(a2c) -> a2b ! msg; …}

I think since the boolean predicate is a single expression when it is true all queues will have space and thus the subsequent send will be truly atomic.