From 817cc3d06d432a883185b4a19e62b7373a36ad6b Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Wed, 9 Mar 2016 12:30:01 +0000 Subject: [PATCH] symbolic LTLModelChecker: add missing treatment for MDP-Rabin MEC computations with -fair and more than one Rabin pair Previously, in case that -fair was active and there were multiple Rabin pairs, fairness was silently not taken into account. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11241 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/LTLModelChecker.java | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index 58c2af6b..42074698 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -795,6 +795,31 @@ public class LTLModelChecker extends PrismComponent acceptanceVector_L_not = statesLnot.get(i); acceptanceVector_K = statesK.get(i); for (JDDNode ec : allecs) { + if (fairness) { + // The goal states in this EC, have to be visited infinitely often + JDDNode goal = JDD.And(ec.copy(), acceptanceVector_K.copy()); + // The safe states in this EC, only they may be visited + JDDNode safeStates = JDD.And(ec.copy(), acceptanceVector_L_not.copy()); + + // Compute the backward set for goal in this EC + JDDNode ecEdges = model.getTransReln().copy(); + // we only care about the outgoing edges of safe states + ecEdges = JDD.And(ecEdges, safeStates.copy()); + JDDNode canReachGoal = backwardSet(model, goal, ecEdges); + + // The good states are those that are safe and can reach goal + JDDNode goodStates = JDD.And(safeStates, canReachGoal); + + // Find accepting states under fairness: + // Those states in goodStates where *all* outgoing transitions + // remain in goodStates, forever. + acceptingStates = findFairECs(model, goodStates); + + allAcceptingStates = JDD.Or(allAcceptingStates, acceptingStates); + + // look at next EC + continue; + } // build bdd of accepting states (under L_i) in the product model List ecs; JDD.Ref(ec);