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);
}

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

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