Error: Impossible to build a BDD FSM with infinite precision variables

Question

我刚刚安装了 nuXmv 并想尝试示例文件夹中的示例 growing-counter-integer。当我尝试运行命令时：build_model，我收到错误消息：

file growing-counter-integer.smv: line 30: Impossible to build a BDD FSM with infinite precision variables

有人知道如何解决这个错误吗？提前致谢。

growing-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。在这种情况下，您仅限于 invariant 和 LTL 有界模型检查。还有用于模拟系统的特殊命令（即 msat_pick_state 和 msat_simulate）。

在 read_model -i <file.smv> 之后，通常会使用命令 go_msat 然后 select 检查给定属性的适当方法。

（幻灯片取自 here）

Error: Impossible to build a BDD FSM with infinite precision variables

Error: Impossible to build a BDD FSM with infinite precision variables

nusmv

nuxmv