Graded-CTL NuSMV

Source Code for "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)