From 7d5105c8c194c8d224a298ac63d8ccb432fa7846 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 21 Jul 2017 13:43:50 +0000 Subject: [PATCH] explicit.SCCInfo, SCCComputer: method for obtaining topological ordering (SCCInfo) An SCCInfo provides IntSet-based access to the various SCCs. This storage option can be more efficient than to store BitSets for each individual SCC, in particular if trivial SCCs are not filtered and there are lots of states. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12112 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/SCCComputer.java | 34 ++++ prism/src/explicit/SCCInfo.java | 242 ++++++++++++++++++++++++++++ 2 files changed, 276 insertions(+) create mode 100644 prism/src/explicit/SCCInfo.java diff --git a/prism/src/explicit/SCCComputer.java b/prism/src/explicit/SCCComputer.java index 54953fc9..fc379c55 100644 --- a/prism/src/explicit/SCCComputer.java +++ b/prism/src/explicit/SCCComputer.java @@ -65,6 +65,40 @@ public abstract class SCCComputer extends PrismComponent return new SCCComputerTarjan(parent, model, consumer); } + /** + * Compute an SCCInfo data structure (topological ordering). + * @param parent PrismComponent (for settings) + * @param model the model + * @param withTrivialSCCs include trivial SCCs? + */ + public static SCCInfo computeTopologicalOrdering(PrismComponent parent, Model model, boolean withTrivialSCCs) throws PrismException + { + return computeTopologicalOrdering(parent, model, withTrivialSCCs, null); + } + + /** + * Compute an SCCInfo data structure (topological ordering). + *
+ * If {@code restrict != null}, restricts the underlying graph to only those states s + * for which {@code restrict.test(s)} evaluates to true ("relevant states"). + * Edges to non-relevant states are ignored and the non-relevant + * states are not considered as potential initial states. + * @param parent PrismComponent (for settings) + * @param model the model + * @param withTrivialSCCs include trivial SCCs? + * @param restrict predicate that indicates that a state is relevant ({@code null}: all states are relevant) + */ + public static SCCInfo computeTopologicalOrdering(PrismComponent parent, Model model, boolean withTrivialSCCs, IntPredicate restrict) throws PrismException + { + SCCInfo sccs = new SCCInfo(model.getNumStates()); + SCCComputer sccComputer = SCCComputer.createSCCComputer(parent, model, sccs); + // Compute SCCInfo, including trivial SCCs in the subgraph obtained when only considering + // states in unknown + sccComputer.computeSCCs(!withTrivialSCCs, restrict); + + return sccs; + } + /** * Base constructor. */ diff --git a/prism/src/explicit/SCCInfo.java b/prism/src/explicit/SCCInfo.java new file mode 100644 index 00000000..c3001423 --- /dev/null +++ b/prism/src/explicit/SCCInfo.java @@ -0,0 +1,242 @@ +//============================================================================== +// +// 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.Arrays; +import java.util.PrimitiveIterator.OfInt; + +import common.IntSet; +import prism.PrismLog; + +/** + * Storage of the SCC information, with a topological order of the SCCs. + *
+ * Provides IntSet-based access to the states in the SCCs. + */ +public class SCCInfo implements SCCConsumer +{ + /** The number of states in the model */ + private int numStates; + /** List of state indizes, in order of SCC membership */ + private int[] stateList; + /** Index into stateList: sccEnd[i] points to the last state in the SCC */ + private int[] sccEnd; + /** Mapping from state index to the SCC index */ + private int[] stateToSCCIndex; + /** Number of SCCs that are stored */ + private int storedSCCCount; + /** Number of states that are stored */ + private int storedStateCount; + + /** + * Constructor. + * + * @param numStates number of states in the model (used for allocating data structures) + */ + public SCCInfo(int numStates) { + this.numStates = numStates; + stateList = new int[numStates]; + sccEnd = new int[numStates]; + stateToSCCIndex = new int[numStates]; + Arrays.fill(stateToSCCIndex, -1); + storedSCCCount = 0; + storedStateCount = 0; + } + + /** SCCConsumer interface: Notification about start of SCC */ + @Override + public void notifyStartSCC() + { + } + + /** SCCConsumer interface: Notification about end of SCC */ + public void notifyEndSCC() + { + // store index of last state of SCC + int curSCC = storedSCCCount; + sccEnd[curSCC] = storedStateCount - 1; + storedSCCCount++; + } + + /** SCCConsumer interface: Notification about state in SCC */ + public void notifyStateInSCC(int stateIndex) + { + int curSCC = storedSCCCount; + stateList[storedStateCount] = stateIndex; + stateToSCCIndex[stateIndex] = curSCC; + storedStateCount++; + } + + /** Returns the number of SCCs */ + public int getNumSCCs() + { + return storedSCCCount; + } + + /** Compute and return the number of SCCs with at least 2 states. */ + public int countNonSingletonSCCs() + { + int nonSingletonSCCs = 0; + for (int i = 0; i < getNumSCCs(); i++) { + if (!isSingletonSCC(i)) { + nonSingletonSCCs++; + } + } + return nonSingletonSCCs; + } + + /** Returns the number of states in the SCC with index {@code sccIndex} */ + public int getNumStatesInSCC(int sccIndex) + { + checkSCCIndex(sccIndex); + return endOfSCC(sccIndex) - startOfSCC(sccIndex) + 1; + } + + /** Returns true if the given SCC is a singleton SCC */ + public boolean isSingletonSCC(int sccIndex) + { + checkSCCIndex(sccIndex); + return getNumStatesInSCC(sccIndex) == 1; + } + + /** + * Returns the index of the SCC containing the given state, + * or -1 if the state does not belong to an SCC. + */ + public int getSCCIndex(int stateIndex) + { + checkStateIndex(stateIndex); + return stateToSCCIndex[stateIndex]; + } + + /** Returns an IntSet for the states in the given SCC */ + public IntSet getStatesForSCC(final int sccIndex) + { + checkSCCIndex(sccIndex); + + final int start = startOfSCC(sccIndex); + final int end = endOfSCC(sccIndex); + + return new IntSet() { + + @Override + public OfInt iterator() + { + return new OfInt() { + int cur = start; + + @Override + public boolean hasNext() + { + return cur <= end; + } + + @Override + public int nextInt() + { + return stateList[cur++]; + } + }; + } + + @Override + public OfInt reversedIterator() + { + return new OfInt() { + int cur = end; + + @Override + public boolean hasNext() + { + return cur >= start; + } + + @Override + public int nextInt() + { + return stateList[cur--]; + } + }; + } + + @Override + public int cardinality() + { + return getNumStatesInSCC(sccIndex); + } + + @Override + public boolean contains(int stateIndex) + { + int sccForState = getSCCIndex(stateIndex); + return sccForState == sccIndex; + } + }; + } + + /** Prints the SCC info to the log */ + public void print(PrismLog log) + { + for (int scc = 0; scc < getNumSCCs(); scc++) { + log.println("SCC " + scc + " (" + getNumStatesInSCC(scc) + "):"); + for (OfInt states = getStatesForSCC(scc).iterator(); states.hasNext();) { + int state = states.nextInt(); + log.print(" "); + log.print(state); + } + log.println(); + } + } + + private void checkStateIndex(int stateIndex) + { + if (stateIndex < 0 || stateIndex >= numStates) + throw new IllegalArgumentException("SCCInfo: State index " + stateIndex + " is out of range"); + } + + private void checkSCCIndex(int sccIndex) + { + if (sccIndex < 0 || sccIndex >= storedSCCCount) + throw new IllegalArgumentException("SCCInfo: SCC index " + sccIndex + " is out of range"); + } + + /** Compute the index in stateList of the first state in the given SCC */ + private int startOfSCC(int sccIndex) + { + if (sccIndex == 0) { + return 0; + } else { + return sccEnd[sccIndex - 1] + 1; + } + } + + /** Compute the index in stateList of the last state in the given SCC */ + private int endOfSCC(int sccIndex) + { + return sccEnd[sccIndex]; + } +}