Многократное повторение .. До тех пор, пока Promela Spin

Question

Как я могу написать следующий код в Promela:

Я пробовал следующее, но я не думаю, что это правильно:

int c0 = 0;
int d1 = 0;
int d2 = 0;
do
    :: true ->
        d1 = x1;
        d2 = x2;
        if
            :: (c0 == c) ->
            if
                :: (c0%2==0) ->
                     c0 = c;
                    :: else;
            fi;
            :: else;
        fi;
       printf(" To simulate use(d1,d2) “);
od;

Переменные в коде не важны.Я просто хочу, чтобы логика была похожа на приведенный выше пример алгоритма.

Answer 1

• Безусловные циклы могут быть записаны do с неохраняемым оператором, поэтому «повторение навсегда» можно записать следующим образом (обратите внимание, что true -> не требуется).

  do
  :: ...
  od;
  

• «Повторять до тех пор, пока» можно записать таким образом

  do
  :: condition -> break
  :: else -> ...
  od;
  

, поэтому окончательный код будет

int c0 = 0;
int d1 = 0;
int d2 = 0;
do
:: do
   :: c0 == c -> break
   :: else -> do
              :: c0 % 2 == 0 -> break
              :: else -> c0 = c
              od;
              d1 = x1;
              d2 = x2;
   od;
   printf(" To simulate use(d1,d2) “);
od;