Spin/Promela를 사용할 때 시간 초과가 발생했습니다.

Question

누군가 다음과 같은 코드를 사용하여 시간 제한을받는 이유를 설명 할 수 있다면 좋습니다. 나는 적어도 타임 아웃에 대한 생각을 이해한다고 생각하지만, do 루프를 사용하면 이것을 막을 수 있다고 생각했다. 모든 조언을 부탁드립니다. 당신이 SPIN 검증을 수행하고 문제가 이러한 '타임 아웃'으로, 발생하는 경우

mtype wantp = false; 
mtype wantq = false; 
mtype turn = 1; 

active proctype p() 
{ 
    do 
    :: printf ("non critical section for p\n"); 
    wantp = true; 
    (wantq ==true); 

    if 
    :: (turn == 2)-> 
     wantp = false; 
     /* wait for turn ==1*/ 
     (turn ==1); 
     wantp = true; 
    fi; 

    printf("CRITICAL SECTION for P\n"); 
    turn = 2; 
    wantp = false; 
    od 
} 

active proctype q() 
{ 
    do 
    :: printf("non critical section for q\n"); 
    wantq = true; 
    (wantp ==true); 

    if 
    :: (turn == 1)-> 
     wantq = false; 
     (turn ==2); 
     wantq = true; 
    fi; 

    printf("CRITICAL SECTION for Q\n"); 
    turn = 1; 
    wantq = false; 
    od 
} 

Answer 1

, 당신은 '흔적'파일로 알려진 있습니다. 트레일 파일은 문제를 일으키는 프로그램 실행을 통해 정확한 경로를 보여줍니다.

위의 파일을 test.pml이라고 가정합니다. 다음 작업을 수행하십시오.

$ spin -a test.pml 
$ gcc -o pan pan.c 
$ ./pan 
# info about verification, shows timeout 
# view the detailed trail file 
$ spin -p -t test.pml 

그런 다음 자세한 내용을보고 제한 시간이 어떻게되는지 확인하십시오.