旋转随机错误，面包房锁答案

【问题标题】：Spin random error, bakery lock旋转随机错误，面包房锁
【发布时间】：2013-10-11 23:55:05
【问题描述】：

我使用 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: assertion denied - invalid array index (at depth 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; ?

【问题讨论】：

我的回答不够吗？

标签： spin promela

【解决方案1】：

它不会“跳过”那一行。 Spin 执行可执行的每一行。在您的do 中，i++ 行始终可执行，因此，因为 Spin 探索所有可能的执行，i++ 行将在(i == n) 时执行。解决方法是：

 do      
 :: (number[i] > max) -> max=number[i];
 :: (i  < n) -> i++
 :: (i == n) -> break;
 od;

【讨论】：