2
によってデッカーの相互排除アルゴリズムを確認し、私のコードは以下の通りです：私はデッカーのアルゴリズムを検証するためにNuSMVを使用NuSMV
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)
が、フィードバックが絵のようなものです、それは「の違法左オペランドのタイプを示しています。 "ブール値でなければなりません。どうしてか分かりません。これは、構文エラーを修正します
TRUE : whatever
にコード NuSMV feedback
