Attempt to check for fairness (not currently working)

node-preds.maude

@@ -32,15 +32,41 @@ omod CHECK-NODE-SYSTEM{N :: NZNAT#} is
   op inCritSec : Nat/{N} -> Prop .
   op twoInCritSec : -> Prop .
   op hasUnsentMessages : -> Prop .
+  op canUndergoFurtherTransitions : -> Prop .
+  op isExhausted : -> Formula .
 
   vars N M : Oid . vars A B : AttributeSet . var C : Configuration .
-  var I : Nat .
+  vars I J K : Nat . var Q : TaskQueue .
 
   eq < N : Node | mode : Queued, A > C |= isQueued(N) = true .
   eq < N : Node | mode : CritSec, A > C |= inCritSec(N) = true .
   eq < N : Node | mode : CritSec, A >
      < M : Node | mode : CritSec, B > C |= twoInCritSec = true .
   eq < N : Node | stimuli : s(I), A > C |= hasUnsentMessages = true .
+
+  eq < N : Node | mode : Queued, A > C |= canUndergoFurtherTransitions = true .
+  ceq < N : Node | runQueue : Q, A > C |= canUndergoFurtherTransitions = true if count(Q) > 0 .
+  ceq < N : Node | ackQueue : Q, A > C |= canUndergoFurtherTransitions = true if count(Q) > 0 .
+  eq < N : Node | mode : Queued, A > C |= canUndergoFurtherTransitions = true .
+  eq < N : Node | mode : CritSec, A > C |= canUndergoFurtherTransitions = true .
+  eq < N : Node | stimuli : s(I), A > C |= canUndergoFurtherTransitions = true .
+  eq < N : Node | numPendingAcks : s(I), A > C |= canUndergoFurtherTransitions = true .
+  eq isExhausted = [] ~ canUndergoFurtherTransitions .
+
+  op isUnfair : -> Formula .
+  op isUnfairAux : Nat/{N} Nat/{N} -> Formula .
+  op isUnfairPair : Oid Oid -> Formula .
+  op isUnfairPre : Oid Oid -> Prop .
+
+  eq isUnfair = isUnfairAux(#, #) .
+  eq isUnfairAux([0], [0]) = False .
+  eq isUnfairAux([s(I)], [0]) = isUnfairPair([s(I)], [0]) \/ isUnfairAux([I], [#]) .
+  eq isUnfairAux([I], [s(J)]) = isUnfairPair([I], [s(J)]) \/ isUnfairAux([I], [J]) .
+  eq isUnfairPair(M, N) =
+    isUnfairPre(M, N) -> ~ ((~ inCritSec(N)) U inCritSec(M)) [owise] .
+  eq < M : Node | mode : Queued, A >
+     < N : Node | mode : Idle, B > C
+    |= isUnfairPre(M, N) = true .
 endom
 
 --- Future Invariants:

test-node-preds.maude

@@ -4,6 +4,11 @@ view 4 from NZNAT# to NAT is
   op # to term 4 .
 endv
 
+--- Kshemkalyani and Singhal (p. 6) lists the requirements of a mutual exclusion algorithm:
+--- * Safety Property: At any instant, only one process can execute the critical section.
+--- * Liveness Property: This property states the absence of deadlock and starvation. Two or more sites should not endlessly wait for messages which will never arrive.
+--- * Fairness: Each process gets a fair chance to execute the CS. Fairness property generally means the CS execution requests are executed in the order of their arrival (time is determined by a logical clock) in the system.
+
 --- Check the mutual exclusion property
 red modelCheck(init, []~ twoInCritSec) .
 --- Expected: true
@@ -13,5 +18,7 @@ red modelCheck(init, []~ twoInCritSec) .
 red modelCheck(init, <>[]~ hasUnsentMessages) .
 --- Expected: true
 
---- Check for another watered-down version of strong liveness.
-red modelCheck(init, []()) .
+--- Check for fairness.
+red modelCheck(init, (<> isExhausted) -> [] ~ isUnfair) .
+---red modelCheck(init, (isUnfair_Pre(N:Oid, I:Nat, M:Oid, J:Nat) -> <> isUnfair_Post(N:Oid, I:Nat, M:Oid, J:Nat))) .
+--- Expected: true