Promela SPIN unreached in proctype error

Question

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

Код ошибки:

unreached in proctype P 
     (0 of 29 states) 
unreached in proctype monitor 
     mutex_assert.pml:39, state 1, "assert(!((mutex>1)))" 
     mutex_assert.pml:42, state 2, "-end-" 
     (2 of 2 states) 
unreached in init 
     (0 of 3 states) 
unreached in claim ltl_0 
     _spin_nvr.tmp:10, state 13, "-end-" 
     (1 of 13 states) 

pan: elapsed time 0 seconds 

Код в основном реализация алгоритма Питерсона и я проверил на безопасность и это, кажется, действует. Но всякий раз, когда я пытаюсь проверить свойство liveness с помощью ltl {[] ((wait -> <> (cs)))}, он сталкивается с вышеуказанными ошибками. Я не уверен, что они означают, так что я не знаю, как поступить ...

Мой код выглядит следующим образом:

#define N 3 
#define wait (P[1]@WAIT) 
#define cs  (P[1]@CRITICAL) 

int pos[N]; 
int step[N]; 
int enter; 
byte mutex; 
ltl {[]((wait -> <> (cs)))} 

proctype P(int i) { 
    int t; 
    int k; 
    WAIT: 
    for (t : 1 .. (N-1)){ 
    pos[i] = t 
    step[t] = i 
    k = 0; 
    do 
    :: atomic {(k != i && k < N && (pos[k] < t|| step[t] != i)) -> k++} 
    :: atomic {k == i -> k++} 
    :: atomic {k == N -> break} 
    od; 
    } 

CRITICAL: 
    atomic {mutex++; 
    printf("MSC: P(%d) HAS ENTERED THE CRITICAL SECTION.\n", i); 
    mutex--;} 
    pos[i] = 0; 
} 

init { 
    atomic { run P(0); } 
} 

Answer 1

Общий ответ

Это предупреждение сообщают вам, что некоторые состояния недоступны из-за переходов, которые никогда не принимаются.

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

Примечание. Вы можете использовать метку end: перед определенной строкой кода, чтобы отметить допустимые состояния завершения, поэтому, чтобы избавиться от этих предупреждений, , например. когда ваша процедура не заканчивается. Больше информации here.

---

Конкретного Ответ

Я не могу воспроизвести ваш выход. В частности, запустив

~$ spin -a file.pml 
~$ gcc pan.c 
~$ ./a.out -a 

я получаю следующий результат, который отличается от вашего:

(Spin Version 6.4.3 -- 16 December 2014) 
    + Partial Order Reduction 

Full statespace search for: 
    never claim    + (ltl_0) 
    assertion violations + (if within scope of claim) 
    acceptance cycles  + (fairness disabled) 
    invalid end states - (disabled by never claim) 

State-vector 64 byte, depth reached 47, errors: 0 
     41 states, stored (58 visited) 
     18 states, matched 
     76 transitions (= visited+matched) 
     0 atomic steps 
hash conflicts:   0 (resolved) 

Stats on memory usage (in Megabytes): 
    0.004 equivalent memory usage for states (stored*(State-vector + overhead)) 
    0.288 actual memory usage for states 
    128.000 memory used for hash table (-w24) 
    0.534 memory used for DFS stack (-m10000) 
    128.730 total actual memory usage 


unreached in proctype P 
    (0 of 29 states) 
unreached in init 
    (0 of 3 states) 
unreached in claim ltl_0 
    _spin_nvr.tmp:10, state 13, "-end-" 
    (1 of 13 states) 

pan: elapsed time 0 seconds 

В частности, у меня нет предупреждений о неохваченных состояний в монитора процесса. Что касается меня, то, исходя из исходного кода, ни одно из предупреждений, которые я получил, не является проблематичным.

Либо вы используете другую версию Spin, чем я, либо вы не указали полный исходный код в своем вопросе. В последнем случае вы могли бы изменить свой вопрос и добавить код? После этого я обновлю ответ.

---

EDIT: в комментариях, вы спросите, что делает следующее сообщение означают: «неохваченных в претензии ltl_0 _spin_nvr.TMP:. 10, состояние 13, "КОНЕЦ"»

Если открыть файл _spin_nvr.tmp, вы можете увидеть следующую часть Promela кода, который соответствует автомату Бюхи который принимает все, и только исполнение, которое нарушает вашу собственность Ltl [] ((ожидание -> <> (CS)))

never ltl_0 { /* !([] ((! ((P[1]@WAIT))) || (<> ((P[1]@CRITICAL))))) */ 
T0_init: 
    do 
    :: (! ((! ((P[1]@WAIT)))) && ! (((P[1]@CRITICAL)))) -> goto accept_S4 
    :: (1) -> goto T0_init 
    od; 
accept_S4: 
    do 
    :: (! (((P[1]@CRITICAL)))) -> goto accept_S4 
    od; 
} 

сообщение просто предупреждает вас о том, что выполнение этого кода никогда не достигнет. последний замыкающий кронштейн } (состояние "-end-"), что означает, что процедура никогда не заканчивается.