Тайм-аут при использовании Spin/Promela

Question

Если кто-то может объяснить мне, почему я получаю таймаут со следующим кодом, который был бы замечательным. Я понимаю, или, по крайней мере, я думаю, что я делаю, идея тайм-аута, но с петлями дела я думал, что это остановит это. Любые советы приветствуются.

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

При выполнении проверки SPIN и возникает проблема, например, «тайм-аут», то есть то, что известно как файл «след». Файл трейла показывает вам точный путь выполнения программы, что приводит к этой проблеме.

Предполагая, что вышеуказанный файл называется 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 

Затем просмотрите детали, напечатанные, чтобы выяснить, как произошел тайм-аут.