promela - promela での配列の定義と開始

Question

1 #define NUM_PHIL 4
2 
3 byte chopstick[4];
4 chopstick[0] = 1;
5 chopstick[1] = 1;
6 chopstick[2] = 1;
7 chopstick[3] = 1;
8 
9 proctype phil(int id) {
10    do 
11      ::printf("Philosopher %d is thinking\n",id);
12      /* ... */
13      printf("Philosopher %d is eating with forks %d and %d\n",id,id,(id+1)%4);
14      /* ... */
15    od
16    }
16a
17 init {
18    int i = 0; 
19    do 
20    :: i >= NUM_PHIL -> break
21    :: else -> run phil(i); 
22               i++ 
23    od 
24    }

上記のコードは、「構文エラーが「チョップスティック」の近くに「識別子」を見ました」というエラーを送信します

Answer 1

init本体で箸配列を初期化します。

#define NUM_PHIL 4

byte chopstick[4];    /* NUM_PHIL */

proctype phil (int n) { /* ... */ }

init {
  chopstick[0] = 1;
  /* ... */

  run phil (0);
  /* ... */
}