From 389e2ba1d3d8a83ea344ef17fe4f3fc6dfd4c942 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 24 Jul 2013 19:23:29 +0000 Subject: [PATCH] Some tidying/refactoring of symbolic MEC generation. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7155 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/ECComputer.java | 3 +- prism/src/prism/ECComputerDefault.java | 101 ++++++++++++++++++------- 2 files changed, 76 insertions(+), 28 deletions(-) diff --git a/prism/src/prism/ECComputer.java b/prism/src/prism/ECComputer.java index e63cca56..00418986 100644 --- a/prism/src/prism/ECComputer.java +++ b/prism/src/prism/ECComputer.java @@ -29,7 +29,6 @@ package prism; import java.util.List; -import java.util.Vector; import jdd.JDDNode; import jdd.JDDVars; @@ -52,7 +51,7 @@ public abstract class ECComputer extends PrismComponent protected JDDVars allDDNondetVars; // stuff for ECs - protected Vector mecs; + protected List mecs; /** * Static method to create a new ECComputer object, depending on current settings. diff --git a/prism/src/prism/ECComputerDefault.java b/prism/src/prism/ECComputerDefault.java index d7c04498..af699832 100644 --- a/prism/src/prism/ECComputerDefault.java +++ b/prism/src/prism/ECComputerDefault.java @@ -37,8 +37,9 @@ import jdd.JDDNode; import jdd.JDDVars; /** - * Symbolic maximal end component computer for a nondeterministic model such as MDP. + * Symbolic maximal end component computer for a nondeterministic model such as an MDP. */ +@SuppressWarnings("unused") public class ECComputerDefault extends ECComputer { /** @@ -78,21 +79,26 @@ public class ECComputerDefault extends ECComputer * (If {@code filter} is null, the acceptance condition is trivially satisfied.) * @param states BDD of the set of containing states * @param filter BDD for the set of accepting states - * @return a vector of (referenced) BDDs representing the ECs + * @return a list of (referenced) BDDs representing the MECs */ - private Vector findEndComponents(JDDNode states, JDDNode filter) throws PrismException + private List findEndComponents(JDDNode states, JDDNode filter) throws PrismException { + Vector mecs = new Vector(); + SCCComputer sccComputer; + + // Initial set of candidates for MECs just contains the whole set we are searching Stack candidates = new Stack(); JDD.Ref(states); candidates.push(states); - Vector ecs = new Vector(); - SCCComputer sccComputer; + // Go through each candidate set while (!candidates.isEmpty()) { JDDNode candidate = candidates.pop(); - // Compute the stable set + + // Compute its maximal stable set JDD.Ref(candidate); JDDNode stableSet = findMaximalStableSet(candidate); + // Drop empty sets if (stableSet.equals(JDD.ZERO)) { JDD.Deref(stableSet); @@ -101,7 +107,7 @@ public class ECComputerDefault extends ECComputer } if (stableSet.equals(candidate) && JDD.GetNumMinterms(stableSet, allDDRowVars.n()) == 1) { - ecs.add(candidate); + mecs.add(candidate); JDD.Deref(stableSet); continue; } @@ -110,8 +116,7 @@ public class ECComputerDefault extends ECComputer JDD.Ref(stableSet); JDDNode stableSetTrans = maxStableSetTrans(stableSet); - // now find the maximal SCCs in (stableSet, stableSetTrans) - List sccs; + // Find the maximal SCCs in (stableSet, stableSetTrans) sccComputer = SCCComputer.createSCCComputer(this, stableSet, stableSetTrans, allDDRowVars, allDDColVars); if (filter != null) sccComputer.computeSCCs(filter); @@ -119,29 +124,74 @@ public class ECComputerDefault extends ECComputer sccComputer.computeSCCs(); JDD.Deref(stableSet); JDD.Deref(stableSetTrans); - sccs = sccComputer.getSCCs(); + List sccs = sccComputer.getSCCs(); JDD.Deref(sccComputer.getNotInSCCs()); - if (sccs.size() > 0) { - if (sccs.size() > 1 || !sccs.get(0).equals(candidate)) { - candidates.addAll(sccs); - JDD.Deref(candidate); - } else { - ecs.add(candidate); - JDD.Deref(sccs.get(0)); - } - } else - JDD.Deref(candidate); + + // If there are no SCCs, do nothing + if (sccs.size() == 0) { + } + // If the whole sub-MDP is one SCC, we found an MEC + else if (sccs.size() == 1 && sccs.get(0).equals(candidate)) { + mecs.add(sccs.get(0)); + } + // Otherwise add SCCs as candidates and proceed + else { + candidates.addAll(sccs); + } + JDD.Deref(candidate); } - return ecs; + return mecs; } /** - * Returns a stable set of states contained in candidateStates - * - * @param candidateStates set of candidate states S x H_i (dereferenced after calling this function) - * @return a referenced BDD with the maximal stable set in c + * Returns the maximal stable set of states contained in {@code candidateStates}, + * i.e. the maximal subset of states which have a choice whose transitions remain in the subset. + * @param candidateStates BDD for a set of states (over allDDRowVars) (dereferenced after calling this function) + * @return A referenced BDD with the maximal stable set in c */ private JDDNode findMaximalStableSet(JDDNode candidateStates) + { + // Store two copies to allow check for fixed point + JDDNode current = candidateStates; + JDDNode old = JDD.Constant(0); + // Fixed point + while (!current.equals(old)) { + // Remember last set + JDD.Deref(old); + JDD.Ref(current); + old = current; + // Find transitions starting in current + JDD.Ref(trans01); + JDD.Ref(current); + JDDNode currTrans = JDD.Apply(JDD.TIMES, trans01, current); + // Find transitions starting in current *and* ending in current + current = JDD.PermuteVariables(current, allDDRowVars, allDDColVars); + JDD.Ref(currTrans); + JDDNode currTrans2 = JDD.Apply(JDD.TIMES, currTrans, current); + // Find transitions leaving current + JDD.Ref(currTrans2); + currTrans = JDD.And(currTrans, JDD.Not(currTrans2)); + // Find choices leaving current + currTrans = JDD.ThereExists(currTrans, allDDColVars); + // Remove leaving choices + currTrans2 = JDD.ThereExists(currTrans2, allDDColVars); + currTrans2 = JDD.And(currTrans2, JDD.Not(currTrans)); + // Keep states with at least one choice + current = JDD.ThereExists(currTrans2, allDDNondetVars); + } + JDD.Deref(old); + return current; + } + + /** + * Returns the maximal stable set of states contained in {@code candidateStates}, + * i.e. the maximal subset of states which have a choice whose transitions remain in the subset. + * @param candidateStates BDD for a set of states (over allDDRowVars) (dereferenced after calling this function) + * @return A referenced BDD with the maximal stable set in c + * + * Old version of the code (uses probability sum, which shouldn't be needed). + */ + private JDDNode findMaximalStableSetOld(JDDNode candidateStates) { JDDNode old = JDD.Constant(0); JDDNode current = candidateStates; @@ -168,7 +218,6 @@ public class ECComputerDefault extends ECComputer } JDD.Deref(old); return current; - } /**