c - 如何在 PROMELA 中广播消息？

Question

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

chanA2B ! message
chanA2C ! message
chanA2D ! message

这是在 PROMELA 中模拟广播的正确方法吗？或者是否有适当的运算符(operator)可以这样做？

Answer 1

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

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

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

那么 a proctype 可以在任意两个发送之间阻塞。您可以尝试:

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

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