1

我使用 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  }

当我测试它时，我得到一个错误：pan：1：断言违反 - 无效的数组索引（深度 5）

当我跑步时，我得到了这个

  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))]

谁能告诉我为什么它跳过这一行 (i == n) -> break; ?

4

1 回答 1

2

它不会“跳过”那条线。Spin 执行可执行的每一行。在您do的行i++中，该行始终是可执行的，因此，由于 Spin 探索了所有可能的执行，i++即使(i == n). 修复方法是：

 do      
 :: (number[i] > max) -> max=number[i];
 :: (i  < n) -> i++
 :: (i == n) -> break;
 od;
于 2013-10-14T22:21:16.300 回答