Joachim Klein
7 years ago
1 changed files with 280 additions and 0 deletions
@ -0,0 +1,280 @@ |
|||||
|
//============================================================================== |
||||
|
// |
||||
|
// Copyright (c) 2002- |
||||
|
// Authors: |
||||
|
// * Christian von Essen <christian.vonessen@imag.fr> (Verimag, Grenoble) |
||||
|
// * Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford) |
||||
|
// * Joachim Klein <klein@tcs.inf.tu-dresden.de> (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<Integer> stack = new ArrayDeque<Integer>(); |
||||
|
/* 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<StackFrame> 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; |
||||
|
} |
||||
|
|
||||
|
} |
||||
|
|
||||
|
} |
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue