prism-accumulation/prism/src/explicit/PredecessorRelation.java

//==============================================================================
//	
//	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 getPre(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;
	}

}