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.