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.
The complete error message does tell you how to get around this issue:
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 propertyinto
You can then verify the model as follows:
You ask:
No,
0.0..500.0
is illegal.You have the following options
If you want to add range constraints to a real/integer variable, you can use INVAR: