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

@@ -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

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) 
 	}
 
 	/**