Spin and Promela: никогда и циклично

Я запускаю вращение в режиме проверки с кодом, как показано ниже. Возникла проблема с функцией под названием «никогда». При выполнении выдает ошибку, что функции inc(), dec() и reset() никогда не выполнялись. Но если я добавлю цикл, он отлично работает. Согласно документации, «никогда» не проверяет переменные на каждом этапе. Итак, почему это не работает без цикла?

int x=0
proctype Inc(){
 do
  ::true ->
    if
      ::x<10->x=x+1
    fi
 od
}

proctype Dec(){
 do
  ::true ->
    if
      ::x>0->x=x-1
    fi
 od
}

proctype Reset(){
 do
  ::true ->
   if
    ::x==10->x=0
   fi
 od
}


never {       // if I need this to work, i have to add
  To_Init:    //  this line
    if 
      :: (x<0) || (10<x) -> goto accept
      :: else -> goto To_Init      //  and that line
    fi;
  accept:
}

init{
  run Inc();
  run Dec();
  run Reset();
}

Блок «Никогда», который дает мне предупреждение

never { 
    if 
        :: (x<0) || (10<x) -> goto accept
    fi;
    accept:
}

на самом деле это не ошибка, это своего рода предупреждение, показывает unreachable в proctype Inc, Dec, Reset, Init. Полный журнал предупреждений приведен ниже.

warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)

(Spin Version 6.2.7 — 2 March 2014)
+ Partial Order Reduction

Full statespace search for:
never claim + (never_0)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)

State-vector 28 byte, depth reached 0, errors: 0
1 states, stored
0 states, matched
1 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)

Stats on memory usage (in Megabytes):
0.000 equivalent memory usage for states (stored*(State-vector + overhead))
0.289 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 Inc
l31never-no-cycle:6, state 3, "x = (x+1)"
l31never-no-cycle:6, state 4, "((x<10))"
l31never-no-cycle:4, state 6, "(1)"
l31never-no-cycle:9, state 9, "-end-"
(4 of 9 states)
unreached in proctype Dec
l31never-no-cycle:15, state 3, "x = (x-1)"
l31never-no-cycle:15, state 4, "((x>0))"
l31never-no-cycle:13, state 6, "(1)"
l31never-no-cycle:18, state 9, "-end-"
(4 of 9 states)
unreached in proctype Reset
l31never-no-cycle:24, state 3, "x = 0"
l31never-no-cycle:24, state 4, "((x==10))"
l31never-no-cycle:22, state 6, "(1)"
l31never-no-cycle:27, state 9, "-end-"
(4 of 9 states)
unreached in claim never_0
l31never-no-cycle:35, state 6, "-end-"
(1 of 6 states)
unreached in init
l31never-no-cycle:39, state 2, "(run Dec())"
l31never-no-cycle:40, state 3, "(run Reset())"
l31never-no-cycle:41, state 4, "-end-"
(3 of 4 states)

spin
person a3dsfcv    schedule 04.04.2014    source источник
comment
Что вы подразумеваете под "без цикла"? Можете показать версию, которая не работает?   -  person GoZoner    schedule 09.04.2014

Ответы (1)


arrow_upward
5
arrow_downward

Утверждение never сообщает об ошибке в двух случаях: 1) обнаружен цикл «принять» или 2) утверждение никогда не завершается. Третья возможность — если заявка never не может сделать шаг; эта третья возможность - это та, которую производит ваш код

Когда ваше заявление было:

never { 
    if 
    :: (x<0) || (10<x) -> goto accept
    fi;
    accept:
}

начальное состояние не имеет возможного шага. То есть начальное состояние заявки never находится непосредственно перед if; из этого состояния, где x==0 нет возможности сделать следующий шаг.

Когда в утверждении never нет возможного шага, верификатор возвращается к состоянию, в котором шаг может быть предпринят. В вашем случае резервную копию делать некуда, и ваша проверка заканчивается, потому что делать больше нечего. Затем верификатор отмечает, что большая часть кода не выполнялась (потому что в вашей модели фактически ничего не выполнялось).

Вы можете сказать, что это не то, что вы ожидали из-за всего невыполненного кода. Но разве это не сообщается как ошибка.

Для вашего последующего случая вы добавили else. В этом случае верификатор может сделать шаг в утверждении never, и, таким образом, ваша проверка будет продолжена.

person GoZoner    schedule 09.04.2014
comment
На самом деле это не ошибка, это предупреждение. Добавил предупреждение в первый пост. Проверьте, пожалуйста. - person a3dsfcv; 10.04.2014
comment
Я обновил ответ... и напомнил себе о поведении never в процессе. Спасибо! - person GoZoner; 10.04.2014
comment
Спасибо за ваш ответ! Я понимаю, почему нет возможности шага в никогда не требовать. Но что такое состояние и шаг, который может быть предпринят в случае фразы, верификатор возвращается к состоянию, в котором шаг может быть предпринят. - person a3dsfcv; 11.04.2014
comment
Ага. Я предполагаю, что состояние1 равно x == 0, после этого верификатор проверяет утверждение «никогда». у него нет возможного шага, и, поскольку инициализация была первым состоянием, верификатор не может найти никаких состояний до этого, и это заканчивается. Я правильно вас понял? - person a3dsfcv; 11.04.2014
comment
Да, точно. Прочтите документацию www.spinroot.com для never. Первым действием верификатора является пошаговое утверждение never, затем модель, затем утверждение never. Если шаг не может быть предпринят в начальном состоянии, нет другого «ожидающего» состояния для изучения (возврата). Проверка заканчивается. - person GoZoner; 11.04.2014