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

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

0 голосов
/ 19 февраля 2019

Возможно ли иметь состояние в NuSMV, которое не имеет переходов в какие-либо другие состояния?Например, действительно ли в моем коде l3 нет переходов?Когда я запускаю этот NuSMV выдает ошибку, что «условия случая не являются исчерпывающими».Спасибо! 

MODULE main

VAR

location: {l1,l2,l3};


ASSIGN

init(location):=l1;

next(location):= case
             (location = l1): l2;
             (location = l2): l1;
             (location = l2): l3;
             esac;

1 Ответ

0 голосов
/ 19 февраля 2019

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

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

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

  • несовместимые 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, которое запускается, когда не применяется ни одно из предыдущих условий.Наиболее распространенный выбор для действия по умолчанию - это self-loop , который кодируется следующим образом: 

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}).

...