title: Assign random value to variables in NuSMV
body: <p>I have the following code in NuSMV.</p>
  
  <pre><code>MODULE main
  VAR
     x : 0..5
  </code></pre>
  
  <p>So x is a variable which can take integer values 0,1,2,3,4,5. Next, I initialize it and lay down its transition rules.</p>
  
  <pre><code>ASSIGN
      init(x):=1;
      next(x) := case
           y=1 &amp; z=23: 4;
           TRUE: 0..5;
      esac;
  </code></pre>
  
  <p>What above should say is that x is initially 1. Then if y=1 and z=23, x becomes 4 otherwise x can assume any random values from its domain. This 'otherwise' part of the logic is what I am doubtful. Have I coded this correctly? y and z are variables whose codes are not shown here. Assume something for y and z.</p>
  
  <p>Or should I have written:</p>
  
  <pre><code>TRUE: {0,1,2,3,4,5};
  </code></pre>
  
  <p>Because I definitely know the above to be correct from page 4 of <a href="http://nusmv.fbk.eu/NuSMV/tutorial/v26/tutorial.pdf" rel="nofollow noreferrer">this</a> document.</p>
  
  <p>But this is infeasible for a very large domain. Suppose x could take any value from 0 to 293.</p>