reintegrated fau

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6782 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/explicit/BirthProcess.java

@@ -0,0 +1,264 @@
+//==============================================================================
+//	
+//	Copyright (c) 2013-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
+//  * Frits Dannenberg <frits.dannenberg@cs.ox.ac.uk> (University of Oxford)
+//	* 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 explicit;
+
+import java.util.ArrayList;
+import prism.PrismException;
+
+/**
+ * Class to efficiently compute transient probabilities of a birth process.
+ *
+ * @author Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
+ * @author Frits Dannenberg <frits.dannenberg@cs.ox.ac.uk> (University of Oxford)
+ * @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk>  (University of Oxford)
+ */
+public class BirthProcess
+{
+	/* uniformisation rate to compute probabilities.
+	 * Must be at least as large as largest rate. */
+	double unifRate;
+	/* precision of computations using Fox-Glynn algorithm */
+	double termCritParam;
+	/* time to compute probabilities for */
+	double time;
+	/* values used to compute probability to be in a given stage */
+	double[] probs;
+	/* same as above */
+	double[] newProbs;
+	/* whether rates added by calculateNextRate will be stored */
+	boolean withRateArray;
+	ArrayList<Double> jumpRates;
+	boolean initialising;
+	/* current birth process stage */
+	int stageNr;
+	/* whether to try to avoid birth process computations in
+	 * case all rates are the same
+	 */
+	boolean avoidBirthComputation; 
+
+	/**
+	 * Construct birth process.
+	 */
+	public BirthProcess()
+	{
+		stageNr = 0;
+		termCritParam = 1E-7;
+		withRateArray = true;
+		initialising = true;
+		avoidBirthComputation = true;
+	}
+
+	/**
+	 * Sets whether rates added by calculateNextRate will be stored.
+	 * The default is to do so. Setting it to false allows to save space,
+	 * but will not allow rates larger than @a unifRate to be added.
+	 *
+	 * @param withRateArray whether to store rates in array
+	 */
+	public void setWithRateArray(boolean withRateArray)
+	{
+		if (!initialising) {
+			throw new IllegalArgumentException("this method might not be called after calculateNextRate");
+		}
+		this.withRateArray = withRateArray;
+	}
+
+	/**
+	 * Sets the time to compute probabilities for.
+	 * 
+	 * @param time time to compute probabilities for
+	 */
+	public void setTime(double time)
+	{
+		if (!initialising) {
+			throw new IllegalArgumentException("this method might not be called after calculateNextRate");
+		}
+		if (time < 0.0) {
+			throw new IllegalArgumentException("time must be nonnegative");
+		}
+		this.time = time;
+	}
+
+	/**
+	 * Sets precision to be used to compute probabilities.
+	 * 
+	 * @param termCritParam precision to be used to compute probabilities
+	 */
+	public void setTermCritParam(double termCritParam)
+	{
+		if (!initialising) {
+			throw new IllegalArgumentException("this method might not be called after calculateNextRate");
+		}
+
+		this.termCritParam = termCritParam;
+	}
+
+	/**
+	 * Chooses whether to try to avoid birth process construction.
+	 * In case all rates provided to calculateNextProb are the same, it is
+	 * possible to use the Fox-Glynn algorithm to compute probabilities in
+	 * the birth process, which is then a Poisson process. If delayBirthComputation
+	 * is true, the more expensive computations will only be computed in case
+	 * this is necessary. Thus, if calculateNextProb is called with the same
+	 * rate all the time, computations are significantly faster. 
+	 * 
+	 * @param avoidBirthComputation true iff birth process construction shall be delayed
+	 */
+	public void setAvoidBirthComputation(boolean avoidBirthComputation)
+	{
+		if (!initialising) {
+			throw new IllegalArgumentException("this method might not be called after calculateNextRate");
+		}
+		this.avoidBirthComputation = avoidBirthComputation;
+	}
+
+	/**
+	 * Computes probability to reside in next process stage at given time.
+	 * If this is the nth call to the process, computes the probability
+	 * to reside in the nth stage of the birth process. The rates of the
+	 * birth process up to the n-1th stage have been set by previous calls
+	 * to the function, the nth rate is set by the current call. The time
+	 * probabilities are computed for must have been set previously by
+	 * setTime.
+	 * 
+	 * @param rate leaving rate of current state
+	 * @return probability to reside in current stage at given time
+	 * @throws PrismException
+	 */
+	public double calculateNextProb(double rate) throws PrismException
+	{
+		if (initialising && 0.0 == unifRate && !withRateArray) {
+			throw new IllegalArgumentException("unifRate must be set if withRateArray is false");
+		}
+		if (withRateArray && initialising) {
+			jumpRates = new ArrayList<Double>();
+		}
+		initialising = false;
+		if (!withRateArray && rate > unifRate) {
+			throw new IllegalArgumentException("cannot use rates larger than initial rate if withRateArray is false");
+		}
+		if (withRateArray) {
+			jumpRates.add(rate);
+		}
+		boolean recompute = false;
+		if (rate > unifRate) {
+			if (!avoidBirthComputation) {
+				recompute = true;
+				unifRate = rate * 1.25 * 1.02;
+			} else {
+				unifRate = rate;
+			}
+		}
+		if ((jumpRates.size() != 1) && (Math.abs(rate - jumpRates.get(jumpRates.size() - 2)) > 1E-100)) {
+			if (avoidBirthComputation) {
+				recompute = true;
+			}
+			avoidBirthComputation = false;
+		}
+		
+		if (null == probs || recompute) {
+			initPoisson();
+		}
+		double result = 0.0;
+		if (recompute) {
+			for (stageNr = 0; stageNr < jumpRates.size(); stageNr++) {
+				result = compNextStageProb(jumpRates.get(stageNr));
+			}
+		} else {
+			if (avoidBirthComputation) {
+			    result = (stageNr < probs.length) ? probs[stageNr] : 0.0;
+				stageNr++;
+			} else {
+				result = compNextStageProb(rate);
+				stageNr++;
+			}
+		}
+
+		return result;
+	}
+
+	private double compNextStageProb(double rate)
+	{
+		assert(rate > 0.0);
+		double prob = rate / unifRate; // p = r / q
+		double omprob = 1.0 - prob; // 1-p
+		double result = 0.0;
+
+		double omprobtti = 1.0; // (1-p)^i
+		for (int i = 0; i < probs.length; i++) {
+			result += omprobtti * probs[i];
+			omprobtti *= omprob;
+		}
+
+		newProbs[newProbs.length - 1] = 0.0;
+		for (int i = probs.length - 1; i >= 1; i--) {
+			newProbs[i - 1] = newProbs[i] * omprob + probs[i] * prob;
+		}
+		double[] temp = probs;
+		probs = newProbs;
+		newProbs = temp;
+		return result;
+	}
+
+	/**
+	 * Initialises probability vectors by Poisson probabilities.
+	 */
+	private void initPoisson() throws PrismException
+	{
+		long left, right;
+		double qt = unifRate * time;
+		double acc = termCritParam / 8.0;
+		double[] weights;
+		double totalWeight;
+		if (unifRate * time == 0.0) {
+			left = 0;
+			right = 0;
+			totalWeight = 1.0;
+			weights = new double[1];
+			weights[0] = 1.0;
+		} else {
+			FoxGlynn fg = new FoxGlynn(qt, 1e-300, 1e+300, acc);
+			left = fg.getLeftTruncationPoint();
+			right = fg.getRightTruncationPoint();
+			if (right < 0) {
+				throw new PrismException("Overflow in Fox-Glynn computation (time bound too big?)");
+			}
+			weights = fg.getWeights();
+			totalWeight = fg.getTotalWeight();
+		}
+		for (long i = left; i <= right; i++) {
+			weights[(int) (i - left)] /= totalWeight;
+		}
+		probs = new double[(int) (right + 1)];
+		newProbs = new double[(int) (right + 1)];
+		for (long entryNr = left; entryNr <= right; entryNr++) {
+			probs[(int) entryNr] = weights[(int) (entryNr - left)];
+		}
+	}
+}

prism/src/explicit/FastAdaptiveUniformisationModelChecker.java

@@ -0,0 +1,275 @@
+//==============================================================================
+//	
+//	Copyright (c) 2013-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
+//	* 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 explicit;
+
+import parser.Values;
+import parser.ast.Expression;
+import parser.ast.ExpressionProb;
+import parser.ast.ExpressionReward;
+import parser.ast.ExpressionTemporal;
+import parser.ast.ModulesFile;
+import parser.ast.PropertiesFile;
+import parser.ast.LabelList;
+import prism.Prism;
+import prism.PrismException;
+import prism.PrismLog;
+import prism.Result;
+import simulator.PrismModelExplorer;
+import parser.ast.RewardStruct;
+
+/**
+ * CTMC model checker based on fast adaptive uniformisation.
+ */
+public class FastAdaptiveUniformisationModelChecker
+{
+	// Prism object
+	private Prism prism;
+	// Log
+	private PrismLog mainLog;
+	// Model file
+	private ModulesFile modulesFile;
+	// Properties file
+	private PropertiesFile propertiesFile;
+	// Constants from model
+	private Values constantValues;
+	// Labels from the model
+	private LabelList labelListModel;
+	// Labels from the property file
+	private LabelList labelListProp;
+	
+	/**
+	 * Constructor.
+	 */
+	public FastAdaptiveUniformisationModelChecker(Prism prism, ModulesFile modulesFile, PropertiesFile propertiesFile) throws PrismException
+	{
+		this.prism = prism;
+		mainLog = prism.getMainLog();
+		this.modulesFile = modulesFile;
+		this.propertiesFile = propertiesFile;
+
+		// Get combined constant values from model/properties
+		constantValues = new Values();
+		constantValues.addValues(modulesFile.getConstantValues());
+		if (propertiesFile != null)
+			constantValues.addValues(propertiesFile.getConstantValues());
+		this.labelListModel = modulesFile.getLabelList();
+		this.labelListProp = propertiesFile.getLabelList();
+	}
+
+	/**
+	 * Model check a property.
+	 */
+	public Result check(Expression expr) throws PrismException
+	{
+		Result res;
+		String resultString;
+		long timer;
+
+		// Starting model checking
+		timer = System.currentTimeMillis();
+
+		// Do model checking
+		res = checkExpression(expr);
+
+		// Model checking complete
+		timer = System.currentTimeMillis() - timer;
+		mainLog.println("\nModel checking completed in " + (timer / 1000.0) + " secs.");
+
+		// Print result to log
+		resultString = "Result";
+		if (!("Result".equals(expr.getResultName())))
+			resultString += " (" + expr.getResultName().toLowerCase() + ")";
+		resultString += ": " + res;
+		mainLog.print("\n" + resultString + "\n");
+
+		// Return result
+		return res;
+	}
+
+	/**
+	 * Model check an expression (used recursively).
+	 */
+	private Result checkExpression(Expression expr) throws PrismException
+	{
+		Result res;
+
+		// Current range of supported properties is quite limited...
+		if (expr instanceof ExpressionProb)
+			res = checkExpressionProb((ExpressionProb) expr);
+		else if (expr instanceof ExpressionReward)
+			res = checkExpressionReward((ExpressionReward) expr);
+		else
+			throw new PrismException("Fast adaptive uniformisation not yet supported for this operator");
+
+		return res;
+	}
+
+	/**
+	 * Model check a P operator.
+	 */
+	private Result checkExpressionProb(ExpressionProb expr) throws PrismException
+	{
+		// Check whether P=? (only case allowed)
+		if (expr.getProb() != null) {
+			throw new PrismException("Fast adaptive uniformisation model checking currently only supports P=? properties");
+		}
+
+		if (!(expr.getExpression() instanceof ExpressionTemporal)) {
+			throw new PrismException("Fast adaptive uniformisation model checking currently only supports simple path operators");
+		}
+		ExpressionTemporal exprTemp = (ExpressionTemporal) expr.getExpression();
+		if (!exprTemp.isSimplePathFormula()) {
+			throw new PrismException("Fast adaptive uniformisation window model checking currently only supports simple until operators");
+		}
+
+		double timeLower = 0.0;
+		if (exprTemp.getLowerBound() != null) {
+			timeLower = exprTemp.getLowerBound().evaluateDouble(constantValues);
+		}
+		if (exprTemp.getUpperBound() == null) {
+			throw new PrismException("Fast adaptive uniformisation window model checking currently requires an upper time bound");
+		}
+		double timeUpper = exprTemp.getUpperBound().evaluateDouble(constantValues);
+
+		if (!exprTemp.hasBounds()) {
+			throw new PrismException("Fast adaptive uniformisation window model checking currently only supports timed properties");
+		}
+
+		mainLog.println("Starting transient probability computation using fast adaptive uniformisation...");
+		PrismModelExplorer modelExplorer = new PrismModelExplorer(prism.getSimulator(), modulesFile);
+		FastAdaptiveUniformisation fau = new FastAdaptiveUniformisation(prism.getSettings(), modelExplorer);
+		fau.setConstantValues(constantValues);
+
+		Expression op1 = exprTemp.getOperand1();
+		if (op1 == null) {
+			op1 = Expression.True();
+		}
+		Expression op2 = exprTemp.getOperand2();
+		op1 = (Expression) op1.expandPropRefsAndLabels(propertiesFile, labelListModel);
+		op1 = (Expression) op1.expandPropRefsAndLabels(propertiesFile, labelListProp);
+		op2 = (Expression) op2.expandPropRefsAndLabels(propertiesFile, labelListModel);
+		op2 = (Expression) op2.expandPropRefsAndLabels(propertiesFile, labelListProp);
+		int operator = exprTemp.getOperator();
+
+		Expression sink = null;
+		Expression target = null;
+		switch (operator) {
+		case ExpressionTemporal.P_U:
+		case ExpressionTemporal.P_F:
+			sink = Expression.Not(op1);
+			break;
+		case ExpressionTemporal.P_G:
+			sink = Expression.False();
+			break;
+		case ExpressionTemporal.P_W:
+		case ExpressionTemporal.P_R:
+		default:
+			throw new PrismException("operator currently not supported for fast adaptive uniformisation");
+		}
+		
+		fau.setSink(sink);
+		fau.computeTransientProbsAdaptive(timeLower);
+		switch (operator) {
+		case ExpressionTemporal.P_U:
+		case ExpressionTemporal.P_F:
+			sink = Expression.Or(Expression.Not(op1), op2);
+			target = op2;
+			break;
+		case ExpressionTemporal.P_G:
+			sink = Expression.Not(op2);
+			target = op2;
+			break;
+		case ExpressionTemporal.P_W:
+		case ExpressionTemporal.P_R:
+		default:
+			throw new PrismException("operator currently not supported for fast adaptive uniformisation");
+		}
+		Values varValues = new Values();
+		varValues.addValue("deadlock", "true");
+		sink.replaceVars(varValues);
+		fau.setAnalysisType(FastAdaptiveUniformisation.AnalysisType.REACH);
+		fau.setSink(sink);
+		fau.setTarget(target);
+		fau.computeTransientProbsAdaptive(timeUpper - timeLower);
+		mainLog.println("\nTotal probability lost is : " + fau.getTotalDiscreteLoss());
+		mainLog.println("Maximal number of states stored during analysis : " + fau.getMaxNumStates());
+
+		return new Result(new Double(fau.getValue()));
+	}
+
+	private RewardStruct findRewardStruct(ExpressionReward expr) throws PrismException
+	{
+		RewardStruct rewStruct = null;		
+		Object rs = expr.getRewardStructIndex();
+		if (modulesFile == null)
+			throw new PrismException("No model file to obtain reward structures");
+		if (modulesFile.getNumRewardStructs() == 0)
+			throw new PrismException("Model has no rewards specified");
+		if (rs == null) {
+			rewStruct = modulesFile.getRewardStruct(0);
+		} else if (rs instanceof Expression) {
+			int i = ((Expression) rs).evaluateInt(constantValues);
+			rs = new Integer(i); // for better error reporting below
+			rewStruct = modulesFile.getRewardStruct(i - 1);
+		} else if (rs instanceof String) {
+			rewStruct = modulesFile.getRewardStructByName((String) rs);
+		}
+		if (rewStruct == null)
+			throw new PrismException("Invalid reward structure index \"" + rs + "\"");
+		return rewStruct;
+	}
+
+	/**
+	 * Model check an R operator.
+	 */
+	private Result checkExpressionReward(ExpressionReward expr) throws PrismException
+	{
+		mainLog.println("Starting transient probability computation using fast adaptive uniformisation...");
+		PrismModelExplorer modelExplorer = new PrismModelExplorer(prism.getSimulator(), modulesFile);
+		FastAdaptiveUniformisation fau = new FastAdaptiveUniformisation(prism.getSettings(), modelExplorer);
+		ExpressionTemporal temporal = (ExpressionTemporal) expr.getExpression();
+		switch (temporal.getOperator()) {
+		case ExpressionTemporal.R_I:
+			fau.setAnalysisType(FastAdaptiveUniformisation.AnalysisType.REW_INST);
+			break;
+		case ExpressionTemporal.R_C:
+			fau.setAnalysisType(FastAdaptiveUniformisation.AnalysisType.REW_CUMUL);
+			break;
+		default:
+			throw new PrismException("Currently only instantaneous or cumulative rewards are allowed.");
+		}
+		double time = temporal.getUpperBound().evaluateDouble(constantValues);
+		RewardStruct rewStruct = findRewardStruct(expr);
+		fau.setRewardStruct(rewStruct);
+		fau.setConstantValues(constantValues);
+		fau.computeTransientProbsAdaptive(time);
+		mainLog.println("\nTotal probability lost is : " + fau.getTotalDiscreteLoss());
+		mainLog.println("Maximal number of states stored during analysis : " + fau.getMaxNumStates());
+		return new Result(new Double(fau.getValue()));
+	}
+}

prism/src/explicit/ModelExplorer.java

@@ -0,0 +1,99 @@
+//==============================================================================
+//	
+//	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 explicit;
+
+import parser.State;
+import prism.PrismException;
+
+public interface ModelExplorer
+{
+	public State getDefaultInitialState() throws PrismException;
+	
+	public void queryState(State state) throws PrismException;
+	
+	public void queryState(State state, double time) throws PrismException;
+	
+	/**
+	 * Returns the current number of available choices.
+	 * @throws PrismException 
+	 */
+	public int getNumChoices() throws PrismException;
+
+	/**
+	 * Returns the current (total) number of available transitions.
+	 * @throws PrismException 
+	 */
+	public int getNumTransitions() throws PrismException;
+	
+	/**
+	 * Returns the current number of available transitions in choice i.
+	 * @throws PrismException 
+	 */
+	public int getNumTransitions(int i) throws PrismException;
+
+	/**
+	 * Get the probability/rate of a transition within a choice, specified by its index/offset.
+	 */
+	public double getTransitionProbability(int i, int offset) throws PrismException;
+
+	/**
+	 * Get the action label of a transition as a string, specified by its index/offset.
+	 * (null for asynchronous/independent transitions)
+	 * (see also {@link #getTransitionModuleOrAction(int, int)} and {@link #getTransitionModuleOrActionIndex(int, int)})
+	 * TODO: change return type to Object?
+	 * @throws PrismException 
+	 */
+	public String getTransitionAction(int i, int offset) throws PrismException;
+
+	/**
+	 * Get the action label of a transition as a string, specified by its index.
+	 * (null for asynchronous/independent transitions)
+	 * (see also {@link #getTransitionModuleOrAction(int)} and {@link #getTransitionModuleOrActionIndex(int)})
+	 * TODO: change return type to Object?
+	 * @throws PrismException 
+	 */
+	public String getTransitionAction(int index) throws PrismException;
+
+	/**
+	 * Get the probability/rate of a transition, specified by its index.
+	 */
+	public double getTransitionProbability(int i) throws PrismException;
+	
+	/**
+	 * Get the sum of probabilities/rates for transitions.
+	 */
+//	public double getTransitionProbabilitySum() throws PrismException;
+	
+	/**
+	 * Get the target (as a new State object) of a transition within a choice, specified by its index/offset.
+	 */
+	public State computeTransitionTarget(int i, int offset) throws PrismException;
+	
+	/**
+	 * Get the target of a transition (as a new State object), specified by its index.
+	 */
+	public State computeTransitionTarget(int i) throws PrismException;
+}

prism/src/prism/Prism.java

@@ -2395,8 +2395,14 @@ public class Prism implements PrismSettingsListener
 			return modelCheckPTA(propertiesFile, prop.getExpression(), definedPFConstants);
 		}
 
+		// For fast adaptive uniformisation
+		if (currentModelType == ModelType.CTMC && settings.getString(PrismSettings.PRISM_TRANSIENT_METHOD).equals("Fast adaptive uniformisation")) {
+			FastAdaptiveUniformisationModelChecker fauMC;
+			fauMC = new FastAdaptiveUniformisationModelChecker(this, currentModulesFile, propertiesFile);
+			return fauMC.check(prop.getExpression());
+		}
 		// Auto-switch engine if required
-		if (currentModelType == ModelType.MDP && !Expression.containsMultiObjective(prop.getExpression())) {
+		else if (currentModelType == ModelType.MDP && !Expression.containsMultiObjective(prop.getExpression())) {
 			if (getMDPSolnMethod() != Prism.MDP_VALITER && !getExplicit()) {
 				mainLog.printWarning("Switching to explicit engine to allow use of chosen MDP solution method.");
 				engineSwitch = true;
@@ -2782,7 +2788,16 @@ public class Prism implements PrismSettingsListener
 
 		l = System.currentTimeMillis();
 
-		if (!getExplicit()) {
+		if (currentModelType == ModelType.CTMC && settings.getString(PrismSettings.PRISM_TRANSIENT_METHOD).equals("Fast adaptive uniformisation")) {
+			PrismModelExplorer modelExplorer = new PrismModelExplorer(getSimulator(), currentModulesFile);
+			FastAdaptiveUniformisation fau = new FastAdaptiveUniformisation(settings, modelExplorer);
+			fau.setConstantValues(currentModulesFile.getConstantValues());
+			mainLog.println("Starting transient probability computation using fast adaptive uniformisation...");
+			probsExpl = fau.doTransient(time, fileIn);
+			mainLog.println("\nTotal probability lost is : " + fau.getTotalDiscreteLoss());
+			mainLog.println("Maximal number of states stored during analysis : " + fau.getMaxNumStates());
+		}
+		else if (!getExplicit()) {
 			if (currentModelType == ModelType.DTMC) {
 				mc = new ProbModelChecker(this, currentModel, null);
 				probs = ((ProbModelChecker) mc).doTransient((int) time, fileIn);

prism/src/prism/PrismSettings.java

@@ -97,6 +97,7 @@ public class PrismSettings implements Observer
 	public static final String PRISM_SCC_METHOD						= "prism.sccMethod";
 	public static final String PRISM_SYMM_RED_PARAMS					= "prism.symmRedParams";
 	public static final String PRISM_PTA_METHOD					= "prism.ptaMethod";
+	public static final String PRISM_TRANSIENT_METHOD				= "prism.transientMethod";
 	public static final String PRISM_AR_OPTIONS					= "prism.arOptions";
 	public static final String PRISM_EXPORT_ADV					= "prism.exportAdv";
 	public static final String PRISM_EXPORT_ADV_FILENAME			= "prism.exportAdvFilename";
@@ -156,6 +157,11 @@ public class PrismSettings implements Observer
 	public static final	String LOG_BG_COLOUR						= "log.bgColour";
 	public static final	String LOG_BUFFER_LENGTH					= "log.bufferLength";
 	
+	//FAU
+	public static final String PRISM_FAU_DELTA						= "prism.faudelta";
+	public static final String PRISM_FAU_INTERVALS					= "prism.fauintervals";
+	public static final String PRISM_FAU_INITIVAL					= "prism.fauinitival";
+	public static final String PRISM_FAU_ARRAYTHRESHOLD				= "prism.fauarraythreshold";
 	
 	//Defaults, types and constaints
 	
@@ -165,7 +171,8 @@ public class PrismSettings implements Observer
 		"Simulator",
 		"Model",
 		"Properties",
-		"Log"
+		"Log",
+		"FAU"
 	};
 	public static final int[] propertyOwnerIDs =
 	{
@@ -173,7 +180,8 @@ public class PrismSettings implements Observer
 		PropertyConstants.SIMULATOR,
 		PropertyConstants.MODEL,
 		PropertyConstants.PROPERTIES,
-		PropertyConstants.LOG
+		PropertyConstants.LOG,
+		PropertyConstants.FAU		
 	};
 	
 	
@@ -198,6 +206,8 @@ public class PrismSettings implements Observer
 																			"Which engine (hybrid, sparse, MTBDD, explicit) should be used for model checking." },
 			{ CHOICE_TYPE,		PRISM_PTA_METHOD,						"PTA model checking method",			"3.3",			"Stochastic games",																	"Digital clocks,Stochastic games",																
 																			"Which method to use for model checking of PTAs." },
+			{ CHOICE_TYPE,		PRISM_TRANSIENT_METHOD,					"Transient probability computation method",	"3.3",		"Uniformisation",															"Uniformisation,Fast adaptive uniformisation",																
+																			"Which method to use for computing transient probabilities in CTMCs." },
 			// NUMERICAL SOLUTION OPTIONS:
 			{ CHOICE_TYPE,		PRISM_LIN_EQ_METHOD,					"Linear equations method",				"2.1",			"Jacobi",																	"Power,Jacobi,Gauss-Seidel,Backwards Gauss-Seidel,Pseudo-Gauss-Seidel,Backwards Pseudo-Gauss-Seidel,JOR,SOR,Backwards SOR,Pseudo-SOR,Backwards Pseudo-SOR",
 																			"Which iterative method to use when solving linear equation systems." },
@@ -327,6 +337,12 @@ public class PrismSettings implements Observer
 			{ FONT_COLOUR_TYPE,	LOG_FONT,								"Display font",							"2.1",			new FontColorPair(new Font("monospaced", Font.PLAIN, 12), Color.black),		"",																							"Font used for the log display." },
 			{ COLOUR_TYPE,		LOG_BG_COLOUR,							"Background colour",					"2.1",			new Color(255,255,255),														"",																							"Background colour for the log display." },
 			{ INTEGER_TYPE,		LOG_BUFFER_LENGTH,						"Buffer length",						"2.1",			new Integer(10000),															"1,",																						"Length of the buffer for the log display." }
+		},
+		{
+			{ DOUBLE_TYPE,      PRISM_FAU_DELTA,					"Cut off delta", 						"4.0.1",   	 	new Double(10E-12),     													"",																							"States which get a probability below this number during the fast adaptive analysis will be removed." },
+			{ INTEGER_TYPE,     PRISM_FAU_ARRAYTHRESHOLD,			"Threshold to swap to array mode", 		"4.0.1",   	 	new Integer(100),    	 													"",																							"If this number of iterations happened during fast adaptive uniformisation without changes to the state space, assume that further changes are unlikely." },
+			{ INTEGER_TYPE,     PRISM_FAU_INTERVALS,				"Number of time intervals",				"4.0.1",   	 	new Integer(1),     														"",																							"Splits the time of a time-bounded property into the specified number of intervals." },
+			{ DOUBLE_TYPE,      PRISM_FAU_INITIVAL,					"Length of initial time interval",		"4.0.1",   	 	new Double(1.0),     														"",																							"Length of initial time interval in addition to regular time intervals." },
 		}
 	};
 	
@@ -781,6 +797,20 @@ public class PrismSettings implements Observer
 				throw new PrismException("No parameter specified for -" + sw + " switch");
 			}
 		}
+		// Transient methods
+		else if (sw.equals("transientmethod")) {
+			if (i < args.length - 1) {
+				s = args[++i];
+				if (s.equals("unif"))
+					set(PRISM_TRANSIENT_METHOD, "Uniformisation");
+				else if (s.equals("fau"))
+					set(PRISM_TRANSIENT_METHOD, "Fast adaptive uniformisation");
+				else
+					throw new PrismException("Unrecognised option for -" + sw + " switch (options are: unif, fau)");
+			} else {
+				throw new PrismException("No parameter specified for -" + sw + " switch");
+			}
+		}
 
 		// NUMERICAL SOLUTION OPTIONS:
 		
@@ -1114,6 +1144,68 @@ public class PrismSettings implements Observer
 			}
 		}
 		
+		// Fast Adaptive Uniformisation
+		
+		// Delta for fast adaptive uniformisation
+		else if (sw.equals("faudelta")) {
+			if (i < args.length - 1) {
+				try {
+					d = Double.parseDouble(args[++i]);
+					if (d < 0)
+						throw new NumberFormatException("");
+					set(PRISM_FAU_DELTA, d);
+				} catch (NumberFormatException e) {
+					throw new PrismException("Invalid value for -" + sw + " switch");
+				}
+			} else {
+				throw new PrismException("No value specified for -" + sw + " switch");
+			}
+		}
+		else if (sw.equals("fauarraythreshold")) {
+			if (i < args.length - 1) {
+				try {
+					j = Integer.parseInt(args[++i]);
+					if (j < 0)
+						throw new NumberFormatException("");
+					set(PRISM_FAU_ARRAYTHRESHOLD, j);
+				} catch (NumberFormatException e) {
+					throw new PrismException("Invalid value for -" + sw + " switch");
+				}
+			} else {
+				throw new PrismException("No value specified for -" + sw + " switch");
+			}			
+		}
+
+		// number of intervals for fast adaptive uniformisation
+		else if (sw.equals("fauintervals")) {
+			if (i < args.length - 1) {
+				try {
+					j = Integer.parseInt(args[++i]);
+					if (j < 0)
+						throw new NumberFormatException("");
+					set(PRISM_FAU_INTERVALS, j);
+				} catch (NumberFormatException e) {
+					throw new PrismException("Invalid value for -" + sw + " switch");
+				}
+			} else {
+				throw new PrismException("No value specified for -" + sw + " switch");
+			}
+		}
+		else if (sw.equals("fauinitival")) {
+			if (i < args.length - 1) {
+				try {
+					d = Double.parseDouble(args[++i]);
+					if (d < 0.0)
+						throw new NumberFormatException("");
+					set(PRISM_FAU_INITIVAL, d);
+				} catch (NumberFormatException e) {
+					throw new PrismException("Invalid value for -" + sw + " switch");
+				}
+			} else {
+				throw new PrismException("No value specified for -" + sw + " switch");
+			}
+		}
+
 		// unknown switch - error
 		else {
 			throw new PrismException("Invalid switch -" + sw + " (type \"prism -help\" for full list)");
@@ -1135,6 +1227,7 @@ public class PrismSettings implements Observer
 		mainLog.println("-hybrid (or -h) ................ Use the Hybrid engine [default]");
 		mainLog.println("-explicit (or -ex) ............. Use the explicit engine");
 		mainLog.println("-ptamethod <name> .............. Specify PTA engine (games, digital) [default: games]");
+		mainLog.println("-transientmethod <name> ........ CTMC transient analysis methof (unif, fau) [default: unif]");
 		mainLog.println();
 		mainLog.println("SOLUTION METHODS (LINEAR EQUATIONS):");
 		mainLog.println("-power (or -pow, -pwr) ......... Use the Power method for numerical computation");
@@ -1198,6 +1291,12 @@ public class PrismSettings implements Observer
 		mainLog.println("-gsmax <n> (or sormax <n>) ..... Set memory limit (KB) for hybrid GS/SOR [default: 1024]");
 		mainLog.println("-cuddmaxmem <n> ................ Set max memory for CUDD package (KB) [default: 200x1024]");
 		mainLog.println("-cuddepsilon <x> ............... Set epsilon value for CUDD package [default: 1e-15]");
+		mainLog.println();
+		mainLog.println("FAST ADAPTIVE UNIFORMISATION OPTIONS:");
+		mainLog.println("-faudelta <x> .................. Set probability threshold for irrelevant states [default: 1e-12]");
+		mainLog.println("-fauarraythreshold <x> ......... Set threshold when to switch to sparse matrix [default: 100]");
+		mainLog.println("-fauintervals <x> .............. Set number of intervals to divide time intervals to [default: 1]");
+		mainLog.println("-fauinitival <x> ............... Set length of additional initial time interval [default: 1.0]");
 	}
 
 	/**

prism/src/prism/PropertyConstants.java

@@ -43,8 +43,9 @@ public final class PropertyConstants
 	public static final int PROPERTIES = 11;
 	public static final int SIMULATOR = 12;
 	public static final int LOG = 13;
-	public static final int SSHHOST = 14;
-	public static final int FILESYSTEM = 15;
-	public static final int NETWORK_PROFILE = 16;
-	public static final int GRAPH_DISPLAY = 17;
+	public static final int FAU = 14;
+	public static final int SSHHOST = 15;
+	public static final int FILESYSTEM = 16;
+	public static final int NETWORK_PROFILE = 17;
+	public static final int GRAPH_DISPLAY = 18;
 }

prism/src/simulator/PrismModelExplorer.java

@@ -0,0 +1,125 @@
+//==============================================================================
+//	
+//	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 parser.State;
+import parser.ast.ModulesFile;
+import prism.PrismException;
+import explicit.ModelExplorer;
+
+public class PrismModelExplorer implements ModelExplorer
+{
+	private SimulatorEngine simEngine;
+	private ModulesFile modulesFile;
+
+	public PrismModelExplorer(SimulatorEngine simEngine, ModulesFile modulesFile) throws PrismException
+	{
+		this.simEngine = simEngine;
+		this.modulesFile = modulesFile;
+		simEngine.createNewOnTheFlyPath(modulesFile);
+
+	}
+
+	@Override
+	public State getDefaultInitialState() throws PrismException
+	{
+		return modulesFile.getDefaultInitialState();
+	}
+	
+	@Override
+	public void queryState(State state) throws PrismException
+	{
+		simEngine.initialisePath(state);
+	}
+
+	@Override
+	public void queryState(State state, double time) throws PrismException
+	{
+		queryState(state);
+	}
+
+	@Override
+	public int getNumChoices() throws PrismException
+	{
+		return simEngine.getNumChoices();
+	}
+	
+	@Override
+	public int getNumTransitions() throws PrismException
+	{
+		return simEngine.getNumTransitions();
+	}
+	
+	@Override
+	public int getNumTransitions(int i) throws PrismException
+	{
+		return simEngine.getNumTransitions(i);
+	}
+	
+	@Override
+	public String getTransitionAction(int i, int offset) throws PrismException
+	{
+		return simEngine.getTransitionAction(i, offset);
+	}
+	
+	@Override
+	public String getTransitionAction(int i) throws PrismException
+	{
+		return simEngine.getTransitionAction(i);
+	}
+	
+	@Override
+	public double getTransitionProbability(int i, int offset) throws PrismException
+	{
+		return simEngine.getTransitionProbability(i, offset);
+	}
+	
+	@Override
+	public double getTransitionProbability(int i) throws PrismException
+	{
+		return simEngine.getTransitionProbability(i);
+	}
+	
+	/*
+	@Override
+	public double getTransitionProbabilitySum() throws PrismException
+	{
+		return simEngine.getTransitionProbabilitySum();
+	}
+	*/
+	
+	@Override
+	public State computeTransitionTarget(int i, int offset) throws PrismException
+	{
+		return simEngine.computeTransitionTarget(i, offset);
+	}
+
+	@Override
+	public State computeTransitionTarget(int i) throws PrismException
+	{
+		return simEngine.computeTransitionTarget(i);
+	}
+}