gt: 		if (file != null)
context: //==============================================================================
  //	
  //	Authors:
  //	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford, formerly University of Birmingham)
  //	* Andrew Hinton <ug60axh@cs.bham.ac.uk> (University of Birmingham)
  //	
  //------------------------------------------------------------------------------
  //	
  //	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 prism;
  
  import hybrid.PrismHybrid;
  
  import java.io.ByteArrayInputStream;
  import java.io.File;
  import java.io.FileInputStream;
  import java.io.FileNotFoundException;
  import java.util.ArrayList;
  import java.util.List;
  
  import jdd.JDD;
  import jdd.JDDNode;
  import jdd.JDDVars;
  import mtbdd.PrismMTBDD;
  import odd.ODDUtils;
  import param.BigRational;
  import param.ModelBuilder;
  import param.ParamModelChecker;
  import param.RegionValues;
  import parser.ExplicitFiles2ModulesFile;
  import parser.PrismParser;
  import parser.State;
  import parser.Values;
  import parser.ast.Expression;
  import parser.ast.ForLoop;
  import parser.ast.LabelList;
  import parser.ast.ModulesFile;
  import parser.ast.PropertiesFile;
  import parser.ast.Property;
  import pta.DigitalClocks;
  import pta.PTAModelChecker;
  import simulator.GenerateSimulationPath;
  import simulator.ModulesFileModelGenerator;
  import simulator.SimulatorEngine;
  import simulator.method.SimulationMethod;
  import sparse.PrismSparse;
  import strat.Strategy;
  import dv.DoubleVector;
  import explicit.CTMC;
  import explicit.CTMCModelChecker;
  import explicit.ConstructModel;
  import explicit.DTMC;
  import explicit.DTMCModelChecker;
  import explicit.FastAdaptiveUniformisation;
  import explicit.FastAdaptiveUniformisationModelChecker;
  
  /**
   * Main class for all PRISM's core functionality.
   * This is independent of the user interface (command line or gui).
   */
  public class Prism extends PrismComponent implements PrismSettingsListener
  {
  	/** PRISM version (e.g. "4.0.3"). Read from prism.Version. */
  	private static String version = prism.Version.versionString;
  
  	/** Optional PRISM version suffix (e.g. "dev", "beta"). Read from prism.Version. */
  	private static String versionSuffix = prism.Version.versionSuffixString;
  
  	/** Build number (e.g. "6667"). Defaults to "" (undefined), read from prism.Revision class if present. */
  	private static String buildNumber = "";
  	static {
  		try {
  			buildNumber = Prism.class.getClassLoader().loadClass("prism.Revision").getField("svnRevision").get(null).toString();
  		} catch (Exception e) {
  			// Any problems (e.g. class not created), ignore.
  		}
  	}
  
  	//------------------------------------------------------------------------------
  	// Constants
  	//------------------------------------------------------------------------------
  
  	// underlying computation engine
  	public static final int MTBDD = 1;
  	public static final int SPARSE = 2;
  	public static final int HYBRID = 3;
  	public static final int EXPLICIT = 4;
  	private static String[] engineStrings = { "?", "MTBDD", "Sparse", "Hybrid", "Explicit" };
  
  	// methods for solving linear equation systems
  	public static final int POWER = 1;
  	public static final int JACOBI = 2;
  	public static final int GAUSSSEIDEL = 3;
  	public static final int BGAUSSSEIDEL = 4;
  	public static final int PGAUSSSEIDEL = 5;
  	public static final int BPGAUSSSEIDEL = 6;
  	public static final int JOR = 7;
  	public static final int SOR = 8;
  	public static final int BSOR = 9;
  	public static final int PSOR = 10;
  	public static final int BPSOR = 11;
  
  	// methods for solving MDPs
  	public static final int MDP_VALITER = 1;
  	public static final int MDP_GAUSSSEIDEL = 2;
  	public static final int MDP_POLITER = 3;
  	public static final int MDP_MODPOLITER = 4;
  	public static final int MDP_LP = 5;
  
  	// methods for solving multi-objective queries on MDPs
  	public static final int MDP_MULTI_VALITER = 1;
  	public static final int MDP_MULTI_GAUSSSEIDEL = 2;
  	public static final int MDP_MULTI_LP = 3;
  
  	// termination criterion for iterative methods
  	public static final int ABSOLUTE = 1;
  	public static final int RELATIVE = 2;
  
  	// options for model matrix export
  	public static final int EXPORT_PLAIN = 1;
  	public static final int EXPORT_MATLAB = 2;
  	public static final int EXPORT_DOT = 3;
  	public static final int EXPORT_MRMC = 4;
  	public static final int EXPORT_ROWS = 5;
  	public static final int EXPORT_DOT_STATES = 6;
  
  	// options for adversary export
  	public static final int EXPORT_ADV_NONE = 1;
  	public static final int EXPORT_ADV_DTMC = 2;
  	public static final int EXPORT_ADV_MDP = 3;
  
  	// methods for SCC decomposition
  	public static final int XIEBEEREL = 1;
  	public static final int LOCKSTEP = 2;
  	public static final int SCCFIND = 3;
  
  	// Options for type of strategy export
  	public enum StrategyExportType {
  		ACTIONS, INDICES, INDUCED_MODEL, DOT_FILE;
  		public String description()
  		{
  			switch (this) {
  			case ACTIONS:
  				return "as actions";
  			case INDICES:
  				return "as indices";
  			case INDUCED_MODEL:
  				return "as an induced model";
  			case DOT_FILE:
  				return "as a dot file";
  			default:
  				return this.toString();
  			}
  		}
  	}
  
  	//------------------------------------------------------------------------------
  	// Settings / flags / options
  	//------------------------------------------------------------------------------
  
  	// Export parsed PRISM model?
  	protected boolean exportPrism = false;
  	protected File exportPrismFile = null;
  	protected boolean exportPrismConst = false;
  	protected File exportPrismConstFile = null;
  	// Export digital clocks translation PRISM model?
  	protected boolean exportDigital = false;
  	protected File exportDigitalFile = null;
  	// Export target state info?
  	protected boolean exportTarget = false;
  	protected String exportTargetFilename = null;
  	// Export product model info?
  	protected boolean exportProductTrans = false;
  	protected String exportProductTransFilename = null;
  	protected boolean exportProductStates = false;
  	protected String exportProductStatesFilename = null;
  	protected boolean exportProductVector = false;
  	protected String exportProductVectorFilename = null;
  	// Store the final results vector after model checking?
  	protected boolean storeVector = false;
  	// Generate/store a strategy during model checking?
  	protected boolean genStrat = false;
  	// Do bisimulation minimisation before model checking?
  	protected boolean doBisim = false;
  
  	// A few miscellaneous options (i.e. defunct/hidden/undocumented/etc.)
  	// See constructor below for default values
  
  	private boolean doReach = true; // do reachability? (sometimes might want to skip it)
  	private boolean bsccComp = true; // do bscc computation before steady-state?
  	private boolean checkZeroLoops = false;
  
  	// MTBDD construction method (NOW DEFUNCT)
  	//  1 - use with ordering 1: nondet vars form a tree at the top
  	//  3 - use with ordering 2: zero for nonexistant bits
  	// nb: option 2 removed because it was stupid
  	private int construction = 3;
  
  	// MTBDD variable ordering
  	//  1 - (s ... s) (l ... l) (r c ... r c)
  	//  2 - (s l ... l r c ... r c) (s l ... l r c ... r c) ...
  	private int ordering = 1;
  
  	// Method to use for (symbolic) state-space reachability
  	private int reachMethod = REACH_BFS;
  
  	//------------------------------------------------------------------------------
  	// Parsers/translators/model checkers/simulators/etc.
  	//------------------------------------------------------------------------------
  
  	private static PrismParser thePrismParser = null;
  	private static boolean prismParserInUse = false;
  	private ExplicitFiles2MTBDD expf2mtbdd = null;
  	private ExplicitModel2MTBDD expm2mtbdd = null;
  	private SimulatorEngine theSimulator = null;
  
  	//------------------------------------------------------------------------------
  	// Event listeners
  	//------------------------------------------------------------------------------
  
  	private List<PrismModelListener> modelListeners;
  
  	//------------------------------------------------------------------------------
  	// State
  	//------------------------------------------------------------------------------
  
  	private enum ModelSource {
  		PRISM_MODEL, MODEL_GENERATOR, EXPLICIT_FILES, BUILT_MODEL
  	}
  
  	// Info about currently loaded model, if any
  	// Model source
  	private ModelSource currentModelSource = ModelSource.PRISM_MODEL;
  	// Model type
  	private ModelType currentModelType = null;
  	// PRISM model (null if none loaded)
  	private ModulesFile currentModulesFile = null;
  	// Model generator (null if none loaded)
  	private ModelGenerator currentModelGenerator = null;
  	// Constants to be defined for PRISM model
  	private Values currentDefinedMFConstants = null;
  	// Built model storage - symbolic or explicit - at most one is non-null
  	private Model currentModel = null;
  	private explicit.Model currentModelExpl = null;
  	// Are we doing digital clocks translation for PTAs?
  	boolean digital = false;
  
  	// Info for explicit files load
  	private File explicitFilesStatesFile = null;
  	private File explicitFilesTransFile = null;
  	private File explicitFilesLabelsFile = null;
  	private int explicitFilesNumStates = -1;
  
  	// Has the CUDD library been initialised yet?
  	private boolean cuddStarted = false;
  
  	//------------------------------------------------------------------------------
  	// Constructors + options methods
  	//------------------------------------------------------------------------------
  
  	/**
  	 * Construct a new Prism object.
  	 * @param mainLog PrismLog where all output will be sent.
  	 */
  	public Prism(PrismLog mainLog)
  	{
  		// set up log
  		this.mainLog = mainLog;
  		// set up some default options
  		settings = new PrismSettings();
  		// add this Prism object as a results listener
  		settings.addSettingsListener(this);
  		// create list of model listeners
  		modelListeners = new ArrayList<PrismModelListener>();
  	}
  
  	/**
  	 * Construct a new Prism object.
  	 * @deprecated ({@code techLog} is no longer used, use the {@link #prism.Prism(PrismLog)} constructor instead).
  	 */
  	public Prism(PrismLog mainLog, PrismLog techLog)
  	{
  		this(mainLog);
  	}
  
  	/**
  	 * Read in PRISM settings from the default file (.prism in user's home directory).
  	 * If no file exists, attempt to create a new one with default settings.
  	 */
  	public void loadUserSettingsFile()
  	{
  		loadUserSettingsFile(null);
  	}
  
  	/**
  	 * Read in PRISM settings from a specified file.
  	 * If the file is null, use the default (.prism in user's home directory).
  	 * If no file exists, attempt to create a new one with default settings.
  	 */
  	public void loadUserSettingsFile(File settingsFile)
  	{
  		// load user's default settings
  		try {
  			if (settingsFile == null)
  				settings.loadSettingsFile();
  			else
  				settings.loadSettingsFile(settingsFile);
  		} catch (PrismException e) {
  			// if there were no user defaults to load, create them
  			try {
  				if (settingsFile == null)
  					settings.saveSettingsFile();
  				else
  					settings.saveSettingsFile(settingsFile);
  			} catch (PrismException ex) {
  				mainLog.printWarning("Failed to create new PRISM settings file.");
  			}
  		}
  	}
  
  	// Set methods
  
  	/**
  	 * Set the PrismLog where messages and model checking output will be sent.
  	 */
  	public void setMainLog(PrismLog l)
  	{
  		// store new log
  		mainLog = l;
  		// pass to other components
  		JDD.SetOutputStream(mainLog.getFilePointer());
  		PrismMTBDD.setMainLog(mainLog);
  		PrismSparse.setMainLog(mainLog);
  		PrismHybrid.setMainLog(mainLog);
  	}
  
  	// Set methods for main prism settings
  	// (provided for convenience and for compatibility with old code)
  
  	public void setEngine(int e) throws PrismException
  	{
  		settings.setChoice(PrismSettings.PRISM_ENGINE, e);
  	}
  
  	public void setVerbose(boolean b) throws PrismException
  	{
  		settings.set(PrismSettings.PRISM_VERBOSE, b);
  	}
  
  	public void setFairness(boolean b) throws PrismException
  	{
  		settings.set(PrismSettings.PRISM_FAIRNESS, b);
  	}
  
  	public void setPrecomp(boolean b) throws PrismException
  	{
  		settings.set(PrismSettings.PRISM_PRECOMPUTATION, b);
  	}
  
  	public void setProb0(boolean b) throws PrismException
  	{
  		settings.set(PrismSettings.PRISM_PROB0, b);
  	}
  
  	public void setProb1(boolean b) throws PrismException
  	{
  		settings.set(PrismSettings.PRISM_PROB1, b);
  	}
  
  	public void setFixDeadlocks(boolean b) throws PrismException
  	{
  		settings.set(PrismSettings.PRISM_FIX_DEADLOCKS, b);
  	}
  
  	public void setDoProbChecks(boolean b) throws PrismException
  	{
  		settings.set(PrismSettings.PRISM_DO_PROB_CHECKS, b);
  	}
  
  	public void setSumRoundOff(double d) throws PrismException
  	{
  		settings.set(PrismSettings.PRISM_SUM_ROUND_OFF, d);
  	}
  
  	public void setCompact(boolean b) throws PrismException
  	{
  		settings.set(PrismSettings.PRISM_COMPACT, b);
  	}
  
  	public void setLinEqMethod(int i) throws PrismException
  	{
  		settings.setChoice(PrismSettings.PRISM_LIN_EQ_METHOD, i);
  	}
  
  	public void setLinEqMethodParam(double d) throws PrismException
  	{
  		settings.set(PrismSettings.PRISM_LIN_EQ_METHOD_PARAM, d);
  	}
  
  	public void setMDPSolnMethod(int i) throws PrismException
  	{
  		settings.setChoice(PrismSettings.PRISM_MDP_SOLN_METHOD, i);
  	}
  
  	public void setMDPMultiSolnMethod(int i) throws PrismException
  	{
  		settings.setChoice(PrismSettings.PRISM_MDP_MULTI_SOLN_METHOD, i);
  	}
  
  	public void setTermCrit(int i) throws PrismException
  	{
  		settings.setChoice(PrismSettings.PRISM_TERM_CRIT, i);
  	}
  
  	public void setTermCritParam(double d) throws PrismException
  	{
  		settings.set(PrismSettings.PRISM_TERM_CRIT_PARAM, d);
  	}
  
  	public void setMaxIters(int i) throws PrismException
  	{
  		settings.set(PrismSettings.PRISM_MAX_ITERS, i);
  	}
  
  	public void setCUDDMaxMem(String s) throws PrismException
  	{
  		settings.set(PrismSettings.PRISM_CUDD_MAX_MEM, s);
  	}
  
  	public void setCUDDEpsilon(double d) throws PrismException
  	{
  		settings.set(PrismSettings.PRISM_CUDD_EPSILON, d);
  	}
  
  	public void setNumSBLevels(int i) throws PrismException
  	{
  		settings.set(PrismSettings.PRISM_NUM_SB_LEVELS, i);
  	}
  
  	public void setSBMaxMem(int i) throws PrismException
  	{
  		settings.set(PrismSettings.PRISM_SB_MAX_MEM, i);
  	}
  
  	public void setNumSORLevels(int i) throws PrismException
  	{
  		settings.set(PrismSettings.PRISM_NUM_SOR_LEVELS, i);
  	}
  
  	public void setSORMaxMem(int i) throws PrismException
  	{
  		settings.set(PrismSettings.PRISM_SOR_MAX_MEM, i);
  	}
  
  	public void setDoSSDetect(boolean b) throws PrismException
  	{
  		settings.set(PrismSettings.PRISM_DO_SS_DETECTION, b);
  	}
  
  	public void setExtraDDInfo(boolean b) throws PrismException
  	{
  		settings.set(PrismSettings.PRISM_EXTRA_DD_INFO, b);
  	}
  
  	public void setExtraReachInfo(boolean b) throws PrismException
  	{
  		settings.set(PrismSettings.PRISM_EXTRA_REACH_INFO, b);
  	}
  
  	public void setSCCMethod(int i) throws PrismException
  	{
  		settings.setChoice(PrismSettings.PRISM_SCC_METHOD, i);
  	}
  
  	public void setExportAdv(int i) throws PrismException
  	{
  		settings.setChoice(PrismSettings.PRISM_EXPORT_ADV, i);
  	}
  
  	public void setExportAdvFilename(String s) throws PrismException
  	{
  		settings.set(PrismSettings.PRISM_EXPORT_ADV_FILENAME, s);
  	}
  
  	// Set methods for miscellaneous options
  
  	public void setExportPrism(boolean b) throws PrismException
  	{
  		exportPrism = b;
  	}
  
  	/**
  	 * Set file to export parsed PRISM file to (null = stdout).
  	 */
  	public void setExportPrismFile(File f) throws PrismException
  	{
  		exportPrismFile = f;
  	}
  
  	public void setExportPrismConst(boolean b) throws PrismException
  	{
  		exportPrismConst = b;
  	}
  
  	/**
  	 * Set file to export parsed PRISM file, with constants expanded, to (null = stdout).
  	 */
  	public void setExportPrismConstFile(File f) throws PrismException
  	{
  		exportPrismConstFile = f;
  	}
  
  	public void setExportDigital(boolean b) throws PrismException
  	{
  		exportDigital = b;
  	}
  
  	/**
  	 * Set file to export digital clocks translation PRISM file to (null = stdout).
  	 */
  	public void setExportDigitalFile(File f) throws PrismException
  	{
  		exportDigitalFile = f;
  	}
  
  	public void setExportTarget(boolean b) throws PrismException
  	{
  		exportTarget = b;
  	}
  
  	public void setExportTargetFilename(String s) throws PrismException
  	{
  		exportTargetFilename = s;
  	}
  
  	public void setExportProductTrans(boolean b) throws PrismException
  	{
  		exportProductTrans = b;
  	}
  
  	public void setExportProductTransFilename(String s) throws PrismException
  	{
  		exportProductTransFilename = s;
  	}
  
  	public void setExportProductStates(boolean b) throws PrismException
  	{
  		exportProductStates = b;
  	}
  
  	public void setExportProductStatesFilename(String s) throws PrismException
  	{
  		exportProductStatesFilename = s;
  	}
  
  	public void setExportProductVector(boolean b) throws PrismException
  	{
  		exportProductVector = b;
  	}
  
  	public void setExportProductVectorFilename(String s) throws PrismException
  	{
  		exportProductVectorFilename = s;
  	}
  
  	/**
  	 * Specify whether or not to store the final results vector after model checking.
  	 */
  	public void setStoreVector(boolean storeVector)
  	{
  		this.storeVector = storeVector;
  	}
  
  	/**
  	 * Specify whether or not a strategy should be generated during model checking.
  	 */
  	public void setGenStrat(boolean genStrat)
  	{
  		this.genStrat = genStrat;
  	}
  
  	/**
  	 * Specify whether or not to do bisimulation minimisation before model checking.
  	 */
  	public void setDoBisim(boolean doBisim)
  	{
  		this.doBisim = doBisim;
  	}
  
  	public void setDoReach(boolean b) throws PrismException
  	{
  		doReach = b;
  	}
  
  	public void setBSCCComp(boolean b) throws PrismException
  	{
  		bsccComp = b;
  	}
  
  	public void setCheckZeroLoops(boolean checkZeroLoops)
  	{
  		this.checkZeroLoops = checkZeroLoops;
  	}
  
  	public void setConstruction(int i) throws PrismException
  	{
  		construction = i;
  	}
  
  	public void setOrdering(int i) throws PrismException
  	{
  		ordering = i;
  	}
  
  	public static int REACH_BFS = 1;
  	public static int REACH_FRONTIER = 2;
  
  	public void setReachMethod(int reachMethod)
  	{
  		this.reachMethod = reachMethod;
  	}
  
  	// Get methods
  
  	/**
  	 * Get the name of this tool.
  	 * ("PRISM" by default, extensions might override) 
  	 */
  	public static String getToolName()
  	{
  		return "PRISM";
  	}
  
  	/**
  	 * Get current version number, as a string. 
  	 */
  	public static String getVersion()
  	{
  		String v = version;
  		// Append version suffix (e.g. "dev", "beta") if non-empty
  		if (versionSuffix.length() > 0) {
  			v += "." + versionSuffix;
  			// In this case, also append any build number
  			if (buildNumber.length() > 0)
  				v += ".r" + buildNumber;
  		}
  		return v;
  	}
  
  	/**
  	 * Get build number (SVN revision) for current version. Returns "" if not set up.
  	 */
  	public static String getBuildNumber()
  	{
  		return buildNumber;
  	}
  
  	public PrismLog getMainLog()
  	{
  		return mainLog;
  	}
  
  	public PrismSettings getSettings()
  	{
  		return settings;
  	}
  
  	// Get methods for main prism settings
  	// (as above, provided for convenience and for compatibility with old code)
  
  	public int getEngine()
  	{
  		return settings.getChoice(PrismSettings.PRISM_ENGINE);
  	}
  
  	/**
  	 * Is the current engine "Explicit"?
  	 */
  	public boolean getExplicit()
  	{
  		return getEngine() == Prism.EXPLICIT;
  	}
  
  	public boolean getFixDeadlocks()
  	{
  		return settings.getBoolean(PrismSettings.PRISM_FIX_DEADLOCKS);
  	}
  
  	public boolean getDoProbChecks()
  	{
  		return settings.getBoolean(PrismSettings.PRISM_DO_PROB_CHECKS);
  	}
  
  	public double getSumRoundOff()
  	{
  		return settings.getDouble(PrismSettings.PRISM_SUM_ROUND_OFF);
  	}
  
  	public int getLinEqMethod()
  	{
  		return settings.getChoice(PrismSettings.PRISM_LIN_EQ_METHOD);
  	}
  
  	public double getLinEqMethodParam()
  	{
  		return settings.getDouble(PrismSettings.PRISM_LIN_EQ_METHOD_PARAM);
  	}
  
  	public int getMDPSolnMethod()
  	{
  		return settings.getChoice(PrismSettings.PRISM_MDP_SOLN_METHOD);
  	}
  
  	public int getMDPMultiSolnMethod()
  	{
  		return settings.getChoice(PrismSettings.PRISM_MDP_MULTI_SOLN_METHOD);
  	}
  
  	public int getTermCrit()
  	{
  		return settings.getChoice(PrismSettings.PRISM_TERM_CRIT);
  	}
  
  	public double getTermCritParam()
  	{
  		return settings.getDouble(PrismSettings.PRISM_TERM_CRIT_PARAM);
  	}
  
  	public int getMaxIters()
  	{
  		return settings.getInteger(PrismSettings.PRISM_MAX_ITERS);
  	}
  
  	public boolean getVerbose()
  	{
  		return settings.getBoolean(PrismSettings.PRISM_VERBOSE);
  	}
  
  	public boolean getPrecomp()
  	{
  		return settings.getBoolean(PrismSettings.PRISM_PRECOMPUTATION);
  	}
  
  	public boolean getProb0()
  	{
  		return settings.getBoolean(PrismSettings.PRISM_PROB0);
  	}
  
  	public boolean getProb1()
  	{
  		return settings.getBoolean(PrismSettings.PRISM_PROB1);
  	}
  
  	public boolean getPreRel()
  	{
  		return settings.getBoolean(PrismSettings.PRISM_PRE_REL);
  	}
  
  	public boolean getFairness()
  	{
  		return settings.getBoolean(PrismSettings.PRISM_FAIRNESS);
  	}
  
  	public int getSBMaxMem()
  	{
  		return settings.getInteger(PrismSettings.PRISM_SB_MAX_MEM);
  	}
  
  	public int getNumSBLevels()
  	{
  		return settings.getInteger(PrismSettings.PRISM_NUM_SB_LEVELS);
  	}
  
  	public int getSORMaxMem()
  	{
  		return settings.getInteger(PrismSettings.PRISM_SOR_MAX_MEM);
  	}
  
  	public boolean getDoSSDetect()
  	{
  		return settings.getBoolean(PrismSettings.PRISM_DO_SS_DETECTION);
  	}
  
  	public boolean getExtraDDInfo()
  	{
  		return settings.getBoolean(PrismSettings.PRISM_EXTRA_DD_INFO);
  	}
  
  	public boolean getExtraReachInfo()
  	{
  		return settings.getBoolean(PrismSettings.PRISM_EXTRA_REACH_INFO);
  	}
  
  	public int getNumSORLevels()
  	{
  		return settings.getInteger(PrismSettings.PRISM_NUM_SOR_LEVELS);
  	}
  
  	public boolean getCompact()
  	{
  		return settings.getBoolean(PrismSettings.PRISM_COMPACT);
  	}
  
  	public String getCUDDMaxMem()
  	{
  		return settings.getString(PrismSettings.PRISM_CUDD_MAX_MEM);
  	}
  
  	public double getCUDDEpsilon()
  	{
  		return settings.getDouble(PrismSettings.PRISM_CUDD_EPSILON);
  	}
  
  	public int getSCCMethod()
  	{
  		return settings.getChoice(PrismSettings.PRISM_SCC_METHOD);
  	}
  
  	public int getExportAdv()
  	{
  		return settings.getChoice(PrismSettings.PRISM_EXPORT_ADV);
  	}
  
  	public String getExportAdvFilename()
  	{
  		return settings.getString(PrismSettings.PRISM_EXPORT_ADV_FILENAME);
  	}
  
  	// Get methods for miscellaneous options
  
  	public boolean getExportPrism()
  	{
  		return exportPrism;
  	}
  
  	public File getExportPrismFile()
  	{
  		return exportPrismFile;
  	}
  
  	public boolean getExportPrismConst()
  	{
  		return exportPrismConst;
  	}
  
  	public File getExportPrismConstFile()
  	{
  		return exportPrismConstFile;
  	}
  
  	public boolean getExportTarget()
  	{
  		return exportTarget;
  	}
  
  	public String getExportTargetFilename()
  	{
  		return exportTargetFilename;
  	}
  
  	public boolean getExportProductTrans()
  	{
  		return exportProductTrans;
  	}
  
  	public String getExportProductTransFilename()
  	{
  		return exportProductTransFilename;
  	}
  
  	public boolean getExportProductStates()
  	{
  		return exportProductStates;
  	}
  
  	public String getExportProductStatesFilename()
  	{
  		return exportProductStatesFilename;
  	}
  
  	public boolean getExportProductVector()
  	{
  		return exportProductVector;
  	}
  
  	public String getExportProductVectorFilename()
  	{
  		return exportProductVectorFilename;
  	}
  
  	/**
  	 * Whether or not to store the final results vector after model checking.
  	 */
  	public boolean getStoreVector()
  	{
  		return storeVector;
  	}
  
  	/**
  	 * Whether or not a strategy should be generated during model checking.
  	 */
  	public boolean getGenStrat()
  	{
  		return genStrat;
  	}
  
  	/**
  	 * Whether or not to do bisimulation minimisation before model checking.
  	 */
  	public boolean getDoBisim()
  	{
  		return doBisim;
  	}
  
  	public boolean getDoReach()
  	{
  		return doReach;
  	}
  
  	public boolean getBSCCComp()
  	{
  		return bsccComp;
  	}
  
  	public boolean getCheckZeroLoops()
  	{
  		return this.checkZeroLoops;
  	}
  
  	public int getConstruction()
  	{
  		return construction;
  	}
  
  	public int getOrdering()
  	{
  		return ordering;
  	}
  
  	public int getReachMethod()
  	{
  		return reachMethod;
  	}
  
  	public void addModelListener(PrismModelListener listener)
  	{
  		modelListeners.add(listener);
  	}
  
  	// String methods for options
  
  	public static String getEngineString(int engine)
  	{
  		return engineStrings[engine];
  	}
  
  	/**
  	 * Let PrismSettings object notify us things have changed
  	 */
  	public void notifySettings(PrismSettings settings)
  	{
  		if (cuddStarted) {
  			JDD.SetCUDDEpsilon(settings.getDouble(PrismSettings.PRISM_CUDD_EPSILON));
  			try {
  				long cuddMaxMem = PrismUtils.convertMemoryStringtoKB(getCUDDMaxMem());
  				JDD.SetCUDDMaxMem(cuddMaxMem);
  			} catch (PrismException e) {
  				// Fail silently if memory string is invalid 
  			}
  		}
  	}
  
  	//------------------------------------------------------------------------------
  	// Access to parser, simulator, etc.
  	//------------------------------------------------------------------------------
  
  	/**
  	 * Get (exclusive) access to the PRISM parser.
  	 */
  	public static PrismParser getPrismParser() throws InterruptedException
  	{
  		// Note: this mutex mechanism is based on public domain code by Doug Lea
  		if (Thread.interrupted())
  			throw new InterruptedException();
  		// this code is synchronized on the whole Prism class
  		// (because this is a static method)
  		synchronized (Prism.class) {
  			try {
  				// wait until parser is free
  				while (prismParserInUse) {
  					Prism.class.wait();
  				}
  				// lock parser
  				prismParserInUse = true;
  				// return parser, creating anew if necessary
  				if (thePrismParser == null)
  					thePrismParser = new PrismParser();
  				return thePrismParser;
  			} catch (InterruptedException e) {
  				Prism.class.notify();
  				throw e;
  			}
  		}
  	}
  
  	/**
  	 * Release (exclusive) access to the PRISM parser.
  	 */
  	public static synchronized void releasePrismParser()
  	{
  		prismParserInUse = false;
  		Prism.class.notify();
  	}
  
  	/**
  	 * Get the SimulatorEngine object for PRISM, creating if necessary.
  	 */
  	public SimulatorEngine getSimulator()
  	{
  		if (theSimulator == null) {
  			theSimulator = new SimulatorEngine(this);
  		}
  		return theSimulator;
  	}
  
  	/**
  	 * Get an SCCComputer object.
  	 * Type (i.e. algorithm) depends on SCCMethod PRISM option.
  	 */
  	public SCCComputer getSCCComputer(Model model) throws PrismException
  	{
  		return SCCComputer.createSCCComputer(this, model);
  	}
  
  	/**
  	 * Get an SCCComputer object.
  	 * Type (i.e. algorithm) depends on SCCMethod PRISM option.
  	 */
  	public SCCComputer getSCCComputer(JDDNode reach, JDDNode trans01, JDDVars allDDRowVars, JDDVars allDDColVars) throws PrismException
  	{
  		return SCCComputer.createSCCComputer(this, reach, trans01, allDDRowVars, allDDColVars);
  	}
  
  	/**
  	 * Get an SCCComputer object for the explicit engine.
  	 */
  	public explicit.SCCComputer getExplicitSCCComputer(explicit.Model model) throws PrismException
  	{
  		return explicit.SCCComputer.createSCCComputer(this, model);
  	}
  
  	/**
  	 * Get an ECComputer object.
  	 */
  	public ECComputer getECComputer(NondetModel model) throws PrismException
  	{
  		return ECComputer.createECComputer(this, model);
  	}
  
  	/**
  	 * Get an ECComputer object.
  	 */
  	public ECComputer getECComputer(JDDNode reach, JDDNode trans, JDDNode trans01, JDDVars allDDRowVars, JDDVars allDDColVars, JDDVars allDDNondetVars)
  			throws PrismException
  	{
  		return ECComputer.createECComputer(this, reach, trans, trans01, allDDRowVars, allDDColVars, allDDNondetVars);
  	}
  
  	/**
  	 * Get an ECComputer object for the explicit engine.
  	 */
  	public explicit.ECComputer getExplicitECComputer(explicit.NondetModel model) throws PrismException
  	{
  		return explicit.ECComputer.createECComputer(this, model);
  	}
  
  	//------------------------------------------------------------------------------
  	// Utility methods
  	//------------------------------------------------------------------------------
  
  	/**
  	 * Compare two version numbers of PRISM (strings).
  	 * Example ordering: { "1", "2.0", "2.1.alpha", "2.1.alpha.r5555", "2.1.alpha.r5557", "2.1.beta", "2.1.beta4", "2.1", "2.1.dev", "2.1.dev.r6666", "2.1.dev1", "2.1.dev2", "2.1.2", "2.9", "3", "3.4"};
  	 * Returns: 1 if v1&gt;v2, -1 if v1&lt;v2, 0 if v1=v2
  	 */
  	public static int compareVersions(String v1, String v2)
  	{
  		String ss1[], ss2[], tmp[];
  		int i, n, x;
  		double s1 = 0, s2 = 0;
  		boolean s1num, s2num;
  
  		// Exactly equal
  		if (v1.equals(v2))
  			return 0;
  		// Otherwise split into sections
  		ss1 = v1.split("\\.");
  		ss2 = v2.split("\\.");
  		// Pad if one is shorter
  		n = Math.max(ss1.length, ss2.length);
  		if (ss1.length < n) {
  			tmp = new String[n];
  			for (i = 0; i < ss1.length; i++)
  				tmp[i] = ss1[i];
  			for (i = ss1.length; i < n; i++)
  				tmp[i] = "";
  			ss1 = tmp;
  		}
  		if (ss2.length < n) {
  			tmp = new String[n];
  			for (i = 0; i < ss2.length; i++)
  				tmp[i] = ss2[i];
  			for (i = ss2.length; i < n; i++)
  				tmp[i] = "";
  			ss2 = tmp;
  		}
  		// Loop through sections of string
  		for (i = 0; i < n; i++) {
  			// 2.1.alpha < 2.1, etc.
  			// 2.1.alpha < 2.1.alpha2 < 2.1.alpha3, etc.
  			// so replace alphax with -10000+x
  			if (ss1[i].matches("alpha.*")) {
  				try {
  					if (ss1[i].length() == 5)
  						x = 0;
  					else
  						x = Integer.parseInt(ss1[i].substring(5));
  				} catch (NumberFormatException e) {
  					x = 0;
  				}
  				ss1[i] = "" + (-10000 + x);
  			}
  			if (ss2[i].matches("alpha.*")) {
  				try {
  					if (ss2[i].length() == 5)
  						x = 0;
  					else
  						x = Integer.parseInt(ss2[i].substring(5));
  				} catch (NumberFormatException e) {
  					x = 0;
  				}
  				ss2[i] = "" + (-10000 + x);
  			}
  			// 2.1.beta < 2.1, etc.
  			// 2.1.beta < 2.1.beta2 < 2.1.beta3, etc.
  			// so replace betax with -100+x
  			if (ss1[i].matches("beta.*")) {
  				try {
  					if (ss1[i].length() == 4)
  						x = 0;
  					else
  						x = Integer.parseInt(ss1[i].substring(4));
  				} catch (NumberFormatException e) {
  					x = 0;
  				}
  				ss1[i] = "" + (-100 + x);
  			}
  			if (ss2[i].matches("beta.*")) {
  				try {
  					if (ss2[i].length() == 4)
  						x = 0;
  					else
  						x = Integer.parseInt(ss2[i].substring(4));
  				} catch (NumberFormatException e) {
  					x = 0;
  				}
  				ss2[i] = "" + (-100 + x);
  			}
  			// 2 < 2.1, etc.
  			// so treat 2 as 2.0
  			if (ss1[i].equals(""))
  				ss1[i] = "0";
  			if (ss2[i].equals(""))
  				ss2[i] = "0";
  			// 2.1 < 2.1.dev, etc.
  			// 2.1.dev < 2.1.dev2 < 2.1.dev3, etc.
  			// so replace devx with 0.5+x/1000
  			if (ss1[i].matches("dev.*")) {
  				try {
  					if (ss1[i].length() == 3)
  						x = 0;
  					else
  						x = Integer.parseInt(ss1[i].substring(3));
  				} catch (NumberFormatException e) {
  					x = 0;
  				}
  				ss1[i] = "" + (0.5 + x / 1000.0);
  			}
  			if (ss2[i].matches("dev.*")) {
  				try {
  					if (ss2[i].length() == 3)
  						x = 0;
  					else
  						x = Integer.parseInt(ss2[i].substring(3));
  				} catch (NumberFormatException e) {
  					x = 0;
  				}
  				ss2[i] = "" + (0.5 + x / 1000.0);
  			}
  			// replace rx (e.g. as in 4.0.alpha.r5555) with x
  			if (ss1[i].matches("r.*")) {
  				try {
  					x = Integer.parseInt(ss1[i].substring(1));
  				} catch (NumberFormatException e) {
  					x = 0;
  				}
  				ss1[i] = "" + x;
  			}
  			if (ss2[i].matches("r.*")) {
  				try {
  					x = Integer.parseInt(ss2[i].substring(1));
  				} catch (NumberFormatException e) {
  					x = 0;
  				}
  				ss2[i] = "" + x;
  			}
  			// See if strings are integers
  			try {
  				s1num = true;
  				s1 = Double.parseDouble(ss1[i]);
  			} catch (NumberFormatException e) {
  				s1num = false;
  			}
  			try {
  				s2num = true;
  				s2 = Double.parseDouble(ss2[i]);
  			} catch (NumberFormatException e) {
  				s2num = false;
  			}
  			if (s1num && s2num) {
  				if (s1 < s2)
  					return -1;
  				if (s1 > s2)
  					return 1;
  				if (s1 == s2)
  					continue;
  			}
  		}
  
  		return 0;
  	}
  
  	/*// Simple test harness for compareVersions
  	public static void main(String[] args)
  	{
  		 String v[] =  { "1", "2.0", "2.1.alpha", "2.1.alpha.r5555", "2.1.alpha.r5557", "2.1.beta", "2.1.beta4", "2.1", "2.1.dev", "2.1.dev.r6666", "2.1.dev1", "2.1.dev2", "2.1.2", "2.9", "3", "3.4"};
  		 for (int i = 0; i < v.length; i++) {
  			 for (int j = 0; j < v.length; j++) {
  				 int d = compareVersions(v[i], v[j]);
  				 System.out.print(d == 1 ? ">" : d==0 ? "=" : d==-1 ? "<" : "?");
  				 if (d != compareVersions(""+i, ""+j))
  					 System.out.print("ERR(" + v[i] + "," + v[j] + ")");
  					 
  			 }
  			 System.out.println();
  		 }
  	}*/
  
  	/**
  	 * Get access to the list of all PRISM language keywords.
  	 */
  	public static List<String> getListOfKeywords()
  	{
  		return PrismParser.getListOfKeywords();
  	}
  
  	//------------------------------------------------------------------------------
  	// Main API methods
  	//------------------------------------------------------------------------------
  
  	/**
  	 * Initialise PRISM.
  	 */
  	public void initialise() throws PrismException
  	{
  		boolean verbose = this.getSettings().getBoolean("PRISM_VERBOSE");
  		mainLog.setVerbosityLevel(verbose ? PrismLog.VL_ALL : PrismLog.VL_DEFAULT);
  		mainLog.print(getToolName() + "\n");
  		mainLog.print(new String(new char[getToolName().length()]).replace("\0", "=") + "\n");
  		mainLog.print("\nVersion: " + getVersion() + "\n");
  		mainLog.print("Date: " + new java.util.Date() + "\n");
  		try {
  			String h = java.net.InetAddress.getLocalHost().getHostName();
  			mainLog.print("Hostname: " + h + "\n");
  		} catch (java.net.UnknownHostException e) {
  		}
  		mainLog.print("Memory limits: cudd=" + getCUDDMaxMem());
  		mainLog.println(", java(heap)=" + PrismUtils.convertBytesToMemoryString(Runtime.getRuntime().maxMemory()));
  
  		// initialise cudd/jdd
  		long cuddMaxMem = PrismUtils.convertMemoryStringtoKB(getCUDDMaxMem());
  		JDD.InitialiseCUDD(cuddMaxMem, getCUDDEpsilon());
  		cuddStarted = true;
  		JDD.SetOutputStream(mainLog.getFilePointer());
  
  		// initialise libraries/engines
  		PrismNative.initialise(this);
  		PrismMTBDD.initialise(mainLog, mainLog);
  		PrismSparse.initialise(mainLog, mainLog);
  		PrismHybrid.initialise(mainLog, mainLog);
  
  		// set cudd manager in other packages
  		DoubleVector.setCUDDManager();
  		ODDUtils.setCUDDManager();
  	}
  
  	/**
  	 * Parse a PRISM model from a file.
  	 * @param file File to read in
  	 */
  	public ModulesFile parseModelFile(File file) throws FileNotFoundException, PrismLangException
  	{
  		return parseModelFile(file, null);
  	}
  
  	/**
  	 * Parse a PRISM model from a file.
  	 * @param file File to read in
  	 * @param typeOverride Optionally, override model type here (null if unused)
  	 */
  	public ModulesFile parseModelFile(File file, ModelType typeOverride) throws FileNotFoundException, PrismLangException
  	{
  		FileInputStream strModel;
  		PrismParser prismParser;
  		ModulesFile modulesFile = null;
  
  		// open file
  		strModel = new FileInputStream(file);
  
  		try {
  			// obtain exclusive access to the prism parser
  			// (don't forget to release it afterwards)
  			prismParser = getPrismParser();
  			try {
  				// parse file
  				modulesFile = prismParser.parseModulesFile(strModel, typeOverride);
  			} finally {
  				// release prism parser
  				releasePrismParser();
  			}
  		} catch (InterruptedException ie) {
  			throw new PrismLangException("Concurrency error in parser");
  		}
  
  		modulesFile.tidyUp();
  
  		return modulesFile;
  	}
  
  	/**
  	 * Parse a PRISM model from a string.
  	 * @param s String containing model
  	 */
  	public ModulesFile parseModelString(String s) throws PrismLangException
  	{
  		return parseModelString(s, null);
  	}
  
  	/**
  	 * Parse a PRISM model from a string.
  	 * @param s String containing model
  	 * @param typeOverride Optionally, override model type here (null if unused)
  	 */
  	public ModulesFile parseModelString(String s, ModelType typeOverride) throws PrismLangException
  	{
  		PrismParser prismParser;
  		ModulesFile modulesFile = null;
  
  		try {
  			// obtain exclusive access to the prism parser
  			// (don't forget to release it afterwards)
  			prismParser = getPrismParser();
  			try {
  				// parse string
  				modulesFile = prismParser.parseModulesFile(new ByteArrayInputStream(s.getBytes()), typeOverride);
  			} finally {
  				// release prism parser
  				releasePrismParser();
  			}
  		} catch (InterruptedException ie) {
  			throw new PrismLangException("Concurrency error in parser");
  		}
  
  		modulesFile.tidyUp();
  
  		return modulesFile;
  	}
  
  	/**
  	 * Import a PRISM model from a PEPA model in a file
  	 * @param file File to read in
  	 */
  	public ModulesFile importPepaFile(File file) throws PrismException, PrismLangException
  	{
  		return importModelFile("pepa", file);
  	}
  
  	/**
  	 * Import a PRISM model from a PEPA model in a string
  	 * @param s String containing model
  	 */
  	public ModulesFile importPepaString(String s) throws PrismException, PrismLangException
  	{
  		return importModelString("pepa", s);
  	}
  
  	/**
  	 * Import a PRISM model from an SBML model in a file
  	 * @param file File to read in
  	 */
  	public ModulesFile importSBMLFile(File file) throws PrismException, PrismLangException
  	{
  		return importModelFile("sbml", file);
  	}
  
  	/**
  	 * Import a PRISM model from an SBML model in a string
  	 * @param file File to read in
  	 */
  	public ModulesFile importSBMLString(String s) throws PrismException, PrismLangException
  	{
  		return importModelString("sbml", s);
  	}
  
  	/**
  	 * Import a PRISM model by translating from another language
  	 */
  	public ModulesFile importModelFile(String lang, File file) throws PrismException, PrismLangException
  	{
  		PrismLanguageTranslator importer = createPrismLanguageTranslator(lang);
  		importer.load(file);
  		String prismModelString = importer.translateToString();
  		return parseModelString(prismModelString);
  	}
  
  	/**
  	 * Import a PRISM model by translating from another language
  	 */
  	public ModulesFile importModelString(String lang, String s) throws PrismException, PrismLangException
  	{
  		PrismLanguageTranslator importer = createPrismLanguageTranslator(lang);
  		importer.load(s);
  		String prismModelString = importer.translateToString();
  		return parseModelString(prismModelString);
  	}
  
  	/**
  	 * Create a translator to the PRISM language.
  	 */
  	private PrismLanguageTranslator createPrismLanguageTranslator(String lang) throws PrismException
  	{
  		PrismLanguageTranslator importer = null;
  		switch (lang) {
  		case "pepa":
  			importer = new PEPA2Prism();
  			break;
  		case "sbml":
  			importer = new SBML2Prism();
  			break;
  		default:
  			throw new PrismException("Unknown import language \"" + lang + "\"");
  		}
  		return importer;
  	}
  
  	/**
  	 * Import a PRISM model from a PRISM preprocessor file
  	 * @param file File to read in
  	 * @param params List of values for preprocessor parameters
  	 */
  	public ModulesFile importPrismPreprocFile(File file, String params[]) throws PrismException
  	{
  		String modelString;
  
  		// Compile preprocessor file to a string
  		Preprocessor pp = new Preprocessor(this, file);
  		pp.setParameters(params);
  		modelString = pp.preprocess();
  		if (modelString == null) {
  			throw new PrismException("No preprocessing information");
  		}
  
  		// Parse string as PRISM model and return
  		return parseModelString(modelString);
  	}
  
  	/**
  	 * Parse a PRISM properties file. Typically, you need to pass in some info about the corresponding model 
  	 * (for access to constants, etc.). This is in the form of a ModelInfo object (e.g. a ModulesFile). If not required, this can be null.
  	 * @param modelInfo Accompanying model info (null if not needed)
  	 * @param file File to read in
  	 */
  	public PropertiesFile parsePropertiesFile(ModelInfo modelInfo, File file) throws FileNotFoundException, PrismLangException
  	{
  		return parsePropertiesFile(modelInfo, file, true);
  	}
  
  	/**
  	 * Parse a PRISM properties file. Typically, you need to pass in some info about the corresponding model 
  	 * (for access to constants, etc.). This is in the form of a ModelInfo object (e.g. a ModulesFile). If not required, this can be null.
  	 * You can also choose whether to do "tidy", i.e. post-parse checks and processing
  	 * (this must be done at some point but may want to postpone to allow parsing of files with errors). 
  	 * @param modelInfo Accompanying model info (null if not needed)
  	 * @param file File to read in
  	 * @param tidy Whether or not to do "tidy" (post-parse checks and processing)
  	 */
  	public PropertiesFile parsePropertiesFile(ModelInfo modelInfo, File file, boolean tidy) throws FileNotFoundException, PrismLangException
  	{
  		FileInputStream strProperties;
  		PrismParser prismParser;
  		PropertiesFile propertiesFile = null;
  
  		// open file
  		strProperties = new FileInputStream(file);
  
  		try {
  			// obtain exclusive access to the prism parser
  			// (don't forget to release it afterwards)
  			prismParser = getPrismParser();
  			try {
  				// parse file
  				propertiesFile = prismParser.parsePropertiesFile(modelInfo, strProperties);
  			} finally {
  				// release prism parser
  				releasePrismParser();
  			}
  		} catch (InterruptedException ie) {
  			throw new PrismLangException("Concurrency error in parser");
  		}
  
  		if (tidy)
  			propertiesFile.tidyUp();
  
  		return propertiesFile;
  	}
  
  	/**
  	 * Parse a PRISM properties file form a string. Typically, you need to pass in some info about the corresponding model 
  	 * (for access to constants, etc.). This is in the form of a ModelInfo object (e.g. a ModulesFile). If not required, this can be null.
  	 * @param modelInfo Accompanying model info (null if not needed)
  	 * @param s String to parse
  	 */
  	public PropertiesFile parsePropertiesString(ModelInfo modelInfo, String s) throws PrismLangException
  	{
  		PrismParser prismParser;
  		PropertiesFile propertiesFile = null;
  
  		try {
  			// obtain exclusive access to the prism parser
  			// (don't forget to release it afterwards)
  			prismParser = getPrismParser();
  			try {
  				// parse string
  				propertiesFile = prismParser.parsePropertiesFile(modelInfo, new ByteArrayInputStream(s.getBytes()));
  			} finally {
  				// release prism parser
  				releasePrismParser();
  			}
  		} catch (InterruptedException ie) {
  			throw new PrismLangException("Concurrency error in parser");
  		}
  
  		propertiesFile.tidyUp();
  
  		return propertiesFile;
  	}
  
  	/**
  	 * Parse a single PRISM expression from a string.
  	 * @param s String to parse
  	 */
  	public Expression parseSingleExpressionString(String s) throws PrismLangException
  	{
  		PrismParser prismParser;
  		Expression expr;
  
  		try {
  			// obtain exclusive access to the prism parser
  			// (don't forget to release it afterwards)
  			prismParser = getPrismParser();
  			try {
  				// parse expression
  				expr = prismParser.parseSingleExpression(new ByteArrayInputStream(s.getBytes()));
  			} finally {
  				// release prism parser
  				releasePrismParser();
  			}
  		} catch (InterruptedException ie) {
  			throw new PrismLangException("Concurrency error in parser");
  		}
  
  		return expr;
  	}
  
  	/**
  	 * Parse a for-loop (as used e.g. in preprocessor) from a string.
  	 * @param s String to parse
  	 */
  	public ForLoop parseForLoopString(String s) throws PrismLangException
  	{
  		PrismParser prismParser;
  		ForLoop fl;
  
  		try {
  			// obtain exclusive access to the prism parser
  			// (don't forget to release it afterwards)
  			prismParser = getPrismParser();
  			try {
  				// parse for loop
  				fl = prismParser.parseForLoop(new ByteArrayInputStream(s.getBytes()));
  			} finally {
  				// release prism parser
  				releasePrismParser();
  			}
  		} catch (InterruptedException ie) {
  			throw new PrismLangException("Concurrency error in parser");
  		}
  
  		return fl;
  	}
  
  	/**
  	 * Load a (parsed) PRISM model, which will be stored and used for subsequent model checking etc.
  	 * Some model constants can still be undefined at this stage.
  	 * Pass in null to clear storage of the current PRISM model.
  	 * @param modulesFile The PRISM model
  	 */
  	public void loadPRISMModel(ModulesFile modulesFile) throws PrismException
  	{
  		currentModelSource = ModelSource.PRISM_MODEL;
  		// Store PRISM model
  		currentModulesFile = modulesFile;
  		// Create a model generator for the PRISM model if appropriate - we will use that where possible
  		if (currentModulesFile.getModelType() != ModelType.PTA && currentModulesFile.getSystemDefn() == null) {
  			currentModelGenerator = new ModulesFileModelGenerator(currentModulesFile, this);
  		}
  		// Clear any existing built model(s)
  		clearBuiltModel();
  		// Reset dependent info
  		currentModelType = currentModulesFile == null ? null : currentModulesFile.getModelType();
  		currentDefinedMFConstants = null;
  		currentModel = null;
  		currentModelExpl = null;
  
  		// Print basic model info
  		mainLog.println("\nType:        " + currentModulesFile.getModelType());
  		mainLog.print("Modules:     ");
  		for (int i = 0; i < currentModulesFile.getNumModules(); i++) {
  			mainLog.print(currentModulesFile.getModuleName(i) + " ");
  		}
  		mainLog.println();
  		mainLog.print("Variables:   ");
  		for (int i = 0; i < currentModulesFile.getNumVars(); i++) {
  			mainLog.print(currentModulesFile.getVarName(i) + " ");
  		}
  		mainLog.println();
  
  		// If required, export parsed PRISM model
  		if (exportPrism) {
  			try {
  				exportPRISMModel(exportPrismFile);
  			}
  			// In case of error, just print a warning
  			catch (FileNotFoundException e) {
  				mainLog.printWarning("PRISM code export failed: Couldn't open file \"" + exportPrismFile + "\" for output");
  			} catch (PrismException e) {
  				mainLog.printWarning("PRISM code export failed: " + e.getMessage());
  			}
  		}
  	}
  
  	/**
  	 * Load a model generator, which will be stored and used for subsequent model checking etc.
  	 * Some model constants can still be undefined at this stage.
  	 * Pass in null to clear storage of the current model.
  	 * @param modelGen The model generator
  	 */
  	public void loadModelGenerator(ModelGenerator modelGen)
  	{
  		currentModelSource = ModelSource.MODEL_GENERATOR;
  		// Store model generator
  		currentModelGenerator = modelGen;
  		// Clear any existing built model(s)
  		clearBuiltModel();
  		// Reset dependent info
  		currentModelType = currentModelGenerator == null ? null : currentModelGenerator.getModelType();
  		currentDefinedMFConstants = null;
  		currentModel = null;
  		currentModelExpl = null;
  
  		// Print basic model info
  		mainLog.println("\nGenerator:   " + currentModelGenerator.getClass().getName());
  		mainLog.println("Type:        " + currentModelGenerator.getModelType());
  		// TODO: print more info 
  		//mainLog.println();
  	}
  	
  	/**
  	 * Set (some or all) undefined constants for the currently loaded PRISM model
  	 * (assuming they have changed since the last time this was called).
  	 * @param definedMFConstants The constant values
  	 */
  	public void setPRISMModelConstants(Values definedMFConstants) throws PrismException
  	{
  		if (currentDefinedMFConstants == null && definedMFConstants == null)
  			return;
  		if (currentDefinedMFConstants != null && currentDefinedMFConstants.equals(definedMFConstants))
  			return;
  
  		// Clear any existing built model(s)
  		clearBuiltModel();
  		// Store constants here and in ModulesFile
  		currentDefinedMFConstants = definedMFConstants;
  		if (currentModulesFile != null) {
  			currentModulesFile.setSomeUndefinedConstants(definedMFConstants);
  		}
  		if (currentModelGenerator != null) {
  			currentModelGenerator.setSomeUndefinedConstants(definedMFConstants);
  		}
  		// Reset dependent info
  		currentModel = null;
  		currentModelExpl = null;
  
  		// If required, export parsed PRISM model, with constants expanded
  		if (exportPrismConst) {
  			try {
  				exportPRISMModelWithExpandedConstants(exportPrismConstFile);
  			}
  			// In case of error, just print a warning
  			catch (FileNotFoundException e) {
  				mainLog.printWarning("PRISM code export failed: Couldn't open file \"" + exportPrismConstFile + "\" for output");
  			} catch (PrismException e) {
  				mainLog.printWarning("PRISM code export failed: " + e.getMessage());
  			}
  		}
  	}
  
  	/**
  	 * Load a (built) model, with an accompanying (parsed) PRISM model.
  	 * These will be stored and used for subsequent model checking etc.
  	 * Pass in nulls to clear storage of the current model.
  	 * @param modulesFile The PRISM model
  	 */
  	public void loadPRISMModelAndBuiltModel(ModulesFile modulesFile, Model model)
  	{
  		currentModelSource = ModelSource.PRISM_MODEL;
  		// Clear any existing built model(s)
  		clearBuiltModel();
  		// Store model info
  		currentModulesFile = modulesFile;
  		currentModel = model;
  		// Reset dependent info
  		currentModelType = currentModulesFile == null ? null : currentModulesFile.getModelType();
  		currentDefinedMFConstants = null;
  		currentModelExpl = null;
  	}
  
  	/**
  	 * Load a (built) model, without an accompanying (parsed) PRISM model.
  	 * The model will be stored and used for subsequent model checking etc.
  	 * Pass in null to clear storage of the current model.
  	 * @param model The built model
  	 */
  	public void loadBuiltModel(Model model)
  	{
  		currentModelSource = ModelSource.BUILT_MODEL;
  		// Clear any existing built model(s)
  		clearBuiltModel();
  		// Store model info
  		currentModulesFile = null;
  		currentModel = model;
  		// Reset dependent info
  		currentModelType = currentModel == null ? null : currentModel.getModelType();
  		currentDefinedMFConstants = null;
  		currentModelExpl = null;
  	}
  
  	/**
  	 * Load files containing an explicit list of transitions/etc. for subsequent model building.
  	 * A corresponding ModulesFile object is created and returned.
  	 * @param statesFile File containing a list of states (optional, can be null)
  	 * @param transFile File containing the list of transitions (required)
  	 * @param labelsFile File containing label definitions (optional, can be null)
  	 * @param typeOverride Type of model to be built (optional, use null if not required)
  	 */
  	public ModulesFile loadModelFromExplicitFiles(File statesFile, File transFile, File labelsFile, ModelType typeOverride) throws PrismException
  	{
  		currentModelSource = ModelSource.EXPLICIT_FILES;
  		// Clear any existing built model(s)
  		clearBuiltModel();
  		// Construct ModulesFile
  		ExplicitFiles2ModulesFile ef2mf = new ExplicitFiles2ModulesFile(this);
  		currentModulesFile = ef2mf.buildModulesFile(statesFile, transFile, typeOverride);
  		// Store explicit files info for later
  		explicitFilesStatesFile = statesFile;
  		explicitFilesTransFile = transFile;
  		explicitFilesLabelsFile = labelsFile;
  		explicitFilesNumStates = ef2mf.getNumStates();
  		// Reset dependent info
  		currentModelType = currentModulesFile == null ? null : currentModulesFile.getModelType();
  		currentDefinedMFConstants = null;
  		currentModel = null;
  		currentModelExpl = null;
  
  		return currentModulesFile;
  	}
  
  	/**
  	 * Get the type of the currently stored model.
  	 * @return
  	 */
  	public ModelType getModelType()
  	{
  		return currentModelType;
  	}
  
  	/**
  	 * Get the currently stored (parsed) PRISM model.
  	 * @return
  	 */
  	public ModulesFile getPRISMModel()
  	{
  		return currentModulesFile;
  	}
  
  	/**
  	 * Get the currently stored built (symbolic) model.
  	 * @return
  	 */
  	public Model getBuiltModel()
  	{
  		return currentModel;
  	}
  
  	/**
  	 * Get the currently stored built explicit model.
  	 * @return
  	 */
  	public explicit.Model getBuiltModelExplicit()
  	{
  		return currentModelExpl;
  	}
  
  	/**
  	 * Returns true if the current model is of a type that can be built (e.g. not a PTA).
  	 */
  	public boolean modelCanBeBuilt()
  	{
  		if (currentModelType == ModelType.PTA)
  			return false;
  		return true;
  	}
  
  	/**
  	 * Returns true if the current model has been built (for the currently selected engine).
  	 */
  	public boolean modelIsBuilt()
  	{
  		return (getExplicit() ? (currentModelExpl != null) : (currentModel != null));
  	}
  
  	/**
  	 * Build the currently loaded PRISM model and store for later use.
  	 * The built model can be accessed subsequently via either
  	 * {@link #getBuiltModel()} or {@link #getBuiltModelExplicit()},
  	 * depending on the engine currently selected.
  	 * Only call this to explicitly force a built; normally it is done automatically.
  	 */
  	public void buildModel() throws PrismException
  	{
  		mainLog.printSeparator();
  		doBuildModel();
  	}
  
  	/**
  	 * Build the currently loaded PRISM model, if it needs to be done,
  	 * i.e. if it has not been constructed yet for the current engine.
  	 */
  	public void buildModelIfRequired() throws PrismException
  	{
  		if (!modelIsBuilt())
  			doBuildModel();
  	}
  
  	/**
  	 * Build the currently loaded PRISM model and store for later use.
  	 * The built model can be accessed subsequently via either
  	 * {@link #getBuiltModel()} or {@link #getBuiltModelExplicit()},
  	 * depending on the engine currently selected.
  	 */
  	private void doBuildModel() throws PrismException
  	{
  		long l; // timer
  
  		// Clear any existing built model(s)
  		clearBuiltModel();
  
  		try {
  			if (currentModelType == ModelType.PTA) {
  				throw new PrismException("You cannot build a PTA model explicitly, only perform model checking");
  			}
  
  			mainLog.print("\nBuilding model...\n");
  			if (currentDefinedMFConstants != null && currentDefinedMFConstants.getNumValues() > 0)
  				mainLog.println("Model constants: " + currentDefinedMFConstants);
  
  			// Build model
  			l = System.currentTimeMillis();
  			switch (currentModelSource) {
  			case PRISM_MODEL:
  				if (currentModulesFile == null)
  					throw new PrismException("There is no currently loaded PRISM model to build");
  				if (!getExplicit()) {
  					Modules2MTBDD mod2mtbdd = new Modules2MTBDD(this, currentModulesFile);
  					currentModel = mod2mtbdd.translate();
  					currentModelExpl = null;
  				} else {
  					if (currentModulesFile.getSystemDefn() != null) {
  						throw new PrismNotSupportedException("Explicit engine does not currently support the system...endsystem construct");
  					}
  					ConstructModel constructModel = new ConstructModel(this);
  					constructModel.setFixDeadlocks(getFixDeadlocks());
  					currentModelExpl = constructModel.constructModel(currentModelGenerator);
  					currentModel = null;
  				}
  				// if (...) ... currentModel = buildModelExplicit(currentModulesFile);
  				break;
  			case MODEL_GENERATOR:
  				if (currentModelGenerator == null)
  					throw new PrismException("There is no currently loaded model generator to build");
  				if (!getExplicit()) {
  					mainLog.printWarning("Switching to explicit engine to use model generator");
  					setEngine(Prism.EXPLICIT);
  				}
  				ConstructModel constructModel = new ConstructModel(this);
  				constructModel.setFixDeadlocks(getFixDeadlocks());
  				currentModelExpl = constructModel.constructModel(currentModelGenerator);
  				currentModel = null;
  				// if (...) ... currentModel = buildModelExplicit(currentModulesFile);
  				break;
  			case EXPLICIT_FILES:
  				if (!getExplicit()) {
  					expf2mtbdd = new ExplicitFiles2MTBDD(this);
  					currentModel = expf2mtbdd.build(explicitFilesStatesFile, explicitFilesTransFile, explicitFilesLabelsFile, currentModulesFile,
  							explicitFilesNumStates);
  				} else {
  					throw new PrismNotSupportedException("Explicit import not yet supported for explicit engine");
  				}
  				break;
  			default:
  				throw new PrismException("Don't know how to build model from source " + currentModelSource);
  			}
  			l = System.currentTimeMillis() - l;
  			mainLog.println("\nTime for model construction: " + l / 1000.0 + " seconds.");
  
  			// For digital clocks, do some extra checks on the built model
  			if (digital) {
  				doBuildModelDigitalClocksChecks();
  			}
  
  			// Deal with deadlocks
  			if (!getExplicit()) {
  				StateList deadlocks = currentModel.getDeadlockStates();
  				int numDeadlocks = deadlocks.size();
  				if (numDeadlocks > 0) {
  					if (getFixDeadlocks()) {
  						mainLog.printWarning("Deadlocks detected and fixed in " + numDeadlocks + " states");
  					} else {
  						currentModel.printTransInfo(mainLog, getExtraDDInfo());
  						mainLog.print("\n" + numDeadlocks + " deadlock states found");
  						if (!getVerbose() && numDeadlocks > 10) {
  							mainLog.print(". The first 10 are below. Use verbose mode to view them all.\n");
  							deadlocks.print(mainLog, 10);
  						} else {
  							mainLog.print(":\n");
  							deadlocks.print(mainLog);
  						}
  						mainLog.print("\nTip: Use the \"fix deadlocks\" option to automatically add self-loops in deadlock states.\n");
  						throw new PrismException("Model contains " + numDeadlocks + " deadlock states");
  					}
  				}
  			} else {
  				explicit.StateValues deadlocks = currentModelExpl.getDeadlockStatesList();
  				int numDeadlocks = currentModelExpl.getNumDeadlockStates();
  				if (numDeadlocks > 0) {
  					if (getFixDeadlocks()) {
  						mainLog.printWarning("Deadlocks detected and fixed in " + numDeadlocks + " states");
  					} else {
  						mainLog.print(currentModelExpl.infoStringTable());
  						mainLog.print("\n" + numDeadlocks + " deadlock states found");
  						if (!getVerbose() && numDeadlocks > 10) {
  							mainLog.print(". The first 10 are below. Use verbose mode to view them all.\n");
  							deadlocks.print(mainLog, 10);
  						} else {
  							mainLog.print(":\n");
  							deadlocks.print(mainLog);
  						}
  						mainLog.print("\nTip: Use the \"fix deadlocks\" option to automatically add self-loops in deadlock states.\n");
  						throw new PrismException("Model contains " + numDeadlocks + " deadlock states");
  					}
  				}
  			}
  
  			// Print model stats
  			mainLog.println();
  			if (!getExplicit()) {
  				mainLog.println("Type:        " + currentModel.getModelType());
  				currentModel.printTransInfo(mainLog, getExtraDDInfo());
  			} else {
  				mainLog.println("Type:        " + currentModelExpl.getModelType());
  				mainLog.print(currentModelExpl.infoStringTable());
  			}
  
  			// Notify model listeners of build success
  			for (PrismModelListener listener : modelListeners) {
  				if (listener != null)
  					listener.notifyModelBuildSuccessful();
  			}
  		} catch (PrismException e) {
  			// Notify model listeners of build failure
  			for (PrismModelListener listener : modelListeners) {
  				if (listener != null)
  					listener.notifyModelBuildFailed(e);
  			}
  			// Throw exception anyway
  			throw e;
  		}
  	}
  
  	private void doBuildModelDigitalClocksChecks() throws PrismException
  	{
  		// For digital clocks, by construction, deadlocks can only occur from timelocks (and are not allowed)
  		if (!getExplicit()) {
  			StateList deadlocks = currentModel.getDeadlockStates();
  			if (deadlocks.size() > 0) {
  				throw new PrismException("Timelock in PTA, e.g. in state (" + deadlocks.getFirstAsValues() + ")");
  			}
  		} else {
  			if (currentModelExpl.getNumDeadlockStates() > 0) {
  				int dl = currentModelExpl.getFirstDeadlockState();
  				String dls = currentModelExpl.getStatesList().get(dl).toString(currentModulesFile);
  				throw new PrismException("Timelock in PTA, e.g. in state " + dls);
  			}
  		}
  
  		/*// Create new model checker object and do model checking
  		PropertiesFile pf = parsePropertiesString(currentModulesFile, "filter(exists,!\"invariants\"); E[F!\"invariants\"]");
  		if (!getExplicit()) {
  			ModelChecker mc = new NondetModelChecker(this, currentModel, pf);
  			if (((Boolean) mc.check(pf.getProperty(0)).getResult()).booleanValue()) {
  				mainLog.println(mc.check(pf.getProperty(1)).getCounterexample());
  			}
  			//sv.pr
  			//mainLog.println("XX" + res.getResult());
  		} else {
  			explicit.StateModelChecker mc = new MDPModelChecker();
  			mc.setLog(mainLog);
  			mc.setSettings(settings);
  			mc.setModulesFileAndPropertiesFile(currentModulesFile, pf);
  			explicit.StateValues sv = mc.checkExpression(currentModelExpl, pf.getProperty(0));
  			sv.print(mainLog, 1);
  		}*/
  	}
  
  	/**
  	 * Build a model from a PRISM modelling language description, storing it symbolically,
  	 * as MTBDDs) via explicit-state reachability and model construction.
  	 * It is assumed that all constants in the model file have been defined by now.  
  	 * @param modulesFile Model to build
  	 */
  	public Model buildModelExplicit(ModulesFile modulesFile) throws PrismException
  	{
  		long l; // timer
  		ConstructModel constructModel;
  		explicit.Model modelExpl;
  		Model model;
  		List<State> statesList;
  
  		if (modulesFile.getModelType() == ModelType.PTA) {
  			throw new PrismException("You cannot build a PTA model explicitly, only perform model checking");
  		}
  
  		mainLog.print("\nBuilding model...\n");
  		if (currentDefinedMFConstants != null && currentDefinedMFConstants.getNumValues() > 0)
  			mainLog.println("Model constants: " + currentDefinedMFConstants);
  
  		constructModel = new ConstructModel(this);
  		modelExpl = constructModel.constructModel(new ModulesFileModelGenerator(modulesFile, this));
  		statesList = constructModel.getStatesList();
  
  		// create Explicit2MTBDD object
  		expm2mtbdd = new ExplicitModel2MTBDD(this);
  
  		// build model
  		l = System.currentTimeMillis();
  		model = expm2mtbdd.buildModel(modelExpl, statesList, modulesFile, false);
  		l = System.currentTimeMillis() - l;
  
  		mainLog.println("\nTime for model construction: " + l / 1000.0 + " seconds.");
  
  		return model;
  	}
  
  	/**
  	 * Export the currently loaded and parsed PRISM model to a file.
  	 * @param file File to export to
  	 */
  	public void exportPRISMModel(File file) throws FileNotFoundException, PrismException
  	{
  		mainLog.print("\nExporting parsed PRISM file ");
  		mainLog.println(getDestinationStringForFile(file));
  		PrismLog tmpLog = getPrismLogForFile(file);
  		tmpLog.print(currentModulesFile.toString());
  		// tidy up
  