Further work on simulator, including sampling.

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

prism/src/simulator/Path.java

@@ -0,0 +1,107 @@
+//==============================================================================
+//	
+//	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.State;
+
+/**
+ * Classes that store and manipulate a path though a model.
+ */
+public abstract class Path
+{
+	// MUTATORS
+	
+	/**
+	 * Initialise the path with an initial state and rewards.
+	 */
+	public abstract void initialise(State initialState, double[] initialStateRewards);
+
+	/**
+	 * Add a step to the path.
+	 */
+	public abstract void addStep(int choice, String action, double[] transRewards, State newState, double[] newStateRewards);
+
+	/**
+	 * Add a timed step to the path.
+	 */
+	public abstract void addStep(double time, int choice, String action, double[] transRewards, State newState, double[] newStateRewards);
+
+	// ACCESSORS
+
+	/**
+	 * Get the size of the path (number of steps; or number of states - 1).
+	 */
+	public abstract int size();
+
+	/**
+	 * Get the previous state, i.e. the penultimate state of the current path.
+	 */
+	public abstract State getPreviousState();
+
+	/**
+	 * Get the current state, i.e. the current final state of the path.
+	 */
+	public abstract State getCurrentState();
+
+	/**
+	 * For paths with continuous-time info, get the total time elapsed so far
+	 * (where zero time has been spent in the current (final) state).
+	 */
+	public abstract double getTimeSoFar();
+	
+	/**
+	 * For paths with continuous-time info, get the time spent in the previous state.
+	 */
+	public abstract double getTimeInPreviousState();
+	
+	/**
+	 * Get the total reward accumulated so far
+	 * (includes reward for previous transition but no state reward for current (final) state).
+	 * @param index Reward structure index
+	 */
+	public abstract double getRewardCumulatedSoFar(int index);
+	
+	/**
+	 * Get the state reward for the previous state.
+	 * (For continuous-time models, need to multiply this by time spent in the state.)
+	 * @param index Reward structure index
+	 */
+	public abstract double getPreviousStateReward(int index);
+	
+	/**
+	 * Get the transition reward for the transition between the previous and current states.
+	 * @param index Reward structure index
+	 */
+	public abstract double getPreviousTransitionReward(int index);
+
+	/**
+	 * Get the state reward for the current state.
+	 * (For continuous-time models, need to multiply this by time spent in the state.)
+	 * @param index Reward structure index
+	 */
+	public abstract double getCurrentStateReward(int index);
+}

prism/src/simulator/sampler/SamplerBoundedUntilCont.java

@@ -66,12 +66,13 @@ public class SamplerBoundedUntilCont extends SamplerBoolean
 	public void update(Path path) throws PrismLangException
 	{
 		if (path.size() > 0) {
-			double time_so_far = path.getTimeSoFar();
-			if (time_so_far > ub) {
+			double timeSoFar = path.getTimeSoFar();
+			// As soon as upper time bound exceeded, we can decide
+			if (timeSoFar > 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 (timeSoFar - path.getTimeInPreviousState() <= lb) {
 					if (right.evaluateBoolean(path.getPreviousState())) {
 						valueKnown = true;
 						value = true;
@@ -83,7 +84,7 @@ public class SamplerBoundedUntilCont extends SamplerBoolean
 					valueKnown = true;
 					value = false;
 				}
-			} else if (time_so_far <= lb) {
+			} else if (timeSoFar <= lb) {
 				if (!left.evaluateBoolean(path.getCurrentState())) {
 					valueKnown = true;
 					value = false;

prism/src/simulator/sampler/SamplerBoundedUntilDisc.java

@@ -62,23 +62,33 @@ public class SamplerBoundedUntilDisc extends SamplerBoolean
 	public void update(Path path) throws PrismLangException
 	{
 		int pathSize = path.size();
+		// Upper bound exceeded
 		if (pathSize > ub) {
 			valueKnown = true;
 			value = false;
-		} else if (pathSize < lb) {
+		}
+		// Lower bound not yet exceeded but LHS of until violated
+		// (no need to check RHS because too early)
+		else if (pathSize < lb) {
 			if (!left.evaluateBoolean(path.getCurrentState())) {
 				valueKnown = true;
 				value = false;
 			}
-		} else {
+		}
+		// Current time is between lower/upper bounds...
+		else {
 			State currentState = path.getCurrentState();
+			// Have we reached the target (i.e. RHS of until)?
 			if (right.evaluateBoolean(currentState)) {
 				valueKnown = true;
 				value = true;
-			} else if (!left.evaluateBoolean(currentState)) {
+			}
+			// Or, if not, have we violated the LJS of the until?
+			else if (!left.evaluateBoolean(currentState)) {
 				valueKnown = true;
 				value = false;
 			}
+			// Otherwise, don't know
 		}
 	}
 }

prism/src/simulator/sampler/SamplerNext.java

@@ -28,7 +28,6 @@ package simulator.sampler;
 
 import simulator.*;
 import prism.*;
-import parser.*;
 import parser.ast.*;
 
 public class SamplerNext extends SamplerBoolean

prism/src/simulator/sampler/SamplerUntil.java

@@ -70,5 +70,6 @@ public class SamplerUntil extends SamplerBoolean
 			valueKnown = true;
 			value = false;
 		}
+		// Otherwise, don't know
 	}
 }