Proctype 오류가 Promela SPIN에 전달되지 않았습니다.

Question

저는 SPIN 및 Promela에 대해 매우 익숙하며 내 모델에서 활성 속성을 확인할 때이 오류를 발견했습니다.

오류 코드 :

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 

코드는 기본적으로 피터슨의 알고리즘의 구현 내가 안전을 확인하고 유효한 것으로 보인다. 그러나 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

일반적인 대답

이것은 경고입니다 : 나는 다음과 같이

내 코드는 ... 그들은 내가 진행하는 방법을 모른다 그래서 무슨 뜻인지 모르겠어요전환하지 않기 때문에 일부 주에 연결할 수 없음을 알리는 일반적으로

,이되지오류이지만, 당신이을 모델로 모든 루틴을 연결할 수없는 상태에 가까운 살펴보고, 당신은 전혀 기대하지 있는지 확인하기 위해 좋은 방법입니다 그들을 도달 할 수 있습니다. 즉 모델이 올바르지 않은 경우 예정된 동작.

참고. 레이블 끝 :을 특정 코드 줄 앞에 사용하여 유효한 종료 상태를 표시 할 수 있으므로 이러한 경고를 제거하려면 예 : 귀하의 절차가 종료되지 않을 때. 더 많은 정보 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 

부족하다. 내가 아는 한, 소스 코드에서 유래 한 것으로, 내가 얻은 경고는 문제가되지 않는다.

다른 스핀을 사용하고 있거나 질문에 전체 소스 코드를 포함하지 않았습니다. 후자의 경우 질문을 편집하고 코드를 추가 할 수 있습니까? 나중에 내 답변을 업데이트하겠습니다.

---

편집는 : 코멘트에 다음과 같은 메시지가 의미하는 무엇을 물어 청구 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-") 이는 프로 시저가 절대로 종료되지 않는다는 것을 의미합니다.