From 79c9bb91fbdce0661c0483109cc2d352eca41292 Mon Sep 17 00:00:00 2001
From: Justin Loew <jloloew@gmail.com>
Date: Fri, 23 Mar 2018 16:17:32 -0500
Subject: [PATCH] Add check for fairness which passes but maybe shouldn't be
passing
---
node-preds.maude | 16 ++++++++++------
test-node-preds.maude | 3 +--
2 files changed, 11 insertions(+), 8 deletions(-)
diff --git a/node-preds.maude b/node-preds.maude
index 891c252..0167031 100644
--- a/node-preds.maude
+++ b/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 .
diff --git a/test-node-preds.maude b/test-node-preds.maude
index 25d330e..17917ed 100644
--- a/test-node-preds.maude
+++ b/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
--
GitLab