prism-accumulation/prism/src/pta/Transition.java

//==============================================================================
//	
//	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;

public class Transition
{
	// Parent PTA
	private PTA parent;
	// Source location
	private int src;
	// Action label ("" = tau)
	private String action;
	// Guard - currently a conjunction of constraints
	private Set<Constraint> guard;
	// Edges
	private int numEdges;
	private ArrayList<Edge> edges;

	/**
	 * Create an empty transition.
	 * @param parent Parent PTA
	 * @param src Source location index
	 * @param action Synchronising action ("" if none)
	 */
	public Transition(PTA parent, int src, String action)
	{
		this.parent = parent;
		this.src = src;
		this.action = action;
		guard = new LinkedHashSet<Constraint>();
		numEdges = 0;
		edges = new ArrayList<Edge>();
	}

	/**
	 * Copy constructor.
	 */
	public Transition(Transition tr)
	{
		this(tr.parent, tr.src, tr.action);
		for (Constraint c : tr.guard) {
			addGuardConstraint(new Constraint(c));
		}
		for (Edge e : tr.edges) {
			addEdge(new Edge(e));
		}
	}
	
	public void addGuardConstraint(Constraint c)
	{
		guard.add(c);
		parent.recomputeMaxClockConstraint(c);
	}

	public Edge addEdge(double prob, int dest)
	{
		Edge e = new Edge(this, prob, dest);
		edges.add(e);
		numEdges++;
		return e;
	}

	public void addEdge(Edge e)
	{
		e.setParent(this);
		edges.add(e);
		numEdges++;
	}
	
	public void setParent(PTA parent)
	{
		this.parent = parent;
	}

	public PTA getParent()
	{
		return parent;
	}

	public String getAction()
	{
		return action;
	}

	public int getSource()
	{
		return src;
	}

	public Iterable<Constraint> getGuardConstraints()
	{
		return guard;
	}

	public int getNumEdges()
	{
		return edges.size();
	}

	public List<Edge> getEdges()
	{
		return edges;
	}

	/**
	 * Perform some basic syntactic checks.
	 */
	public void check() throws PrismException
	{
		// Check edges
		// Also check that  total probability is 1 (ish)
		double prob = 0.0;
		double err = 1e-10;
		for (Edge e : edges) {
			e.check();
			prob += e.getProbability();
		}
		if (prob < 1.0-err || prob > 1.0+err)
			throw new PrismException("Non-1 probability ("+prob+") for PTA transition \""+this+"\"");
	}

	public String toString()
	{
		boolean first;
		String s = "";
		s += parent.getLocationName(src) + " -";
		if (action != null)
			s += action + ":";
		s += Constraint.toStringList(parent, guard);
		s += "-> ";
		first = true;
		for (Edge e : edges) {
			if (first)
				first = false;
			else
				s += " + ";
			s += e;
		}
		return s;
	}

	public void writeToDesFile(Writer out) throws PrismException, IOException
	{
		out.write("\t[\n");
		for (Edge e : edges) {
			e.writeToDesFile(out, ((action == null || "".equals(action)) ? "" : action + "||"), guard);
		}
		out.write("\t]\n");
	}
}