model-checkingnuxmv

NuXMV use of Real numbers

I am using nuXmv on a work that I am developing, and I am having troubles using Reals.

Suppose I have the program:

MODULE main

VAR
  t : Real;
  r : 0..5000;

ASSIGN
  init(t):=0;
  init(r):=0;

TRANS
    case
      r>=500 :next(r)=0 & next(t)=0 & r<600;
      r<500 : next(t)-t>0 -> next(r)=r+t & next(r)<600;
    esac;

SPEC
    AG r<=600

The property on this example that I am trying to prove is that r is always less or equal to 600. Note that this is just an illustrative example with no concrete meaning.

Now on command line I type

$ nuXmv <fileName>

in order to run the program and check if the property is achieved, but this message appears

"In this version of nuXmv, batch mode is not available with models containing infinite domain variables."

So the problem that I have identified is the use of Real on variable t. Is there a way to specify a range of Real values like the one I have used on variable r (which is of type Integer)? I know that if this exists that could solve the problem, if not, how can I use Reals in my program?

Thank you in advance for your time.

Solution

  • The complete error message does tell you how to get around this issue:

    In this version of nuXmv, batch mode is not available with models containing infinite domain variables.

    You can enter interactive mode calling: 

    ./nuXmv -int file_name.smv

    Alternatively, you can write the commands you want to execute in a file and then call:

    ./nuXmv -source <command-file> file_name.smv

    AFAIK, to deal with an infinite domain variables, you are expected to take advantage of the model checking techniques based on the MathSAT 5 SMT Solver. This means that you should focus on commands which have msat as prefix or suffix in their name when you look at the manual.

    Notice that there is no msat_ command for doing CTL Model Checking within nuXmv, though LTL and Invariant Model Checking are available, so you should change your property

    SPEC AG r <= 600

    into

    LTLSPEC G r <= 600

    You can then verify the model as follows:

         ~$ nuXmv -int
nuXmv > reset ;
nuXmv > read_model -i file_name.smv ;
nuXmv > go_msat ;
nuXmv > msat_check_ltlspec_bmc

    You ask:

    Is there a way to specify a range of Real values like the one I have used on variable r (which is of type Integer) ?

    No, 0.0..500.0 is illegal.

    You have the following options

    rv : real ;      -- can represent any rational value, infinite domain
iv : integer ;   -- can represent any integer value, infinite domain
fv : LB..UB ;    -- can represent any integer value in the domain [LB, UB]
sv : {0, 2, 4} ; -- can represent either 0, 2 or 4.

    If you want to add range constraints to a real/integer variable, you can use INVAR:

    INVAR 0.0 <= rv & rv <= 500.0 ;