code: //==============================================================================
  //	
  //	Copyright (c) 2013-
  //	Authors:
  //	* Ernst Moritz Hahn <emhahn@cs.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 param;
  
  import java.io.File;
  import java.util.BitSet;
  import java.util.Iterator;
  import java.util.LinkedList;
  import java.util.Map.Entry;
  import java.util.TreeSet;
  
  import parser.Values;
  import prism.ModelType;
  import prism.PrismException;
  import prism.PrismLog;
  import strat.MDStrategy;
  import explicit.MDPGeneric;
  import explicit.Model;
  import explicit.ModelExplicit;
  import explicit.SuccessorsIterator;
  import explicit.graphviz.Decorator;
  
  /**
   * Represents a parametric Markov model.
   * This class is used to store all types of parametric model, both models
   * with and without nondeterminism, discrete- as well as continuous-time.
   * This turned out the be the most convenient way to implement model checking
   * for parametric models.
   */
  public final class ParamModel extends ModelExplicit implements MDPGeneric<Function>
  {
  	/** total number of nondeterministic choices over all states */
  	private int numTotalChoices;
  	/** total number of probabilistic transitions over all states */
  	private int numTotalTransitions;
  	/** the maximal number of choices per state, over all states */
  	private int numMaxChoices;
  	/** begin and end of state transitions */
  	private int[] rows;
  	/** begin and end of a distribution in a nondeterministic choice */
  	private int[] choices;
  	/** targets of distribution branches */
  	private int[] cols;
  	/** probabilities of distribution branches */
  	private Function[] nonZeros;
  	/** labels - per transition, <i>not</i> per action */
  	private String[] labels;
  	/** total sum of leaving rates for a given nondeterministic choice */
  	private Function[] sumRates;
  	/** model type */
  	private ModelType modelType;
  	/** function factory which manages functions used on transitions, etc. */
  	private FunctionFactory functionFactory;
  
  	/**
  	 * Constructs a new parametric model.
  	 */
  	ParamModel()
  	{
  		numStates = 0;
  		numTotalChoices = 0;
  		numTotalTransitions = 0;
  		initialStates = new LinkedList<Integer>();
  		deadlocks = new TreeSet<Integer>();
  	}
  
  	/**
  	 * Sets the type of the model.
  	 * 
  	 * @param modelType type the model shall have
  	 */
  	void setModelType(ModelType modelType)
  	{
  		this.modelType = modelType;
  	}
  
  	// Accessors (for Model)
  
  	@Override
  	public ModelType getModelType()
  	{
  		return modelType;
  	}
  
  	@Override
  	public Values getConstantValues()
  	{
  		throw new UnsupportedOperationException();
  	}
  
  	@Override
  	public int getNumTransitions()
  	{
  		return numTotalTransitions;
  	}
  
  	@Override
  	public SuccessorsIterator getSuccessors(final int s)
  	{
  		return SuccessorsIterator.chain(new Iterator<SuccessorsIterator>() {
  			private int choice = 0;
  			private int choices = getNumChoices(s);
  
  			@Override
  			public boolean hasNext()
  			{
  				return choice < choices;
  			}
  
  			@Override
  			public SuccessorsIterator next()
  			{
  				return getSuccessors(s, choice++);
  			}
  		});
  	}
  
  	/**
  	 * Get a SuccessorsIterator for state s and choice i.
  	 * @param s The state
  	 * @param i Choice index
  	 */
  	public SuccessorsIterator getSuccessors(int s, int i)
  	{
  		return new SuccessorsIterator()
  		{
  			final int start = choiceBegin(stateBegin(s) + i);
  			int col = start;
  			final int end = choiceBegin(stateBegin(s) + i + 1);
  
  			@Override
  			public boolean hasNext()
  			{
  				return col < end;
  			}
  
  			@Override
  			public int nextInt()
  			{
  				assert (col < end);
  				int i = col;
  				col++;
  				return cols[i];
  			}
  
  			@Override
  			public boolean successorsAreDistinct()
  			{
  				return false;
  			}
  		};
  	}
  	
  	@Override
  	public boolean isSuccessor(int s1, int s2)
  	{
  		for (int choice = stateBegin(s1); choice < stateEnd(s1); choice++) {
  			for (int succ = choiceBegin(choice); succ < choiceEnd(choice); succ++) {
  				if (succState(succ) == s2) {
  					return true;
  				}
  			}
  		}
  		return false;
  	}
  
  	/**
  	 * Get an iterator over the transitions from choice {@code i} of state {@code s}.
  	 * <br>
  	 * For DTMC/CTMCs, there is only a single choice.
  	 */
  	public Iterator<Entry<Integer, Function>> getTransitionsIterator(final int s, final int i)
  	{
  		return new Iterator<Entry<Integer, Function>>()
  		{
  			final int start = choiceBegin(stateBegin(s) + i);
  			int col = start;
  			final int end = choiceBegin(stateBegin(s) + i + 1);
  
  			@Override
  			public boolean hasNext()
  			{
  				return col < end;
  			}
  
  			@Override
  			public Entry<Integer, Function> next()
  			{
  				assert (col < end);
  				final int i = col;
  				col++;
  				return new Entry<Integer, Function>()
  				{
  					int key = cols[i];
  					Function value = nonZeros[i];
  
  					@Override
  					public Integer getKey()
  					{
  						return key;
  					}
  
  					@Override
  					public Function getValue()
  					{
  						return value;
  					}
  
  					@Override
  					public Function setValue(Function arg0)
  					{
  						throw new UnsupportedOperationException();
  					}
  				};
  			}
  		};
  	}
  
  	@Override
  	public void findDeadlocks(boolean fix) throws PrismException
  	{
  		throw new UnsupportedOperationException();
  	}
  
  	@Override
  	public void checkForDeadlocks() throws PrismException
  	{
  		throw new UnsupportedOperationException();
  	}
  
  	@Override
  	public void checkForDeadlocks(BitSet except) throws PrismException
  	{
  		throw new UnsupportedOperationException();
  	}
  
  	@Override
  	public void exportToPrismExplicit(String baseFilename) throws PrismException
  	{
  		throw new UnsupportedOperationException();
  	}
  
  	@Override
  	public void exportToPrismExplicitTra(String filename) throws PrismException
  	{
  		throw new UnsupportedOperationException();
  	}
  
  	@Override
  	public void exportToPrismExplicitTra(File file) throws PrismException
  	{
  		throw new UnsupportedOperationException();
  	}
  
  	@Override
  	public void exportToPrismExplicitTra(PrismLog log)
  	{
  		throw new UnsupportedOperationException();
  	}
  
  	@Override
  	public void exportTransitionsToDotFile(int i, PrismLog out, Iterable<explicit.graphviz.Decorator> decorators)
  	{
  		int numChoices = getNumChoices(i);
  		for (int j = 0; j < numChoices; j++) {
  			// action = getAction(i, j);
  			String nij = null;
  			if (modelType.nondeterministic()) {
  				nij = "n" + i + "_" + j;
  				out.print(i + " -> " + nij + " ");
  				explicit.graphviz.Decoration d = new explicit.graphviz.Decoration();
  				d.attributes().put("arrowhead", "none");
  				d.setLabel(Integer.toString(j));
  
  				if (decorators != null) {
  					for (Decorator decorator : decorators) {
  						d = decorator.decorateTransition(i, j, d);
  					}
  				}
  				out.print(d);
  				out.println(";");
  
  				out.print(nij + " [ shape=point,width=0.1,height=0.1,label=\"\" ];\n");
  			}
  
  			Iterator<Entry<Integer, Function>> it = getTransitionsIterator(i, j);
  			while (it.hasNext()) {
  				Entry<Integer, Function> e = it.next();
  
  				// Note: For CTMCs, param stores the embedded DTMC, so we output that
  
  				if (!modelType.nondeterministic()) {
  					out.print(i + " -> " + e.getKey() + " ");
  				} else {
  					out.print(nij + " -> " + e.getKey() + " ");
  				}
  
  				Object value;
  				if (e.getValue().isConstant()) {
  					value = e.getValue().asBigRational();
  				} else {
  					value = e.getValue();
  				}
  
  				explicit.graphviz.Decoration d = new explicit.graphviz.Decoration();
  				d.setLabel(value.toString());
  
  				if (decorators != null) {
  					for (Decorator decorator : decorators) {
  						if (!modelType.nondeterministic()) {
  							d = decorator.decorateProbability(i, e.getKey(), value, d);
  						} else {
  							d = decorator.decorateProbability(i, e.getKey(), j, value, d);
  						}
  					}
  				}
  
  				out.print(d);
  				out.println(";");
  			}
  		}
  	}
  
  	@Override
  	public void exportToDotFileWithStrat(PrismLog out, BitSet mark, int[] strat)
  	{
  		throw new UnsupportedOperationException();
  	}
  
  	@Override
  	public void exportToPrismLanguage(String filename) throws PrismException
  	{
  		throw new UnsupportedOperationException();
  	}
  
  	@Override
  	public Model constructInducedModel(MDStrategy strat)
  	{
  		throw new UnsupportedOperationException();
  	}
  
  	@Override
  	public String infoString()
  	{
  		throw new UnsupportedOperationException();
  	}
  
  	@Override
  	public String infoStringTable()
  	{
  		String s = "";
  		s += "States:      " + numStates + " (" + getNumInitialStates() + " initial)\n";
  		s += "Transitions: " + getNumTransitions() + "\n";
  		return s;
  	}
  
  	// Other
  	
  	public int getNumChoices(int state)
  	{
  		return stateEnd(state) - stateBegin(state);
  	}
  
  	@Override
  	public int getMaxNumChoices()
  	{
  		return numMaxChoices;
  	}
  
  	@Override
  	public int getNumChoices()
  	{
  		return numTotalChoices;
  	}
  
  	@Override
  	public int getNumTransitions(int s, int i)
  	{
  		return choiceEnd(stateBegin(s) + i) - choiceBegin(stateBegin(s) + i);
  	}
  
  	@Override
  	public Object getAction(int s, int i)
  	{
  		return null;
  	}
  
  	@Override
  	public boolean areAllChoiceActionsUnique()
  	{
  		// we don't know
  		return false;
  	}
  
  	/**
  	 * Allocates memory for subsequent construction of model. 
  	 * 
  	 * @param numStates number of states of the model
  	 * @param numTotalChoices total number of nondeterministic choices of the model
  	 * @param numTotalSuccessors total number of probabilistic transitions of the model
  	 */
  	void reserveMem(int numStates, int numTotalChoices, int numTotalSuccessors)
  	{
  		rows = new int[numStates + 1];
  		choices = new int[numTotalChoices + 1];
  		labels = new String[numTotalSuccessors];
  		cols = new int[numTotalSuccessors];
  		nonZeros = new Function[numTotalSuccessors];
  		sumRates = new Function[numTotalChoices];
  	}
  
  	/**
  	 * Finish the current state.
  	 * Starting with the 0th state, this function shall be called once all
  	 * nondeterministic decisions of the current nth state have been added.
  	 * Subsequent method calls of {@code finishChoice} and {@code addTransition}
  	 * will then apply to the (n+1)th state. Notice that this method must be
  	 * called for each state of the method, even the last one, once all its
  	 * transitions have been added.
  	 */
  	void finishState()
  	{
  		int state = numStates;
  		rows[numStates + 1] = numTotalChoices;
  		numStates++;
  
  		numMaxChoices = Math.max(numMaxChoices, getNumChoices(state));
  	}
  
  	/**
  	 * Finished the current nondeterministic choice.
  	 * Subsequent calls of {@code addTransition} will in turn add probabilistic
  	 * branches to the next nondeterministic choice. Notice that this method has
  	 * to be called for all nondeterministic choices of a state, even the last
  	 * one. Notice that DTMCs and CTMCs should only have a single
  	 * nondeterministic choice per state.
  	 */
  	void finishChoice()
  	{
  		choices[numTotalChoices + 1] = numTotalTransitions;
  		numTotalChoices++;
  	}
  
  	/**
  	 * Adds a probabilistic branch to the current nondeterministic choice.
  	 * Notice that by this function the probability to leave to a given state
  	 * shall be specified, <i>not</i> the rate to this state. Instead, the
  	 * sum of rates leaving a certain nondeterministic decision shall be
  	 * specified using {@code setSumLeaving}.
  	 * 
  	 * @param toState to which state the probabilistic choice leads
  	 * @param probFn with which probability it leads to this state
  	 * @param action action with which the choice is labelled
  	 */
  	void addTransition(int toState, Function probFn, String action)
  	{
  		cols[numTotalTransitions] = toState;
  		nonZeros[numTotalTransitions] = probFn;
  		labels[numTotalTransitions] = action;
  		numTotalTransitions++;
  	}
  
  	/**
  	 * Sets the total sum of leaving rate of the current nondeterministic choice.
  	 * For discrete-time models, this function shall always be called with
  	 * {@code leaving = 1}.
  	 * 
  	 * @param leaving total sum of leaving rate of the current nondeterministic choice
  	 */
  	void setSumLeaving(Function leaving)
  	{
  		sumRates[numTotalChoices] = leaving;
  	}
  
  	/**
  	 * Returns the number of the first nondeterministic choice of {@code state}.
  	 * 
  	 * @param state state to return number of first nondeterministic choice of
  	 * @return number of first nondeterministic choice of {@code state}
  	 */
  	int stateBegin(int state)
  	{
  		return rows[state];
  	}
  
  	/**
  	 * Returns the number of the last nondeterministic choice of {@code state} plus one.
  	 * 
  	 * @param state state to return number of last nondeterministic choice of
  	 * @return number of first nondeterministic choice of {@code state} plus one
  	 */
  	int stateEnd(int state)
  	{
  		return rows[state + 1];
  	}
  
  	/**
  	 * Returns the first probabilistic branch of the given nondeterministic decision.
  	 * 
  	 * @param choice choice of which to return the first probabilitic branch
  	 * @return number of first probabilistic branch of {@choice}
  	 */
  	int choiceBegin(int choice)
  	{
  		return choices[choice];
  	}
  
  	/**
  	 * Returns the last probabilistic branch of the given nondeterministic decision plus one.
  	 * 
  	 * @param choice choice of which to return the first probabilitic branch
  	 * @return number of last probabilistic branch of {@choice} plus one
  	 */
  	int choiceEnd(int choice)
  	{
  		return choices[choice + 1];
  	}
  
  	/**
  	 * Returns the successor state of the given probabilistic branch.
  	 * 
  	 * @param succNr probabilistic branch to return successor state of
  	 * @return state which probabilistic branch leads to
  	 */
  	int succState(int succNr)
  	{
  		return cols[succNr];
  	}
  
  	/**
  	 * Returns the probability of the given probabilistic branch
  	 * 
  	 * @param succNr probabilistic branch to return probability of
  	 * @return probability of given probabilistic branch
  	 */
  	Function succProb(int succNr)
  	{
  		return nonZeros[succNr];
  	}
  
  	/**
  	 * Returns the label of the given probabilistic branch
  	 * 
  	 * @param succNr probabilistic branch to return label of
  	 * @return label of given probabilistic branch
  	 */
  	String getLabel(int succNr)
  	{
  		return labels[succNr];
  	}
  
  	/**
  	 * Returns the total sum of leaving rates of the given nondeterministic choice 
  	 * 
  	 * @param choice nondeterministic choice to return sum of leaving rates of
  	 * @return sum of leaving rates of given nondeterministic choice
  	 */
  	Function sumLeaving(int choice)
  	{
  		return sumRates[choice];
  	}
  
  	/**
  	 * Instantiates the parametric model at a given point.
  	 * All transition probabilities, etc. will be evaluated and set as
  	 * probabilities of the concrete model at the given point. 
  	 * <br>
  	 * If {@code checkWellDefinedness} is {@code true}, checks that the
  	 * instantiated probabilities are actually probabilities and graph-preserving.
  	 * If that is not the case, this method then returns {@code null}.
  	 * 
  	 * @param point point to instantiate model at
  	 * @param checkWellDefinedness should we check that the model is well-defined?
  	 * @return nonparametric model instantiated at {@code point}
  	 */
  	ParamModel instantiate(Point point, boolean checkWellDefinedness)
  	{
  		ParamModel result = new ParamModel();
  		result.setModelType(getModelType());
  		result.reserveMem(numStates, numTotalChoices, numTotalTransitions);
  		result.initialStates = new LinkedList<Integer>(this.initialStates);
  		for (int state = 0; state < numStates; state++) {
  			for (int choice = stateBegin(state); choice < stateEnd(state); choice++) {
  				for (int succ = choiceBegin(choice); succ < choiceEnd(choice); succ++) {
  					BigRational p = succProb(succ).evaluate(point);
  					if (checkWellDefinedness) {
  						if (p.isSpecial() || p.compareTo(BigRational.ONE) == 1 || p.signum() <= 0) {
  							// For graph-preservation, probabilities have to be >0 and <=1
  							// Note: for CTMCs, succProb yields the probabilities of the embedded
  							// DTMC, while the rates are available separately (sumLeaving)
  							return null;
  						}
  					}
  					result.addTransition(succState(succ), functionFactory.fromBigRational(p), labels[succ]);
  
  				}
  				result.setSumLeaving(functionFactory.fromBigRational(this.sumLeaving(choice).evaluate(point)));
  				result.finishChoice();
  			}
  			result.finishState();
  		}
  		result.functionFactory = this.functionFactory;
  
  		return result;
  	}
  
  	@Override
  	public void buildFromPrismExplicit(String filename) throws PrismException
  	{
  		throw new UnsupportedOperationException();
  	}
  
  	/**
  	 * Sets the function factory to be used in this parametric model.
  	 * 
  	 * @param functionFactory function factory to be used in this parametric model
  	 */
  	void setFunctionFactory(FunctionFactory functionFactory)
  	{
  		this.functionFactory = functionFactory;
  	}
  
  	/**
  	 * Returns the function factory used in this parametric model.
  	 * 
  	 * @return function factory used in this parametric model
  	 */
  	FunctionFactory getFunctionFactory()
  	{
  		return functionFactory;
  	}
  
  }
  