prism-accumulation/prism/src/simulator/TransitionList.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 simulator;

import java.util.*;

import parser.*;
import prism.*;

public class TransitionList
{
	private ArrayList<Choice> choices = new ArrayList<Choice>();
	private ArrayList<Integer> transitionIndices = new ArrayList<Integer>();
	private ArrayList<Integer> transitionOffsets = new ArrayList<Integer>();
	private int numChoices = 0;
	private int numTransitions = 0;
	private double probSum = 0.0;

	// TODO: document this
	public class Ref
	{
		public int i;
		public int offset;
		//int index;
		//Choice ch;
	}

	public void clear()
	{
		choices.clear();
		transitionIndices.clear();
		transitionOffsets.clear();
		numChoices = 0;
		numTransitions = 0;
		probSum = 0.0;
	}

	public void add(Choice tr)
	{
		int i, n;
		choices.add(tr);
		n = tr.size();
		for (i = 0; i < n; i++) {
			transitionIndices.add(choices.size() - 1);
			transitionOffsets.add(i);
		}
		numChoices++;
		numTransitions += tr.size();
		probSum += tr.getProbabilitySum();
	}
	
	/**
	 * Check the validity of the available transitions for a given model type.
	 * Throw a PrismExecption if an error is found.
	 */
	public void checkValid(ModelType modelType) throws PrismException
	{
		for (Choice ch : choices) {
			ch.checkValid(modelType);
		}
	}
	
	// ACCESSORS

	/**
	 * Get the number of choices.
	 */
	public int getNumChoices()
	{
		return numChoices;
	}

	/**
	 * Get the number of transitions.
	 */
	public int getNumTransitions()
	{
		return numTransitions;
	}

	/**
	 * Get the total sum of all probabilities (or rates).
	 */
	public double getProbabilitySum()
	{
		return probSum;
	}

	// Get access to Choice objects 

	/**
	 * Get the ith choice.
	 */
	public Choice getChoice(int i)
	{
		return choices.get(i);
	}

	/**
	 * Get the choice containing a transition of a given index.
	 */
	public Choice getChoiceOfTransition(int index)
	{
		return choices.get(transitionIndices.get(index));
	}

	// Get index/offset info

	/**
	 * Get the index of the choice containing a transition of a given index.
	 */
	public int getChoiceIndexOfTransition(int index)
	{
		return transitionIndices.get(index);
	}

	/**
	 * Get the offset of a transition within its containing choice.
	 */
	public int getChoiceOffsetOfTransition(int index)
	{
		return transitionOffsets.get(index);
	}

	/**
	 * Get the (total) index of a transition from the index of its containing choice and its offset within it.
	 */
	public int getTotalIndexOfTransition(int i, int offset)
	{
		return transitionOffsets.get(i);
	}

	// Random selection of a choice 

	/**
	 * Get a reference to a transition according to a total probability (rate) sum, x.
	 * i.e.the first transition for which the sum of probabilities of all prior transitions
	 * (across all choices) exceeds x.
	 * Note: this only really makes sense for models where these are rates, rather than probabilities.
	 * @param x Probability (or rate) sum
	 * @param ref Empty transition reference to store result
	 */
	public void getChoiceIndexByProbabilitySum(double x, Ref ref)
	{
		int i;
		Choice choice;
		double d = 0.0, tot = 0.0;
		// Add up choice prob/rate sums to find choice
		for (i = 0; x >= tot && i < numChoices; i++) {
			d = getChoice(i).getProbabilitySum();
			tot += d;
		}
		ref.i = i - 1;
		// Pick transition within choice 
		choice = getChoice(i - 1);
		if (choice.size() > 1) {
			ref.offset = choice.getIndexByProbabilitySum(x - (tot - d));
		} else {
			ref.offset = 0;
		}
	}

	// Direct access to transition info

	/**
	 * Get a string describing the action/module of a transition, specified by its index.
	 */
	public String getTransitionModuleOrAction(int index)
	{
		return getChoiceOfTransition(index).getModuleOrAction();
	}

	/**
	 * Get the probability/rate of a transition, specified by its index.
	 */
	public double getTransitionProbability(int index)
	{
		return getChoiceOfTransition(index).getProbability(transitionOffsets.get(index));
	}

	/**
	 * Get a string describing the updates making up a transition, specified by its index.
	 * This is in abbreviated form, i.e. x'=1, rather than x'=x+1.
	 * Format is: x'=1, y'=0, with empty string for empty update.
	 * Only variables updated are included in list (even if unchanged).
	 */
	public String getTransitionUpdateString(int index, State currentState) throws PrismLangException
	{
		return getChoiceOfTransition(index).getUpdateString(transitionOffsets.get(index), currentState);
	}

	/**
	 * Get a string describing the updates making up a transition, specified by its index.
	 * This is in full, i.e. of the form x'=x+1, rather than x'=1.
	 * Format is: (x'=x+1) & (y'=y-1), with empty string for empty update.
	 * Only variables updated are included in list.
	 * Note that expressions may have been simplified from original model. 
	 */
	public String getTransitionUpdateStringFull(int index)
	{
		return getChoiceOfTransition(index).getUpdateStringFull(transitionOffsets.get(index));
	}

	/**
	 * Get the target of a transition (as a new State object), specified by its index.
	 */
	public State computeTransitionTarget(int index, State currentState) throws PrismLangException
	{
		return getChoiceOfTransition(index).computeTarget(transitionOffsets.get(index), currentState);
	}

	/**
	 * Is there a deadlock (i.e. no available transitions)?
	 */
	public boolean isDeadlock()
	{
		return numChoices == 0;
	}

	/**
	 * Are the choices deterministic? (i.e. a single probability 1.0 transition)
	 */
	public boolean isDeterministic()
	{
		return numTransitions == 1 && getChoice(0).getProbability(0) == 1.0;
	}

	/**
	 * Is there a deterministic self-loop, i.e. do all transitions go to the current state.
	 */
	public boolean isDeterministicSelfLoop(State currentState)
	{
		// TODO: make more efficient, and also limit calls to it
		// (e.g. only if already stayed in state twice?)
		int i, n;
		State newState = new State(currentState);
		try {
			for (Choice ch : choices) {
				n = ch.size();
				for (i = 0; i < n; i++) {
					ch.computeTarget(i, currentState, newState);
					if (!currentState.equals(newState)) {
						// Found a non-loop
						return false;
					}
				}
			}
		} catch (PrismLangException e) {
			// If anything goes wrong when evaluating, just return false.
			return false;
		}
		// All targets loop
		return true;
	}

	@Override
	public String toString()
	{
		String s = "";
		boolean first = true;
		for (Choice ch : choices) {
			if (first)
				first = false;
			else
				s += ", ";
			s += ch.toString();
		}
		return s;
	}
}