NuSMV передает неправильную спецификацию

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

MODULE main ()
VAR
  state : {a,b,c};

ASSIGN
  init(state):=a;
  next(state):=b;

---

Комментарии к вашему подходу. Свойство SPEC !EF(state=a -> state=c) можно прочитать как:

неверно, что существует путь, начинающийся из начального состояния, такой, что рано или поздно логическое условие state=a -> state=c становится true.

Условие state = a -> state = c является true для всех состояний, таких как state != a, потому что не существует состояния, в котором условия state = a и state = c могут выполняться одновременно.

Если вы запустите NuSMV, вы получите следующий контрпример:

NuSMV > reset; read_model -i test.smv; go; check_property
-- specification !(EF (state = a -> state = c))  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
-> State: 1.1 <-
  state = a
-> State: 1.2 <-
  state = b

В состоянии 1.2 переменная state равна b, поэтому state = a -> state = c равно true, а !EF(state = a -> state = c) нарушается.

Аналогичные соображения справедливы для свойства SPEC !EF(state=b -> state=a).

---

Одношаговая достижимость. Если вы хотите проверить, что не существует одношагового перехода из состояния, в котором state = a, в состояние в который содержит state = c, вы можете использовать следующее свойство:

SPEC AG (state = a -> AX state != c)

Это гласит:

для всех состояний, которые могут быть достигнуты по всем путям выполнения, начиная со всех начальных состояний, свойство CTL state = a -> AX state != c всегда проверяется. Такое свойство говорит о том, что если в текущем состоянии state = a, то обязательно имеет место случай, когда во всех возможных непосредственных следующих состояниях значение state отличается от c.

Если мы проверим такое свойство с помощью NuSMV, мы обнаружим, что оно проверено:

NuSMV > reset; read_model -i test.smv; go; check_property
-- specification AG (state = a -> AX state != c)  is true

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

---

Достижимость пути. Если вы хотите проверить, что не существует пути, образованного произвольным и переменным числом промежуточные переходы, которые достигают состояния, в котором выполняется state = c, начиная с состояния, в котором выполняется state = a, тогда кодировка немного отличается:

SPEC AG (state = a -> AX AG state != c)

Это гласит:

для всех состояний, которые могут быть достигнуты по всем путям выполнения, начиная со всех начальных состояний, свойство CTL state = a -> AX AG state != c всегда проверяется. Таким свойством является true для всех состояний s' с.т.

• state != a in s'

or

• state = a в s' и state != c для всех достижимых состояний s'' на всех исходящих путях, начинающихся в s'

Если мы проверим такое свойство с помощью NuSMV, мы обнаружим, что оно проверено:

NuSMV > reset; read_model -i test.smv; go; check_property
-- specification AG (state = a -> AX (AG state != c))  is true

---

Чтобы лучше показать разницу между двумя кодировками, я приведу здесь пример модели, в которой первое свойство равно false, а второе это true:

MODULE main ()
VAR
  state : {a,b,c};

ASSIGN
  init(state):=a;
  next(state) := case
     state = a : b;
     state = b : c;
     TRUE : state;
    esac;

SPEC AG (state = a -> AX state != c)
SPEC AG (state = a -> AX AG state != c)

Если вы запустите NuSMV для этого примера, результат будет следующим:

NuSMV > reset; read_model -i test.smv; go; check_property
-- specification AG (state = a -> AX state != c)  is true
-- specification AG (state = a -> AX (AG state != c))  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
-> State: 1.1 <-
  state = a
-> State: 1.2 <-
  state = b
-> State: 1.3 <-
  state = c

Очевидно, что если свойство first имеет значение false, то свойство second также обязательно должно иметь значение false.

---

K-шагов достижимости. одношаговое кодирование достижимости можно обобщить до достижимости в точное k шагов путем увеличения количество AX в формуле:

SPEC AG (state = a -> AX state != c)       -- state != c after 1 transition
SPEC AG (state = a -> AX AX state != c)    -- state != c after 2 transitions
SPEC AG (state = a -> AX AX AX state != c) -- state != c after 3 transitions
SPEC AG (state = a -> AX ... state != c)   -- state != c after 1 + |...| transitions

---

Приблизительное время прибытия:

В этом сценарии использования свойство

SPEC AG (state = a -> AX AG state != c)

можно упростить до

SPEC AG (state = a -> AG state != c)

и, очевидно, все равно будет работать.

Однако есть причина, по которой я этого не сделал: существует незначительная семантическая разница между двумя кодировками, и хотя последняя может использоваться для проверки достижимости в некоторых случаях прежнее кодирование является более надежным, поскольку оно более точно соответствует фактической семантике < em>достижимость проблема. например, шаблон B_COND_1 -> AG B_COND_2 с треском терпит неудачу всякий раз, когда B_COND_2 := !B_COND_1, потому что для любого состояния s', подтверждающего посылку B_COND_1, вывод AG B_COND_2, который можно переписать как AG !B_COND_1-, не может иметь места; добавление AXк заключению добавляет один уровень косвенности, и это более правильно, поскольку заключение должно сохраняться только начиная с следующих состояний в дереве выполнения.

---

Расчетное время прибытия №2:

Ты пишешь:

как мне написать спецификацию для "доступно ли A из B?" - это должно вернуть false, так как переход не определен

Свойство, которое возвращает false при отсутствии пути от state = b до state = a, выглядит следующим образом:

SPEC AG (state = b -> EF state = a)

Если вы хотите убедиться в том, что никогда не бывает так, чтобы state = a был доступен из state = b, то это на самом деле плохая идея по двум причинам:

• если свойство проверено, вам не возвращается контрпример свидетеля для трассировки выполнения s.t. state = a доступен из state = b, поэтому вам остается самостоятельно определить, почему это так на вашей модели.

• если свойство равно false, инструменту потребуется перечислить все (возможно, экспоненциально много) пути, начинающиеся с state = b, так что state = a недоступен.

По этим причинам я фактически закодировал проблему достижимости наоборот, возвращая true, когда state = a недоступен из state = b, и false + один контрпример в противном случае.