Как проверить произвольное условие в очереди сообщений в Spin?

Я пытаюсь смоделировать поведение других средств проверки моделей с помощью Spin. Для этого мне нужно иметь возможность проверить какое-то произвольное условие в очереди сообщений. Например, я хочу проверить, есть ли где-то в канале какое-то сообщение с int больше 5. Мало того, мне нужно, чтобы такое условие было внутри атомарного блока.

Я попытался сделать что-то вроде этого:

int mid;

do
:: atomic {
  in??[msg(mid)] && mid > 5 -> (...)
}

Но Спин читает это условие как

in??[msg(mid)] && 0 > 5

Я пробовал что-то в этом роде:

do
:: atomic {
    in??<msg(mid)>;
    if
    :: mid > 5 ->
        in??msg(eval(mid));
        (...)
    :: else -> skip
    fi }

Это работает, но семантически отличается от того, что я хочу, потому что он попадает в атомарный блок только для того, чтобы не выполнить это условие и пропустить его.

Итак, есть ли способ проверить произвольное условие в очереди сообщений и выполнить атомарный блок только в том случае, если такое условие действительно?


promela spin model-checking
person 9thScientist    schedule 09.04.2019    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Как вы обнаружили, встроенный механизм фильтрации, предлагаемый Spin, способен фильтровать только по значению и, точнее, не может фильтровать по выражению.

Это может показаться не идеальным решением, но самый простой подход — оценить логическое выражение, связанное с условием фильтрации, перед отправкой сообщения.

Пример:

chan c = [42] of { int, bool };

proctype Test()
{
    int value;
    do
        :: atomic {
            c??[value, true] ->
                c??value, true; // true: filter messages larger than 5
                printf("Popped: %d\n", value);
            }
        :: else ->
            printf("No more messages larger than 5.\n");
            break;
    od;

    bool cond;
    printf("\nDischarging Channel..\n");
    do
        :: c?[value, cond] ->
           c?value, cond;
           printf("Popped: %d\n", value);
        :: else ->
            break;
    od;
}

init {
    int i;
    for (i : 1 .. 10) {
        c!i(i >= 5)  // evaluate filtering condition when message is sent
    }

    run Test();
}

Вывод:

~$ spin test.pml 
          Popped: 5
          Popped: 6
          Popped: 7
          Popped: 8
          Popped: 9
          Popped: 10
          No more messages larger than 5.

Discharging Channel..
          Popped: 1
          Popped: 2
          Popped: 3
          Popped: 4
2 processes created

Я признаю, что это не очень масштабируемый подход, но я не смог найти другого решения.

person Patrick Trentin    schedule 09.04.2019