From 02af30b8fe3103444f39fc6f6c16c388d48f39fa Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 12 Oct 2018 14:24:35 +0200 Subject: [PATCH] imported patch tmp-tarjan-iterative-2.patch --- .../explicit/SCCComputerTarjanIterative.java | 280 ++++++++++++++++++ 1 file changed, 280 insertions(+) create mode 100644 prism/src/explicit/SCCComputerTarjanIterative.java diff --git a/prism/src/explicit/SCCComputerTarjanIterative.java b/prism/src/explicit/SCCComputerTarjanIterative.java new file mode 100644 index 00000000..23042b49 --- /dev/null +++ b/prism/src/explicit/SCCComputerTarjanIterative.java @@ -0,0 +1,280 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Christian von Essen (Verimag, Grenoble) +// * Dave Parker (University of Birmingham/Oxford) +// * 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.ArrayDeque; +import java.util.Arrays; +import java.util.BitSet; +import java.util.Deque; +import java.util.function.IntPredicate; + +import prism.PrismComponent; +import prism.PrismException; + +/** + * Tarjan's SCC algorithm operating on a Model object, implemented + * without recursion, i.e., using an explicit stack. This allows to + * deal with deep models without exhausting the Java stack. + */ +public class SCCComputerTarjanIterative extends SCCComputer +{ + /* The model to compute (B)SCCs for */ + private Model model; + /* Number of nodes (model states) */ + private int numNodes; + + /* Next index to give to a node */ + private int index = 0; + /* Stack of nodes */ + private Deque stack = new ArrayDeque(); + /* Nodes currently on the stack. */ + private BitSet onStack = new BitSet(); + + /** The lowlink information for the nodes (states) */ + private int[] nodeLowlink; + /** The index information for the nodes (states) */ + private int[] nodeIndex; + + /** The stack for simulating the recursive calls of Tarjan's algorithm */ + private Deque recursionStack = new ArrayDeque<>(); + + /** + * Set to remember those states that had a direct self loop + * (to distinguish between trivial and non-trivial single state SCCs + * if we have to filter the former). + */ + private BitSet statesWithSelfloop; + + /** Should we filter trivial SCCs? */ + private boolean filterTrivialSCCs; + + /** + * (optional) A predicate to restrict the explored state space + * and transition relation to those states that satisfy restrict + */ + private IntPredicate restrict; + + /** + * Build (B)SCC computer for a given model. + */ + public SCCComputerTarjanIterative(PrismComponent parent, Model model, SCCConsumer consumer) throws PrismException + { + super(parent, consumer); + this.model = model; + this.numNodes = model.getNumStates(); + nodeLowlink = new int[numNodes]; + Arrays.fill(nodeLowlink, -1); + nodeIndex = new int[numNodes]; + Arrays.fill(nodeIndex, -1); + } + + // Methods for SCCComputer interface + + @Override + public void computeSCCs(boolean filterTrivialSCCs, IntPredicate restrict) throws PrismException + { + this.filterTrivialSCCs = filterTrivialSCCs; + if (filterTrivialSCCs) + statesWithSelfloop = new BitSet(); + consumer.notifyStart(model); + this.restrict = restrict; + tarjan(); + consumer.notifyDone(); + } + + // SCC Computation + + /** + * Execute Tarjan's algorithm. Determine maximal strongly connected components + * (SCCS) for the graph of the model and report to the consumer. + */ + public void tarjan() throws PrismException + { + for (int i = 0; i < numNodes; i++) { + if (restrict != null && !restrict.test(i)) + continue; // skip state if not one of the relevant states + if (nodeLowlink[i] == -1) { + beginVisit(i); + loop(); + } + } + } + + /** + * Begin the visit to node i. + */ + private void beginVisit(int i) + { + // initialise index and lowindex + nodeIndex[i] = index; + nodeLowlink[i] = index; + index++; + // push on Tarjan stack + stack.push(i); + onStack.set(i); + // push corresponding frame (state and successor iterator) on the recursion stack + recursionStack.push(new StackFrame(i, model.getSuccessors(i))); + } + + /** Main loop, process the recursion stack until empty */ + private void loop() throws PrismException + { + while (!recursionStack.isEmpty()) { + StackFrame frame = recursionStack.peek(); + // the current node + int v = frame.getNode(); + + if (frame.hasPending()) { + // first, finish the visit of the previous edge, if there was one + int w = frame.getPending(); + nodeLowlink[v] = Math.min(nodeLowlink[v], nodeLowlink[w]); + } + + final int w = frame.nextSuccessor(restrict); + if (w != -1) { + if (v == w) { + // a self loop + if (statesWithSelfloop != null) + statesWithSelfloop.set(v); + + // ignore this edge, continue with loop + frame.clearPending(); + continue; + } + + if (nodeIndex[w] == -1) { + // setup visit of successor w, then continue with loop + beginVisit(w); + continue; + } else if (onStack.get(w)) { + // back edge, update lowlink, don't explore successor + nodeLowlink[v] = Math.min(nodeLowlink[v], nodeIndex[w]); + } + // the current edge v->w is not actually explored, + // so we clear the pending successor (w) in the frame + // and continue with the loop + frame.clearPending(); + continue; + } + + // no more successors for this frame, remove from recursion stack + recursionStack.pop(); + + // finished exploring node v, perform necessary steps + if (nodeLowlink[v] == nodeIndex[v]) { + // we have found the root node of an SCC + + // this is a singleton SCC if the top of the stack equals i + boolean singletonSCC = (stack.peek() == v); + if (singletonSCC && filterTrivialSCCs) { + if (!statesWithSelfloop.get(v)) { + // singleton SCC & no selfloop -> trivial + // ignore this SCC and cleanup the Tarjan stack + stack.pop(); + onStack.set(v, false); + continue; + } + } + + int n; + consumer.notifyStartSCC(); + do { + n = stack.pop(); + onStack.set(n, false); + consumer.notifyStateInSCC(n); + } while (n != v); + consumer.notifyEndSCC(); + } + } + } + + /** + * The stack frame with all the information for Tarjan's algorithm + * (current node, successor iterator, currently explored edge). + */ + private static class StackFrame { + /** The current 'from' node */ + int node; + /** The iterator over the successors */ + private SuccessorsIterator it; + /** The successor that is currently explored (-1 = none) */ + private int pending = -1; + + /** Constructor */ + StackFrame(int node, SuccessorsIterator it) { + this.node = node; + this.it = it; + } + + /** Get the current node */ + public int getNode() + { + return node; + } + + /** + * Returns the next successor. If there is none, returns {@code -1}. + * If restrict is non-null, only those successors that satisfy restrict are returned. + */ + public int nextSuccessor(IntPredicate restrict) + { + while (it.hasNext()) { + int i = it.nextInt(); + if (restrict != null && !restrict.test(i)) + // skip + continue; + + pending = i; + return i; + } + return -1; + } + + /** Do we have a successor whose edge is currently explored? */ + public boolean hasPending() + { + return pending != -1; + } + + /** Return (and clear) the current pending successor */ + public int getPending() { + int p = pending; + pending = -1; + return p; + } + + /** Clear the current pending successor */ + public void clearPending() + { + pending = -1; + } + + } + +}