Промела - недетерминизм не недетерминирован?

Рассмотрим этот фрагмент:

chan sel = [0] of {int};

active proctype Selector(){
    int not_me;

    endselector:
    do
    ::  sel ? not_me;
        if
        :: 0 != not_me -> sel ! 0;
        :: 1 != not_me -> sel ! 1;
        :: 2 != not_me -> sel ! 2;
        :: 3 != not_me -> sel ! 3;
        :: else -> -1;
        fi

    od
}

proctype H(){
    int i = -1;
    int count = 1000;
    do
    :: sel ! i; sel ? i; printf("currently selected: %d\n",i); count = count -1;
    :: count < 0 -> break;
    od

    assert(false);
}

init{
    atomic{
        run H();
    }
}

Вы ожидаете, что это будет печатать довольно произвольно значения 0..3, пока счетчик не упадет ниже 0, после чего он может либо напечатать другое число, либо завершиться.

Однако, похоже, это не так.

Единственные возвращаемые значения: 0, затем 1, затем 0, затем 1, затем 0, затем 1,...

Я как-то неправильно понял «недетерминизм» утверждений if/fi?

(используя ispin на Ubuntu, если это имеет значение).


verification non-deterministic promela spin
person User1291    schedule 04.02.2016    source источник

Ответы (2)


arrow_upward
1
arrow_downward

Соответствующая часть спецификации языка. Мне кажется недетерминированным.

Если вы смотрите только на (несколько) следов системы, то вы находитесь во власти (псевдо) генератора случайных чисел.

Я думал, что основная цель SPIN — доказать свойства. Итак, вы можете написать формулу F, описывающую нужные вам трассы, а затем заставить SPIN проверить, что «система и F» имеют модель.

person d8d0d65b3f7cf42    schedule 05.02.2016
comment
Вы также можете попробовать запустить его в интерактивном режиме и посмотреть, включены ли все недетерминированные параметры. - person Brishna Batool; 13.09.2018

arrow_upward
0
arrow_downward

Если вы запускаете Spin в режиме «симуляции», то я полагаю, что параметры else посещаются детерминировано. Таким образом, в процедуре Selector симуляция продолжается в if путем проверки следующих опций: 0 ~= not_me, а затем опции 1, 2, 3. Таким образом, для вашего исполнения вы пинг-понг между 0 и 1.

Вы можете подтвердить это, заменив свой оператор if на:

if
:: 0 != not_me -> sel ! 0;
:: 1 != not_me -> sel ! 1;
:: else -> assert(false)
fi

и ваша симуляция никогда не достигнет утверждения.

Spin также можно запустить в режиме «проверки» — сгенерируйте исполняемый файл pan и выполните его. Затем будут посещены все случаи (по модулю ограничений по памяти и времени). Однако в режиме «проверки» ничего не распечатывается, поэтому вам может быть трудно увидеть другие случаи!

person GoZoner    schedule 10.02.2016