timeout - 使用 Spin/Promela 时超时

Question

如果有人可以向我解释为什么我会使用以下代码超时，那就太好了。我理解，或者至少我认为我理解，超时的想法，但是使用 do 循环我认为这会阻止这种情况。任何建议表示赞赏。

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

然后，查看打印出来的详细信息，了解超时是如何发生的。