verification - 多个 proctype 实例的 Promela 原子命题

Question

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

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

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

Answer 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) && ...)