algorithm - NuSMV による Dekker の相互排除アルゴリズムの検証

Question

NuSMV を使用して Dekker アルゴリズムを検証します。私のコードは次のとおりです。

MODULE main
VAR
b1 : {true, false};
b2 : {true, false};
k : {1, 2};
pr1 : process proc(k, b1, b2, 1);
pr2 : process proc(k, b2, b1, 2);
ASSIGN
init(b1) := false;
init(b2) := false;
init(k) := {1, 2};

MODULE proc(k, bi, bj, i)
VAR
state : {noncritical, test_bj, ftest_k,
stest_k, critical};
DEFINE
j :=
case
i = 1 : 2;
i = 2 : 1;
esac;
ASSIGN
init(state) := noncritical;
next(state) :=
case
state = noncritical : {noncritical, test_bj};
state = test_bj & (bj = false) : critical;
state = test_bj & (bj = true) : ftest_k;
state = ftest_k & (k = j) : stest_k;
state = ftest_k & (k != j) : test_bj;
state = stest_k & (k = j) : stest_k;
state = stest_k & (k !=j) : test_bj;
state = critical : {critical, noncritical};
esac;
next(bi) :=
case
state = noncritical &
next(state) = test_bj : true;
state = ftest_k & (k = j) : false;
state = stest_k & (k != j) : true;
state = critical &
next(state) = noncritical : false;
1 : bi;
esac;
next(k) :=
case
state = critical &
next(state) = noncritical : j;
1 : k;
esac;

FAIRNESS
running
FAIRNESS
!(state = critical)
FAIRNESS
!(state = noncritical)

しかし、フィードバックは写真のようなもので、「:」の不正な左オペランド型を示しています。ブール値にする必要があります。どうしてか分かりません。助けてください... コードの何が問題なの NuSMV フィードバック