Multiple Repeat..Until in Promela Spin

Question

How can I write the following code in Promela:

I tried the following but I do not think that it is correct:

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;

The variables in the code are not important. I just want the logic to be similar to the example algorithm above.

Answer 1

You may want to take a look at the Q/A: "How to implement repeat-until in promela?".

Example:

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

Answer 2

• Unconditional loops can be written by a do with an unguarded statement, so the "repeat forever" can be written as follows (note that true -> isn't needed).

  do
  :: ...
  od;
  

• "Repeat until"s can be written this way

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

so the final code would be

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;