From 906052cb5b08d2ed4ee0533d93e309ba31f05883 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sat, 16 Jun 2012 21:42:28 +0000 Subject: [PATCH] SCC computation using Tarjan for explicit engine (from Christian von Essen). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5362 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/SCCComputer.java | 79 +++++++++++ prism/src/explicit/SCCComputerTarjan.java | 157 ++++++++++++++++++++++ 2 files changed, 236 insertions(+) create mode 100644 prism/src/explicit/SCCComputer.java create mode 100644 prism/src/explicit/SCCComputerTarjan.java diff --git a/prism/src/explicit/SCCComputer.java b/prism/src/explicit/SCCComputer.java new file mode 100644 index 00000000..62b80b1b --- /dev/null +++ b/prism/src/explicit/SCCComputer.java @@ -0,0 +1,79 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Christian von Essen (Verimag, Grenoble) +// * Dave Parker (University of Birmingham/Oxford) +// +//------------------------------------------------------------------------------ +// +// 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.List; + +/** + * Abstract class for classes that compute (B)SCCs, + * i.e. (bottom) strongly connected components, for a model's transition graph. + */ +public abstract class SCCComputer +{ + // Method used for finding (B)SCCs + public enum SCCMethod { + TARJAN; + public String fullName() + { + switch (this) { + case TARJAN: + return "Tarjan"; + default: + return this.toString(); + } + } + }; + + /** + * Static method to create a new SCCComputer object, depending on requested method. + */ + public static SCCComputer createSCCComputer(SCCMethod sccMethod, Model model) + { + return new SCCComputerTarjan(model); + } + + /** + * Compute SCCs and store them. They can be retrieved using {@link #getSCCs()}. + */ + public abstract void computeSCCs(); + + /** + * Compute SCCs and store them. They can be retrieved using {@link #getBSCCs()}. + */ + public abstract void computeBSCCs(); + + /** + * Get the list of computed SCCs. + */ + public abstract List> getSCCs(); + + /** + * Get the list of computed BSCCs. + */ + public abstract List> getBSCCs(); +} diff --git a/prism/src/explicit/SCCComputerTarjan.java b/prism/src/explicit/SCCComputerTarjan.java new file mode 100644 index 00000000..692a13b7 --- /dev/null +++ b/prism/src/explicit/SCCComputerTarjan.java @@ -0,0 +1,157 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Christian von Essen (Verimag, Grenoble) +// * Dave Parker (University of Birmingham/Oxford) +// +//------------------------------------------------------------------------------ +// +// 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.Iterator; +import java.util.LinkedList; +import java.util.List; + +/** + * Tarjan's SCC algorithm operating on a Model object. + */ +public class SCCComputerTarjan extends SCCComputer +{ + /* The model to compute (B)SCCs for */ + private Model model; + /* Number of nodes (model states) */ + private int numNodes; + /* Computed list of SCCs */ + private List> sccs = new ArrayList>(); + + /* Next index to give to a node */ + private int index = 0; + /* Stack of nodes */ + private List stack = new LinkedList(); + /* List of nodes in the graph. Invariant: {@code nodeList.get(i).id == i} */ + private ArrayList nodeList; + /* True iff node {@code i} currently is on the stack. */ + boolean[] onStack; + + /** + * Build (B)SCC computer for a given model. + */ + public SCCComputerTarjan(Model model) + { + this.model = model; + this.numNodes = model.getNumStates(); + this.nodeList = new ArrayList(numNodes); + for (int i = 0; i < numNodes; i++) { + nodeList.add(new Node(i)); + } + onStack = new boolean[numNodes]; + } + + // Methods for SCCComputer interface + + @Override + public void computeSCCs() + { + tarjan(); + } + + @Override + public void computeBSCCs() + { + throw new UnsupportedOperationException(); + } + + @Override + public List> getSCCs() + { + return sccs; + } + + @Override + public List> getBSCCs() + { + return null; + } + + // 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() + { + for (int i = 0; i < numNodes; i++) { + if (nodeList.get(i).lowlink == -1) + tarjan(i); + } + + } + + private void tarjan(Integer i) + { + final Node v = nodeList.get(i); + v.index = index; + v.lowlink = index; + index++; + stack.add(0, i); + onStack[i] = true; + Iterator it = model.getSuccessorsIterator(i); + while (it.hasNext()) { + Integer e = it.next(); + Node n = nodeList.get(e); + if (n.index == -1) { + tarjan(e); + v.lowlink = Math.min(v.lowlink, n.lowlink); + } else if (onStack[e]) { + v.lowlink = Math.min(v.lowlink, n.index); + } + } + if (v.lowlink == v.index) { + Integer n; + List component = new ArrayList(); + do { + n = stack.remove(0); + onStack[n] = false; + component.add(n); + } while (n != i); + sccs.add(component); + } + } + + /** + * A small class wrapping a node. + * It carries extra information necessary for Tarjan's algorithm. + */ + protected static class Node + { + public int lowlink = -1; + public int index = -1; + public int id; + + public Node(int id) + { + this.id = id; + } + } +}