что никогда не утверждает в этой модели promela

bool p = true;

active proctype q() {
  do
    :: p=false; p=true; p=false
  od
}

never {
do
  :: !p -> goto acceptRun
  :: else -> skip; skip
od;
acceptRun : skip

}

В этой модели промелы утверждение «никогда» проверяет, что сначала, а затем на каждом втором временном шаге выполняется p. Почему? Спасибо!


promela
person user3132300    schedule 28.12.2013    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Утверждение «никогда» занимает один шаг с каждым шагом модели. Так что, если !p, следующим шагом будет состояние принятия (никогда заявка не терпит неудачу). Но если p, то заявке никогда не потребуется два дополнительных шага, прежде чем она снова вернется к проверке p.

Хотя заявка не «ищет p», вы можете «прокрасться» в другое значение для p.

person GoZoner    schedule 04.01.2014