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 に答える