cygwin - proctype エラーで Promela SPIN に到達できませんでした

Question

私は SPIN と Promela にかなり慣れていないので、モデルの liveness プロパティを検証しようとしているときにこのエラーに遭遇しました。

エラーコード：

unreached in proctype P
        (0 of 29 states)
unreached in proctype monitor
        mutex_assert.pml:39, state 1, "assert(!((mutex>1)))"
        mutex_assert.pml:42, state 2, "-end-"
        (2 of 2 states)
unreached in init
        (0 of 3 states)
unreached in claim ltl_0
        _spin_nvr.tmp:10, state 13, "-end-"
        (1 of 13 states)

pan: elapsed time 0 seconds

コードは基本的にピーターソンのアルゴリズムの実装であり、安全性をチェックしたところ、有効なようです。しかし、ltl {[]((wait -> <> (cs)))} を使用して liveness プロパティを検証しようとすると、上記のエラーが発生します。意味がよくわからないのでどうすればいいのかわかりません...

私のコードは次のとおりです。

#define N 3
#define wait   (P[1]@WAIT)
#define cs     (P[1]@CRITICAL)

int pos[N]; 
int step[N]; 
int enter;
byte mutex;
ltl {[]((wait -> <> (cs)))}

proctype P(int i) {
  int t;
  int k;
  WAIT:
  for (t : 1 .. (N-1)){
  pos[i] = t
  step[t] = i
  k = 0;
  do
  ::  atomic {(k != i && k < N && (pos[k] < t|| step[t] != i)) -> k++}
  ::  atomic {k == i -> k++}
  ::  atomic {k == N -> break}
  od;
  }

CRITICAL:
  atomic {mutex++;
  printf("MSC: P(%d) HAS ENTERED THE CRITICAL SECTION.\n", i);
  mutex--;}
  pos[i] = 0;
}

init {
  atomic { run P(0); }
}