code: //==============================================================================
  //	
  //	Copyright (c) 2002-
  //	Authors:
  //	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of 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 pta;
  
  import java.util.*;
  
  import explicit.*;
  import prism.*;
  
  /**
   * Class to store a forwards reachability graph for a PTA.
   */
  public class ReachabilityGraph
  {
  	// PTA
  	PTA pta;
  	// List of symbolic states (Z)
  	List<LocZone> states;
  	// List of symbolic transitions (grouped by source location)
  	// (thus source is not stored explicitly in the symbolic transition)
  	ArrayList<ArrayList<SymbolicTransition>> trans;
  
  	/**
  	 * Construct empty reachability graph.
  	 * @param pta PTA associated with this graph.
  	 */
  	public ReachabilityGraph(PTA pta)
  	{
  		this.pta = pta;
  		states = null;
  		trans = new ArrayList<ArrayList<SymbolicTransition>>();
  	}
  
  	public void addState()
  	{
  		trans.add(new ArrayList<SymbolicTransition>());
  	}
  
  	public void copyState(int i)
  	{
  		ArrayList<SymbolicTransition> listOld, listNew;
  		listOld = trans.get(i);
  		listNew = new ArrayList<SymbolicTransition>(listOld.size());
  		for (SymbolicTransition g : listOld)
  			listNew.add(new SymbolicTransition(g));
  		trans.add(listNew);
  	}
  
  	/**
  	 * Add a new symbolic transition to the graph.
  	 * @param src Source state index
  	 * @param tr Corresponding transition in the PTA
  	 * @param dests List of destinations
  	 * @param valid Validity condition (usually left null and computed later)
  	 */
  	public void addTransition(int src, Transition tr, int dests[], Zone valid)
  	{
  		trans.get(src).add(new SymbolicTransition(tr, dests, valid));
  	}
  
  	/**
  	 * Returns true if state s2 is a successor of state s1
  	 * (i.e. if there is a symbolic transition with s1 as source and s2 in destinations).
  	 */
  	public boolean isSuccessor(int s1, int s2)
  	{
  		for (SymbolicTransition st : trans.get(s1)) {
  			if (st.hasSuccessor(s2))
  				return true;
  		}
  		return false;
  	}
  
  	/**
  	 * Compute the validity conditions for all symbolic transitions in the graph.
  	 */
  	public void computeAllValidities()
  	{
  		int i, n;
  		ArrayList<SymbolicTransition> list;
  		n = trans.size();
  		for (i = 0; i < n; i++) {
  			list = trans.get(i);
  			for (SymbolicTransition st : list) {
  				st.valid = computeValidity(i, st.tr, st.dests);
  			}
  		}
  	}
  
  	/**
  	 * Print the list of symbolic states to a log.
  	 */
  	public void printStates(PrismLog log)
  	{
  		int i = 0;
  		for (LocZone lz : states) {
  			if (i > 0)
  				log.print(" ");
  			log.print("#" + (i++) + ":" + lz);
  		}
  	}
  	
  	@Override
  	public String toString()
  	{
  		int i, n;
  		boolean first;
  		String s = "";
  		n = trans.size();
  		first = true;
  		s = "[ ";
  		for (i = 0; i < n; i++) {
  			if (first)
  				first = false;
  			else
  				s += ", ";
  			s += i + ":" + trans.get(i);
  		}
  		s += " ]";
  		return s;
  	}
  
  	/**
  	 * Compute the validity condition for a symbolic transition
  	 * @param src The index of the source state of the symbolic transition 
  	 * @param tr The PTA transition corresponding to the symbolic transition
  	 * @param dests The list of destination state indices of the symbolic transition
  	 */
  	public Zone computeValidity(int src, Transition tr, int[] dests)
  	{
  		Zone z = new DBMList(DBM.createTrue(pta));
  		int count = 0;
  		for (Edge edge : tr.getEdges()) {
  			LocZone lz2 = states.get(dests[count]).deepCopy();
  			lz2.dPre(edge);
  			z.intersect(lz2.zone);
  			count++;
  		}
  		z.down();
  		z.intersect(states.get(src).zone);
  
  		return z;
  	}
  	
  	/**
  	 * Build an MDP from this forwards reachability graph.
  	 * The set of initial states should also be specified.
  	 */
  	public MDP buildMDP(List<Integer> initialStates) throws PrismException
  	{
  		Distribution distr;
  		int numStates, src, count, dest;
  		MDPSimple mdp;
  
  		// Building MDP...
  		mdp = new MDPSimple();
  
  		// Add all states
  		mdp.addStates(states.size());
  
  		// For each symbolic state...
  		numStates = states.size(); 
  		for (src = 0; src < numStates; src++) {
  			// And for each outgoing transition in PTA...
  			for (SymbolicTransition st : trans.get(src)) {
  				distr = new Distribution();
  				count = -1;
  				for (Edge edge : st.tr.getEdges()) {
  					count++;
  					dest = st.dests[count];
  					distr.add(dest, edge.getProbability());
  				}
  				if (!distr.isEmpty())
  					mdp.addChoice(src, distr);
  			}
  		}
  
  		// Set initial states
  		for (int i : initialStates) {
  			mdp.addInitialState(i);
  		}
  
  		return mdp;
  	}
  }
  