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

@@ -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);
 	}
 
 	/**