使用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 

然後，查看打印出的詳細信息以瞭解超時是如何發生的。