多个 proctype 实例的 Promela 原子命题

【问题标题】：Promela atomic propositions for multiple proctype instances多个 proctype 实例的 Promela 原子命题
【发布时间】：2015-03-26 11:31:17
【问题描述】：

我想知道如何编写代表 proctype 的所有实例的 never 声明。例如，如果我有以下命题：

#define c (camera_node[SomePid]:start_publishing == 0)

现在，如果我实例化 camera_node 的 5 个实例，我如何创建一个原子命题来检查 start_publishing 对于所有这 5 个实例是否都为零？

【问题讨论】：

标签： verification spin promela model-checking

【解决方案1】：

嗯，这不是最漂亮的，但我过去做过这种事情。（注意：这段代码可能不是正确的 Promela，但你明白了）

#define NUMBER_OF_CAMERA_NODES  5

pid_t  cameraPids [NUMBER_OF_CAMERA_NODES];
byte_t cameraPidIndex = 0

active [NUMBER_OF_CAMERA_NODES] proctype cameraTask () {
  atomic { cameraPids[cameraPidIndex++] = _pid }
  // ...
}

#define cameraCheck( index ) (0 == camera_node[cameraPids[(index)]]:start_publishing)

#define checkAllCameras  (cameraCheck(0) && cameraCheck(1) && ...)

【讨论】：

好吧，我的论文中包含它有点太晚了，但仍然很高兴知道！ :) 谢谢