From 2bf26806e4e984777a514a19b3e0fde54a53146e Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 30 Jul 2013 09:36:30 +0000 Subject: [PATCH] EC generation: comments and refactoring. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7190 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/ECComputer.java | 7 +++-- prism/src/explicit/ECComputerDefault.java | 34 +++++++++++++--------- prism/src/prism/ECComputer.java | 18 ++++++------ prism/src/prism/ECComputerDefault.java | 35 +++++++++++++---------- 4 files changed, 54 insertions(+), 40 deletions(-) diff --git a/prism/src/explicit/ECComputer.java b/prism/src/explicit/ECComputer.java index da590e3c..de4ca04e 100644 --- a/prism/src/explicit/ECComputer.java +++ b/prism/src/explicit/ECComputer.java @@ -62,11 +62,12 @@ public abstract class ECComputer extends PrismComponent public abstract void computeMECStates() throws PrismException; /** - * Compute states of all maximal end components (MECs) contained within {@code states}, and store them. + * Compute states of all maximal end components (MECs) in the submodel obtained + * by restricting this one to the set of states {@code restrict}, and store them. * They can be retrieved using {@link #getMECStates()}. - * @param states BitSet for the set of containing states + * @param restrict BitSet for the set of states to restrict to. */ - public abstract void computeMECStates(BitSet states) throws PrismException; + public abstract void computeMECStates(BitSet restrict) throws PrismException; /** * Get the list of states for computed MECs. diff --git a/prism/src/explicit/ECComputerDefault.java b/prism/src/explicit/ECComputerDefault.java index 54a093cf..581daba1 100644 --- a/prism/src/explicit/ECComputerDefault.java +++ b/prism/src/explicit/ECComputerDefault.java @@ -65,16 +65,13 @@ public class ECComputerDefault extends ECComputer @Override public void computeMECStates() throws PrismException { - // Look within set of all reachable states - BitSet reach = new BitSet(); - reach.set(0, model.getNumStates()); - computeMECStates(reach); + mecs = findEndComponents(null, null); } @Override - public void computeMECStates(BitSet states) throws PrismException + public void computeMECStates(BitSet restrict) throws PrismException { - mecs = findEndComponents(states, null); //TODO + mecs = findEndComponents(restrict, null); } @Override @@ -85,21 +82,30 @@ public class ECComputerDefault extends ECComputer // Computation + // TODO: handle 'accept' + /** - * Find all accepting maximal end components (MECs) contained within {@code states}, - * where acceptance is defined as those which intersect with {@code filter}. - * (If {@code filter} is null, the acceptance condition is trivially satisfied.) - * @param states BitSet for the set of containing states - * @param filter BitSet for the set of accepting states + * Find all accepting maximal end components (MECs) in the submodel obtained + * by restricting this one to the set of states {@code restrict}, + * where acceptance is defined as those which intersect with {@code accept}. + * If {@code restrict} is null, we look at the whole model, not a submodel. + * If {@code accept} is null, the acceptance condition is trivially satisfied. + * @param restrict BitSet for the set of states to restrict to + * @param accept BitSet for the set of accepting states * @return a list of BitSets representing the MECs */ - private List findEndComponents(BitSet states, BitSet filter) throws PrismException + private List findEndComponents(BitSet restrict, BitSet accept) throws PrismException { + // If restrict is null, look within set of all reachable states + if (restrict == null) { + restrict = new BitSet(); + restrict.set(0, model.getNumStates()); + } // Initialise L with set of all states to look in (if non-empty) List L = new ArrayList(); - if (states.cardinality() == 0) + if (restrict.cardinality() == 0) return L; - L.add(states); + L.add(restrict); boolean changed = true; while (changed) { diff --git a/prism/src/prism/ECComputer.java b/prism/src/prism/ECComputer.java index 00418986..a289a45b 100644 --- a/prism/src/prism/ECComputer.java +++ b/prism/src/prism/ECComputer.java @@ -96,22 +96,24 @@ public abstract class ECComputer extends PrismComponent public abstract void computeMECStates() throws PrismException; /** - * Compute states of all maximal end components (MECs) contained within {@code states}, and store them. + * Compute states of all maximal end components (MECs) in the submodel obtained + * by restricting this one to the set of states {@code restrict}, and store them. * They can be retrieved using {@link #getMECStates()}. * You will need to to deref these afterwards. - * @param states BDD of the set of containing states + * @param restrict BDD for the set of states to restrict to */ - public abstract void computeMECStates(JDDNode states) throws PrismException; + public abstract void computeMECStates(JDDNode restrict) throws PrismException; /** - * Compute states of all accepting maximal end components (MECs) contained within {@code states}, and store them, - * where acceptance is defined as those which intersect with {@code filter}. + * Compute states of all maximal end components (MECs) in the submodel obtained + * by restricting this one to the set of states {@code restrict}, and store them, + * where acceptance is defined as those which intersect with {@code accept}. * They can be retrieved using {@link #getMECStates()}. * You will need to to deref these afterwards. - * @param states BDD of the set of containing states - * @param filter BDD for the set of accepting states + * @param restrict BDD for the set of states to restrict to + * @param accept BDD for the set of accepting states */ - public abstract void computeMECStates(JDDNode states, JDDNode filter) throws PrismException; + public abstract void computeMECStates(JDDNode restrict, JDDNode accept) throws PrismException; /** * Get the list of states for computed MECs. diff --git a/prism/src/prism/ECComputerDefault.java b/prism/src/prism/ECComputerDefault.java index af699832..0799ebbd 100644 --- a/prism/src/prism/ECComputerDefault.java +++ b/prism/src/prism/ECComputerDefault.java @@ -56,40 +56,45 @@ public class ECComputerDefault extends ECComputer @Override public void computeMECStates() throws PrismException { - mecs = findEndComponents(reach, null); + mecs = findEndComponents(null, null); } @Override - public void computeMECStates(JDDNode states) throws PrismException + public void computeMECStates(JDDNode restrict) throws PrismException { - mecs = findEndComponents(states, null); + mecs = findEndComponents(restrict, null); } @Override - public void computeMECStates(JDDNode states, JDDNode filter) throws PrismException + public void computeMECStates(JDDNode restrict, JDDNode accept) throws PrismException { - mecs = findEndComponents(states, filter); + mecs = findEndComponents(restrict, accept); } // Computation /** - * Find all accepting maximal end components (MECs) contained within {@code states}, - * where acceptance is defined as those which intersect with {@code filter}. - * (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 + * Find all accepting maximal end components (MECs) in the submodel obtained + * by restricting this one to the set of states {@code restrict}, + * where acceptance is defined as those which intersect with {@code accept}. + * If {@code restrict} is null, we look at the whole model, not a submodel. + * If {@code accept} is null, the acceptance condition is trivially satisfied. + * @param restrict BDD for the set of states to restrict to + * @param accept BDD for the set of accepting states * @return a list of (referenced) BDDs representing the MECs */ - private List findEndComponents(JDDNode states, JDDNode filter) throws PrismException + private List findEndComponents(JDDNode restrict, JDDNode accept) throws PrismException { Vector mecs = new Vector(); SCCComputer sccComputer; // Initial set of candidates for MECs just contains the whole set we are searching + // (which, if null, is all states) + if (restrict == null) + restrict = reach; Stack candidates = new Stack(); - JDD.Ref(states); - candidates.push(states); + JDD.Ref(restrict); + candidates.push(restrict); // Go through each candidate set while (!candidates.isEmpty()) { @@ -118,8 +123,8 @@ public class ECComputerDefault extends ECComputer // Find the maximal SCCs in (stableSet, stableSetTrans) sccComputer = SCCComputer.createSCCComputer(this, stableSet, stableSetTrans, allDDRowVars, allDDColVars); - if (filter != null) - sccComputer.computeSCCs(filter); + if (accept != null) + sccComputer.computeSCCs(accept); else sccComputer.computeSCCs(); JDD.Deref(stableSet);