promela - 如何在 promela 中实现重复直到（条件）循环？

Question

这将是正确的做法：

repeat{
...
} until(<condition>)

在普罗米拉？

我努力了 ：

do::
 //..
(condition) -> break;
od

和

do ::
  //..
  if::(condition) -> break;
  else
  fi;
od

Answer 1

您的第一次尝试是不正确的，因为如果<condition>不是true，该过程将永远阻塞。

您的第二次尝试在功能上是正确的。就个人而言，我更喜欢您的解决方案的一个小变体，它不会放弃执行批量代码true的入口条件。

---

给定

repeat{
    // bulk code
} until(<condition>)

您有以下选择：

• 做：

  do
      :: true ->
          // bulk code
          if
              :: <condition> ->
                  break;
              :: else;
          fi;
  od;
  

  或者

  do
      :: true ->
          // bulk code
          if
              :: ! <condition>;
              :: else ->
                  break;
          fi;
  od;
  

• 转到：

  L1:
      // bulk code
      if
          :: <condition>;
          :: else
              -> goto L1;
      fi;
  

  或者

  L1:
      // bulk code
      if
          :: ! <condition>
              -> goto L1;
          :: else;
      fi;
  

• 除非 （不要使用！）：

  do
      :: true ->
          d_step {
              // bulk code
          }
  od unless { <condition> };
  

  请注意，这种方法有两个问题：

  • 它假定 的值在代码内部而不是其他任何地方<condition>被更改（例如，通过其他一些进程）// bulk code

  • 根据 的内容// bulk code，可能根本无法使用d_step。

  只有在改变评估的指令恰好是内部的最后一条的情况下，<condition>才允许删除一条而不// bulk code影响d_step语义。

  要了解为什么会出现这种情况，请观察Spin以下代码示例中的行为：

  active proctype example()
  {
      int cc = 0;
      do
          :: true ->
              printf("before %d\n", cc);
              cc++;
              printf("after  %d\n", cc);
      od unless { cc == 3 };
  }
  

  它具有以下输出：

  ~$ spin test.pml 
        before 0
        after  1
        before 1
        after  2
        before 2
  1 process created
  

  由于cc++改变了对代码序列的评估cc == 3但不是最后一条指令，因此该语句after 3永远不会打印在屏幕上。

---

编辑：

当然，也可以尝试使用该unless语句的另一种代码变体，例如

bool flag;
do
    :: true ->
        // bulk code
        flag = true;
        flag = false;
od unless { flag && <condition> };

这显然总是正确的，即使在一般情况下也是如此，但它会用不属于原始问题的附加变量阻塞源代码，所以我仍然不鼓励使用unlessto replacedo/until。

以下是如何使用它的示例：

active proctype example()
{
    int cc = 0;
    bool flag = false;
    do
        :: true ->
            printf("before %d\n", cc);
            cc++;
            printf("after  %d\n", cc);
            flag = true;
            flag = false;
    od unless { flag && (cc == 3) };
}

实际上它产生了正确的输出：

~$ spin test.pml 
      before 0
      after  1
      before 1
      after  2
      before 2
      after  3
1 process created