多次重复..直到在 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 和无保护语句来编写，所以 "repeat forever" 可以写成如下（注意 true -> 不是需要）。
```
do
:: ...
od;
```

"Repeat until"s可以这样写

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;

Answer 2

您可能想看看 Q/A："How to implement repeat-until in promela?"。

示例：

proctype example_do_od(int c, x1, x2)
{
    int c0 = 0;
    int d1 = 0;
    int d2 = 0;

do_od_loop:
    // REPEAT:
    do
        :: true ->
            // REPEAT:
            do
                :: true ->
                    c0 = c;
                    // UNTIL:
                    if
                        :: c0 % 2 == 0 -> break;
                        :: else;
                    fi;
            od;
            d1 = x1;
            d2 = x2;
            // UNTIL:
            if
                :: c0 == c -> break;
                :: else;
            fi;
    od;
    printf("Use(%d, %d)\n", d1, d2);
    goto do_od_loop;
}

proctype example_goto(int c, x1, x2)
{
    int c0 = 0;
    int d1 = 0;
    int d2 = 0;

goto_loop:
repeat_01:
repeat_02:
    c0 = c;
    if
        :: c0 % 2 == 0;
        :: else -> goto repeat_02;
    fi;
    d1 = x1;
    d2 = x2;
    if
        :: c0 == c;
        :: else -> goto repeat_01;
    fi;
    printf("Use(%d, %d)\n", d1, d2);
    goto goto_loop;
}

active proctype main()
{
    int c = 2;
    int x1 = 5;
    int x2 = 6;

    run example_do_od(c, x1, x2);
    run example_goto(c, x1, x2);
}

多次重复..直到在 Promela Spin

Multiple Repeat..Until in Promela Spin

spin

promela