diff --git a/prism/src/automata/DASimplifyAcceptance.java b/prism/src/automata/DASimplifyAcceptance.java index 8f386ae7..a9e1b6aa 100644 --- a/prism/src/automata/DASimplifyAcceptance.java +++ b/prism/src/automata/DASimplifyAcceptance.java @@ -4,7 +4,9 @@ import java.util.BitSet; import prism.PrismComponent; import prism.PrismException; +import explicit.LTS; import explicit.SCCComputer; +import explicit.SCCConsumerStore; import acceptance.AcceptanceOmega; import acceptance.AcceptanceRabin; import acceptance.AcceptanceReach; @@ -29,9 +31,11 @@ public class DASimplifyAcceptance if (da.getAcceptance() instanceof AcceptanceRabin) { DA dra = (DA) da; // K_i states that do not occur in a (non-trivial) SCC of the DRA may as well be removed - SCCComputer sccComp = explicit.SCCComputer.createSCCComputer(parent, new LTSFromDA(da)); - sccComp.computeBSCCs(); - BitSet trivial = sccComp.getNotInSCCs(); + LTS lts = new LTSFromDA(da); + SCCConsumerStore sccStore = new SCCConsumerStore(); + SCCComputer sccComp = explicit.SCCComputer.createSCCComputer(parent, lts, sccStore); + sccComp.computeSCCs(); + BitSet trivial = sccStore.getNotInSCCs(); for (RabinPair pair : dra.getAcceptance()) { if (pair.getK().intersects(trivial)) { pair.getK().andNot(trivial); diff --git a/prism/src/automata/LTL2WDBA.java b/prism/src/automata/LTL2WDBA.java index 8290a9ec..371805c8 100644 --- a/prism/src/automata/LTL2WDBA.java +++ b/prism/src/automata/LTL2WDBA.java @@ -53,6 +53,7 @@ import explicit.LTS; import explicit.LTSExplicit; import explicit.NonProbModelChecker; import explicit.SCCComputer; +import explicit.SCCConsumerStore; /** *

@@ -316,9 +317,10 @@ public class LTL2WDBA extends PrismComponent { LTS daLTS = new LTSFromDA(P.da); - SCCComputer sccComputer = SCCComputer.createSCCComputer(this, daLTS); + SCCConsumerStore sccStore = new SCCConsumerStore(); + SCCComputer sccComputer = SCCComputer.createSCCComputer(this, daLTS, sccStore); sccComputer.computeSCCs(); - for (BitSet scc : sccComputer.getSCCs()) { + for (BitSet scc : sccStore.getSCCs()) { if (hasAcceptingCycle(P, scc)) { // mark all SCC states as final in powerset automaton P.F.or(scc); @@ -364,9 +366,10 @@ public class LTL2WDBA extends PrismComponent // perform cycle check // TODO: use nested-DFS? boolean hasCycleViaF = false; - SCCComputer sccComputer = SCCComputer.createSCCComputer(this, buchilts.lts); + SCCConsumerStore sccStore = new SCCConsumerStore(); + SCCComputer sccComputer = SCCComputer.createSCCComputer(this, buchilts.lts, sccStore); sccComputer.computeSCCs(); - for (BitSet subSCC : sccComputer.getSCCs()) { + for (BitSet subSCC : sccStore.getSCCs()) { if (subSCC.intersects(buchilts.F)) { hasCycleViaF = true; break; diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 7d8e6604..2a465706 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -354,9 +354,10 @@ public class DTMCModelChecker extends ProbModelChecker mainLog.println("\nStarting total reward computation..."); // Compute bottom strongly connected components (BSCCs) - SCCComputer sccComputer = SCCComputer.createSCCComputer(this, dtmc); - sccComputer.computeBSCCs(); - List bsccs = sccComputer.getBSCCs(); + SCCConsumerStore sccStore = new SCCConsumerStore(); + SCCComputer sccComputer = SCCComputer.createSCCComputer(this, dtmc, sccStore); + sccComputer.computeSCCs(); + List bsccs = sccStore.getBSCCs(); numBSCCs = bsccs.size(); // Find BSCCs with non-zero reward @@ -1478,10 +1479,11 @@ public class DTMCModelChecker extends ProbModelChecker solnProbs = new double[n]; // Compute bottom strongly connected components (BSCCs) - SCCComputer sccComputer = SCCComputer.createSCCComputer(this, dtmc); - sccComputer.computeBSCCs(); - List bsccs = sccComputer.getBSCCs(); - BitSet notInBSCCs = sccComputer.getNotInBSCCs(); + SCCConsumerStore sccStore = new SCCConsumerStore(); + SCCComputer sccComputer = SCCComputer.createSCCComputer(this, dtmc, sccStore); + sccComputer.computeSCCs(); + List bsccs = sccStore.getBSCCs(); + BitSet notInBSCCs = sccStore.getNotInBSCCs(); numBSCCs = bsccs.size(); // See which states in the initial distribution do *not* have non-zero prob @@ -1569,10 +1571,11 @@ public class DTMCModelChecker extends ProbModelChecker n = dtmc.getNumStates(); // Compute bottom strongly connected components (BSCCs) - SCCComputer sccComputer = SCCComputer.createSCCComputer(this, dtmc); - sccComputer.computeBSCCs(); - List bsccs = sccComputer.getBSCCs(); - BitSet notInBSCCs = sccComputer.getNotInBSCCs(); + SCCConsumerStore sccStore = new SCCConsumerStore(); + SCCComputer sccComputer = SCCComputer.createSCCComputer(this, dtmc, sccStore); + sccComputer.computeSCCs(); + List bsccs = sccStore.getBSCCs(); + BitSet notInBSCCs = sccStore.getNotInBSCCs(); numBSCCs = bsccs.size(); // Compute steady-state probability for each BSCC... diff --git a/prism/src/explicit/ECComputerDefault.java b/prism/src/explicit/ECComputerDefault.java index 020ebbc4..63b0ce29 100644 --- a/prism/src/explicit/ECComputerDefault.java +++ b/prism/src/explicit/ECComputerDefault.java @@ -195,9 +195,10 @@ public class ECComputerDefault extends ECComputer private List computeSCCs(NondetModel model) throws PrismException { - SCCComputer sccc = SCCComputer.createSCCComputer(this, model); + SCCConsumerStore sccs = new SCCConsumerStore(); + SCCComputer sccc = SCCComputer.createSCCComputer(this, model, sccs); sccc.computeSCCs(); - return sccc.getSCCs(); + return sccs.getSCCs(); } private List translateStates(SubNondetModel model, List sccs) diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java index 13122255..4d6a5333 100644 --- a/prism/src/explicit/LTLModelChecker.java +++ b/prism/src/explicit/LTLModelChecker.java @@ -651,9 +651,10 @@ public class LTLModelChecker extends PrismComponent public BitSet findAcceptingBSCCs(Model model, AcceptanceOmega acceptance) throws PrismException { // Compute bottom strongly connected components (BSCCs) - SCCComputer sccComputer = SCCComputer.createSCCComputer(this, model); - sccComputer.computeBSCCs(); - List bsccs = sccComputer.getBSCCs(); + SCCConsumerStore sccStore = new SCCConsumerStore(); + SCCComputer sccComputer = SCCComputer.createSCCComputer(this, model, sccStore); + sccComputer.computeSCCs(); + List bsccs = sccStore.getBSCCs(); BitSet result = new BitSet(); diff --git a/prism/src/explicit/NonProbModelChecker.java b/prism/src/explicit/NonProbModelChecker.java index f571b2be..7ee9d96d 100644 --- a/prism/src/explicit/NonProbModelChecker.java +++ b/prism/src/explicit/NonProbModelChecker.java @@ -504,7 +504,8 @@ public class NonProbModelChecker extends StateModelChecker mainLog.print("Searching for non-trivial, accepting SCCs in product LTS..."); mainLog.flush(); - SCCComputer sccComputer = SCCComputer.createSCCComputer(this, product.getProductModel()); + SCCConsumerStore sccConsumerStore = new SCCConsumerStore(); + SCCComputer sccComputer = SCCComputer.createSCCComputer(this, product.getProductModel(), sccConsumerStore); sccComputer.computeSCCs(); // We determine the SCCs that intersect F, as those are guaranteed to @@ -513,7 +514,7 @@ public class NonProbModelChecker extends StateModelChecker int accepting = 0; int sccs = 0; BitSet acceptingSCCs = new BitSet(); - for (BitSet scc : sccComputer.getSCCs()) { + for (BitSet scc : sccConsumerStore.getSCCs()) { sccs++; if (scc.intersects(product.getAcceptingStates())) { acceptingSCCs.or(scc); diff --git a/prism/src/explicit/SCCComputer.java b/prism/src/explicit/SCCComputer.java index cc1d4f56..b3090341 100644 --- a/prism/src/explicit/SCCComputer.java +++ b/prism/src/explicit/SCCComputer.java @@ -4,6 +4,7 @@ // Authors: // * Christian von Essen (Verimag, Grenoble) // * Dave Parker (University of Birmingham/Oxford) +// * Joachim Klein (TU Dresden) // //------------------------------------------------------------------------------ // @@ -27,9 +28,6 @@ package explicit; -import java.util.BitSet; -import java.util.List; - import prism.PrismComponent; import prism.PrismException; @@ -39,6 +37,9 @@ import prism.PrismException; */ public abstract class SCCComputer extends PrismComponent { + /** The consumer */ + protected SCCConsumer consumer; + // Method used for finding (B)SCCs public enum SCCMethod { TARJAN; @@ -56,52 +57,45 @@ public abstract class SCCComputer extends PrismComponent /** * Static method to create a new SCCComputer object, depending on current settings. */ - public static SCCComputer createSCCComputer(PrismComponent parent, Model model) throws PrismException + public static SCCComputer createSCCComputer(PrismComponent parent, Model model, SCCConsumer consumer) throws PrismException { // Only one algorithm implemented currently - return new SCCComputerTarjan(parent, model); + return new SCCComputerTarjan(parent, model, consumer); } /** * Base constructor. */ - public SCCComputer(PrismComponent parent) throws PrismException + public SCCComputer(PrismComponent parent, SCCConsumer consumer) throws PrismException { super(parent); + this.consumer = consumer; } /** - * Compute (non-trivial) strongly connected components (SCCs) and store them. - * They should be retrieved using {@link #getSCCs()}. - * States in trivial SCCs (those comprising a single state without a self-loop) are also stored. - * They should be retrieved using {@link #getNotInSCCs()}. - */ - public abstract void computeSCCs(); - - /** - * Get the list of computed (non-trivial) SCCs. - */ - public abstract List getSCCs(); - - /** - * Get the states not in any (non-trivial) SCC. - * In other words, this is all states in trivial SCCs (those comprising a single state without a self-loop). + * Compute strongly connected components (SCCs) and notify the consumer. + * This will only report non-trivial SCCs */ - public abstract BitSet getNotInSCCs(); + public void computeSCCs() throws PrismException + { + computeSCCs(true); + } /** - * Compute bottom strongly connected components (BSCCs) and store them. - * They can be retrieved using {@link #getBSCCs()} and {@link #getNotInBSCCs()}. + * Compute strongly connected components (SCCs) and notify the consumer. + * Ignores trivial SCCS if {@code filterTrivialSCCs} is set to true. */ - public abstract void computeBSCCs(); + public abstract void computeSCCs(boolean filterTrivialSCCs) throws PrismException; /** - * Get the list of computed BSCCs. + * Returns true if {@code state}, assumed to be an SCC, is a trivial SCC, + * i.e., has no self lopp. + * @param model the model + * @param state the state index */ - public abstract List getBSCCs(); - - /** - * Get the states not in any BSCC. - */ - public abstract BitSet getNotInBSCCs(); + protected boolean isTrivialSCC(Model model, int state) + { + // false if there is a self-loop, i.e., a successor t == state + return !(model.someSuccessorsMatch(state, (t) -> {return t == state;})); + } } diff --git a/prism/src/explicit/SCCComputerTarjan.java b/prism/src/explicit/SCCComputerTarjan.java index 193bdb1b..afa62cf1 100644 --- a/prism/src/explicit/SCCComputerTarjan.java +++ b/prism/src/explicit/SCCComputerTarjan.java @@ -44,14 +44,6 @@ public class SCCComputerTarjan extends SCCComputer private Model model; /* Number of nodes (model states) */ private int numNodes; - /* Computed list of SCCs */ - private List sccs = new ArrayList(); - /* States not in non-trivial SCCs */ - private BitSet notInSCCs; - /* Computed list of BSCCs */ - private List bsccs = new ArrayList(); - /* States not in any BSCC */ - private BitSet notInBSCCs; /* Next index to give to a node */ private int index = 0; @@ -61,13 +53,15 @@ public class SCCComputerTarjan extends SCCComputer private ArrayList nodeList; /* Nodes currently on the stack. */ private BitSet onStack; + /** Should we filter trivial SCCs? */ + private boolean filterTrivialSCCs; /** * Build (B)SCC computer for a given model. */ - public SCCComputerTarjan(PrismComponent parent, Model model) throws PrismException + public SCCComputerTarjan(PrismComponent parent, Model model, SCCConsumer consumer) throws PrismException { - super(parent); + super(parent, consumer); this.model = model; this.numNodes = model.getNumStates(); this.nodeList = new ArrayList(numNodes); @@ -80,76 +74,21 @@ public class SCCComputerTarjan extends SCCComputer // Methods for SCCComputer interface @Override - public void computeSCCs() + public void computeSCCs(boolean filterTrivialSCCs) throws PrismException { + this.filterTrivialSCCs = filterTrivialSCCs; + consumer.notifyStart(model); tarjan(); - // Now remove trivial SCCs - notInSCCs = new BitSet(); - for (Iterator it = sccs.iterator(); it.hasNext(); ) { - BitSet scc = it.next(); - if (scc.cardinality() == 1) { - int s = scc.nextSetBit(0); - if (!model.someSuccessorsInSet(s, scc)) { - it.remove(); // remove this SCC from sccs list - notInSCCs.set(s); - } - } - } - } - - @Override - public void computeBSCCs() - { - computeSCCs(); - notInBSCCs = (BitSet) getNotInSCCs().clone(); - int n = sccs.size(); - for (int i = 0; i < n; i++) { - BitSet scc = sccs.get(i); - boolean bottom = true; - for (int s = scc.nextSetBit(0); s >= 0; s = scc.nextSetBit(s + 1)) { - if (!model.allSuccessorsInSet(s, scc)) { - bottom = false; - break; - } - } - if (bottom) - bsccs.add(scc); - else - notInBSCCs.or(scc); - } - } - - @Override - public List getSCCs() - { - return sccs; + consumer.notifyDone(); } - @Override - public BitSet getNotInSCCs() - { - return notInSCCs; - } - - @Override - public List getBSCCs() - { - return bsccs; - } - - @Override - public BitSet getNotInBSCCs() - { - return notInBSCCs; - } - // SCC Computation /** * Execute Tarjan's algorithm. Determine maximal strongly connected components * (SCCS) for the graph of the model and stored in {@code sccs}. */ - public void tarjan() + public void tarjan() throws PrismException { for (int i = 0; i < numNodes; i++) { if (nodeList.get(i).lowlink == -1) @@ -158,7 +97,7 @@ public class SCCComputerTarjan extends SCCComputer } - private void tarjan(int i) + private void tarjan(int i) throws PrismException { final Node v = nodeList.get(i); v.index = index; @@ -166,9 +105,17 @@ public class SCCComputerTarjan extends SCCComputer index++; stack.add(0, i); onStack.set(i); + + boolean hadSelfloop = false; SuccessorsIterator it = model.getSuccessors(i); while (it.hasNext()) { int e = it.nextInt(); + + if (e == i) { + hadSelfloop = true; + continue; + } + Node n = nodeList.get(e); if (n.index == -1) { tarjan(e); @@ -178,14 +125,24 @@ public class SCCComputerTarjan extends SCCComputer } } if (v.lowlink == v.index) { + // this is a singleton SCC if the top of the stack equals i + boolean singletonSCC = (stack.get(0) == i); + if (singletonSCC && filterTrivialSCCs) { + if (!hadSelfloop) { // singleton SCC & no selfloop -> trivial + stack.remove(0); + onStack.set(i, false); + return; + } + } + int n; - BitSet component = new BitSet(); + consumer.notifyStartSCC(); do { n = stack.remove(0); onStack.set(n, false); - component.set(n); + consumer.notifyStateInSCC(n); } while (n != i); - sccs.add(component); + consumer.notifyEndSCC(); } } diff --git a/prism/src/explicit/SCCConsumer.java b/prism/src/explicit/SCCConsumer.java new file mode 100644 index 00000000..62588ec8 --- /dev/null +++ b/prism/src/explicit/SCCConsumer.java @@ -0,0 +1,69 @@ +//============================================================================== +// +// Copyright (c) 2016- +// Authors: +// * Joachim Klein (TU Dresden) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package explicit; + +import prism.PrismException; + +/** + * Interface for a consumer of SCC information, for use with an {@code SCCComputer}. + * When a new SCC is discovered, first {@code notifyStartSCC()} will be called. + * Subsequently, for each state of the SCC, {@code notifyStateInSCC()} will be called. + * When all states of the SCC have been notified, {@code notifyEndSCC()} will be called. + * When the whole SCC computation is finished, {@code notifyDone()} will be called once. + */ +public interface SCCConsumer { + /** + * Call-back function, will be called once at the start. + * Default implementation: Ignore. + */ + public default void notifyStart(Model model) + { + // ignore + } + + /** + * Call-back function, will be called when a new SCC is discovered. + **/ + public void notifyStartSCC() throws PrismException; + + /** + * Call-back function, will be called once for each state in the SCC. + */ + public void notifyStateInSCC(int stateIndex) throws PrismException; + + /** + * Call-back function, will be called when all states of the SCC have been + * discovered. + **/ + public void notifyEndSCC() throws PrismException; + + /** + * Call-back function. Will be called after SCC computation is complete. + */ + public default void notifyDone() {} + +} diff --git a/prism/src/explicit/SCCConsumerBSCCs.java b/prism/src/explicit/SCCConsumerBSCCs.java new file mode 100644 index 00000000..453832c1 --- /dev/null +++ b/prism/src/explicit/SCCConsumerBSCCs.java @@ -0,0 +1,77 @@ +//============================================================================== +// +// Copyright (c) 2014- +// Authors: +// * Joachim Klein (TU Dresden) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package explicit; + +import java.util.BitSet; + +import prism.PrismComponent; +import prism.PrismException; + +/** + * Abstract base class for an SCC consumer that is only interested in + * the bottom strongly-connected components (BSCCs).
+ * + * Intercepts the {@code notifyNextSCC()} call, checks whether the SCC + * is a BSCC and calls {@code notifyNextBSCC()} if that is the case. + */ +public abstract class SCCConsumerBSCCs extends SCCConsumerBitSet { + + protected Model model; + + /** Constructor */ + public SCCConsumerBSCCs() + { + model = null; // will be set by notifyStart call + } + + public void notifyStart(Model model) + { + this.model = model; + } + + /** + * Call-back function. Called upon discovery of a BSCC. + */ + public abstract void notifyNextBSCC(BitSet bscc) throws PrismException; + + @Override + public void notifyNextSCC(BitSet scc) throws PrismException + { + boolean bottom = true; + // BSCC <=> for all states s, all successors are again in the SCC. + for (int s = scc.nextSetBit(0); s >= 0; s = scc.nextSetBit(s + 1)) { + if (!model.allSuccessorsInSet(s, scc)) { + bottom = false; + break; + } + } + + if (bottom) { + notifyNextBSCC(scc); + } + } +} diff --git a/prism/src/explicit/SCCConsumerBitSet.java b/prism/src/explicit/SCCConsumerBitSet.java new file mode 100644 index 00000000..89a3ee82 --- /dev/null +++ b/prism/src/explicit/SCCConsumerBitSet.java @@ -0,0 +1,94 @@ +//============================================================================== +// +// Copyright (c) 2016- +// Authors: +// * Joachim Klein (TU Dresden) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package explicit; + +import java.util.BitSet; + +import prism.PrismException; + +/** + * Abstract base class for a consumer of SCC information, for use with an {@code SCCComputer}, + * where each SCC is stored as a BitSet. + *
+ * When a new SCC is discovered, {@code notifyNextSCC()} will be called with a {@code BitSet} of the + * states in the SCC. When the SCC computation is finished, {@code notifyDone()} will be + * called once. + *
+ * By default, for each SCC a fresh BitSet is created. If the BitSets that are + * passed to {@code notifyNextSCC} can be reused for the next call, the {@code reuseBitSet} + * flag can be set in the constructor. + */ +public abstract class SCCConsumerBitSet implements SCCConsumer +{ + private BitSet curSCC = null; + private boolean reuseBitSet = false; + + /** Default constructor. Don't reuse the BitSets */ + public SCCConsumerBitSet() + { + this(false); + } + + /** + * Constructor. If {@code reuseBitSet} is set, reuse the same BitSet for all + * calls to {@code notifyNextSCC}. + * @param reuseBitSet allow reuse of BitSets + */ + public SCCConsumerBitSet(boolean reuseBitSet) + { + this.reuseBitSet = reuseBitSet; + if (reuseBitSet) + curSCC = new BitSet(); + } + + @Override + public void notifyStartSCC() throws PrismException + { + if (reuseBitSet) { + curSCC.clear(); + } else { + curSCC = new BitSet(); + } + } + + @Override + public void notifyStateInSCC(int stateIndex) throws PrismException + { + curSCC.set(stateIndex); + } + + @Override + public void notifyEndSCC() throws PrismException + { + notifyNextSCC(curSCC); + if (!reuseBitSet) { + curSCC = null; + } + } + + public abstract void notifyNextSCC(BitSet scc) throws PrismException; +} diff --git a/prism/src/explicit/SCCConsumerStore.java b/prism/src/explicit/SCCConsumerStore.java new file mode 100644 index 00000000..04de6b8f --- /dev/null +++ b/prism/src/explicit/SCCConsumerStore.java @@ -0,0 +1,162 @@ +//============================================================================== +// +// Copyright (c) 2014- +// Authors: +// * Joachim Klein (TU Dresden) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package explicit; + +import java.util.ArrayList; +import java.util.BitSet; +import java.util.List; + +/** + * SCC consumer that stores lists of the discovered SCCs and BSCCs. + * The list of BSCCs is computed on demand from the list of SCCs. + */ +public class SCCConsumerStore extends SCCConsumerBitSet { + /* Computed list of SCCs */ + private List sccs = new ArrayList(); + /* Computed list of BSCCs */ + private List bsccs; + /* States not in any BSCC */ + private BitSet notInBSCCs; + /* States not in any SCC */ + private BitSet notInSCCs; + + /** Is the SCC computation finished? */ + private boolean finished = false; + + private Model model; + + /** Constructor */ + public SCCConsumerStore() + { + model = null; // will be set by notifyStart call + } + + @Override + public void notifyStart(Model model) + { + this.model = model; + } + + @Override + public void notifyNextSCC(BitSet scc) + { + sccs.add(scc); + } + + @Override + public void notifyDone() + { + finished = true; + } + + /** + * Get a list of the SCCs. Can only be called once the SCC computation is finished. + */ + public List getSCCs() + { + if (!finished) + throw new UnsupportedOperationException("SCC computation is not yet finished."); + + return sccs; + } + + /** + * Get a list of the BSCCs. Can only be called once the SCC computation is finished. + */ + public List getBSCCs() + { + if (!finished) + throw new UnsupportedOperationException("SCC computation is not yet finished."); + + // If we don't have the list of BSCCs already, compute it. + if (bsccs == null) { + computeBSCCs(); + } + return bsccs; + } + + /** + * Get the set of states not in any BSCCs. Can only be called once the SCC computation is finished. + */ + public BitSet getNotInBSCCs() + { + if (!finished) + throw new UnsupportedOperationException("SCC computation is not yet finished."); + + // If we don't have the set already, compute it. + if (notInBSCCs == null) { + computeBSCCs(); + } + return notInBSCCs; + } + + /** + * Compute the list of BSCCs from the list of SCCs. + */ + private void computeBSCCs() + { + if (!finished) + throw new UnsupportedOperationException("SCC computation is not yet finished."); + + bsccs = new ArrayList(); + notInBSCCs = (BitSet) getNotInSCCs().clone(); + for (BitSet scc : sccs) { + boolean bottom = true; + // BSCC <=> for all states s, all successors are again in SCC + for (int s = scc.nextSetBit(0); s >= 0; s = scc.nextSetBit(s + 1)) { + if (!model.allSuccessorsInSet(s, scc)) { + bottom = false; + break; + } + } + if (bottom) + // store SCC as a BSCC + bsccs.add(scc); + else + // add states in scc to notInBSCCs + notInBSCCs.or(scc); + } + } + + public BitSet getNotInSCCs() + { + if (!finished) + throw new UnsupportedOperationException("SCC computation is not yet finished."); + + if (notInSCCs != null) { + return notInSCCs; + } + BitSet result = new BitSet(); + for (BitSet scc : getSCCs()) { + result.or(scc); + } + result.flip(0, model.getNumStates()); + notInSCCs = result; + return notInSCCs; + } + +} diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index d9402477..8396c24b 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -1095,10 +1095,11 @@ public class Prism extends PrismComponent implements PrismSettingsListener /** * Get an SCCComputer object for the explicit engine. + * @param consumer the SCCConsumer */ - public explicit.SCCComputer getExplicitSCCComputer(explicit.Model model) throws PrismException + public explicit.SCCComputer getExplicitSCCComputer(explicit.Model model, explicit.SCCConsumer consumer) throws PrismException { - return explicit.SCCComputer.createSCCComputer(this, model); + return explicit.SCCComputer.createSCCComputer(this, model, consumer); } /** @@ -2454,7 +2455,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener long l; // timer PrismLog tmpLog; SCCComputer sccComputer = null; - explicit.SCCComputer sccComputerExpl = null; + explicit.SCCConsumerStore sccConsumerExpl = null; //Vector bsccs; //JDDNode not, bscc; @@ -2475,8 +2476,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener sccComputer = getSCCComputer(currentModel); sccComputer.computeBSCCs(); } else { - sccComputerExpl = getExplicitSCCComputer(currentModelExpl); - sccComputerExpl.computeBSCCs(); + sccConsumerExpl = new explicit.SCCConsumerStore(); + getExplicitSCCComputer(currentModelExpl, sccConsumerExpl).computeSCCs(); } l = System.currentTimeMillis() - l; mainLog.println("\nTime for BSCC computation: " + l / 1000.0 + " seconds."); @@ -2504,7 +2505,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener if (!getExplicit()) { n = sccComputer.getBSCCs().size(); } else { - n = sccComputerExpl.getBSCCs().size(); + n = sccConsumerExpl.getBSCCs().size(); } for (i = 0; i < n; i++) { tmpLog.println(); @@ -2520,8 +2521,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener new StateListMTBDD(sccComputer.getBSCCs().get(i), currentModel).printMatlab(tmpLog); JDD.Deref(sccComputer.getBSCCs().get(i)); } else { - explicit.StateValues.createFromBitSet(sccComputerExpl.getBSCCs().get(i), currentModelExpl).print(tmpLog, true, exportType == EXPORT_MATLAB, - true, true); + explicit.StateValues.createFromBitSet(sccConsumerExpl.getBSCCs().get(i), currentModelExpl).print(tmpLog, true, exportType == EXPORT_MATLAB, true, true); } if (exportType == EXPORT_MATLAB) tmpLog.println("];"); @@ -2640,7 +2640,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener long l; // timer PrismLog tmpLog; SCCComputer sccComputer = null; - explicit.SCCComputer sccComputerExpl = null; + explicit.SCCConsumerStore sccConsumerExpl = null; // no specific states format for MRMC if (exportType == EXPORT_MRMC) @@ -2659,8 +2659,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener sccComputer = getSCCComputer(currentModel); sccComputer.computeSCCs(); } else { - sccComputerExpl = getExplicitSCCComputer(currentModelExpl); - sccComputerExpl.computeSCCs(); + sccConsumerExpl = new explicit.SCCConsumerStore(); + getExplicitSCCComputer(currentModelExpl, sccConsumerExpl).computeSCCs(); } l = System.currentTimeMillis() - l; mainLog.println("\nTime for SCC computation: " + l / 1000.0 + " seconds."); @@ -2688,7 +2688,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener if (!getExplicit()) { n = sccComputer.getSCCs().size(); } else { - n = sccComputerExpl.getSCCs().size(); + n = sccConsumerExpl.getSCCs().size(); } for (i = 0; i < n; i++) { tmpLog.println(); @@ -2704,8 +2704,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener new StateListMTBDD(sccComputer.getSCCs().get(i), currentModel).printMatlab(tmpLog); JDD.Deref(sccComputer.getSCCs().get(i)); } else { - explicit.StateValues.createFromBitSet(sccComputerExpl.getSCCs().get(i), currentModelExpl).print(tmpLog, true, exportType == EXPORT_MATLAB, - true, true); + explicit.StateValues.createFromBitSet(sccConsumerExpl.getSCCs().get(i), currentModelExpl).print(tmpLog, true, exportType == EXPORT_MATLAB, true, true); } if (exportType == EXPORT_MATLAB) tmpLog.println("];");