From d128da069bf7a406e73f68034d7c603671c0744f Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 6 Jan 2014 13:45:24 +0000 Subject: [PATCH] Bug fix: simulator was normalising DTMC bu dividing by number of choices (which was inconsistent with symbolic construction when using -noprobchecks). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7797 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/simulator/SimulatorEngine.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index e976422d..531e45af 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -743,7 +743,7 @@ public class SimulatorEngine extends PrismComponent 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)); + double p = (modelType == ModelType.DTMC ? choice.getProbability(offset) / transitions.getProbabilitySum() : choice.getProbability(offset)); // Compute its transition rewards updater.calculateTransitionRewards(path.getCurrentState(), choice, tmpTransitionRewards); // Compute next state. Note use of path.getCurrentState() because currentState @@ -1028,7 +1028,7 @@ public class SimulatorEngine extends PrismComponent TransitionList transitions = getTransitionList(); double p = transitions.getChoice(i).getProbability(offset); // For DTMCs, we need to normalise (over choices) - return (modelType == ModelType.DTMC ? p / transitions.getNumChoices() : p); + return (modelType == ModelType.DTMC ? p / transitions.getProbabilitySum() : p); } /** @@ -1039,7 +1039,7 @@ public class SimulatorEngine extends PrismComponent TransitionList transitions = getTransitionList(); double p = transitions.getTransitionProbability(index); // For DTMCs, we need to normalise (over choices) - return (modelType == ModelType.DTMC ? p / transitions.getNumChoices() : p); + return (modelType == ModelType.DTMC ? p / transitions.getProbabilitySum() : p); } /**