스핀 "- 끝 -"

Question

나는 스핀 모델 검사 꽤 새로 온 사람이 오류가 무엇을 의미하는지 알고 싶어 여기

unreached in proctype P1 
    ex2.pml:16, state 11, "-end-" 
    (1 of 11 states) 
unreached in proctype P2 
    ex2.pml:29, state 11, "-end-" 
    (1 of 11 states) 

내 코드입니다 :

int y1, y2; 
byte insideCritical; 

active proctype P1(){ 
do 
    ::true-> 
     y2 = y1 + 1; 
     (y1 == 0 || y2 < y1); 
     /* Entering critical section */ 
      insideCritical++; 
      assert(insideCritical < 2); 
      insideCritical--; 
     /* Exiting critical section */ 
     y2 = 0; 
od 
} 
active proctype P2(){ 
do 
    ::true-> 
     y1 = y2 + 1; 
     (y2 == 0 || y1 < y2); 
     /* Entering critical section */ 
      insideCritical++; 
      assert(insideCritical < 2); 
      insideCritical--; 
     /* Exiting critical section */ 
     y1 = 0; 
od 
} 

이 실제로 종료 할 필요는 없습니다. 두 프로세스가 중요한 섹션에 있지 않은지 여부를 확인하는 상호 제외 프로그램입니다. 오류는 프로그램이 종료되지 않았 음을 의미합니까? 감사합니다.

Answer 1

스핀은 귀하의 proctype이 결코 "끝"상태에 이르지 않는다는 것을 알려주며, 이것은 끝없는 루프로 구성되어 있기 때문에 사실입니다. 이것이 의도 된 행동이 아니라면 유용한 정보가 될 것입니다. 귀하의 경우에는, 그러나, 당신은 단지 프로그램, 코드에 끝 라벨을 추가하여 DO 루프에 해당하는 상태로 종료 허용되는 스핀을 말할 수있는 예 :

active proctype P1(){ 
    endHere: 
    do 
    :: true-> 
    y2 = y1 + 1; 
    (y1 == 0 || y2 < y1); 
    /* Entering critical section */ 
     insideCritical++; 
     assert(insideCritical < 2); 
     insideCritical--; 
    /* Exiting critical section */ 
    y2 = 0; 
    od 
} 

최종 레이블을 "end"로 시작하는 레이블입니다. Proctype이 그런 상태로 끝나면 Spin은 경고를 표시하지 않습니다.

Answer 2

확인 된 대답이 좋습니다. end 레이블을 적절하게 추가하는 것이 명확한 형식입니다. 그러나, 그렇게하는 것이 불가능하며, 따라서 당신은 -n 플래그와 함께 pan 검증을 실행하여 스핀을 조용히 수 있습니다

-n : no listing of unreached states at the end of the run