如何在 PROMELA 中广播消息？

Question

所以我想要的是进程 A 广播一条消息，告诉进程 B 到 D。这怎么做？这样做的正确方法似乎是在 A 和进程 B 到 D 之间建立通道，然后将相同的消息发送到从 B 到 D 的每个进程，如下所示。

chanA2B ! message
chanA2C ! message
chanA2D ! message

这是在 PROMELA 中模拟广播的正确方法，还是有合适的操作员这样做？

Answer 1

Promela 中没有“广播”；所有通道都是点对点的。

您希望广播是原子的，但如果您只是将三个消息发送包装在一个原子中，如下所示：

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

那么a proctype 可以在任意两次发送之间阻塞。你可以试试：

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

我认为由于布尔谓词是单个表达式，当它为真时，所有队列都会有空间，因此后续发送将是真正的原子。