// Description: Module initialises an index variable, a sum variable and the first 10 elements of an array to 0. At each step, the next block increments the index variable and stores the value of the index variable in that position in the array, and adds the value of the index variable to the sum. The invariant checks that the sum of the first 10 elements of the array is equal to the sum variable. The invariant is checked with bounded model checking.

module main
{
  var numbers : [integer]integer;
  var sum, index : integer;


  init {
    for i in range(0, 9) {
      numbers[i] = 0;
    }
    sum = 0;
    index = 0;
  }

  next {
    sum' = sum + index;
    numbers' = numbers[index -> index];
    index' = index + 1;

  }

  invariant num_sum:
      ((numbers[0] + numbers[1] + numbers[2] + numbers[3] +
        numbers[4] + numbers[5] + numbers[6] + numbers[7]) == sum);
  control {
    // print_module;
    unroll (5);
    check;
    print_results;
  }
}
