Проверка модели LTL с использованием синтаксиса Spin и Promela

Я пытаюсь воспроизвести код ALGOL 60, написанный Дейкстрой в статье под названием «Взаимодействующие последовательные процессы», код является первой попыткой решить проблему мьютекса, вот синтаксис:

begin integer turn; turn:= 1;
      parbegin
      process 1: begin Ll: if turn = 2 then goto Ll;
                           critical section 1;
                           turn:= 2;
                           remainder of cycle 1; goto L1
                 end;
      process 2: begin L2: if turn = 1 then goto L2;
                           critical section 2;
                           turn:= 1;
                           remainder of cycle 2; goto L2
                  end
      parend
end

Итак, я попытался воспроизвести приведенный выше код в Promela, и вот мой код:

#define true    1
#define Aturn true
#define Bturn false

bool turn, status;

active proctype A()
{   
    L1: (turn == 1); 
    status = Aturn;
    goto L1;
    /* critical section */
    turn = 1;

}

active proctype B()
{   
    L2: (turn == 2); 
    status = Bturn;
    goto L2;
    /* critical section */
    turn = 2;
}

never{ /* ![]p */ 
    if
    :: (!status) -> skip
    fi;
}

init
{   turn = 1;
    run A(); run B();
}

Что я пытаюсь сделать, так это убедиться, что свойство честности никогда не будет выполняться, потому что метка L1 работает бесконечно.

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

вот фактический вывод из iSpin

spin -a  dekker.pml
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DSAFETY -DNOCLAIM -w -o pan pan.c
./pan -m10000 
Pid: 46025

(Spin Version 6.2.3 -- 24 October 2012)
    + Partial Order Reduction

Full statespace search for:
    never claim             - (not selected)
    assertion violations    +
    cycle checks        - (disabled by -DSAFETY)
    invalid end states  +

State-vector 44 byte, depth reached 8, errors: 0
       11 states, stored
        9 states, matched
       20 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.001   equivalent memory usage for states (stored*(State-vector + overhead))
    0.291   actual memory usage for states
  128.000   memory used for hash table (-w24)
    0.534   memory used for DFS stack (-m10000)
  128.730   total actual memory usage


unreached in proctype A
    dekker.pml:13, state 4, "turn = 1"
    dekker.pml:15, state 5, "-end-"
    (2 of 5 states)
unreached in proctype B
    dekker.pml:20, state 2, "status = 0"
    dekker.pml:23, state 4, "turn = 2"
    dekker.pml:24, state 5, "-end-"
    (3 of 5 states)
unreached in claim never_0
    dekker.pml:30, state 5, "-end-"
    (1 of 5 states)
unreached in init
    (0 of 4 states)

pan: elapsed time 0 seconds
No errors found -- did you verify all claims?

Я прочитал всю документацию по спину на блоке never{..}, но не смог найти ответ (вот ссылка), также я пробовал использовать блоки ltl{..} (ссылка), но это только что дало мне синтаксическую ошибку, хотя в документации явно упоминается, что она может быть за пределами init и proctypes, может ли кто-нибудь помочь мне исправить этот код, пожалуйста?

Спасибо


promela spin model-checking
person ymg    schedule 05.03.2013    source источник
comment
Это вопрос программирования, а не информатики; отправляет вас в переполнение стека.   -  person Raphael    schedule 05.03.2013

Ответы (1)


arrow_upward
1
arrow_downward

Вы переопределили «истину», что не может быть хорошо. Я отказался от этого переопределения, и требование никогда не терпит неудачу. Но неудача не имеет значения для вашей цели - это начальное состояние "статус" является "ложным", и, таким образом, требование никогда не выходит, что является неудачей.

Кроме того, немного дурным тоном присваивать логическому значению 1 или 0; вместо этого назначьте true или false - или используйте бит. Почему бы не следовать коду Дейкстры более точно — использовать «int» или «byte». Не то чтобы производительность была проблемой в этой проблеме.

Вам не нужно «активно», если вы собираетесь вызывать «бег» — только одно или другое.

Мой перевод «процесса 1» будет таким:

proctype A ()
{
L1: turn !=2 ->
  /* critical section */
  status = Aturn;
  turn = 2
  /* remainder of cycle 1 */
  goto L1;
}

но я могу ошибаться в этом.

person GoZoner    schedule 06.03.2013
comment
Спасибо за вашу помощь, могу я просто спросить, что означает здесь (-›)? и почему правило блокировки здесь считается плохим, я имею в виду (true==1); - person ymg; 06.03.2013
comment
'-›' означает то же самое, что и ';' но используется стилистически после блокирующего выражения. - person GoZoner; 06.03.2013
comment
[Я думаю, вы имели в виду '(turn==1)'; не правда']. Нет ничего плохого в использовании 'turn==1' или 'turn!=2' - я использовал 'turn!=2' по аналогии с кодом Дейкстры. - person GoZoner; 06.03.2013
comment
хорошо, спасибо за ваш вклад, я в данный момент создаю свои формулы, чтобы начать проверку свойств, еще раз спасибо за вашу помощь. - person ymg; 06.03.2013