Further work on simulator, including sampling.

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

prism/src/simulator/Makefile

@@ -12,7 +12,7 @@
 THIS_DIR = simulator
 PRISM_DIR_REL = ../..
 
-JAVA_FILES = $(wildcard *.java networking/*.java)
+JAVA_FILES = $(wildcard *.java sampler/*.java networking/*.java)
 CLASS_FILES = $(JAVA_FILES:%.java=$(PRISM_DIR_REL)/$(CLASSES_DIR)/$(THIS_DIR)/%.class)
 
 default: all

prism/src/simulator/Path.java → prism/src/simulator/PathFull.java

@@ -36,8 +36,10 @@ import prism.PrismLog;
 
 /**
  * Stores and manipulates a path though a model.
+ * The full path is stored, i.e. all info at all steps.
+ * State objects and arrays are copied for storage.
  */
-public class Path
+public class PathFull extends Path
 {
 	class Step
 	{
@@ -74,57 +76,10 @@ public class Path
 	protected double totalStateReward[];
 	protected double totalTransitionReward[];
 
-	// ACCESSORS
-
-	public int size()
-	{
-		return size;
-	}
-
-	public State getState(int step)
-	{
-		return path.get(step).state;
-	}
-
-	public double getStateReward(int step, int i)
-	{
-		return path.get(step).stateRewards[i];
-	}
-
-	public State getCurrentState()
-	{
-		return getState(size - 1);
-	}
-
-	public double getTime(int i)
-	{
-		return path.get(i).time;
-	}
-
-	public double getCumulativeTime(int i)
-	{
-		return path.get(i).timeCumul;
-	}
-
-	public int getChoice(int i)
-	{
-		return path.get(i).choice;
-	}
-
-	public String getAction(int i)
-	{
-		return path.get(i).action;
-	}
-
-	public double getTransitionReward(int i, int j)
-	{
-		return path.get(i).transitionRewards[j];
-	}
-
 	/**
-	 * Constructor: creates a new (empty) Path object for a specific model.
+	 * Constructor: creates a new (empty) PathFull object for a specific model.
 	 */
-	public Path(SimulatorEngine engine, ModulesFile modulesFile)
+	public PathFull(SimulatorEngine engine, ModulesFile modulesFile)
 	{
 		// Store ptr to engine
 		this.engine = engine;
@@ -141,7 +96,7 @@ public class Path
 	}
 
 	/**
-	 * Clear the path
+	 * Clear the path.
 	 */
 	protected void clear()
 	{
@@ -155,9 +110,9 @@ public class Path
 		}
 	}
 
-	/**
-	 * Initialise the path with an initial state and rewards.
-	 */
+	// MUTATORS (for Path)
+
+	@Override
 	public void initialise(State initialState, double[] initialStateRewards)
 	{
 		clear();
@@ -173,17 +128,20 @@ public class Path
 
 	/**
 	 * Add a step to the path.
+	 * The passed in State object and arrays (of rewards) will be copied to store in the path.
 	 */
+	@Override
 	public void addStep(int choice, String action, double[] transRewards, State newState, double[] newStateRewards)
 	{
 		addStep(0, choice, action, transRewards, newState, newStateRewards);
 	}
 
 	/**
-	 * Add a (timed) step to the path.
+	 * Add a timed step to the path.
+	 * The passed in State object and arrays (of rewards) will be copied to store in the path.
 	 */
-	public void addStep(double time, int choice, String action, double[] transRewards, State newState,
-			double[] newStateRewards)
+	@Override
+	public void addStep(double time, int choice, String action, double[] transRewards, State newState, double[] newStateRewards)
 	{
 		Step step;
 		// Add info to last existing step
@@ -204,17 +162,111 @@ public class Path
 		// Add (copies of) new state and state rewards to new step
 		step.state = new State(newState);
 		step.stateRewards = newStateRewards.clone();
+		// Update totals
+		totalTime += time;
+	}
+
+	// ACCESSORS (for Path)
+
+	@Override
+	public int size()
+	{
+		return size;
+	}
+
+	@Override
+	public State getPreviousState()
+	{
+		return path.get(path.size() - 2).state;
+	}
+
+	@Override
+	public State getCurrentState()
+	{
+		return path.get(path.size() - 1).state;
+	}
+
+	@Override
+	public double getTimeSoFar()
+	{
+		return totalTime;
+	}
+
+	@Override
+	public double getTimeInPreviousState()
+	{
+		return path.get(path.size() - 2).time;
+	}
+
+	@Override
+	public double getRewardCumulatedSoFar(int index)
+	{
+		return totalReward[index];
+	}
+	
+	@Override
+	public double getPreviousStateReward(int index)
+	{
+		return path.get(path.size() - 2).stateRewards[index];
+	}
+	
+	@Override
+	public double getPreviousTransitionReward(int index)
+	{
+		return path.get(path.size() - 2).transitionRewards[index];
+	}
+	
+	@Override
+	public double getCurrentStateReward(int index)
+	{
+		return path.get(path.size() - 1).stateRewards[index];
+	}
+	
+	// ACCESSORS (additional)
+
+	public State getState(int step)
+	{
+		return path.get(step).state;
+	}
+
+	public double getStateReward(int step, int i)
+	{
+		return path.get(step).stateRewards[i];
+	}
+
+	public double getTime(int i)
+	{
+		return path.get(i).time;
+	}
+
+	public double getCumulativeTime(int i)
+	{
+		return path.get(i).timeCumul;
+	}
+
+	public int getChoice(int i)
+	{
+		return path.get(i).choice;
+	}
+
+	public String getAction(int i)
+	{
+		return path.get(i).action;
+	}
+
+	public double getTransitionReward(int i, int j)
+	{
+		return path.get(i).transitionRewards[j];
 	}
 
 	/**
-	 * Exports path to a file.
+	 * Export path to a file.
 	 * @param log: PrismLog to which the path should be exported to.
 	 * @param timeCumul: Show time in cumulative form?
 	 * @param colSep: String used to separate columns in display
 	 * @param vars: Restrict printing to these variables (indices) and steps which change them (ignore if null)
 	 */
-	public void exportToLog(PrismLog log, boolean timeCumul, String colSep, ArrayList<Integer> vars)
-			throws PrismException
+	public void exportToLog(PrismLog log, boolean timeCumul, String colSep, ArrayList<Integer> vars) throws PrismException
 	{
 		int i, j, n, nv;
 		double d, t;
@@ -304,9 +356,7 @@ public class Path
 		log.close();
 	}
 
-	/**
-	 * Generate string representation.
-	 */
+	@Override
 	public String toString()
 	{
 		int i;

prism/src/simulator/PathOnTheFly.java

@@ -0,0 +1,198 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package simulator;
+
+import parser.*;
+import parser.ast.*;
+
+/**
+ * Stores and manipulates a path though a model.
+ * Minimal info is stored - just enough to allow checking of properties.
+ * State objects and arrays are just stored as references to existing objects, but never modified.
+ * TODO: decide whether to copy states (we already copy rewards actually)
+ */
+public class PathOnTheFly extends Path
+{
+	// Parent simulator engine
+	protected SimulatorEngine engine;
+	// Model to which the path corresponds
+	protected ModulesFile modulesFile;
+	// Does model use continuous time?
+	protected boolean continuousTime;
+	// Model info/stats
+	protected int numRewardStructs;
+
+	// Path info required to implement Path abstract class:
+	protected int size;
+	protected State previousState;
+	protected State currentState;
+	protected double totalTime;
+	double timeInPreviousState;
+	protected double totalRewards[];
+	protected double previousStateRewards[];
+	protected double previousTransitionRewards[];
+	protected double currentStateRewards[];
+	
+	/**
+	 * Constructor: creates a new (empty) PathOnTheFly object for a specific model.
+	 */
+	public PathOnTheFly(SimulatorEngine engine, ModulesFile modulesFile)
+	{
+		// Store ptr to engine
+		this.engine = engine;
+		// Store model and info
+		this.modulesFile = modulesFile;
+		continuousTime = modulesFile.getModelType().continuousTime();
+		numRewardStructs = modulesFile.getNumRewardStructs();
+		// Create arrays to store totals
+		totalRewards = new double[numRewardStructs];
+		previousStateRewards = new double[numRewardStructs];
+		previousTransitionRewards = new double[numRewardStructs];
+		currentStateRewards = new double[numRewardStructs];
+		// Initialise path info
+		clear();
+	}
+
+	/**
+	 * Clear the path.
+	 */
+	protected void clear()
+	{
+		// Initialise all path info
+		size = 0;
+		previousState = null;
+		currentState = null;
+		totalTime = 0.0;
+		timeInPreviousState = 0.0;
+		for (int i = 0; i < numRewardStructs; i++) {
+			totalRewards[i] = 0.0;
+			previousStateRewards[i] = 0.0;
+			previousTransitionRewards[i] = 0.0;
+			currentStateRewards[i] = 0.0;
+		}
+	}
+
+	// MUTATORS (for Path)
+
+	@Override
+	public void initialise(State initialState, double[] initialStateRewards)
+	{
+		clear();
+		currentState = initialState;
+		currentStateRewards = initialStateRewards;
+	}
+
+	/**
+	 * Add a step to the path.
+	 * The passed in State object and arrays (of rewards) will be stored as references, but never modified.
+	 */
+	@Override
+	public void addStep(int choice, String action, double[] transRewards, State newState, double[] newStateRewards)
+	{
+		addStep(0, choice, action, transRewards, newState, newStateRewards);
+	}
+
+	/**
+	 * Add a timed step to the path.
+	 * The passed in State object and arrays (of rewards) will be stored as references, but never modified.
+	 */
+	@Override
+	public void addStep(double time, int choice, String action, double[] transRewards, State newState, double[] newStateRewards)
+	{
+		size = 0;
+		previousState = currentState;
+		currentState = newState;
+		totalTime += time;
+		timeInPreviousState = time;
+		for (int i = 0; i < numRewardStructs; i++) {
+			if (continuousTime) {
+				totalRewards[i] += currentStateRewards[i] * time + transRewards[i];
+			} else {
+				totalRewards[i] += currentStateRewards[i] + transRewards[i];
+			}
+			previousStateRewards[i] = currentStateRewards[i];
+			previousTransitionRewards[i] = transRewards[i];
+			currentStateRewards[i] = newStateRewards[i];
+		}
+	}
+
+	// ACCESSORS (for Path)
+
+	@Override
+	public int size()
+	{
+		return size;
+	}
+
+	@Override
+	public State getPreviousState()
+	{
+		return previousState;
+	}
+
+	@Override
+	public State getCurrentState()
+	{
+		return currentState;
+	}
+
+	@Override
+	public double getTimeSoFar()
+	{
+		return totalTime;
+	}
+
+	@Override
+	public double getTimeInPreviousState()
+	{
+		return timeInPreviousState;
+	}
+
+	@Override
+	public double getRewardCumulatedSoFar(int index)
+	{
+		return totalRewards[index];
+	}
+	
+	@Override
+	public double getPreviousStateReward(int index)
+	{
+		return previousStateRewards[index];
+	}
+	
+	@Override
+	public double getPreviousTransitionReward(int index)
+	{
+		return previousTransitionRewards[index];
+	}
+	
+	@Override
+	public double getCurrentStateReward(int index)
+	{
+		return currentStateRewards[index];
+	}
+}

prism/src/simulator/SimulatorEngine.java

@@ -30,6 +30,7 @@ package simulator;
 import java.util.*;
 import java.io.*;
 
+import simulator.sampler.*;
 import parser.*;
 import parser.ast.*;
 import parser.type.*;
@@ -152,9 +153,6 @@ import prism.*;
  * @author Andrew Hinton
  */
 
-// REMOVED:
-// exportBinary functions
-
 public class SimulatorEngine
 {
 	// PRISM stuff
@@ -173,7 +171,9 @@ public class SimulatorEngine
 
 	// Properties info
 	private PropertiesFile propertiesFile;
-	private List<ExpressionTemporal> pathProps;
+	private List<Expression> properties;
+	private List<Sampler> propertySamplers;
+
 	private Values propertyConstants;
 	private ArrayList loadedProperties;
 
@@ -188,15 +188,14 @@ public class SimulatorEngine
 	// NEW STUFF:
 	protected boolean onTheFly;
 
-	protected State lastState;
+	protected State previousState;
 	protected State currentState;
 	protected double currentStateRewards[];
 
 	// PATH:
-	protected Path path = null;
+	protected PathFull path = null;
 	// TRANSITIONS:
 
-
 	protected List<Expression> labels;
 
 	// ------------------------------------------------------------------------------
@@ -243,7 +242,6 @@ public class SimulatorEngine
 	// Current model
 	private Values constants;
 
-
 	// ------------------------------------------------------------------------------
 	// Basic setup
 	// ------------------------------------------------------------------------------
@@ -262,7 +260,8 @@ public class SimulatorEngine
 		propertiesFile = null;
 		constants = null;
 		propertyConstants = null;
-		loadedProperties = null;
+		properties = null;
+		propertySamplers = null;
 	}
 
 	/**
@@ -298,7 +297,7 @@ public class SimulatorEngine
 		this.propertiesFile = (propertiesFile == null) ? new PropertiesFile(modulesFile) : propertiesFile;
 		propertyConstants = this.propertiesFile.getConstantValues();
 		// Create empty path object associated with this model
-		path = new Path(this, modulesFile);
+		path = new PathFull(this, modulesFile);
 		// This is not on-the-fly
 		onTheFly = false;
 	}
@@ -349,6 +348,9 @@ public class SimulatorEngine
 		// Initialise stored path if necessary
 		if (!onTheFly)
 			path.initialise(currentState, currentStateRewards);
+		// Reset and then update samplers for any loaded properties
+		resetSamplers();
+		updateSamplers();
 		// Generate updates for initial state 
 		updater.calculateTransitions(currentState, transitionList);
 	}
@@ -566,12 +568,7 @@ public class SimulatorEngine
 	 */
 	public int addLabel(Expression label) throws PrismLangException
 	{
-		// Take a copy, get rid of any constants and simplify
-		Expression labelNew = label.deepCopy();
-		labelNew = (Expression) labelNew.replaceConstants(constants);
-		labelNew = (Expression) labelNew.simplify();
-		labels.add(labelNew);
-		return labels.size() - 1;
+		return addLabel(label, null);
 	}
 
 	/**
@@ -585,8 +582,11 @@ public class SimulatorEngine
 		// Take a copy, get rid of any constants and simplify
 		Expression labelNew = label.deepCopy();
 		labelNew = (Expression) labelNew.replaceConstants(constants);
-		labelNew = (Expression) labelNew.replaceConstants(pf.getConstantValues());
+		if (pf != null) {
+			labelNew = (Expression) labelNew.replaceConstants(pf.getConstantValues());
+		}
 		labelNew = (Expression) labelNew.simplify();
+		// Add to list and return index
 		labels.add(labelNew);
 		return labels.size() - 1;
 	}
@@ -594,13 +594,32 @@ public class SimulatorEngine
 	/**
 	 * Add a (path) property to the simulator, whose value will be computed during path generation.
 	 * The resulting index of the property is returned: this is used for later queries about the property.
+	 * Any constants/formulas etc. appearing in the label must have been defined in the current model.
+	 * If there are additional constants (e.g. from a properties file),
+	 * then use the {@link #addProperty(Expression, PropertiesFile)} method. 
 	 */
-	private int addProperty(Expression prop)
+	public int addProperty(Expression prop) throws PrismException
 	{
-		// clone, converttountil, simplify ???
-		
-		// TODO
-		return -1;
+		return addProperty(prop, null);
+	}
+
+	/**
+	 * Add a (path) property to the simulator, whose value will be computed during path generation.
+	 * The resulting index of the property is returned: this is used for later queries about the property.
+	 * Any constants/formulas etc. appearing in the property must have been defined in the current model
+	 * or be supplied in the (optional) passed in PropertiesFile.
+	 */
+	public int addProperty(Expression prop, PropertiesFile pf) throws PrismException
+	{
+		// Take a copy, get rid of any constants and simplify
+		Expression propNew = prop.deepCopy();
+		propNew = (Expression) propNew.replaceConstants(constants);
+		propNew = (Expression) propNew.replaceConstants(pf.getConstantValues());
+		propNew = (Expression) propNew.simplify();
+		// Create sampler, update lists and return index
+		properties.add(propNew);
+		propertySamplers.add(Sampler.createSampler(propNew, modulesFile));
+		return properties.size() - 1;
 	}
 
 	/**
@@ -692,9 +711,9 @@ public class SimulatorEngine
 		// Evaluate constants and optimise (a copy of) modules file for simulation
 		modulesFile = (ModulesFile) modulesFile.deepCopy().replaceConstants(constants).simplify();
 		mainLog.println(modulesFile);
-		
+
 		// Create state/transition storage
-		lastState = new State(numVars);
+		previousState = new State(numVars);
 		currentState = new State(numVars);
 		currentStateRewards = new double[modulesFile.getNumRewardStructs()];
 		transitionList = new TransitionList();
@@ -702,8 +721,10 @@ public class SimulatorEngine
 		// Create updater for model
 		updater = new Updater(this, modulesFile);
 
-		// Create storage for labels
+		// Create storage for labels/properties
 		labels = new ArrayList<Expression>();
+		properties = new ArrayList<Expression>();
+		propertySamplers = new ArrayList<Sampler>();
 	}
 
 	/**
@@ -720,8 +741,8 @@ public class SimulatorEngine
 		// Get corresponding choice
 		Choice choice = transitionList.getChoice(i);
 		// Remember last state and compute next one (and its state rewards)
-		lastState.copy(currentState);
-		choice.computeTarget(offset, lastState, currentState);
+		previousState.copy(currentState);
+		choice.computeTarget(offset, previousState, currentState);
 		updater.calculateStateRewards(currentState, currentStateRewards);
 		// Store path info (if necessary)
 		if (!onTheFly) {
@@ -730,6 +751,8 @@ public class SimulatorEngine
 			path.addStep(index, choice.getAction(), currentStateRewards, currentState, currentStateRewards);
 			// TODO: first currentStateRewards in above should be new *trans* rewards!
 		}
+		// Update samplers for any loaded properties
+		updateSamplers();
 		// Generate updates for next state 
 		updater.calculateTransitions(currentState, transitionList);
 	}
@@ -752,8 +775,8 @@ public class SimulatorEngine
 		// Get corresponding choice
 		Choice choice = transitionList.getChoice(i);
 		// Remember last state and compute next one (and its state rewards)
-		lastState.copy(currentState);
-		choice.computeTarget(offset, lastState, currentState);
+		previousState.copy(currentState);
+		choice.computeTarget(offset, previousState, currentState);
 		updater.calculateStateRewards(currentState, currentStateRewards);
 		// Store path info (if necessary)
 		if (!onTheFly) {
@@ -762,10 +785,33 @@ public class SimulatorEngine
 			path.addStep(time, index, choice.getAction(), currentStateRewards, currentState, currentStateRewards);
 			// TODO: first currentStateRewards in above should be new *trans* rewards!
 		}
+		// Update samplers for any loaded properties
+		updateSamplers();
 		// Generate updates for next state 
 		updater.calculateTransitions(currentState, transitionList);
 	}
 
+	/**
+	 * Reset samplers for any loaded properties that a new step has occurred.
+	 */
+	private void resetSamplers() throws PrismLangException
+	{
+		for (Sampler sampler : propertySamplers) {
+			sampler.reset();
+		}
+	}
+
+	/**
+	 * Notify samplers for any loaded properties that a new step has occurred.
+	 */
+	private void updateSamplers() throws PrismLangException
+	{
+		for (Sampler sampler : propertySamplers) {
+			if (!sampler.isCurrentValueKnown())
+				sampler.update(path);
+		}
+	}
+
 	// ------------------------------------------------------------------------------
 	// Queries regarding model
 	// ------------------------------------------------------------------------------
@@ -930,9 +976,7 @@ public class SimulatorEngine
 	// ------------------------------------------------------------------------------
 
 	/**
-	 * Returns the number of states stored in the current path table.
-	 * 
-	 * @return the number of states stored in the current path table.
+	 * Get the size of the current path (number of steps; or number of states - 1).
 	 */
 	public int getPathSize()
 	{
@@ -1204,16 +1248,15 @@ public class SimulatorEngine
 	 *             if anything goes wrong.
 	 * @return the result.
 	 */
-	public Object modelCheckSingleProperty(ModulesFile modulesFile, PropertiesFile propertiesFile, Expression expr,
-			Values initialState, int noIterations, int maxPathLength) throws PrismException
+	public Object modelCheckSingleProperty(ModulesFile modulesFile, PropertiesFile propertiesFile, Expression expr, Values initialState, int noIterations,
+			int maxPathLength) throws PrismException
 	{
 		ArrayList exprs;
 		Object res[];
 
 		exprs = new ArrayList();
 		exprs.add(expr);
-		res = modelCheckMultipleProperties(modulesFile, propertiesFile, exprs, initialState, noIterations,
-				maxPathLength);
+		res = modelCheckMultipleProperties(modulesFile, propertiesFile, exprs, initialState, noIterations, maxPathLength);
 
 		if (res[0] instanceof PrismException)
 			throw (PrismException) res[0];
@@ -1240,11 +1283,12 @@ public class SimulatorEngine
 	 * </UL>
 	 * 
 	 */
-	public Object[] modelCheckMultipleProperties(ModulesFile modulesFile, PropertiesFile propertiesFile,
-			List<Expression> exprs, Values initialState, int noIterations, int maxPathLength)
-			throws PrismException
+	public Object[] modelCheckMultipleProperties(ModulesFile modulesFile, PropertiesFile propertiesFile, List<Expression> exprs, Values initialState,
+			int noIterations, int maxPathLength) throws PrismException
 	{
-		createNewOnTheFlyPath(modulesFile, propertiesFile);
+		// TODO: make on the fly again
+		//createNewOnTheFlyPath(modulesFile, propertiesFile);
+		createNewPath(modulesFile, propertiesFile);
 
 		Object[] results = new Object[exprs.size()];
 		int[] indices = new int[exprs.size()];
@@ -1256,7 +1300,7 @@ public class SimulatorEngine
 		for (int i = 0; i < exprs.size(); i++) {
 			try {
 				checkPropertyForSimulation((Expression) exprs.get(i), modulesFile.getModelType());
-				indices[i] = addProperty((Expression) exprs.get(i));
+				indices[i] = addProperty((Expression) exprs.get(i), propertiesFile);
 				if (indices[i] >= 0)
 					validPropsCount++;
 			} catch (PrismException e) {
@@ -1267,18 +1311,14 @@ public class SimulatorEngine
 
 		// as long as there are at least some valid props, do sampling
 		if (validPropsCount > 0) {
-			initialisePath(initialState);
-			int result = 0;//doSampling(noIterations, maxPathLength);
-			if (result == ERROR) {
-				throw new PrismException(getLastErrorMessage());
-			}
+			doSampling(new State(initialState), noIterations, maxPathLength);
 		}
 
 		// process the results
 		for (int i = 0; i < results.length; i++) {
 			// if we have already stored an error for this property, keep it as the result
 			if (!(results[i] instanceof PrismException))
-				results[i] = processSamplingResult((Expression) exprs.get(i), indices[i]);
+				results[i] = propertySamplers.get(indices[i]).getMeanValue();
 		}
 
 		// display results to log
@@ -1323,10 +1363,9 @@ public class SimulatorEngine
 	 * @throws PrismException
 	 *             if something goes wrong with the sampling algorithm
 	 */
-	public void modelCheckExperiment(ModulesFile modulesFile, PropertiesFile propertiesFile,
-			UndefinedConstants undefinedConstants, ResultsCollection resultsCollection, Expression propertyToCheck,
-			Values initialState, int maxPathLength, int noIterations) throws PrismException, InterruptedException,
-			PrismException
+	public void modelCheckExperiment(ModulesFile modulesFile, PropertiesFile propertiesFile, UndefinedConstants undefinedConstants,
+			ResultsCollection resultsCollection, Expression propertyToCheck, Values initialState, int maxPathLength, int noIterations) throws PrismException,
+			InterruptedException, PrismException
 	{
 		int n;
 		Values definedPFConstants = new Values();
@@ -1347,7 +1386,7 @@ public class SimulatorEngine
 			propertyConstants = propertiesFile.getConstantValues();
 			try {
 				checkPropertyForSimulation(propertyToCheck, modulesFile.getModelType());
-				indices[i] = addProperty(propertyToCheck);
+				indices[i] = addProperty(propertyToCheck, propertiesFile);
 				if (indices[i] >= 0)
 					validPropsCount++;
 			} catch (PrismException e) {
@@ -1381,64 +1420,61 @@ public class SimulatorEngine
 				mainLog.println("\nResult: " + results[0]);
 		} else {
 			mainLog.println("\nResults:");
-			mainLog.print(resultsCollection.toStringPartial(undefinedConstants.getMFConstantValues(), true, " ", " : ",
-					false));
+			mainLog.print(resultsCollection.toStringPartial(undefinedConstants.getMFConstantValues(), true, " ", " : ", false));
 		}
 	}
 
-	/*
-	private int doSampling(State initialState, int numIters, int maxPathLength)
+	private void doSampling(State initialState, int numIters, int maxPathLength) throws PrismException
 	{
-		int iteration_counter = 0;
-		int last_percentage_done = -1;
-		int percentage_done = -1;
-		double average_path_length = 0;
-		int min_path_length = 0, max_path_length = 0;
-		boolean stopped_early = false;
+		int iters = 0;
+		int lastPercentageDone = 0;
+		int percentageDone = 0;
+		double avgPathLength = 0;
+		int minPathFound = 0, maxPathFound = 0;
+		boolean stoppedEarly = false;
 		boolean deadlocks_found = false;
-		//The current path
-		int current_index;
-		
+		boolean allKnown = false;
+		int i;
+
 		//double* path_cost = new double[no_reward_structs];
 		//double* total_state_cost = new double[no_reward_structs];
 		//double* total_transition_cost = new double[no_reward_structs];
-		
+
 		// Timing info
 		long start, start2, stop;
 		double time_taken;
-		
+
 		//Loop detection requires that deterministic paths are
 		//stored, until that determinism is broken.  This path
 		//is allocated dynamically, 10 steps at a time.
 		//CSamplingLoopDetectionHandler* loop_detection = new CSamplingLoopDetectionHandler();
-		
+
 		//TODO: allow stopping of sampling mid-way through?
 		//External flag set to false
 		boolean should_stop_sampling = false;
-		
+
 		start = start2 = System.currentTimeMillis();
-		
+
 		mainLog.print("\nSampling progress: [");
 		mainLog.flush();
-		
+
 		//The loop continues until each pctl/csl formula is satisfied:
 		//E.g. usually, this is when the correct number of iterations
 		//has been performed, but for some, such as cumulative rewards
 		//this can be early if a loop is detected at any point, this
 		//is all handled by the All_Done_Sampling() function
-		
+
 		// Main sampling loop
-		while (!should_stop_sampling && !isSamplingDone()) {
-			
+		while (!should_stop_sampling && !isSamplingDone() && iters < numIters) {
+
 			// Display progress
-			percentage_done = ((10*(iteration_counter))/numIters)*10;
-			if (percentage_done > last_percentage_done) {
-				last_percentage_done = percentage_done;
-				//cout << " " << last_percentage_done << "%" << endl;
-				mainLog.print(" " + last_percentage_done + "%");
+			percentageDone = ((10 * (iters)) / numIters) * 10;
+			if (percentageDone > lastPercentageDone) {
+				lastPercentageDone = percentageDone;
+				mainLog.print(" " + lastPercentageDone + "%");
 				mainLog.flush();
 			}
-			
+
 			//do polling and feedback every 2 seconds
 			stop = System.currentTimeMillis();
 			if (stop - start2 > 2000) {
@@ -1446,32 +1482,34 @@ public class SimulatorEngine
 				//int poll = Poll_Control_File();
 				//if(poll & STOP_SAMPLING == STOP_SAMPLING)
 				//	should_stop_sampling = true;
-				 start2 = System.currentTimeMillis();
+				start2 = System.currentTimeMillis();
 			}
-			
-			iteration_counter++;
-			
+
+			iters++;
+
 			// Start the new path for this iteration (sample)
-			initialisePath(initialState);			
-			
+			initialisePath(initialState);
+
 			//loop_detection->Reset();
-			
-			
-			notifyPathFormulae(last_state, state_variables, loop_detection);
-			
+
 			// Generate a path, up to at most maxPathLength steps
-			for (current_index = 0; 
-				!All_PCTL_Answers_Known(loop_detection) &&	//not got answers for all properties yet
-				//!loop_detection->Is_Proven_Looping()		//not looping (removed this - e.g. cumul rewards can't stop yet)
-				current_index < path_length;				//not exceeding path_length
-				current_index++)
-			{
-				// Make a random transition
-				automaticChoice(detect);
+			for (i = 0; i < maxPathLength; i++) {
 				
-				//if(!loop_detection->Is_Proven_Looping()) { // removed this: for e.g. cumul rewards need to keep counting in loops...
+				// See if all samplers have established a value; if so, stop.
+				allKnown = true;
+				for (Sampler sampler : propertySamplers) {
+					if (!sampler.isCurrentValueKnown())
+						allKnown = false;
+				}
+				if (allKnown)
+					break;
 				
-				if (modelType.continuousTime()) {
+				// Make a random transition
+				automaticChoice(true);
+
+				//if(!loop_detection->Is_Proven_Looping()) { // removed this: for e.g. cumul rewards need to keep counting in loops...
+
+				/*if (modelType.continuousTime()) {
 					double time_in_state = Get_Sampled_Time();
 					
 					last_state->time_spent_in_state = time_in_state;
@@ -1503,84 +1541,67 @@ public class SimulatorEngine
 					}
 					
 					Notify_Path_Formulae(last_state, state_variables, loop_detection); 
-				}
+				}*/
 				//}
-			
+
 			}
-			
+
 			// record if we found any deadlocks (can check this outside path gen loop because never escape deadlocks)
-			if (loop_detection->Is_Deadlock()) deadlocks_found = true;
-			
-			// compute path length statistics so far
-			average_path_length = (average_path_length*(iteration_counter-1)+(current_index))/iteration_counter;
-			min_path_length = (iteration_counter == 1) ? current_index : ((current_index < min_path_length) ? current_index : min_path_length);
-			max_path_length = (iteration_counter == 1) ? current_index : ((current_index > max_path_length) ? current_index : max_path_length);
-			
-			//Get samples and notify sample collectors
-			Do_A_Sample(loop_detection);
+			//if (loop_detection->Is_Deadlock()) deadlocks_found = true;
+
+			// Update path length statistics
+			avgPathLength = (avgPathLength * (iters - 1) + (i)) / iters;
+			minPathFound = (iters == 1) ? i : Math.min(minPathFound, i);
+			maxPathFound = (iters == 1) ? i : Math.max(maxPathFound, i);
 			
-			// stop early if any of the properties couldn't be sampled
-			if (Get_Total_Num_Reached_Max_Path() > 0) { stopped_early = true; break; }
+			// If not all samplers could produce values, this an error
+			if (!allKnown) {
+				stoppedEarly = true;
+				break;
+			}
 			
-		}//end sampling while
-		
-		if (!stopped_early) {
+			// Update state of samplers based on last path
+			for (Sampler sampler : propertySamplers) {
+				sampler.updateStats();
+			}
+		}
+
+		if (!stoppedEarly) {
 			if (!should_stop_sampling)
 				mainLog.print(" 100% ]");
 			mainLog.println();
 			stop = System.currentTimeMillis();
 			time_taken = (stop - start) / 1000.0;
 			mainLog.print("\nSampling complete: ");
-			mainLog.print(iteration_counter + " iterations in " + time_taken + " seconds (average " + time_taken/iteration_counter + ")\n");
-			mainLog.print("Path length statistics: average " + average_path_length + ", min " + min_path_length + ", max " + max_path_length + "\n");
+			mainLog.print(iters + " iterations in " + time_taken + " seconds (average " + time_taken / iters + ")\n");
+			mainLog.print("Path length statistics: average " + avgPathLength + ", min " + minPathFound + ", max " + maxPathFound + "\n");
 		} else {
-			mainLog.print(" ...\n\nSampling terminated early after " + iteration_counter + " iterations.\n");
+			mainLog.print(" ...\n\nSampling terminated early after " + iters + " iterations.\n");
 		}
-		
+
 		// print a warning if deadlocks occurred at any point
 		if (deadlocks_found)
 			mainLog.print("\nWarning: Deadlocks were found during simulation: self-loops were added\n");
-		
+
 		// print a warning if simulation was stopped by the user
 		if (should_stop_sampling)
 			mainLog.print("\nWarning: Simulation was terminated before completion.\n");
-		
+
 		//write to feedback file with true to indicate that we have finished sampling
-		Write_Feedback(iteration_counter, numIters, true);
-		
-		//Print_Sampling_Results();
-		delete loop_detection;
-		delete[] starting_variables;
-		delete last_state;
-		delete[] path_cost;
-		delete[] total_state_cost;
-		delete[] total_transition_cost;
-		
-		if (stopped_early) {
-			Report_Error("One or more of the properties being sampled could not be checked on a sample. Consider increasing the maximum path length");
-			throw 0;
-		}
-		
-		
-		// TODO:
-		return -1;
-	}*/
+		//Write_Feedback(iteration_counter, numIters, true);
 
-	private void notifyPathFormulae()
-	{
-		/*for(int i = 0; i< no_path_formulae; i++)
-		{
-			if(!registered_path_formulae[i]->Is_Answer_Known(loop_detection))
-				registered_path_formulae[i]->Notify_State(last_state, current_state);
-		}*/
+		if (stoppedEarly) {
+			throw new PrismException(
+					"One or more of the properties being sampled could not be checked on a sample. Consider increasing the maximum path length");
+		}
 	}
-	
+
 	private boolean isSamplingDone()
 	{
 		// TODO
 		return false;
 	}
-	
+
 	private static native double getSamplingResult(int propertyIndex);
 
 	private static native int getNumReachedMaxPath(int propertyIndex);
@@ -1647,8 +1668,7 @@ public class SimulatorEngine
 			expr = ((ExpressionReward) prop).getExpression();
 		}
 		if (!ok)
-			throw new PrismException(
-					"Simulator can only be applied to properties of the form \"P=? [ ... ]\" or \"R=? [ ... ]\"");
+			throw new PrismException("Simulator can only be applied to properties of the form \"P=? [ ... ]\" or \"R=? [ ... ]\"");
 
 		// Check that there are no nested probabilistic operators
 		try {

prism/src/simulator/Updater.java

@@ -108,8 +108,8 @@ public class Updater
 		int i, j, n, count, n2, n3;
 		double p;
 
-		System.out.println("Synchs: " + synchs);
-		System.out.println("Calc updates for " + state);
+		//System.out.println("Synchs: " + synchs);
+		//System.out.println("Calc updates for " + state);
 		// Clear lists/bitsets
 		transitionList.clear();
 		for (i = 0; i < numModules; i++) {
@@ -125,7 +125,7 @@ public class Updater
 		for (i = 0; i < numModules; i++) {
 			calculateUpdatesForModule(i, state);
 		}
-		System.out.println("updateLists: " + updateLists);
+		//System.out.println("updateLists: " + updateLists);
 
 		// Combination of updates depends on model type
 		/*switch (modelType) {
@@ -167,7 +167,7 @@ public class Updater
 						// TODO
 						throw new PrismLangException("Don't handle local nondet yet");
 					}
-					System.out.println("prod" + j + ": " + prod);
+					//System.out.println("prod" + j + ": " + prod);
 				}
 				transitionList.add(prod);
 				n++;
@@ -226,7 +226,7 @@ public class Updater
 
 		// For DTMCs, need to randomise
 
-		System.out.println(transitionList);
+		//System.out.println(transitionList);
 
 	}
 

prism/src/simulator/sampler/Sampler.java

@@ -0,0 +1,205 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package simulator.sampler;
+
+import simulator.*;
+import parser.ast.*;
+import prism.PrismException;
+import prism.PrismLangException;
+
+/**
+ * Samplers: determine values based on a sequence of simulation paths. 
+ */
+public abstract class Sampler
+{
+	protected boolean valueKnown;
+
+	/**
+	 * Is the current value of the sampler known, based on the path seen so far?
+	 */
+	public boolean isCurrentValueKnown()
+	{
+		return valueKnown;
+	}
+
+	/**
+	 * Reset the current value of the sampler and whether it is known or not.
+	 */
+	public abstract void reset();
+
+	/**
+	 * Reset all statistics for the sampler.
+	 */
+	public abstract void resetStats();
+
+	/**
+	 * Update the current value of the sampler based on the current simulation path.
+	 * It is assumed that this is called at every step of the path.
+	 * It is also assumed that this is not called after the value becomes known. 
+	 */
+	public abstract void update(Path path) throws PrismLangException;
+
+	/**
+	 * Update the statistics for the sampler, assuming that the current path is finished.
+	 */
+	public abstract void updateStats();
+
+	/**
+	 * Get the current value of the sampler.
+	 */
+	public abstract Object getCurrentValue();
+
+	/**
+	 * Get the mean value of the sampler, over all paths seen.
+	 */
+	public abstract Object getMeanValue();
+
+	// Static methods for sampler creation
+
+	/**
+	 * Create a sampler for an expression (P=? or R=?).
+	 * Expression should contain no constants/formula/etc.
+	 * The model to which the property applies should also be specified. 
+	 */
+	public static Sampler createSampler(Expression expr, ModulesFile mf) throws PrismException
+	{
+		Sampler sampler = null;
+		// P=?
+		if (expr instanceof ExpressionProb) {
+			ExpressionProb propProb = (ExpressionProb) expr;
+			// Test whether this is a simple path formula (i.e. non-LTL)
+			if (propProb.getExpression().isSimplePathFormula()) {
+				sampler = createSamplerForProbPathPropertySimple(propProb.getExpression(), mf);
+			} else {
+				throw new PrismException("LTL-style path formulas are not supported by the simulator");
+			}
+		}
+		// R=?
+		else if (expr instanceof ExpressionReward) {
+			sampler = createSamplerForRewardProperty((ExpressionReward) expr, mf);
+		}
+		// Neither
+		else {
+			throw new PrismException("Can't create sampler for property \"" + expr + "\"");
+		}
+		return sampler;
+	}
+
+	private static SamplerBoolean createSamplerForProbPathPropertySimple(Expression expr, ModulesFile mf) throws PrismException
+	{
+		// Negation/parentheses
+		if (expr instanceof ExpressionUnaryOp) {
+			ExpressionUnaryOp exprUnary = (ExpressionUnaryOp) expr;
+			// Parentheses
+			if (exprUnary.getOperator() == ExpressionUnaryOp.PARENTH) {
+				// Recurse
+				return createSamplerForProbPathPropertySimple(exprUnary.getOperand(), mf);
+			}
+			// Negation
+			else if (exprUnary.getOperator() == ExpressionUnaryOp.NOT) {
+				// Recurse, then negate meaning
+				SamplerBoolean sampler = createSamplerForProbPathPropertySimple(exprUnary.getOperand(), mf);
+				sampler.negate();
+				return sampler;
+			}
+		}
+		// Temporal operators
+		else if (expr instanceof ExpressionTemporal) {
+			ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
+			// Next
+			if (exprTemp.getOperator() == ExpressionTemporal.P_X) {
+				return new SamplerNext(exprTemp);
+			}
+			// Until
+			else if (exprTemp.getOperator() == ExpressionTemporal.P_U) {
+				if (exprTemp.hasBounds()) {
+					if (mf.getModelType().continuousTime()) {
+						// Continuous-time bounded until
+						return new SamplerBoundedUntilCont(exprTemp);
+					} else {
+						// Discrete-time bounded until
+						return new SamplerBoundedUntilDisc(exprTemp);
+					}
+				} else {
+					// Unbounded until
+					return new SamplerUntil(exprTemp);
+				}
+			}
+			// Anything else - convert to until and recurse
+			else {
+				return createSamplerForProbPathPropertySimple(exprTemp.convertToUntilForm(), mf);
+			}
+		}
+
+		throw new PrismException("Can't create sampler for property \"" + expr + "\"");
+	}
+
+	private static SamplerDouble createSamplerForRewardProperty(ExpressionReward expr, ModulesFile mf) throws PrismException
+	{
+		// Extract reward structure index
+		Object rs = expr.getRewardStructIndex();
+		int rsi = -1;
+		if (mf.getNumRewardStructs() == 0)
+			throw new PrismException("Model has no rewards specified");
+		if (rs == null) {
+			rsi = 0;
+		} else if (rs instanceof Expression) {
+			rsi = ((Expression) rs).evaluateInt() - 1;
+			rs = new Integer(rsi + 1); // for better error reporting below
+		} else if (rs instanceof String) {
+			rsi = mf.getRewardStructIndex((String) rs);
+		}
+		if (rsi == -1)
+			throw new PrismException("Invalid reward structure index \"" + rs + "\"");
+
+		// Construct sampler based on type
+		ExpressionTemporal exprTemp = (ExpressionTemporal) expr.getExpression();
+		switch (exprTemp.getOperator()) {
+		case ExpressionTemporal.R_C:
+			if (mf.getModelType().continuousTime()) {
+				// Continuous-time cumulative reward
+				return new SamplerRewardCumulCont(exprTemp, rsi);
+			} else {
+				// Discrete-time cumulative reward
+				return new SamplerRewardCumulDisc(exprTemp, rsi);
+			}
+		case ExpressionTemporal.R_I:
+			if (mf.getModelType().continuousTime()) {
+				// Continuous-time instantaneous reward
+				return new SamplerRewardInstCont(exprTemp, rsi);
+			} else {
+				// Discrete-time instantaneous reward
+				return new SamplerRewardInstDisc(exprTemp, rsi);
+			}
+		case ExpressionTemporal.R_F:
+			// reachability reward
+			return new SamplerRewardReach(exprTemp, rsi);
+		}
+
+		throw new PrismException("Can't create sampler for property \"" + expr + "\"");
+	}
+}

prism/src/simulator/sampler/SamplerBoolean.java

@@ -0,0 +1,99 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package simulator.sampler;
+
+import simulator.*;
+import prism.PrismLangException;
+
+/**
+ * Samplers for properties that associate a simulation path with a Boolean value.
+ */
+public abstract class SamplerBoolean extends Sampler
+{
+	// Value of current path
+	protected boolean value;
+	// Whether the actual value should be the negation of 'value'
+	protected boolean negated = false;
+	// Stats over all paths
+	protected int numSamples;
+	protected int numTrue;
+
+	@Override
+	public void reset()
+	{
+		valueKnown = false;
+		value = false;
+	}
+
+	@Override
+	public void resetStats()
+	{
+		numSamples = 0;
+		numTrue = 0;
+	}
+
+	@Override
+	public abstract void update(Path path) throws PrismLangException;
+
+	@Override
+	public void updateStats()
+	{
+		numSamples++;
+		// XOR: value && !negated || !value && negated 
+		if (value != negated) 
+			numTrue++;
+	}
+
+	@Override
+	public Object getCurrentValue()
+	{
+		// XOR: value && !negated || !value && negated 
+		return new Boolean(value != negated);
+	}
+
+	@Override
+	public Object getMeanValue()
+	{
+		return new Double(numTrue / (double) numSamples);
+	}
+	
+	/**
+	 * Negate the meaning of this sampler.
+	 */
+	public boolean negate()
+	{
+		return negated = !negated;
+	}
+	
+	/**
+	 * Is this sampler negated?
+	 */
+	public boolean getNegated()
+	{
+		return negated;
+	}
+}

prism/src/simulator/sampler/SamplerBoundedUntilCont.java

@@ -0,0 +1,114 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package simulator.sampler;
+
+import simulator.*;
+import prism.*;
+import parser.ast.*;
+
+/**
+ * Construct a sampler for a (continuous-time) bounded until property.
+ * Passed in ExpressionTemporal should be a formula of this type.
+ * All constants should have already been evaluated/replaced.
+ */
+public class SamplerBoundedUntilCont extends SamplerBoolean
+{
+	private Expression left;
+	private Expression right;
+	private double lb;
+	private double ub;
+
+	/**
+	 * Construct a sampler for a (continuous) time-bounded until formula.
+	 * Passed in ExpressionTemporal should be a property of this type.
+	 * All constants should have already been evaluated/replaced.
+	 */
+	public SamplerBoundedUntilCont(ExpressionTemporal expr) throws PrismException
+	{
+		// Make sure expression is of the correct type
+		// Then extract other required info
+		if (expr.getOperator() != ExpressionTemporal.P_U)
+			throw new PrismException("Error creating Sampler");
+		left = expr.getOperand1();
+		right = expr.getOperand2();
+		lb = expr.getLowerBound() == null ? 0.0 : expr.getLowerBound().evaluateDouble();
+		ub = expr.getUpperBound() == null ? Double.POSITIVE_INFINITY: expr.getUpperBound().evaluateDouble();
+		// Initialise sampler info
+		reset();
+		resetStats();
+	}
+
+	@Override
+	public void update(Path path) throws PrismLangException
+	{
+		if (path.size() > 0) {
+			double time_so_far = path.getTimeSoFar();
+			if (time_so_far > ub) {
+				// must take into account the possibility of missing lower bound
+
+				// could have missed out evaluation of right
+				if (time_so_far - path.getTimeInPreviousState() <= lb) {
+					if (right.evaluateBoolean(path.getPreviousState())) {
+						valueKnown = true;
+						value = true;
+					} else {
+						valueKnown = true;
+						value = false;
+					}
+				} else {
+					valueKnown = true;
+					value = false;
+				}
+			} else if (time_so_far <= lb) {
+				if (!left.evaluateBoolean(path.getCurrentState())) {
+					valueKnown = true;
+					value = false;
+				}
+			} else {
+				if (right.evaluateBoolean(path.getCurrentState())) {
+					valueKnown = true;
+					value = true;
+				} else if (!left.evaluateBoolean(path.getCurrentState())) {
+					valueKnown = true;
+					value = false;
+				}
+			}
+		} else {
+			if (lb == 0.0) {
+				if (right.evaluateBoolean(path.getCurrentState())) {
+					valueKnown = true;
+					value = true;
+				}
+			} else {
+				if (!left.evaluateBoolean(path.getCurrentState())) {
+					valueKnown = true;
+					value = false;
+				}
+			}
+		}
+	}
+}

prism/src/simulator/sampler/SamplerBoundedUntilDisc.java

@@ -0,0 +1,84 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package simulator.sampler;
+
+import simulator.*;
+import prism.*;
+import parser.*;
+import parser.ast.*;
+
+public class SamplerBoundedUntilDisc extends SamplerBoolean
+{
+	private Expression left;
+	private Expression right;
+	private int lb;
+	private int ub;
+
+	/**
+	 * Construct a sampler for a (discrete-time) bounded until property.
+	 * Passed in ExpressionTemporal should be a property of this type.
+	 * All constants should have already been evaluated/replaced.
+	 */
+	public SamplerBoundedUntilDisc(ExpressionTemporal expr) throws PrismException
+	{
+		// Make sure expression is of the correct type
+		// Then extract other required info
+		if (expr.getOperator() != ExpressionTemporal.P_U)
+			throw new PrismException("Error creating Sampler");
+		left = expr.getOperand1();
+		right = expr.getOperand2();
+		lb = expr.getLowerBound() == null ? 0 : expr.getLowerBound().evaluateInt();
+		ub = expr.getUpperBound() == null ? Integer.MAX_VALUE : expr.getUpperBound().evaluateInt();
+		// Initialise sampler info
+		reset();
+		resetStats();
+	}
+
+	@Override
+	public void update(Path path) throws PrismLangException
+	{
+		int pathSize = path.size();
+		if (pathSize > ub) {
+			valueKnown = true;
+			value = false;
+		} else if (pathSize < lb) {
+			if (!left.evaluateBoolean(path.getCurrentState())) {
+				valueKnown = true;
+				value = false;
+			}
+		} else {
+			State currentState = path.getCurrentState();
+			if (right.evaluateBoolean(currentState)) {
+				valueKnown = true;
+				value = true;
+			} else if (!left.evaluateBoolean(currentState)) {
+				valueKnown = true;
+				value = false;
+			}
+		}
+	}
+}

prism/src/simulator/sampler/SamplerDouble.java

@@ -0,0 +1,78 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package simulator.sampler;
+
+import simulator.*;
+import prism.PrismLangException;
+
+/**
+ * Samplers for properties that associate a simulation path with a real (double) value.
+ */
+public abstract class SamplerDouble extends Sampler
+{
+	// Value of current path
+	protected double value;
+	// Stats over all paths
+	protected double valueSum;
+	protected int numSamples;
+
+	@Override
+	public void reset()
+	{
+		valueKnown = false;
+		value = 0.0;
+	}
+
+	@Override
+	public void resetStats()
+	{
+		valueSum = 0.0;
+		numSamples = 0;
+	}
+
+	@Override
+	public abstract void update(Path path) throws PrismLangException;
+
+	@Override
+	public void updateStats()
+	{
+		valueSum += value;
+		numSamples++;
+	}
+
+	@Override
+	public Object getCurrentValue()
+	{
+		return new Double(value);
+	}
+
+	@Override
+	public Object getMeanValue()
+	{
+		return new Double(valueSum / numSamples);
+	}
+}

prism/src/simulator/sampler/SamplerNext.java

@@ -0,0 +1,66 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package simulator.sampler;
+
+import simulator.*;
+import prism.*;
+import parser.*;
+import parser.ast.*;
+
+public class SamplerNext extends SamplerBoolean
+{
+	private Expression target;
+
+	/**
+	 * Construct a sampler for a "next" property.
+	 * Passed in ExpressionTemporal should be a property of this type.
+	 * All constants should have already been evaluated/replaced.
+	 */
+	public SamplerNext(ExpressionTemporal expr) throws PrismException
+	{
+		// Make sure expression is of the correct type
+		// Then extract other required info
+		if (expr.getOperator() != ExpressionTemporal.P_X)
+			throw new PrismException("Error creating Sampler");
+		target = expr.getOperand2();
+		// Initialise sampler info
+		reset();
+		resetStats();
+	}
+
+	@Override
+	public void update(Path path) throws PrismLangException
+	{
+		// X "target" is true iff state 1 satisfies "target"
+		if (path.size() == 1) {
+			valueKnown = true;
+			value = target.evaluateBoolean(path.getCurrentState());
+		}
+		// Nothing else to do: if path size is 0, can't decide;
+		// if path size > 1 (should never happen), nothing changes
+	}
+}

prism/src/simulator/sampler/SamplerRewardCumulCont.java

@@ -0,0 +1,75 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package simulator.sampler;
+
+import simulator.*;
+import prism.*;
+import parser.ast.*;
+
+public class SamplerRewardCumulCont extends SamplerDouble
+{
+	private double timeBound;
+	private int rewardStructIndex;
+
+	/**
+	 * Construct a sampler for a (continuous-time) cumulative reward property.
+	 * Passed in ExpressionTemporal should be a property of this type.
+	 * Reward structure index should also be specified.
+	 * All constants should have already been evaluated/replaced.
+	 */
+	public SamplerRewardCumulCont(ExpressionTemporal expr, int rewardStructIndex) throws PrismException
+	{
+		// Make sure expression is of the correct type
+		// Then extract other required info
+		if (expr.getOperator() != ExpressionTemporal.R_C)
+			throw new PrismException("Error creating Sampler");
+		timeBound = expr.getUpperBound().evaluateDouble();
+		this.rewardStructIndex = rewardStructIndex;
+		// Initialise sampler info
+		reset();
+		resetStats();
+	}
+
+	@Override
+	public void update(Path path) throws PrismLangException
+	{
+		// As soon as time bound exceeded, compute reward total
+		if (path.getTimeSoFar() >= timeBound) {
+			valueKnown = true;
+			value = path.getRewardCumulatedSoFar(rewardStructIndex);
+			// Compute excess time, i.e. how long ago time bound was reached
+			double excessTime = timeBound - path.getTimeSoFar();
+			// If this is > 0 (very likely, unless time bound = 0),
+			// need to subtract reward accumulated in excess time
+			// (i.e. fraction of previous state reward, and transition reward)
+			if (excessTime > 0) {
+				value -= path.getPreviousStateReward(rewardStructIndex) * (excessTime / path.getTimeInPreviousState());
+				value -= path.getPreviousTransitionReward(rewardStructIndex);
+			}
+		}
+	}
+}

prism/src/simulator/sampler/SamplerRewardCumulDisc.java

@@ -0,0 +1,66 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package simulator.sampler;
+
+import simulator.*;
+import prism.*;
+import parser.ast.*;
+
+public class SamplerRewardCumulDisc extends SamplerDouble
+{
+	private int timeBound;
+	private int rewardStructIndex;
+
+	/**
+	 * Construct a sampler for a (discrete-time) cumulative reward property.
+	 * Passed in ExpressionTemporal should be a property of this type.
+	 * Reward structure index should also be specified.
+	 * All constants should have already been evaluated/replaced.
+	 */
+	public SamplerRewardCumulDisc(ExpressionTemporal expr, int rewardStructIndex) throws PrismException
+	{
+		// Make sure expression is of the correct type
+		// Then extract other required info
+		if (expr.getOperator() != ExpressionTemporal.R_C)
+			throw new PrismException("Error creating Sampler");
+		timeBound = expr.getUpperBound().evaluateInt();
+		this.rewardStructIndex = rewardStructIndex;
+		// Initialise sampler info
+		reset();
+		resetStats();
+	}
+
+	@Override
+	public void update(Path path) throws PrismLangException
+	{
+		// As soon as time bound reached, store current reward total
+		if (path.size() == timeBound) {
+			valueKnown = true;
+			value = path.getRewardCumulatedSoFar(rewardStructIndex);
+		}
+	}
+}

prism/src/simulator/sampler/SamplerRewardInstCont.java

@@ -0,0 +1,72 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package simulator.sampler;
+
+import simulator.*;
+import prism.*;
+import parser.ast.*;
+
+public class SamplerRewardInstCont extends SamplerDouble
+{
+	private double time;
+	private int rewardStructIndex;
+
+	/**
+	 * Construct a sampler for a (continuous-time) instantaneous reward property.
+	 * Passed in ExpressionTemporal should be a property of this type.
+	 * Reward structure index should also be specified.
+	 * All constants should have already been evaluated/replaced.
+	 */
+	public SamplerRewardInstCont(ExpressionTemporal expr, int rewardStructIndex) throws PrismException
+	{
+		// Make sure expression is of the correct type
+		// Then extract other required info
+		if (expr.getOperator() != ExpressionTemporal.R_C)
+			throw new PrismException("Error creating Sampler");
+		time = expr.getUpperBound().evaluateDouble();
+		this.rewardStructIndex = rewardStructIndex;
+		// Initialise sampler info
+		reset();
+		resetStats();
+	}
+
+	@Override
+	public void update(Path path) throws PrismLangException
+	{
+		// As soon as time bound exceeded, compute reward
+		if (path.getTimeSoFar() >= time) {
+			valueKnown = true;
+			// Time bound was exceeded in either previous or current state
+			// (unless the time bound is 0, the latter is very unlikely)
+			if (path.getTimeSoFar() > time) {
+				value = path.getPreviousStateReward(rewardStructIndex);
+			} else {
+				value = path.getCurrentStateReward(rewardStructIndex);
+			}
+		}
+	}
+}

prism/src/simulator/sampler/SamplerRewardInstDisc.java

@@ -0,0 +1,66 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package simulator.sampler;
+
+import simulator.*;
+import prism.*;
+import parser.ast.*;
+
+public class SamplerRewardInstDisc extends SamplerDouble
+{
+	private int time;
+	private int rewardStructIndex;
+
+	/**
+	 * Construct a sampler for a (discrete-time) instantaneous reward property.
+	 * Passed in ExpressionTemporal should be a property of this type.
+	 * Reward structure index should also be specified.
+	 * All constants should have already been evaluated/replaced.
+	 */
+	public SamplerRewardInstDisc(ExpressionTemporal expr, int rewardStructIndex) throws PrismException
+	{
+		// Make sure expression is of the correct type
+		// Then extract other required info
+		if (expr.getOperator() != ExpressionTemporal.R_C)
+			throw new PrismException("Error creating Sampler");
+		time = expr.getUpperBound().evaluateInt();
+		this.rewardStructIndex = rewardStructIndex;
+		// Initialise sampler info
+		reset();
+		resetStats();
+	}
+
+	@Override
+	public void update(Path path) throws PrismLangException
+	{
+		// As soon as time bound reached, store current state reward
+		if (path.size() == time) {
+			valueKnown = true;
+			value = path.getCurrentStateReward(rewardStructIndex);
+		}
+	}
+}

prism/src/simulator/sampler/SamplerRewardReach.java

@@ -0,0 +1,65 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package simulator.sampler;
+
+import simulator.*;
+import prism.*;
+import parser.ast.*;
+
+public class SamplerRewardReach extends SamplerDouble
+{
+	private Expression target;
+	private int rewardStructIndex;
+
+	/**
+	 * Construct a sampler for a reachability reward property.
+	 * Passed in ExpressionTemporal should be a property of this type.
+	 * Reward structure index should also be specified.
+	 * All constants should have already been evaluated/replaced.
+	 */
+	public SamplerRewardReach(ExpressionTemporal expr, int rewardStructIndex) throws PrismException
+	{
+		// Make sure expression is of the correct type
+		// Then extract other required info
+		if (expr.getOperator() != ExpressionTemporal.R_F)
+			throw new PrismException("Error creating Sampler");
+		target = expr.getOperand2();
+		this.rewardStructIndex = rewardStructIndex;
+		// Initialise sampler info
+		reset();
+		resetStats();
+	}
+
+	@Override
+	public void update(Path path) throws PrismLangException
+	{
+		if (target.evaluateBoolean(path.getCurrentState())) {
+			valueKnown = true;
+			value = path.getRewardCumulatedSoFar(rewardStructIndex);
+		}
+	}
+}

prism/src/simulator/sampler/SamplerUntil.java

@@ -0,0 +1,74 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package simulator.sampler;
+
+import simulator.*;
+import parser.State;
+import parser.ast.Expression;
+import parser.ast.ExpressionTemporal;
+import prism.PrismException;
+import prism.PrismLangException;
+
+public class SamplerUntil extends SamplerBoolean
+{
+	private Expression left;
+	private Expression right;
+
+	/**
+	 * Construct a sampler for a (unbounded) until property.
+	 * Passed in ExpressionTemporal should be a property of this type.
+	 * All constants should have already been evaluated/replaced.
+	 */
+	public SamplerUntil(ExpressionTemporal expr) throws PrismException
+	{
+		// Make sure expression is of the correct type
+		// Then extract other required info
+		if (expr.getOperator() != ExpressionTemporal.P_U)
+			throw new PrismException("Error creating Sampler");
+		left = expr.getOperand1();
+		right = expr.getOperand2();
+		// Initialise sampler info
+		reset();
+		resetStats();
+	}
+
+	@Override
+	public void update(Path path) throws PrismLangException
+	{
+		State currentState = path.getCurrentState();
+		// Have we reached the target (i.e. RHS of until)?
+		if (right.evaluateBoolean(currentState)) {
+			valueKnown = true;
+			value = true;
+		}
+		// Or, if not, have we violated the LJS of the until?
+		else if (!left.evaluateBoolean(currentState)) {
+			valueKnown = true;
+			value = false;
+		}
+	}
+}