From 2690b87ff536c17b90bf577d40a5958009a8dbae Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 3 Dec 2014 14:03:44 +0000 Subject: [PATCH] Bug fix in simulator: in DTMCs with local nondeterminism, random transitions can be wrongly chosen due to the distributions not being normalised. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9352 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/simulator/SimulatorEngine.java | 10 +++++++++- prism/src/simulator/TransitionList.java | 7 +++---- 2 files changed, 12 insertions(+), 5 deletions(-) diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index d3b0c534..67cacb44 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -299,8 +299,16 @@ public class SimulatorEngine extends PrismComponent return false; //throw new PrismException("Deadlock found at state " + path.getCurrentState().toString(modulesFile)); + TransitionList.Ref ref; switch (modelType) { case DTMC: + // Pick a random number to determine choice/transition + d = rng.randomUnifDouble(); + ref = transitions.new Ref(); + transitions.getChoiceIndexByProbabilitySum(d, ref); + // Execute + executeTransition(ref.i, ref.offset, -1); + break; case MDP: // Pick a random choice i = rng.randomUnifInt(numChoices); @@ -316,7 +324,7 @@ public class SimulatorEngine extends PrismComponent r = transitions.getProbabilitySum(); // Pick a random number to determine choice/transition d = rng.randomUnifDouble(r); - TransitionList.Ref ref = transitions.new Ref(); + ref = transitions.new Ref(); transitions.getChoiceIndexByProbabilitySum(d, ref); // Execute executeTimedTransition(ref.i, ref.offset, rng.randomExpDouble(r), -1); diff --git a/prism/src/simulator/TransitionList.java b/prism/src/simulator/TransitionList.java index 36cb68e6..68d43ac2 100644 --- a/prism/src/simulator/TransitionList.java +++ b/prism/src/simulator/TransitionList.java @@ -158,10 +158,9 @@ public class TransitionList // Random selection of a choice /** - * Get a reference to a transition according to a total probability (rate) sum, x. - * i.e.the first transition for which the sum of probabilities of that and all prior - * transitions (across all choices) exceeds x. Really, this is designed for the case - * where these are rates, rather than probabilities. + * Get a reference to a transition according to a total probability (or rate) sum, x. + * i.e.the first transition for which the sum of probabilities/rates of that and all prior + * transitions (across all choices) exceeds x. * @param x Probability (or rate) sum * @param ref Empty transition reference to store result */