Никогда не претендовать не работает в Promela модели

Question

Рассмотрим эту простую Promela модель:

#define p (x!=4) 

int x = 0; 

init { 
    do 
    :: x < 10 -> 
     x++; 
    od 
} 

Я хотел проверить эту модель с этой простой претензии, которая была сгенерирована с помощью спин -f:

never { /* []p */ 
accept_init: 
T0_init: 
    do 
    :: ((p)) -> goto T0_init 
    od; 
} 

Однако проверка с помощью

spin -a model.pml 
cc -o pan pan.c 
./pan 

не дает результата. Попытка опции -a также не дает результатов. Любое случайное симуляция показывает, что, очевидно, p является ложным в какой-то момент, так почему же никогда не претендует на работу, несмотря на то, что я произвел ее со спином?

Я пропустил что-то фундаментальное?

Answer 1

Если вы хотите проверить []p, вам понадобится построить заявку never на номер ![]p.

От reference:

Чтобы перевести формулу LTL в никогда не утверждают, что мы должны рассмотреть первый выражает ли формула положительное или отрицательное свойство. Положительное свойство выражает хорошее поведение, которое нам бы хотелось, чтобы наша система имела. Отрицательное свойство выражает плохое поведение, которое мы утверждаем, что система не имеет. Никогда не претендует, как правило, только для формализации отрицательных свойств (поведения, которое никогда не должно происходить), что означает, что положительные свойства должны быть сведены на нет, прежде чем они будут переведены в заявку.

Answer 2

поставил требование в исходном коде (скажем, check.pml)

int x = 0; 

init { 
    do 
    :: x < 10 -> 
     x++; 
    od 
} 

ltl { [] (x != 4) } 

затем

spin -a check.pml 
cc  pan.c -o pan 
./pan -a 

это дает

pan:1: assertion violated !(!((x!=4))) (at depth 16) 
pan: wrote check.pml.trail 

вы можете посмотреть след с

./pan -r -v 

IMHO, используя дополнительный инструмент для создания автомата из заявки, является ужасно неудобным и часто путающим.