Bug fix in -simpath: state/step indices were not being displayed correctly when changes=true was set.

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

prism/src/simulator/GenerateSimulationPath.java

@@ -386,7 +386,7 @@ public class GenerateSimulationPath
 			i++;
 			if (simPathType != PathType.SIM_PATH_DEADLOCK) {
 				displayer.step(path.getTimeInPreviousState(), path.getTotalTime(), path.getPreviousModuleOrAction(), path.getPreviousProbability(),
-						path.getPreviousTransitionRewards(), path.getCurrentState(), path.getCurrentStateRewards());
+						path.getPreviousTransitionRewards(), path.size(), path.getCurrentState(), path.getCurrentStateRewards());
 			}
 			// Check for termination (depending on type)
 			switch (simPathType) {

prism/src/simulator/PathDisplayer.java

@@ -159,19 +159,19 @@ public abstract class PathDisplayer
 		}
 	}
 
-	public void step(double timeSpent, double timeCumul, Object action, double probability, double[] transitionRewards, State newState, double[] newStateRewards)
+	public void step(double timeSpent, double timeCumul, Object action, double probability, double[] transitionRewards, int newStateIndex, State newState, double[] newStateRewards)
 	{
 		if (showSnapshots) {
 			if (timeCumul < nextTime) {
 				return;
 			} else {
 				while (timeCumul >= nextTime) {
-					displaySnapshot(nextTime, newState, newStateRewards);
+					displaySnapshot(nextTime, newStateIndex, newState, newStateRewards);
 					nextTime += snapshotTimeStep;
 				}
 			}
 		} else {
-			displayStep(timeSpent, timeCumul, action, probability, transitionRewards, newState, newStateRewards);
+			displayStep(timeSpent, timeCumul, action, probability, transitionRewards, newStateIndex, newState, newStateRewards);
 		}
 	}
 
@@ -190,12 +190,12 @@ public abstract class PathDisplayer
 	/**
 	 * Displaying a step of a path.
 	 */
-	public abstract void displayStep(double timeSpent, double timeCumul, Object action, double probability, double[] transitionRewards, State newState, double[] newStateRewards);
+	public abstract void displayStep(double timeSpent, double timeCumul, Object action, double probability, double[] transitionRewards, int newStateIndex, State newState, double[] newStateRewards);
 
 	/**
 	 * Displaying a snapshot of a path at a particular time instant.
 	 */
-	public abstract void displaySnapshot(double timeCumul, State newState, double[] newStateRewards);
+	public abstract void displaySnapshot(double timeCumul, int newStateIndex, State newState, double[] newStateRewards);
 
 	/**
 	 * Finish displaying a path..

prism/src/simulator/PathFull.java

@@ -497,7 +497,7 @@ public class PathFull extends Path implements PathFullInfo
 		displayer.start(getState(0), getStateRewards(0));
 		int n = size();
 		for (int i = 1; i <= n; i++) {
-			displayer.step(getTime(i - 1), getCumulativeTime(i), getModuleOrAction(i - 1), getProbability(i - 1), getTransitionRewards(i), getState(i), getStateRewards(i));
+			displayer.step(getTime(i - 1), getCumulativeTime(i), getModuleOrAction(i - 1), getProbability(i - 1), getTransitionRewards(i), i, getState(i), getStateRewards(i));
 		}
 		displayer.end();
 	}

prism/src/simulator/PathToGraph.java

@@ -115,13 +115,13 @@ public class PathToGraph extends PathDisplayer
 	}
 
 	@Override
-	public void displayStep(double timeSpent, double timeCumul, Object action, double probability, double[] transitionRewards, State newState, double[] newStateRewards)
+	public void displayStep(double timeSpent, double timeCumul, Object action, double probability, double[] transitionRewards, int newStateIndex, State newState, double[] newStateRewards)
 	{
 		displayState(timeCumul, newState, newStateRewards, !showChangesOnly);
 	}
 
 	@Override
-	public void displaySnapshot(double timeCumul, State newState, double[] newStateRewards)
+	public void displaySnapshot(double timeCumul, int newStateIndex, State newState, double[] newStateRewards)
 	{
 		displayState(timeCumul, newState, newStateRewards, !showChangesOnly);
 	}

prism/src/simulator/PathToText.java

@@ -50,8 +50,6 @@ public class PathToText extends PathDisplayer
 	private String colSep = " ";
 
 	// Displayer state
-	/** Step counter */
-	private int step;
 	/** Is the next column the first? */
 	private boolean firstCol;
 	/** Last state */
@@ -147,7 +145,6 @@ public class PathToText extends PathDisplayer
 
 		// Display initial step
 		changed = true;
-		step = 0;
 		firstCol = true;
 		if (!getShowSnapshots()) {
 			log.print(getColSep() + "-");
@@ -168,7 +165,7 @@ public class PathToText extends PathDisplayer
 	}
 
 	@Override
-	public void displayStep(double timeSpent, double timeCumul, Object action, double probability, double[] transitionRewards, State newState, double[] newStateRewards)
+	public void displayStep(double timeSpent, double timeCumul, Object action, double probability, double[] transitionRewards, int newStateIndex, State newState, double[] newStateRewards)
 	{
 		if (!showChangesOnly || changed) {
 			// display rewards for last state
@@ -191,7 +188,6 @@ public class PathToText extends PathDisplayer
 				return;
 		}
 
-		step++;
 		firstCol = true;
 
 		// display action
@@ -200,7 +196,7 @@ public class PathToText extends PathDisplayer
 		if (showProbs)
 			log.print(getColSep() + probability);
 		// display state index
-		log.print(getColSep() + step);
+		log.print(getColSep() + newStateIndex);
 		// display cumulative time
 		if (contTime && showTimeCumul)
 			log.print(getColSep() + timeCumul);
@@ -213,9 +209,8 @@ public class PathToText extends PathDisplayer
 	}
 
 	@Override
-	public void displaySnapshot(double timeCumul, State newState, double[] newStateRewards)
+	public void displaySnapshot(double timeCumul, int newStateIndex, State newState, double[] newStateRewards)
 	{
-		step++;
 		firstCol = true;
 
 		// display cumulative time