It doesn't 'skip' that line. Spin executes every line that is executable. In your do
the line i++
is always executable and therefore, because Spin explores all possible executions, the i++
line will be executed even when (i == n)
. The fix is:
do
:: (number[i] > max) -> max=number[i];
:: (i < n) -> i++
:: (i == n) -> break;
od;