Select statement in Promela much slower than the equivalent if statement?

Question

So I used the following line in my Promela code.

select( cycles: 26..31 );

However, it was causing state explosion. I replaced it with the following if statement and suddenly the state explosion problem vanished. Isn't the select statement I showed above supposed to be the equivalent of the if statement below? What is going on here?

if 
:: cycles = 26;
:: cycles = 27;
:: cycles = 28;
:: cycles = 29;
:: cycles = 30;
:: cycles = 31;
fi;

Answer 1

Your select statement is converted by Spin into

cycles = 26;
do
  :: cycles < 31 -> cycles++
  :: break
od

This means that there are, in every loop execution, two possibilities to choose among, i.e. two different successor states in the transition system. If not break is chosen, you have to do a comparison and an assignment (two states), and then continue. If you want to reach the value 31, you have had 5 comparisons and 5 assignments before, whereas in the if version there is just a non-deterministic choice for an assignment.

I visualized the two different versions with spinspider, which should make the problem better understandable.

The following picture depicts the state space generated from a program with the "if"-version, where there are clearly only 6 possibilities to choose among:

int cycles;

active proctype testWithIf() {
  if 
    :: cycles = 26;
    :: cycles = 27;
    :: cycles = 28;
    :: cycles = 29;
    :: cycles = 30;
    :: cycles = 31;
  fi;

  assert(cycles >= 26 && cycles <= 31);
}

Compare to this the image generated from a program obtained as a transformation of your select statement into a do-loop:

int cycles;
active proctype test1() {
  cycles = 26;
  do
    :: cycles < 31 -> cycles++
    :: break
  od;

  assert(cycles >= 26 && cycles <= 31);
}

Do you see the differences? As I said, I think the main problem is that whereas in the if-version you just choose an assignment, you have to do multiple things in the do-version at each state where you do not choose break: You have to do the comparison, increment the counter, and then continue. This clearly generates a larger state space.