promela - Promela 中如何检查数组中的所有值是否相等？

Question

如何在 Promela 中检查数组的所有值是否相等？

我希望这段代码是原子的并且是可执行的(如果它们是的话)(忙着等待直到所有的都相等)。

有什么办法可以使用for循环吗？ (数组的长度作为参数给出)

Answer 1

您可以尝试类似以下代码片段的操作(其中假定数组非空):

#define N 3
int arr[N];

proctype Test(int length) {
  int i, val;
  bool result = true;

  do
    :: atomic {
         /* check for equality */
         val = arr[0];
         for (i : 1 .. length-1) {
           if
            :: arr[i] != val ->
                 result = false;
                 break
            :: else -> skip
           fi
         }

         /* Leave loop if all values are equal,
            else one more iteration (active waiting).
            Before the next entrance into the atomic
            block, other proctypes will have the chance
            to interleave and change the array values */
         if
           :: result -> break;
           :: else -> result = true
         fi
       }
  od

  /* will end up here iff result == true */
}

init {  
  arr[0] = 2;
  arr[1] = 2;
  arr[2] = 2;

  run Test(N);
}

原子 block 内的代码不会阻塞，因此可以连续执行。

/edit (2019-01-24):在原子语句之后的条件 block 的 else 部分中将 result 设置为 true。否则，如果最初的值不相等，检查将永远不会成功。