Ошибка: Невозможно построить BDD FSM с переменными бесконечной точности

Question

Я только что установил nuXmv и хотел попробовать пример grow-counter-integer из папки примеров.Когда я пытаюсь выполнить команду: build_model, я получаю сообщение об ошибке:

file grow-counter-integer.smv: строка 30: Невозможно создать BDD FSM с переменными бесконечной точности

Кто-нибудь знает, как исправить эту ошибку?Заранее спасибо.

растущий файл counter-integer.smv:

MODULE main

VAR state : { s0, s1, s2, s3 };

VAR c : integer;
VAR lim : real;

ASSIGN
 init(state) := s0;
 next(state) :=
  case
   state = s0 : s1;
   state = s1 : s2;
   state = s2 & c < lim : s2;
   state = s2 & c >= lim : s3;
   state = s3 : s1;
   TRUE : state;
  esac;

 init(c) := 0;
 next(c) := (state = s2 & next(state) = s2)?(c+1):(0);

 init(lim) := 2;
 next(lim) := (state = s3 & next(state) = s1)?(lim + 1):(lim);

INVARSPEC c < 3;
INVARSPEC c < 4;
INVARSPEC c < 5;
INVARSPEC c < 6;
INVARSPEC c < 20;

LTLSPEC G F (state = s3);

Answer 1

Когда входная модель содержит некоторую переменную бесконечной области , такую ​​как типы real и integer в вашей модели, конечный пользователь должен использовать MathSAT5 бэкэнд двигателя вместо обычных подходов (например, основанных на BDD).

Команды, основанные на MathSAT5, легко определяются в руководстве nuXmv благодаря тому, что в них содержится ключевое слово msat. В этом случае вы ограничены инвариантом и LTL Проверка ограниченной модели. Существуют также специальные команды для моделирования системы (т. Е. msat_pick_state и msat_simulate).

После read_model -i <file.smv> обычно используют команду go_msat, а затем выбирают подходящий подход для проверки заданных свойств.

(слайд взят из здесь )