Fixes and tidies to the simulator.

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

prism/src/simulator/PathFull.java

@@ -120,7 +120,6 @@ public class PathFull extends Path
 		// Add new step item to the path
 		Step step = new Step();
 		path.add(step);
-		size++;
 		// Add (copies of) initial state and state rewards to new step
 		step.state = new State(initialState);
 		step.stateRewards = initialStateRewards.clone();

prism/src/simulator/PathOnTheFly.java

@@ -123,7 +123,7 @@ public class PathOnTheFly extends Path
 	@Override
 	public void addStep(double time, int choice, String action, double[] transRewards, State newState, double[] newStateRewards)
 	{
-		size = 0;
+		size++;
 		previousState = currentState;
 		currentState = newState;
 		totalTime += time;

prism/src/simulator/SimulatorEngine.java

@@ -614,7 +614,9 @@ public class SimulatorEngine
 		// 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());
+		if (pf != null) {
+			propNew = (Expression) propNew.replaceConstants(pf.getConstantValues());
+		}
 		propNew = (Expression) propNew.simplify();
 		// Create sampler, update lists and return index
 		properties.add(propNew);
@@ -710,7 +712,6 @@ 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
 		previousState = new State(numVars);
@@ -1573,8 +1574,8 @@ public class SimulatorEngine
 			stop = System.currentTimeMillis();
 			time_taken = (stop - start) / 1000.0;
 			mainLog.print("\nSampling complete: ");
-			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");
+			mainLog.print(iters + " iterations in " + time_taken + " seconds (average " + PrismUtils.formatDouble(2, time_taken / iters) + ")\n");
+			mainLog.print("Path length statistics: average " + PrismUtils.formatDouble(2, avgPathLength) + ", min " + minPathFound + ", max " + maxPathFound + "\n");
 		} else {
 			mainLog.print(" ...\n\nSampling terminated early after " + iters + " iterations.\n");
 		}

prism/src/simulator/sampler/SamplerBoundedUntilCont.java

@@ -56,7 +56,7 @@ public class SamplerBoundedUntilCont extends SamplerBoolean
 		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();
+		ub = expr.getUpperBound() == null ? Double.POSITIVE_INFINITY : expr.getUpperBound().evaluateDouble();
 		// Initialise sampler info
 		reset();
 		resetStats();
@@ -65,50 +65,72 @@ public class SamplerBoundedUntilCont extends SamplerBoolean
 	@Override
 	public void update(Path path) throws PrismLangException
 	{
-		if (path.size() > 0) {
-			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
+		// For continuous-time bounded until, we may need to look back at previous state.
+		// So, treat first/subsequent calls to update() differently. 
 
-				// could have missed out evaluation of right
-				if (timeSoFar - path.getTimeInPreviousState() <= lb) {
-					if (right.evaluateBoolean(path.getPreviousState())) {
-						valueKnown = true;
-						value = true;
-					} else {
-						valueKnown = true;
-						value = false;
-					}
-				} else {
+		// First path state:
+		if (path.size() == 0) {
+			// Initially, zero time has elapsed so to satisfy the until,
+			// we need a lower time bound of 0 and the RHS to be satisfied 
+			if (lb == 0.0) {
+				if (right.evaluateBoolean(path.getCurrentState())) {
 					valueKnown = true;
-					value = false;
+					value = true;
 				}
-			} else if (timeSoFar <= lb) {
+			}
+			// If LHS of the until violated, will never be true
+			else {
 				if (!left.evaluateBoolean(path.getCurrentState())) {
 					valueKnown = true;
 					value = false;
 				}
-			} else {
-				if (right.evaluateBoolean(path.getCurrentState())) {
+			}
+		}
+		// Second and subsequent path states:
+		else {
+			double timeSoFar = path.getTimeSoFar();
+			// As soon as upper time bound exceeded, we can decide
+			if (timeSoFar > ub) {
+				// Upper time bound was exceeded (for first time) in *previous* state
+				// Had we reached the target (i.e. RHS of until)?
+				if (right.evaluateBoolean(path.getPreviousState())) {
 					valueKnown = true;
 					value = true;
-				} else if (!left.evaluateBoolean(path.getCurrentState())) {
+				}
+				// If not, it's too late now
+				else {
 					valueKnown = true;
 					value = false;
 				}
 			}
-		} else {
-			if (lb == 0.0) {
+			// Lower bound not yet exceeded but LHS of until violated
+			// (no need to check RHS because too early)
+			else if (timeSoFar <= lb) {
+				if (!left.evaluateBoolean(path.getCurrentState())) {
+					valueKnown = true;
+					value = false;
+				}
+			}
+			// Current time is between lower/upper bounds...
+			else {
+				// Have we reached the target (i.e. RHS of until)?
 				if (right.evaluateBoolean(path.getCurrentState())) {
 					valueKnown = true;
 					value = true;
 				}
-			} else {
-				if (!left.evaluateBoolean(path.getCurrentState())) {
+				// Or, if not, have we violated the LHS of the until?
+				else if (!left.evaluateBoolean(path.getCurrentState())) {
 					valueKnown = true;
 					value = false;
 				}
+				// If the lower bound was exceeded for the first time in the
+				// previous state, and that one satisfies the RHS of the until...
+				else if (timeSoFar - path.getTimeInPreviousState() <= lb) {
+					if (right.evaluateBoolean(path.getPreviousState())) {
+						valueKnown = true;
+						value = true;
+					}
+				}
 			}
 		}
 	}

prism/src/simulator/sampler/SamplerRewardCumulCont.java

@@ -66,7 +66,11 @@ public class SamplerRewardCumulCont extends SamplerDouble
 			// 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)
+			// Note that this cannot be the case for the first state of path,
+			// so the call to getTimeInPreviousState() is safe.
 			if (excessTime > 0) {
+				// Note: Time so far > 0 so cannot be first state,
+				// so safe to look at previous state.
 				value -= path.getPreviousStateReward(rewardStructIndex) * (excessTime / path.getTimeInPreviousState());
 				value -= path.getPreviousTransitionReward(rewardStructIndex);
 			}

prism/src/simulator/sampler/SamplerRewardInstCont.java

@@ -63,6 +63,8 @@ public class SamplerRewardInstCont extends SamplerDouble
 			// 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) {
+				// Note: Time so far > 0 so cannot be first state,
+				// so safe to look at previous state.
 				value = path.getPreviousStateReward(rewardStructIndex);
 			} else {
 				value = path.getCurrentStateReward(rewardStructIndex);