Add check for fairness which passes but maybe shouldn't be passing

node-preds.maude

@@ -58,12 +58,16 @@ omod CHECK-NODE-SYSTEM{N :: NZNAT#} is
   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] .
+  --- TODO: Why does this work? Shouldn't it break if M and N transition to Queued at the same timestamp if N < M?
+  eq isUnfair = isUnfairAux([0], [0]) .
+  ceq isUnfairAux([I], [J]) =
+    isUnfairPair([I], [J]) \/ isUnfairAux([I], [s(J)])
+    if I < # /\ J < # .
+  ceq isUnfairAux([I], [J]) =
+    isUnfairAux([s(I)], [0])
+    if I < # /\ J >= # .
+  ceq isUnfairAux([I], [J]) = False if I >= # .
+  eq isUnfairPair(M, N) = isUnfairPre(M, N) /\ (isQueued(M) U inCritSec(N)) .
   eq < M : Node | mode : Queued, A >
      < N : Node | mode : Idle, B > C
     |= isUnfairPre(M, N) = true .

test-node-preds.maude

@@ -19,6 +19,5 @@ red modelCheck(init, <>[]~ hasUnsentMessages) .
 --- Expected: true
 
 --- 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))) .
+red modelCheck(init, [] ~ isUnfair) .
 --- Expected: true