Как проверить наличие произвольного условия в очереди сообщений в Spin? - PullRequest
Новая
       51

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

1 голос
/ 09 апреля 2019

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

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

int mid;

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

Но Spin читает это условие как 

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

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

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

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

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

1 Ответ

1 голос
/ 09 апреля 2019

Как вы обнаружили, собственный механизм фильтрации, предлагаемый 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

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

...