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.io.*;
  import java.util.*;
  
  import prism.PrismException;
  import prism.PrismLangException;
  import parser.*;
  import pta.parser.PTAParser;
  
  public class PTA
  {
  	// Info about clocks
  	// Note: from an external point of view, clocks are indexed from 1
  	// (to allow use of index 0 for the zero clock)
  	protected int numClocks;
  	protected ArrayList<String> clockNames;
  	// Locations info
  	protected int numLocations;
  	protected ArrayList<Object> locationNames;
  	protected ArrayList<LinkedHashSet<Constraint>> invariants;
  	protected List<String> locationNameVars;
  	// Transitions
  	protected int numTransitions;
  	protected ArrayList<ArrayList<Transition>> transitions;
  	// Alphabet
  	protected List<String> alphabet;
  	// Maximum clock constraint value
  	protected int cMax;
  
  	/**
  	 * Constructor: build an empty PTA.
  	 * 
  	 * @param alphabet The set of (non-tau) actions that can label transitions.
  	 * This is *syntactically* defined, e.g., in PRISM it's the list of all actions appearing in commands,
  	 * but may be a strict superset of the actions that actually label transitions.
  	 */
  	public PTA(List<String> alphabet)
  	{
  		numClocks = 0;
  		clockNames = new ArrayList<String>();
  		numLocations = 0;
  		locationNames = new ArrayList<Object>();
  		invariants = new ArrayList<LinkedHashSet<Constraint>>();
  		locationNameVars = null;
  		numTransitions = 0;
  		transitions = new ArrayList<ArrayList<Transition>>();
  		this.alphabet = alphabet;
  		cMax = 0;
  	}
  
  	// Setters
  
  	public int addClock(String name)
  	{
  		numClocks++;
  		clockNames.add(name);
  		// Note: returned index starts from 1, not 0
  		return numClocks;
  	}
  
  	public int getOrAddClock(String name)
  	{
  		int i = clockNames.indexOf(name);
  		if (i == -1) {
  			return addClock(name);
  		} else
  			return i + 1;
  	}
  
  	public int addLocation()
  	{
  		return addLocation(null);
  	}
  
  	public int addLocation(Object name)
  	{
  		numLocations++;
  		locationNames.add(name == null ? "L" + (numLocations - 1) : name);
  		invariants.add(new LinkedHashSet<Constraint>());
  		transitions.add(new ArrayList<Transition>());
  		return numLocations - 1;
  	}
  
  	public int getOrAddLocation(Object name)
  	{
  		int i = locationNames.indexOf(name);
  		if (i == -1) {
  			return addLocation(name);
  		} else
  			return i;
  	}
  
  	public void addInvariantCondition(int loc, Constraint c)
  	{
  		invariants.get(loc).add(c);
  		recomputeMaxClockConstraint(c);
  	}
  
  	public void setInvariantConditions(int loc, LinkedHashSet<Constraint> cs)
  	{
  		invariants.set(loc, cs);
  		recomputeMaxClockConstraint(cs);
  	}
  
  	/**
  	 * Add a new "tau" transition (no action label) to the PTA.
  	 * @param loc Source location of the new transition.  
  	 */
  	public Transition addTransition(int loc)
  	{
  		return addTransition(loc, null);
  	}
  
  	/**
  	 * Add a new transition to the PTA.
  	 * @param loc Source location of the new transition.  
  	 * @param action Action label for the transition  
  	 */
  	public Transition addTransition(int loc, String action)
  	{
  		if (action == null)
  			action = "";
  		Transition transition = new Transition(this, loc, action);
  		ArrayList<Transition> list = transitions.get(loc);
  		list.add(transition);
  		numTransitions++;
  		return transition;
  	}
  
  	/**
  	 * Add a previously created transition to the PTA.
  	 */
  	public void addTransition(Transition transition)
  	{
  		transition.setParent(this);
  		ArrayList<Transition> list = transitions.get(transition.getSource());
  		list.add(transition);
  		numTransitions++;
  	}
  
  	public void removeTransition(int loc, Transition transition)
  	{
  		ArrayList<Transition> list = transitions.get(loc);
  		if (list.remove(transition))
  			numTransitions--;
  	}
  
  	public int recomputeMaxClockConstraint(Constraint c)
  	{
  		cMax = Math.max(cMax, Math.abs(DB.getSignedDiff(c.db)));
  		return cMax;
  	}
  
  	public int recomputeMaxClockConstraint(Iterable<Constraint> cs)
  	{
  		for (Constraint c : cs)
  			recomputeMaxClockConstraint(c);
  		return cMax;
  	}
  
  	public void setLocationNameVars(List<String> locationNameVars)
  	{
  		this.locationNameVars = locationNameVars;
  	}
  	
  	// Getters
  
  	public int getNumClocks()
  	{
  		return numClocks;
  	}
  
  	public String getClockName(int x)
  	{
  		if (x == 0)
  			return "0";
  		return clockNames.get(x - 1);
  	}
  
  	/**
  	 * Return index (starting from 1) of a clock, or -1 if non-existent 
  	 */
  	public int getClockIndex(String name)
  	{
  		int i = clockNames.indexOf(name);
  		return i == -1 ? -1 : i + 1;
  	}
  
  	public Object getLocationName(int loc)
  	{
  		return locationNames.get(loc);
  	}
  
  	public Object getLocationNameString(int loc)
  	{
  		Object name = locationNames.get(loc);
  		if (name instanceof State && locationNameVars != null)
  			return ((State)name).toString(locationNameVars);
  		else
  			return name.toString();
  	}
  
  	public List<Object> getLocationNameList()
  	{
  		return locationNames;
  	}
  
  	public int getLocationIndex(Object name)
  	{
  		return locationNames.indexOf(name);
  	}
  
  	public int getNumLocations()
  	{
  		return numLocations;
  	}
  
  	public Iterable<Constraint> getInvariantConstraints(int loc)
  	{
  		return invariants.get(loc);
  	}
  
  	public List<Transition> getTransitions(int loc)
  	{
  		return transitions.get(loc);
  	}
  
  	public Iterable<Transition> getTransitionsByAction(final int loc, final String action)
  	{
  		return new Iterable<Transition>()
  		{
  			public Iterator<Transition> iterator()
  			{
  				return new TransitionsByActionIterator(loc, action);
  			}
  		};
  	}
  
  	public int getMaxClockConstraint()
  	{
  		return cMax;
  	}
  
  	public List<String> getAlphabet()
  	{
  		return alphabet;
  	}
  
  	public boolean isActionInAlphabet(String action)
  	{
  		return alphabet.contains(action);
  	}
  
  	/**
  	 * Perform some basic syntactic checks.
  	 */
  	public void check() throws PrismException
  	{
  		for (int i = 0; i < numLocations; i++) {
  			for (Transition t : getTransitions(i)) {
  				t.check();
  			}
  		}
  	}
  
  	public String infoString()
  	{
  		return numClocks + " clocks, " + numLocations + " locations, " + numTransitions + " transitions";
  	}
  
  	public String toString()
  	{
  		int i;
  		String s = "";
  		s += "PTA: " + numLocations + " locations, " + numTransitions + " transitions\n";
  		s += "  cMax = " + cMax + ", clocks = " + clockNames + "\n";
  		s += "   alphabet = " + alphabet + "\n";
  		for (i = 0; i < numLocations; i++) {
  			s += "Location " + i + " (" + locationNames.get(i) + "):\n";
  			s += "  Invariant: " + Constraint.toStringList(this, invariants.get(i)) + "\n";
  			for (Transition t : getTransitions(i))
  				s += "  " + t + "\n";
  		}
  		return s;
  	}
  
  	public void writeToDesFile(String filename) throws PrismException
  	{
  		int i;
  		try {
  			FileWriter out = new FileWriter(filename);
  			out.write("#no update for variables\n");
  			for (i = 0; i < numLocations; i++) {
  				out.write("#" + i + "\n{\n");
  				if (i == 0)
  					out.write("init\n");
  				out.write("\tnode " + getLocationName(i).toString().replace(':', '_') + "; ");
  				out.write(Constraint.toStringList(this, invariants.get(i)) + "\n");
  				for (Transition t : getTransitions(i))
  					t.writeToDesFile(out);
  				if (transitions.get(i).isEmpty())
  					out.write("\t[\n\t]\n");
  				out.write(i == numLocations - 1 ? "*" : "}");
  				out.write("\n");
  			}
  			out.close();
  		} catch (IOException e) {
  			throw new PrismException("Could not write PTA to file \"" + filename + "\"");
  		}
  	}
  
  	// Static utility methods
  
  	/**
  	 * Combine the names of two PTA locations (e.g. to put in parallel).
  	 */
  	public static Object combineLocationNames(Object name1, Object name2)
  	{
  		// Different strategies depending on the types of Object used for names
  		// Strings: colon-delimited concatenation
  		if (name1 instanceof String && name2 instanceof String) {
  			return name1 + ":" + name2;
  		}
  		// Object arrays: concatenation
  		else if (name1 instanceof Object[] && name2 instanceof Object[]) {
  			Object[] arr1 = (Object[]) name1;
  			Object[] arr2 = (Object[]) name2;
  			Object[] arr = new Object[arr1.length + arr2.length];
  			int i;
  			for (i = 0; i < arr1.length; i++)
  				arr[i] = arr1[i];
  			for (i = 0; i < arr2.length; i++)
  				arr[arr1.length + i] = arr2[i];
  			return arr;
  		}
  		// State objects: concatenation
  		else if (name1 instanceof State && name2 instanceof State) {
  			return new State((State) name1, (State) name2);
  		}
  		// Values objects: union
  		else if (name1 instanceof Values && name2 instanceof Values) {
  			Values vals = new Values((Values) name1);
  			vals.addValues((Values) name2);
  			return vals;
  		}
  		// Default: convert to strings, colon-delimited concatenation
  		return name1 + ":" + name2;
  	}
  
  	/**
  	 * Compute the index (in newPta) of a clock name (from oldPta)
  	 */
  	public static int renameClock(PTA oldPta, PTA newPta, int x)
  	{
  		int xNew = 0;
  		if (x > 0) {
  			xNew = newPta.getClockIndex(oldPta.getClockName(x));
  			if (xNew == -1)
  				System.out.println("Warning: Error renaming clock index " + x);
  		}
  		return xNew;
  	}
  
  	private static PTAParser parser = null;
  
  	/**
  	 * Construct a PTA by reading in a 'des' file
  	 */
  	public static PTA buildPTAFromDesFile(String file)
  	{
  		PTA pta = null;
  		try {
  			if (parser == null)
  				parser = new PTAParser();
  			pta = parser.parsePTA(new FileInputStream(file));
  		} catch (PrismLangException e) {
  			System.out.println("Error in " + file + ": " + e.getMessage() + ".");
  			System.exit(1);
  		} catch (FileNotFoundException e) {
  			System.out.println(e);
  			System.exit(1);
  		}
  		return pta;
  	}
  
  	/**
  	 * Build a simple test PTA.
  	 */
  	public static PTA buildTestPTA()
  	{
  		PTA pta;
  		Transition t;
  		Edge e;
  		pta = new PTA(Collections.emptyList());
  		int x = pta.addClock("x");
  		int y = pta.addClock("y");
  		pta.addLocation(); // L0
  		pta.addLocation(); // L1
  		pta.addLocation(); // L2
  		pta.addLocation(); // L3
  		t = pta.addTransition(0);
  		e = t.addEdge(0.5, 1);
  		e.addReset(x);
  		e = t.addEdge(0.5, 2);
  		t = pta.addTransition(1);
  		t.addGuardConstraint(Constraint.buildLeq(x, 0));
  		t.addGuardConstraint(Constraint.buildLeq(y, 1));
  		t.addGuardConstraint(Constraint.buildGeq(y, 0));
  		e = t.addEdge(1.0, 3);
  		e.addReset(y);
  		t = pta.addTransition(2);
  		t.addGuardConstraint(Constraint.buildLeq(x, 0));
  		t.addGuardConstraint(Constraint.buildLeq(y, 0));
  		e = t.addEdge(1.0, 3);
  		return pta;
  	}
  
  	// Inner class used by getTransitionsByAction
  
  	private class TransitionsByActionIterator implements Iterator<Transition>
  	{
  		private Iterator<Transition> it;
  		private String action;
  		private Transition next;
  
  		private TransitionsByActionIterator(int loc, String action)
  		{
  			it = transitions.get(loc).iterator();
  			this.action = action;
  			computeNext();
  		}
  
  		public boolean hasNext()
  		{
  			return next != null;
  		}
  
  		public Transition next()
  		{
  			if (next == null)
  				throw new NoSuchElementException();
  			Transition tr = next;
  			computeNext();
  			return tr;
  		}
  
  		public void remove()
  		{
  			throw new UnsupportedOperationException();
  		}
  
  		private void computeNext()
  		{
  			next = null;
  			while (it.hasNext()) {
  				Transition tr = it.next();
  				if (tr != null && tr.getAction().equals(action)) {
  					next = tr;
  					break;
  				}
  			}
  		}
  	}
  }
  