Spin random error, bakery lock

Question

I've created a bakery lock using Spin

1   int n=3;
2       int choosing[4] ; // initially 0 
3       int number[4];  // initially 0 
4        
5   active [3] proctype p()
6   {
7        
8        choosing[_pid] = 1; 
9        int max = 0; 
10       int i=0;
11  
12      do      
13      ::(number[i] > max) -> max=number[i];
14      ::i++;
15      :: (i == n) -> break;
16      od;
17      
18      number[_pid] = max + 1;
19      choosing[_pid] = 0;
20  
21      int j=0;
22      
23      do
24      ::(j==n) -> break; 
25      ::  do
26          ::(choosing[j] == 0)-> break;
27          od;
28      ::  if
29          ::(number[j] ==0) -> j++;
30          ::(number[j] > number[_pid]) -> j++;
31          ::((number[j] == number[_pid]) && ( j> _pid)) -> j++;
32          fi;
33      od;
34  
35      number[_pid]=0
36      
37  }

when I test it I get an error: pan:1: assertion violated - invalid array index (at depth 5)

when I run the trail I get this back

  1:    proc  2 (p) Bakery_lock.pml:8 (state 1) [choosing[_pid] = 1]
  2:    proc  2 (p) Bakery_lock.pml:10 (state 2)    [max = 0]
  2:    proc  2 (p) Bakery_lock.pml:12 (state 3)    [i = 0]
  3:    proc  2 (p) Bakery_lock.pml:14 (state 6)    [i = (i+1)]
  4:    proc  2 (p) Bakery_lock.pml:14 (state 6)    [i = (i+1)]
  5:    proc  2 (p) Bakery_lock.pml:14 (state 6)    [i = (i+1)]
spin: indexing number[3] - size is 3
spin: Bakery_lock.pml:13, Error: indexing array 'number'
  6:    proc  2 (p) Bakery_lock.pml:13 (state 4)    [((number[i]>max))]

Can anyone tell me why it skips this line (i == n) -> break; ?

Answer 1

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;