Add explicit.PredecessorRelation class for computing / storing predecessor relation of models. [from Joachim Klein]

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10191 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/explicit/PredecessorRelation.java

@@ -0,0 +1,195 @@
+//==============================================================================
+//	
+//	Copyright (c) 2014-
+//	Authors:
+//	* 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.ArrayList;
+import java.util.BitSet;
+import java.util.Iterator;
+import java.util.List;
+import java.util.Stack;
+
+import prism.PrismComponent;
+import common.IterableBitSet;
+
+/**
+ * A class for storing and accessing the predecessor relation of an explicit Model.
+ * <p>
+ * As Model only provide easy access to successors of states,
+ * the predecessor relation is computed and stored for subsequent efficient access.
+ * <p>
+ * Note: Naturally, if the model changes, the predecessor relation
+ * has to be recomputed to remain accurate.
+ */
+public class PredecessorRelation
+{
+	/**
+	 * pre[i] provides the list of predecessors of state with index i.
+	 */
+	List<ArrayList<Integer>> pre;
+
+	/**
+	 * Constructor. Computes the predecessor relation for the given model
+	 * by considering the successors of each state.
+	 *
+	 * @param model the Model
+	 */
+	public PredecessorRelation(Model model)
+	{
+		pre = new ArrayList<ArrayList<Integer>>(model.getNumStates());
+		// construct the (empty) array list for all states
+		for (int s = 0; s < model.getNumStates(); s++) {
+			pre.add(s, new ArrayList<Integer>());
+		}
+
+		compute(model);
+	}
+
+	/** Compute the predecessor relation using getSuccessorsIterator. */
+	private void compute(Model model)
+	{
+		int n = model.getNumStates();
+
+		for (int s = 0; s < n; s++) {
+			Iterator<Integer> it = model.getSuccessorsIterator(s);
+			while (it.hasNext()) {
+				Integer successor = it.next();
+
+				// Add the current state s to pre[successor].
+				//
+				// As getSuccessorsIterator guarantees that
+				// there are no duplicates in the successors,
+				// s will be added to successor exactly once.
+				pre.get(successor).add(s);
+			}
+		}
+	}
+
+	/**
+	 * Get an Iterable over the predecessor states of {@code s}.
+	 */
+	public Iterable<Integer> getPre(int s)
+	{
+		return pre.get(s);
+	}
+
+	/**
+	 * Get an Iterator over the predecessor states of {@code s}.
+	 */
+	public Iterator<Integer> getPredecessorsIterator(int s)
+	{
+		return pre.get(s).iterator();
+	}
+
+	/**
+	 * Static constructor to compute the predecessor relation for the given model.
+	 * Logs diagnostic information to the log of the given PrismComponent.
+	 *
+	 * @param parent a PrismComponent (for obtaining the log and settings)
+	 * @param model the model for which the predecessor relation should be computed
+	 * @returns the predecessor relation
+	 **/
+	public static PredecessorRelation forModel(PrismComponent parent, Model model)
+	{
+		long timer = System.currentTimeMillis();
+		
+		parent.getLog().print("Calculating predecessor relation for "+model.getModelType().fullName()+"...  ");
+		parent.getLog().flush();
+
+		PredecessorRelation pre = new PredecessorRelation(model);
+		
+		timer = System.currentTimeMillis() - timer;
+		parent.getLog().println("done (" + timer / 1000.0 + " seconds)");
+
+		return pre;
+	}
+
+
+	/**
+	 * Computes the set Pre*(target) via a DFS, i.e., all states that
+	 * are in {@code target} or can reach {@code target} via one or more transitions
+	 * from states contained in {@code remain}.
+	 * <br/>
+	 * If the parameter {@code remain} is {@code null}, then
+	 * {@code remain} is considered to include all states in the model.
+	 * <br/>
+	 * If the parameter {@code absorbing} is not {@code null},
+	 * then the states in {@code absorbing} are considered to be absorbing,
+	 * i.e., to have a single self-loop, disregarding other outgoing edges.
+
+	 * @param remain restriction on the states that may occur
+	 *               on the path to target, {@code null} = all states
+	 * @param target The set of target states
+	 * @param absorbing (optional) set of states that should be considered to be absorbing,
+	 *               i.e., their outgoing edges are ignored, {@code null} = no states
+	 * @return the set of states Pre*(target)
+	 */
+	public BitSet calculatePreStar(BitSet remain, BitSet target, BitSet absorbing)
+	{
+		BitSet result;
+
+		// all target states are in Pre*
+		result = (BitSet)target.clone();
+
+		// the stack of states whose predecessors have to be considered
+		Stack<Integer> todo = new Stack<Integer>();
+
+		// initial todo: all the target states
+		for (Integer s : IterableBitSet.getSetBits(target)) {
+			todo.add(s);
+		};
+
+		// the set of states that are finished
+		BitSet done = new BitSet();
+
+		while (!todo.isEmpty()) {
+			int s = todo.pop();
+			// already considered?
+			if (done.get(s)) continue;
+
+			done.set(s);
+
+			// for each predecessor in the graph
+			for (int p : getPre(s)) {
+				if (absorbing != null && absorbing.get(p)) {
+					// predecessor is absorbing, thus the edge is considered to not exist
+					continue;
+				}
+				if (remain == null || remain.get(p)) {
+					// can reach result (and is in remain)
+					result.set(p);
+					if (!done.get(p)) {
+						// add to stack
+						todo.add(p);
+					}
+				}
+			}
+		}
+
+		return result;
+	}
+
+}