title: Programming a bubblesort in NuSMV
body: <p>I'm trying to program a simple bubble sort as a FSM in NuSMV, but i'm facing a major problem, I can't do the swap in the array, when I try to make a swap between 2 elements os the array, the program stops. Can anyone help solve this? Thanks a lot.</p>
  
  <pre><code>MODULE main
  VAR
  
  y: 0..5;
  x : 0..5;
  low : 0..10;
  big : 0..10;
  
  DEFINE
  arr : [3,4,2,3,5,6];
  output : [0,0,0,0,0,0];
  
  ASSIGN
  
  init(x) := 0;
  init(y) := 1;
  init(low) := 0;
  init(big) := 0; 
  
  
  next(low) := case
      arr[x] &gt; arr[y] : arr[y];
      TRUE : arr[x];
      esac;
  
  next(big) := case
      arr[x] &gt; arr[y] : arr[x];
      TRUE : arr[x];
      esac;
  
  TRANS
  case
      arr[x] &lt;= arr[y] : output[x] = low &amp; output[y] = big &amp; next(y) = y + 1 &amp; next(x) = x + 1;
      arr[x] &gt; arr[y] : output[x] = big &amp; output[y] = low &amp; next(y) = y + 1 &amp; next(x) = x + 1;
      y = 5 | x = 5 : next(y) = 0 &amp; next(x) = 1;
      TRUE : next(y) = y + 1 &amp; next(x) = x + 1;
  esac
  </code></pre>