diff --git a/prism/src/simulator/Choice.java b/prism/src/simulator/Choice.java index 57736804..dfd45efa 100644 --- a/prism/src/simulator/Choice.java +++ b/prism/src/simulator/Choice.java @@ -31,6 +31,11 @@ import prism.*; public interface Choice { + /** + * Scale probability/rate of all transitions, multiplying by d. + */ + public void scaleProbabilitiesBy(double d); + /** * Get the module/action for this choice, as an integer index * (-i for independent in ith module, i for synchronous on ith action) diff --git a/prism/src/simulator/ChoiceList.java b/prism/src/simulator/ChoiceList.java index 2e4f2ea6..168e0673 100644 --- a/prism/src/simulator/ChoiceList.java +++ b/prism/src/simulator/ChoiceList.java @@ -92,6 +92,16 @@ public class ChoiceList implements Choice this.command.set(i, command); } + @Override + public void scaleProbabilitiesBy(double d) + { + int i, n; + n = size(); + for (i = 0; i < n; i++) { + probability.set(i, probability.get(i) * d); + } + } + // Get methods public int getModuleOrActionIndex() diff --git a/prism/src/simulator/ChoiceListFlexi.java b/prism/src/simulator/ChoiceListFlexi.java index a8175fbb..ce7749ef 100644 --- a/prism/src/simulator/ChoiceListFlexi.java +++ b/prism/src/simulator/ChoiceListFlexi.java @@ -102,9 +102,7 @@ public class ChoiceListFlexi implements Choice this.probability.add(probability); } - /** - * Scale probability/rate of all transitions, multiplying by d. - */ + @Override public void scaleProbabilitiesBy(double d) { int i, n; diff --git a/prism/src/simulator/ChoiceSingleton.java b/prism/src/simulator/ChoiceSingleton.java index efe52c1e..c36e3147 100644 --- a/prism/src/simulator/ChoiceSingleton.java +++ b/prism/src/simulator/ChoiceSingleton.java @@ -63,6 +63,12 @@ public class ChoiceSingleton implements Choice this.probability = probability; } + @Override + public void scaleProbabilitiesBy(double d) + { + probability *= d; + } + // Get methods public int getModuleOrActionIndex() diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index 420ff588..45efadd6 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -741,8 +741,8 @@ public class SimulatorEngine extends PrismComponent 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.getProbabilitySum() : choice.getProbability(offset)); + // Get probability for transition + 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 @@ -780,7 +780,7 @@ public class SimulatorEngine extends PrismComponent 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) + // Get probability for transition double p = choice.getProbability(offset); // Compute its transition rewards updater.calculateTransitionRewards(path.getCurrentState(), choice, tmpTransitionRewards); @@ -1025,9 +1025,7 @@ public class SimulatorEngine extends PrismComponent public double getTransitionProbability(int i, int offset) throws PrismException { TransitionList transitions = getTransitionList(); - double p = transitions.getChoice(i).getProbability(offset); - // For DTMCs, we need to normalise (over choices) - return (modelType == ModelType.DTMC ? p / transitions.getProbabilitySum() : p); + return transitions.getChoice(i).getProbability(offset); } /** @@ -1036,9 +1034,7 @@ public class SimulatorEngine extends PrismComponent public double getTransitionProbability(int index) throws PrismException { TransitionList transitions = getTransitionList(); - double p = transitions.getTransitionProbability(index); - // For DTMCs, we need to normalise (over choices) - return (modelType == ModelType.DTMC ? p / transitions.getProbabilitySum() : p); + return transitions.getTransitionProbability(index); } /** diff --git a/prism/src/simulator/TransitionList.java b/prism/src/simulator/TransitionList.java index 68c0a671..36cb68e6 100644 --- a/prism/src/simulator/TransitionList.java +++ b/prism/src/simulator/TransitionList.java @@ -75,6 +75,16 @@ public class TransitionList probSum += tr.getProbabilitySum(); } + /** + * Scale probability/rate of all transitions in all choices, multiplying by d. + */ + public void scaleProbabilitiesBy(double d) + { + for (int i = 0; i < numChoices; i++) { + getChoice(i).scaleProbabilitiesBy(d); + } + } + // ACCESSORS /** diff --git a/prism/src/simulator/Updater.java b/prism/src/simulator/Updater.java index 5f4b9268..6dcf11c2 100644 --- a/prism/src/simulator/Updater.java +++ b/prism/src/simulator/Updater.java @@ -226,6 +226,14 @@ public class Updater extends PrismComponent } } + // For a DTMC, we need to normalise across all transitions + // This is partly to handle "local nondeterminism" + // and also to handle any dubious trickery done by disabling probability checks + if (modelType == ModelType.DTMC) { + double probSum = transitionList.getProbabilitySum(); + transitionList.scaleProbabilitiesBy(1.0 / probSum); + } + // Check validity of the computed transitions // (not needed currently) //transitionList.checkValid(modelType);