title: NuXMV use of Real numbers
body: <p>I am using <strong>nuXmv</strong> on a work that I am developing, and I am having troubles using Reals.</p>
  
  <p>Supose I have the program:</p>
  
  <pre><code>MODULE main
  
  VAR
    t : Real;
    r : 0..5000;
  
  ASSIGN
    init(t):=0;
    init(r):=0;
  
  TRANS
      case
        r&gt;=500 :next(r)=0 &amp; next(t)=0 &amp; r&lt;600;
        r&lt;500 : next(t)-t&gt;0 -&gt; next(r)=r+t &amp; next(r)&lt;600;
      esac;
  
  SPEC
      AG r&lt;=600
  </code></pre>
  
  <p>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.</p>
  
  <p>Now on comand line I type</p>
  
  <pre><code>$ nuXmv &lt;fileName&gt;
  </code></pre>
  
  <p>in order to run the program and check if the property is achieved, but this message appears</p>
  
  <blockquote>
    <p>"In this version of nuXmv, batch mode is not available with models containing infinite domain variables."</p>
  </blockquote>
  
  <p>So the problem that I have identified is the use of <code>Real</code> on variable <code>t</code>.
  Is there a way to specify a range of Real values like the one I have used on variable <code>r</code> (wich 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?</p>
  
  <p>Thank you in advance for your time.</p>