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

Question

I just installed nuXmv and wanted to try out the example growing-counter-integer from the examples folder. When I try to run the command: build_model, I get the error message:

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

Does somebody know how to fix this error? Thanks in advance.

growing-counter-integer.smv file:

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

When the input model contains some infinite-domain variable, like the real and integer types in your model, the end-user is supposed to use the MathSAT5 engine back-end instead of the regular approaches (like, e.g., those based on BDDs).

The commands based on MathSAT5 are easily identifiable in the nuXmv manual by the fact that they have the keyword msat in them. In this case, you are limited to invariant and LTL Bounded Model Checking. There are special commands also for simulating the system (i.e. msat_pick_state and msat_simulate).

After read_model -i <file.smv>, one would typically use the command go_msat and then select the appropriate approach for checking the given properties.

(slide taken from here)