Можем ли мы иметь терминальные состояния в NuSMV?

По построению, в так называемом стиле присвоения [используется в вашей модели]:

• всегда есть хотя бы одно начальное состояние
• все состояния имеют по крайней мере одно следующее состояние
• недетерминированность очевидна

В качестве альтернативы можно использовать так называемый тип ограничения , который позволяет :

• противоречивые ограничения INIT, которые не приводят к отсутствию начальных состояний
• противоречивые ограничения TRANS, которые приводят к состояниям взаимоблокировки (то есть состояние без какого-либо исходящего перехода в какое-то следующее состояние)
• недетерминизм скрыт

Для получения дополнительной информации см. вторую часть этого курса , которая применяется также к NuSMV по большей части.

Пример автомата, в котором у какого-либо состояния нет будущего состояния:

MODULE main
VAR b : boolean;
TRANS b -> FALSE;

Состояние, в котором b равен true, не имеет будущего состояния. И наоборот, состояние, в котором b является false, может само по себе зацикливаться или переходить в состояние, в котором b = true.

Вы можете использовать команду check_fsm для обнаружения тупиковых состояний.

Обратите внимание, что наличие взаимоблокировочных состояний может препятствовать правильности проверки модели в некоторых ситуациях. Например:

FAQ # 007: Спецификация CTL с квантификатором экзистенциального пути верхнего уровня ошибочно сообщается как нарушенная. Например, для модели, представленной ниже, обе спецификации указываются как ложные, хотя одна является просто отрицанием другой! Я знаю, что такие проблемы могут возникать с тупиковыми состояниями, но запуск его с -ctt говорит, что все в порядке.

MODULE main
VAR b : boolean;
TRANS next(b) = b;
CTLSPEC EF b
CTLSPEC !(EF b)

О других критических последствиях тупиковых состояний в переходном соотношении см. на этой странице .

---

Обычно, когда NuSMV говорит, что «условия падежа не являются исчерпывающими» , добавляется действие по умолчанию с условием TRUE в конце case конструкция, которая срабатывает, когда не применяется ни одно из предыдущих условий. Наиболее распространенным выбором для действия по умолчанию является автопетля , которая кодируется следующим образом:

MODULE main
VAR
  location: {l1,l2,l3};
ASSIGN
  init(location):= l1;
  next(location):=
    case
      (location = l1): l2;
      (location = l2): {l1, l3};
      TRUE           : location;
    esac;

ПРИМЕЧАНИЕ: пожалуйста обратите внимание, что если существует несколько условий с одинаковым защитным устройством , только первое из этих условий когда-либо используется. По этой причине, когда в вашей модели location = l2 следующее значение location может быть только l1 и никогда l3. Чтобы исправить это и иметь некоторый недетерминированный выбор среди l1 и l3, необходимо перечислить все возможные будущие значения при том же условии, что и набор значений (то есть {l1, l3}).