0

誰かが私に次のコードでタイムアウトが発生する理由を説明できれば、それは素晴らしいことです。私はタイムアウトの考えを理解している、または少なくとも私は理解していると思いますが、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
}
4

1 に答える 1

2

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

次に、印刷された詳細を見て、タイムアウトがどのように発生したかを把握します。

于 2013-03-19T06:54:03.070 に答える