diff --git a/prism/src/simulator/GenerateSimulationPath.java b/prism/src/simulator/GenerateSimulationPath.java index 0a941805..c5029623 100644 --- a/prism/src/simulator/GenerateSimulationPath.java +++ b/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 warnings = new ArrayList(); @@ -66,6 +66,7 @@ public class GenerateSimulationPath private ArrayList 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 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) { diff --git a/prism/src/simulator/Path.java b/prism/src/simulator/Path.java index 01f6ceed..82b09837 100644 --- a/prism/src/simulator/Path.java +++ b/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). diff --git a/prism/src/simulator/PathDisplayer.java b/prism/src/simulator/PathDisplayer.java index ace287bc..960083c6 100644 --- a/prism/src/simulator/PathDisplayer.java +++ b/prism/src/simulator/PathDisplayer.java @@ -49,6 +49,9 @@ public abstract class PathDisplayer /** Indices of variables to show (null = all) */ protected List 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(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. diff --git a/prism/src/simulator/PathFull.java b/prism/src/simulator/PathFull.java index db29801f..7d6ac19b 100644 --- a/prism/src/simulator/PathFull.java +++ b/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[]; } diff --git a/prism/src/simulator/PathFullPrefix.java b/prism/src/simulator/PathFullPrefix.java index 46402e6e..59fc1c9e 100644 --- a/prism/src/simulator/PathFullPrefix.java +++ b/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() { diff --git a/prism/src/simulator/PathOnTheFly.java b/prism/src/simulator/PathOnTheFly.java index 3b42ed64..a684530a 100644 --- a/prism/src/simulator/PathOnTheFly.java +++ b/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() { diff --git a/prism/src/simulator/PathToGraph.java b/prism/src/simulator/PathToGraph.java index 8a71b31b..b0ce20fa 100644 --- a/prism/src/simulator/PathToGraph.java +++ b/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); } diff --git a/prism/src/simulator/PathToText.java b/prism/src/simulator/PathToText.java index d2f2fcbd..96afdbf0 100644 --- a/prism/src/simulator/PathToText.java +++ b/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 diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index 297fee8d..910d5965 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/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;