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

Если бы кто-нибудь мог объяснить мне, почему я получаю тайм-аут со следующим кодом, это было бы здорово. Я понимаю, или, по крайней мере, я думаю, что понимаю идею тайм-аута, но с циклами 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
}

timeout promela spin
person mcdowesj    schedule 19.03.2013    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Когда вы выполняете проверку 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

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

person GoZoner    schedule 19.03.2013
comment
Спасибо. Я новичок в этом, и я пытался получить это с сайта spinroot, но я явно делал что-то не так. Спасибо еще раз. - person mcdowesj; 19.03.2013