Проверьте алгоритм взаимного исключения Деккера по NuSMV

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 feedback

Answer 1

Изменение

1 : whatever 

в

TRUE : whatever 

это будет исправить ошибки синтаксиса.

Я надеюсь, что это вам помогло.