如何在promela中實現重複直到（條件）循環？

Question

這將是正確的方法做：

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

在PROMELA

？

我曾嘗試：

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

和

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

Answer 1

你的第一次嘗試是不正確的，因爲如果<condition>不是true過程只會永遠阻塞。

你的第二次嘗試在功能上是正確的。就個人而言，我希望您的解決方案有一個小的變體，它不會丟失執行批量代碼的true條目條件。

---

鑑於

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

你有以下幾種選擇：

• do：

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

  或

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

• goto：

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

  或

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

• unless（不要使用！）：

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

這顯然是永遠正確的，即使是在一般的情況下，但它堵塞源代碼不屬於原始問題的一部分額外的變量，所以我仍然會阻礙使用unless更換do/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