Added probs option to -simpath switch allow displaying of transition probabilities/rates (+ addition of this info to underlying path data structures, interfaces, etc.)

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

prism/src/simulator/GenerateSimulationPath.java

@@ -43,7 +43,7 @@ public class GenerateSimulationPath
 	// The simulator engine and a log for output
 	private SimulatorEngine engine;
 	private PrismLog mainLog;
-	
+
 	// Store warnings
 	private List<String> warnings = new ArrayList<String>();
 
@@ -66,6 +66,7 @@ public class GenerateSimulationPath
 	private ArrayList<Integer> simVars = null;
 	private boolean simLoopCheck = true;
 	private int simPathRepeat = 1;
+	private boolean simPathShowProbs = false;
 	private boolean simPathShowRewards = false;
 	private boolean simPathShowChangesOnly = false;
 	private boolean simPathSnapshots = false;
@@ -75,12 +76,12 @@ public class GenerateSimulationPath
 	{
 		return warnings.size();
 	}
-	
+
 	public List<String> getWarnings()
 	{
 		return warnings;
 	}
-	
+
 	/**
 	 * Send a warning messages to the log;
 	 * also, store a copy for later retrieval.
@@ -90,7 +91,7 @@ public class GenerateSimulationPath
 		mainLog.printWarning(msg + ".");
 		warnings.add(msg);
 	}
-	
+
 	public GenerateSimulationPath(SimulatorEngine engine, PrismLog mainLog)
 	{
 		this.engine = engine;
@@ -255,6 +256,15 @@ public class GenerateSimulationPath
 				} catch (NumberFormatException e) {
 					throw new PrismException("Value for \"snapshot\" option must be a positive double");
 				}
+			} else if (ss[i].indexOf("probs=") == 0) {
+				// display probabilities/rates?
+				String bool = ss[i].substring(6).toLowerCase();
+				if (bool.equals("true"))
+					simPathShowProbs = true;
+				else if (bool.equals("false"))
+					simPathShowProbs = false;
+				else
+					throw new PrismException("Value for \"rewards\" option must \"true\" or \"false\"");
 			} else if (ss[i].indexOf("rewards=") == 0) {
 				// display rewards?
 				String bool = ss[i].substring(8).toLowerCase();
@@ -314,6 +324,7 @@ public class GenerateSimulationPath
 		displayer = new PathToText(log, modulesFile);
 		displayer.setColSep(simPathSep);
 		displayer.setVarsToShow(simVars);
+		displayer.setShowProbs(simPathShowProbs);
 		displayer.setShowRewards(simPathShowRewards);
 		displayer.setShowChangesOnly(simPathShowChangesOnly);
 		if (simPathSnapshots)
@@ -331,6 +342,7 @@ public class GenerateSimulationPath
 
 		displayer = new PathToGraph(graphModel, modulesFile);
 		displayer.setVarsToShow(simVars);
+		displayer.setShowProbs(simPathShowProbs);
 		displayer.setShowRewards(simPathShowRewards);
 		displayer.setShowChangesOnly(simPathShowChangesOnly);
 		if (simPathSnapshots)
@@ -373,8 +385,8 @@ public class GenerateSimulationPath
 			engine.automaticTransition();
 			i++;
 			if (simPathType != PathType.SIM_PATH_DEADLOCK) {
-				displayer.step(path.getTimeInPreviousState(), path.getTotalTime(), path.getPreviousModuleOrAction(), path.getPreviousTransitionRewards(),
-						path.getCurrentState(), path.getCurrentStateRewards());
+				displayer.step(path.getTimeInPreviousState(), path.getTotalTime(), path.getPreviousModuleOrAction(), path.getPreviousProbability(),
+						path.getPreviousTransitionRewards(), path.getCurrentState(), path.getCurrentStateRewards());
 			}
 			// Check for termination (depending on type)
 			switch (simPathType) {

prism/src/simulator/Path.java

@@ -45,13 +45,13 @@ public abstract class Path
 	 * Add a step to the path.
 	 * Note: State object and arrays will be copied, not stored directly.
 	 */
-	public abstract void addStep(int choice, int actionIndex, double[] transRewards, State newState, double[] newStateRewards, TransitionList transitionList);
+	public abstract void addStep(int choice, int actionIndex, double probability, double[] transRewards, State newState, double[] newStateRewards, TransitionList transitionList);
 
 	/**
 	 * Add a timed step to the path.
 	 * Note: State object and arrays will be copied, not stored directly.
 	 */
-	public abstract void addStep(double time, int choice, int actionIndex, double[] transRewards, State newState, double[] newStateRewards, TransitionList transitionList);
+	public abstract void addStep(double time, int choice, int actionIndex, double probability, double[] transRewards, State newState, double[] newStateRewards, TransitionList transitionList);
 
 	// ACCESSORS
 
@@ -87,6 +87,11 @@ public abstract class Path
 	 */
 	public abstract String getPreviousModuleOrAction();
 	
+	/**
+	 * Get the probability or rate associated wuth the previous step.
+	 */
+	public abstract double getPreviousProbability();
+	
 	/**
 	 * Get the total time elapsed so far (where zero time has been spent in the current (final) state).
 	 * For discrete-time models, this is just the number of steps (but returned as a double).

prism/src/simulator/PathDisplayer.java

@@ -49,6 +49,9 @@ public abstract class PathDisplayer
 	/** Indices of variables to show (null = all) */
 	protected List<Integer> varsToShow = null;
 
+	/** Should we show transition probabilities/rates? */
+	protected boolean showProbs = false;
+	
 	/** Should we display rewards? */
 	protected boolean showRewards = false;
 
@@ -78,6 +81,14 @@ public abstract class PathDisplayer
 		return showChangesOnly;
 	}
 	
+	/**
+	 * Should we display transition probabilities/rates?
+	 */
+	public boolean getShowProbs()
+	{
+		return showProbs;
+	}
+	
 	/**
 	 * Should we display rewards?
 	 */
@@ -122,6 +133,14 @@ public abstract class PathDisplayer
 		this.varsToShow = varsToShow == null ? null : new ArrayList<Integer>(varsToShow);
 	}
 
+	/**
+	 * Set whether we show the probability/rate for each transition
+	 */
+	public void setShowProbs(boolean showProbs)
+	{
+		this.showProbs = showProbs;
+	}
+
 	/**
 	 * Set whether we we display rewards.
 	 */
@@ -140,7 +159,7 @@ public abstract class PathDisplayer
 		}
 	}
 
-	public void step(double timeSpent, double timeCumul, Object action, double[] transitionRewards, State newState, double[] newStateRewards)
+	public void step(double timeSpent, double timeCumul, Object action, double probability, double[] transitionRewards, State newState, double[] newStateRewards)
 	{
 		if (showSnapshots) {
 			if (timeCumul < nextTime) {
@@ -152,7 +171,7 @@ public abstract class PathDisplayer
 				}
 			}
 		} else {
-			displayStep(timeSpent, timeCumul, action, transitionRewards, newState, newStateRewards);
+			displayStep(timeSpent, timeCumul, action, probability, transitionRewards, newState, newStateRewards);
 		}
 	}
 
@@ -171,7 +190,7 @@ public abstract class PathDisplayer
 	/**
 	 * Displaying a step of a path.
 	 */
-	public abstract void displayStep(double timeSpent, double timeCumul, Object action, double[] transitionRewards, State newState, double[] newStateRewards);
+	public abstract void displayStep(double timeSpent, double timeCumul, Object action, double probability, double[] transitionRewards, State newState, double[] newStateRewards);
 
 	/**
 	 * Displaying a snapshot of a path at a particular time instant.

prism/src/simulator/PathFull.java

@@ -104,13 +104,13 @@ public class PathFull extends Path implements PathFullInfo
 	}
 
 	@Override
-	public void addStep(int choice, int moduleOrActionIndex, double[] transitionRewards, State newState, double[] newStateRewards, TransitionList transitionList)
+	public void addStep(int choice, int moduleOrActionIndex, double probability, double[] transitionRewards, State newState, double[] newStateRewards, TransitionList transitionList)
 	{
-		addStep(1.0, choice, moduleOrActionIndex, transitionRewards, newState, newStateRewards, transitionList);
+		addStep(1.0, choice, moduleOrActionIndex, probability, transitionRewards, newState, newStateRewards, transitionList);
 	}
 
 	@Override
-	public void addStep(double time, int choice, int moduleOrActionIndex, double[] transitionRewards, State newState, double[] newStateRewards,
+	public void addStep(double time, int choice, int moduleOrActionIndex, double probability, double[] transitionRewards, State newState, double[] newStateRewards,
 			TransitionList transitionList)
 	{
 		Step stepOld, stepNew;
@@ -119,6 +119,7 @@ public class PathFull extends Path implements PathFullInfo
 		stepOld.time = time;
 		stepOld.choice = choice;
 		stepOld.moduleOrActionIndex = moduleOrActionIndex;
+		stepOld.probability = probability;
 		stepOld.transitionRewards = transitionRewards.clone();
 		// Add new step item to the path
 		stepNew = new Step();
@@ -160,6 +161,7 @@ public class PathFull extends Path implements PathFullInfo
 		last.time = 0.0;
 		last.choice = -1;
 		last.moduleOrActionIndex = 0;
+		last.probability = 0.0;
 		for (i = 0; i < numRewardStructs; i++)
 			last.transitionRewards[i] = 0.0;
 		// Update size too
@@ -250,6 +252,12 @@ public class PathFull extends Path implements PathFullInfo
 			return "?";
 	}
 
+	@Override
+	public double getPreviousProbability()
+	{
+		return steps.get(steps.size() - 2).probability;
+	}
+	
 	@Override
 	public double getTotalTime()
 	{
@@ -415,6 +423,15 @@ public class PathFull extends Path implements PathFullInfo
 			return "?";
 	}
 
+	/**
+	 * Get the probability or rate associated with a given step.
+	 * @param step Step index (0 = initial state/step of path)
+	 */
+	public double getProbability(int step)
+	{
+		return steps.get(steps.size() - 2).probability;
+	}
+	
 	/**
 	 * Get a transition reward associated with a given step.
 	 * @param step Step index (0 = initial state/step of path)
@@ -480,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), getTransitionRewards(i), getState(i), getStateRewards(i));
+			displayer.step(getTime(i - 1), getCumulativeTime(i), getModuleOrAction(i - 1), getProbability(i - 1), getTransitionRewards(i), getState(i), getStateRewards(i));
 		}
 		displayer.end();
 	}
@@ -551,6 +568,7 @@ public class PathFull extends Path implements PathFullInfo
 			time = 0.0;
 			choice = -1;
 			moduleOrActionIndex = 0;
+			probability = 0.0;
 			transitionRewards = new double[numRewardStructs];
 		}
 
@@ -569,6 +587,8 @@ public class PathFull extends Path implements PathFullInfo
 		// Action label taken (i.e. the index in the model's list of all actions).
 		// This is 1-indexed, with 0 denoting an independent ("tau"-labelled) command.
 		public int moduleOrActionIndex;
+		// Probability or rate of step
+		public double probability;
 		// Transition rewards associated with step
 		public double transitionRewards[];
 	}

prism/src/simulator/PathFullPrefix.java

@@ -57,13 +57,13 @@ public class PathFullPrefix extends Path
 	}
 
 	@Override
-	public void addStep(int choice, int moduleOrActionIndex, double[] transitionRewards, State newState, double[] newStateRewards, TransitionList transitionList)
+	public void addStep(int choice, int moduleOrActionIndex, double probability, double[] transitionRewards, State newState, double[] newStateRewards, TransitionList transitionList)
 	{
 		// Do nothing (we are not allowed to modify the underlying PathFull)
 	}
 
 	@Override
-	public void addStep(double time, int choice, int moduleOrActionIndex, double[] transitionRewards, State newState, double[] newStateRewards, TransitionList transitionList)
+	public void addStep(double time, int choice, int moduleOrActionIndex, double probability, double[] transitionRewards, State newState, double[] newStateRewards, TransitionList transitionList)
 	{
 		// Do nothing (we are not allowed to modify the underlying PathFull)
 	}
@@ -113,6 +113,12 @@ public class PathFullPrefix extends Path
 		return pathFull.getModuleOrAction(prefixLength - 1);
 	}
 	
+	@Override
+	public double getPreviousProbability()
+	{
+		return pathFull.getProbability(prefixLength - 1);
+	}
+
 	@Override
 	public double getTotalTime()
 	{

prism/src/simulator/PathOnTheFly.java

@@ -47,6 +47,7 @@ public class PathOnTheFly extends Path
 	protected State previousState;
 	protected State currentState;
 	protected int previousModuleOrActionIndex;
+	protected double previousProbability;
 	protected double totalTime;
 	double timeInPreviousState;
 	protected double totalRewards[];
@@ -114,18 +115,19 @@ public class PathOnTheFly extends Path
 	}
 
 	@Override
-	public void addStep(int choice, int moduleOrActionIndex, double[] transRewards, State newState, double[] newStateRewards, TransitionList transitionList)
+	public void addStep(int choice, int moduleOrActionIndex, double probability, double[] transRewards, State newState, double[] newStateRewards, TransitionList transitionList)
 	{
-		addStep(1.0, choice, moduleOrActionIndex, transRewards, newState, newStateRewards, transitionList);
+		addStep(1.0, choice, moduleOrActionIndex, probability, transRewards, newState, newStateRewards, transitionList);
 	}
 
 	@Override
-	public void addStep(double time, int choice, int moduleOrActionIndex, double[] transRewards, State newState, double[] newStateRewards, TransitionList transitionList)
+	public void addStep(double time, int choice, int moduleOrActionIndex, double probability, double[] transRewards, State newState, double[] newStateRewards, TransitionList transitionList)
 	{
 		size++;
 		previousState.copy(currentState);
 		currentState.copy(newState);
 		previousModuleOrActionIndex = moduleOrActionIndex;
+		previousProbability = probability;
 		totalTime += time;
 		timeInPreviousState = time;
 		for (int i = 0; i < numRewardStructs; i++) {
@@ -186,6 +188,12 @@ public class PathOnTheFly extends Path
 			return "?";
 	}
 
+	@Override
+	public double getPreviousProbability()
+	{
+		return previousProbability;
+	}
+
 	@Override
 	public double getTotalTime()
 	{

prism/src/simulator/PathToGraph.java

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

prism/src/simulator/PathToText.java

@@ -114,6 +114,8 @@ public class PathToText extends PathDisplayer
 		firstCol = true;
 		if (!getShowSnapshots()) {
 			log.print(getColSep() + "action");
+			if (showProbs)
+				log.print(getColSep() + "probability");
 			log.print(getColSep() + "step");
 		}
 		if (contTime && showTimeCumul)
@@ -148,7 +150,10 @@ public class PathToText extends PathDisplayer
 		step = 0;
 		firstCol = true;
 		if (!getShowSnapshots()) {
-			log.print(getColSep() + "-" + getColSep() + "0");
+			log.print(getColSep() + "-");
+			if (showProbs)
+				log.print(getColSep() + "-");
+			log.print(getColSep() + "0");
 		}
 		if (contTime && showTimeCumul)
 			log.print(getColSep() + "0.0");
@@ -163,7 +168,7 @@ public class PathToText extends PathDisplayer
 	}
 
 	@Override
-	public void displayStep(double timeSpent, double timeCumul, Object action, double[] transitionRewards, State newState, double[] newStateRewards)
+	public void displayStep(double timeSpent, double timeCumul, Object action, double probability, double[] transitionRewards, State newState, double[] newStateRewards)
 	{
 		if (!showChangesOnly || changed) {
 			// display rewards for last state
@@ -191,6 +196,9 @@ public class PathToText extends PathDisplayer
 
 		// display action
 		log.print(getColSep() + action);
+		// display probability/rate
+		if (showProbs)
+			log.print(getColSep() + probability);
 		// display state index
 		log.print(getColSep() + step);
 		// display cumulative time

prism/src/simulator/SimulatorEngine.java

@@ -705,6 +705,8 @@ public class SimulatorEngine
 		Choice choice = transitions.getChoice(i);
 		if (!onTheFly && index == -1)
 			index = transitions.getTotalIndexOfTransition(i, offset);
+		// Compute probability for transition (is normalised for a DTMC)
+		double p = (modelType == ModelType.DTMC ? choice.getProbability(offset) / transitions.getNumChoices() : choice.getProbability(offset));
 		// Compute its transition rewards
 		updater.calculateTransitionRewards(path.getCurrentState(), choice, tmpTransitionRewards);
 		// Compute next state. Note use of path.getCurrentState() because currentState
@@ -713,7 +715,7 @@ public class SimulatorEngine
 		// Compute state rewards for new state 
 		updater.calculateStateRewards(currentState, tmpStateRewards);
 		// Update path
-		path.addStep(index, choice.getModuleOrActionIndex(), tmpTransitionRewards, currentState, tmpStateRewards, transitions);
+		path.addStep(index, choice.getModuleOrActionIndex(), p, tmpTransitionRewards, currentState, tmpStateRewards, transitions);
 		// Reset transition list 
 		transitionListBuilt = false;
 		transitionListState = null;
@@ -740,6 +742,8 @@ public class SimulatorEngine
 		Choice choice = transitions.getChoice(i);
 		if (!onTheFly && index == -1)
 			index = transitions.getTotalIndexOfTransition(i, offset);
+		// Get probability for transition (no need to normalise because DTMC transitions are never timed)
+		double p = choice.getProbability(offset);
 		// Compute its transition rewards
 		updater.calculateTransitionRewards(path.getCurrentState(), choice, tmpTransitionRewards);
 		// Compute next state. Note use of path.getCurrentState() because currentState
@@ -748,7 +752,7 @@ public class SimulatorEngine
 		// Compute state rewards for new state 
 		updater.calculateStateRewards(currentState, tmpStateRewards);
 		// Update path
-		path.addStep(time, index, choice.getModuleOrActionIndex(), tmpTransitionRewards, currentState, tmpStateRewards, transitions);
+		path.addStep(time, index, choice.getModuleOrActionIndex(), p, tmpTransitionRewards, currentState, tmpStateRewards, transitions);
 		// Reset transition list 
 		transitionListBuilt = false;
 		transitionListState = null;