From 97fddcb1b98c28bd0afd349554a98a440ade4cf4 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Wed, 30 Jun 2010 09:52:07 +0000
Subject: [PATCH] Remove preceding states added to simulator.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1960 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/simulator/PathFull.java        | 36 ++++++++++++++++++++++++
 prism/src/simulator/SimulatorEngine.java | 27 +++++++++++++-----
 2 files changed, 56 insertions(+), 7 deletions(-)

diff --git a/prism/src/simulator/PathFull.java b/prism/src/simulator/PathFull.java
index 33452056..4ba6826e 100644
--- a/prism/src/simulator/PathFull.java
+++ b/prism/src/simulator/PathFull.java
@@ -160,6 +160,42 @@ public class PathFull extends Path
 		size = step;
 	}
 	
+	/**
+	 * Remove the prefix of the current path up to the given path step.
+	 * Index step should be >=0 and <= the total path size. 
+	 * @param step The step before which state will be removed.
+	 */
+	public void removePrecedingStates(int step)
+	{
+		int i, j, n, n2;
+		double timeCumul, rewardsCumul[];
+		
+		// Ignore trivial case
+		if (step == 0)
+			return;
+		// Get cumulative time/reward for index 'step'
+		timeCumul = getCumulativeTime(step);
+		rewardsCumul = new double[numRewardStructs];
+		for (j = 0; j < numRewardStructs; j++)
+			rewardsCumul[j] = getCumulativeReward(step, j);
+		// Move later steps of path 'step' places forward 
+		// and subtract time/reward as appropriate 
+		n = steps.size() - step;
+		for (i = 0; i < n; i++) {
+			Step tmp = steps.get(i + step);
+			tmp.timeCumul -= timeCumul;
+			for (j = 0; j < numRewardStructs; j++)
+				tmp.rewardsCumul[j] -= rewardsCumul[j];
+			steps.set(i, tmp);
+		}
+		// Remove steps after index 'step'
+		n2 = steps.size() - 1;
+		for (i = n2; i >= n; i--)
+			steps.remove(i);
+		// Update size too
+		size = steps.size() - 1;
+	}
+	
 	// ACCESSORS (for Path)
 
 	@Override
diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java
index 8ca9d724..3329dec7 100644
--- a/prism/src/simulator/SimulatorEngine.java
+++ b/prism/src/simulator/SimulatorEngine.java
@@ -505,16 +505,29 @@ public class SimulatorEngine
 	}
 
 	/**
-	 * This function removes states of the path that precede those of the given index
-	 * 
-	 * @param step
-	 *            the index before which the states should be removed.
-	 * @throws PrismException
-	 *             if anything goes wrong with the state removal.
+	 * Remove the prefix of the current path up to the given path step.
+	 * Index step should be >=0 and <= the total path size. 
+	 * (Not applicable for on-the-fly paths)
+	 * @param step The step before which state will be removed.
 	 */
 	public void removePrecedingStates(int step) throws PrismException
 	{
-		//doRemovePrecedingStates(step);
+		// Check step is valid
+		if (step < 0) {
+			throw new PrismException("Cannot remove states before a negative step index");
+		}
+		if (step > path.size()) {
+			throw new PrismException("There is no step " + step + " in the path");
+		}
+		// Modify path
+		((PathFull) path).removePrecedingStates(step);
+		// Update previous state info (if required)
+		// (No need to update current state info)
+		if (path.size() == 1)
+			previousState.clear();
+		// Recompute samplers for any loaded properties
+		recomputeSamplers();
+		// (No need to re-generate updates for new current state) 
 	}
 
 	/**