Move normalisation of DTMC probabilities from SimulatorEngine into Updater class.

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

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)

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()

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;

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()

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

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
 
 	/**

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);