From 6bf2d093946f3f18854ebbe30a7d0b0f78006d03 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 23 Apr 2010 10:01:32 +0000 Subject: [PATCH] Updates to simulator, including random choices for CTMCs. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1846 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/simulator/Choice.java | 2 +- prism/src/simulator/ChoiceList.java | 2 +- prism/src/simulator/ChoiceListFlexi.java | 8 +- prism/src/simulator/ChoiceSingleton.java | 2 +- .../src/simulator/GenerateSimulationPath.java | 6 ++ .../src/simulator/RandomNumberGenerator.java | 18 +++- prism/src/simulator/SimulatorEngine.java | 38 +++++--- prism/src/simulator/TransitionList.java | 87 +++++++++++++++++-- prism/src/simulator/Updater.java | 6 +- 9 files changed, 136 insertions(+), 33 deletions(-) diff --git a/prism/src/simulator/Choice.java b/prism/src/simulator/Choice.java index 97452e80..f47f3c68 100644 --- a/prism/src/simulator/Choice.java +++ b/prism/src/simulator/Choice.java @@ -45,5 +45,5 @@ public interface Choice public void computeTarget(State oldState, State newState) throws PrismLangException; public State computeTarget(int i, State oldState) throws PrismLangException; public void computeTarget(int i, State oldState, State newState) throws PrismLangException; - public int getIndexByProbSum(double x); + public int getIndexByProbabilitySum(double x); } diff --git a/prism/src/simulator/ChoiceList.java b/prism/src/simulator/ChoiceList.java index 734e2ec3..7db04ff4 100644 --- a/prism/src/simulator/ChoiceList.java +++ b/prism/src/simulator/ChoiceList.java @@ -173,7 +173,7 @@ public class ChoiceList implements Choice return command.get(i); } - public int getIndexByProbSum(double x) + public int getIndexByProbabilitySum(double x) { int i, n; double d; diff --git a/prism/src/simulator/ChoiceListFlexi.java b/prism/src/simulator/ChoiceListFlexi.java index 64403469..bc0686d2 100644 --- a/prism/src/simulator/ChoiceListFlexi.java +++ b/prism/src/simulator/ChoiceListFlexi.java @@ -191,12 +191,16 @@ public class ChoiceListFlexi implements Choice return command.get(i); } - public int getIndexByProbSum(double x) + /** + * Return the index of a transition according to a probability (or rate) sum, x. + * i.e. return the index of the first transition in this choice for which the + * sum of probabilities/rates for all prior transitions exceeds x. + */ + public int getIndexByProbabilitySum(double x) { int i, n; double d; n = size(); - i = 0; d = 0.0; for (i = 0; x >= d && i < n; i++) { d += probability.get(i); diff --git a/prism/src/simulator/ChoiceSingleton.java b/prism/src/simulator/ChoiceSingleton.java index f5f7478f..178bbac3 100644 --- a/prism/src/simulator/ChoiceSingleton.java +++ b/prism/src/simulator/ChoiceSingleton.java @@ -70,7 +70,7 @@ public class ChoiceSingleton implements Choice return 1; } - public int getIndexByProbSum(double x) + public int getIndexByProbabilitySum(double x) { return 0; } diff --git a/prism/src/simulator/GenerateSimulationPath.java b/prism/src/simulator/GenerateSimulationPath.java index b44df653..27725058 100644 --- a/prism/src/simulator/GenerateSimulationPath.java +++ b/prism/src/simulator/GenerateSimulationPath.java @@ -83,6 +83,9 @@ public class GenerateSimulationPath generatePath(); } + /** + * Parse a string specifying how to generate a simulation path. + */ private void parseDetails(String details) throws PrismException { String s, ss[]; @@ -185,6 +188,9 @@ public class GenerateSimulationPath throw new PrismException("Invalid path details \"" + details + "\""); } + /** + * Generate a random path using the simulator. + */ private void generatePath() throws PrismException { int i = 0, j = 0; diff --git a/prism/src/simulator/RandomNumberGenerator.java b/prism/src/simulator/RandomNumberGenerator.java index b6db4fde..43ab19d7 100644 --- a/prism/src/simulator/RandomNumberGenerator.java +++ b/prism/src/simulator/RandomNumberGenerator.java @@ -40,7 +40,7 @@ public class RandomNumberGenerator /** * Pick a (uniformly) random integer in range [0,...,n-1]. */ - public int randomInt(int n) + public int randomUnifInt(int n) { return random.nextInt(n); } @@ -48,7 +48,7 @@ public class RandomNumberGenerator /** * Pick a (uniformly) random double in range [0,1). */ - public double randomDouble() + public double randomUnifDouble() { return random.nextDouble(); } @@ -56,8 +56,20 @@ public class RandomNumberGenerator /** * Pick a (uniformly) random double in range [0,x). */ - public double randomDouble(double x) + public double randomUnifDouble(double x) { return x * random.nextDouble(); } + + /** + * Pick a random double according to exponential distribution with rate x. + */ + public double randomExpDouble(double x) + { + double y; + // Pick (non-zero) random y in (0,1) + while ((y = random.nextDouble()) == 0); + // Sample exponential + return (-Math.log(y)) / x; + } } diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index 18c54b3c..77666d81 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -403,25 +403,37 @@ public class SimulatorEngine Choice choice; int numChoices, i, j; - double d; + double d, r; switch (modelType) { case DTMC: case MDP: // Check for deadlock - numChoices = transitionList.numChoices; + numChoices = transitionList.getNumChoices(); if (numChoices == 0) throw new PrismException("Deadlock found at state " + currentState.toString(modulesFile)); // Pick a random choice - i = rng.randomInt(numChoices); + i = rng.randomUnifInt(numChoices); choice = transitionList.getChoice(i); // Pick a random transition from this choice - d = rng.randomDouble(); - j = choice.getIndexByProbSum(d); + d = rng.randomUnifDouble(); + j = choice.getIndexByProbabilitySum(d); + // Execute executeTransition(i, j, -1); break; case CTMC: - // TODO: automaticUpdateContinuous(); + // Check for deadlock + numChoices = transitionList.getNumChoices(); + if (numChoices == 0) + throw new PrismException("Deadlock found at state " + currentState.toString(modulesFile)); + // Get sum of all rates + r = transitionList.getProbabilitySum(); + // Pick a random number to determine choice/transition + d = r * rng.randomUnifDouble(); + TransitionList.Ref ref = transitionList.new Ref(); + transitionList.getChoiceIndexByProbabilitySum(d, ref); + // Execute + executeTimedTransition(ref.i, ref.offset, rng.randomExpDouble(r), -1); break; } @@ -460,7 +472,7 @@ public class SimulatorEngine /** * Execute a transition from the current transition list and update path (if being stored). - * Transition is specified by index of it choice and offset within it. If known, its index + * Transition is specified by index of its choice and offset within it. If known, its index * (within the whole list) can optionally be specified (since this may be needed for storage * in the path). If this is -1, it will be computed automatically if needed. * @param i Index of choice containing transition to execute @@ -488,7 +500,7 @@ public class SimulatorEngine /** * Execute a (timed) transition from the current transition list and update path (if being stored). - * Transition is specified by index of it choice and offset within it. If known, its index + * Transition is specified by index of its choice and offset within it. If known, its index * (within the whole list) can optionally be specified (since this may be needed for storage * in the path). If this is -1, it will be computed automatically if needed. * In addition, the amount of time to be spent in the current state before this transition occurs @@ -726,7 +738,7 @@ public class SimulatorEngine */ public int getNumTransitions() { - return transitionList.numTransitions; + return transitionList.getNumTransitions(); } /** @@ -736,7 +748,7 @@ public class SimulatorEngine */ public String getTransitionAction(int index) throws PrismException { - if (index < 0 || index >= transitionList.numTransitions) + if (index < 0 || index >= transitionList.getNumTransitions()) throw new PrismException("Invalid transition index " + index); return transitionList.getChoiceOfTransition(index).getAction(); } @@ -764,13 +776,13 @@ public class SimulatorEngine public double getTransitionProbability(int index) throws PrismException { double p = transitionList.getTransitionProbability(index); - return (modelType == ModelType.DTMC ? p / transitionList.numChoices : p); + return (modelType == ModelType.DTMC ? p / transitionList.getNumChoices() : p); } public State computeTransitionTarget(int index) throws PrismLangException { - // TODO - if (index < 0 || index >= transitionList.numTransitions) + // TODO: need to check bounds? + if (index < 0 || index >= transitionList.getNumTransitions()) return null; //throw new PrismException("Invalid transition index " + index); return transitionList.computeTransitionTarget(index, currentState); diff --git a/prism/src/simulator/TransitionList.java b/prism/src/simulator/TransitionList.java index 869a6f23..d3cf4286 100644 --- a/prism/src/simulator/TransitionList.java +++ b/prism/src/simulator/TransitionList.java @@ -33,13 +33,22 @@ import prism.*; public class TransitionList { - public ArrayList choices = new ArrayList(); - public ArrayList transitionIndices = new ArrayList(); - public ArrayList transitionOffsets = new ArrayList(); - public int numChoices = 0; - public int numTransitions = 0; - public double probSum = 0.0; + private ArrayList choices = new ArrayList(); + private ArrayList transitionIndices = new ArrayList(); + private ArrayList transitionOffsets = new ArrayList(); + private int numChoices = 0; + private int numTransitions = 0; + private double probSum = 0.0; + // TODO: document this + public class Ref + { + public int i; + public int offset; + //int index; + //Choice ch; + } + public void clear() { choices.clear(); @@ -63,7 +72,33 @@ public class TransitionList numTransitions += tr.size(); probSum += tr.getProbabilitySum(); } - + + // ACCESSORS + + /** + * Get the number of choices. + */ + public int getNumChoices() + { + return numChoices; + } + + /** + * Get the number of transitions. + */ + public int getNumTransitions() + { + return numTransitions; + } + + /** + * Get the total sum of all probabilities (or rates). + */ + public double getProbabilitySum() + { + return probSum; + } + // Get access to Choice objects /** @@ -108,6 +143,36 @@ public class TransitionList return transitionOffsets.get(i); } + // 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 all prior transitions + * (across all choices) exceeds x. + * Note: this only really makes sense for models where these are rates, rather than probabilities. + * @param x Probability (or rate) sum + * @param ref Empty transition reference to store result + */ + public void getChoiceIndexByProbabilitySum(double x, Ref ref) + { + int i; + Choice choice; + double d = 0.0, tot = 0.0; + // Add up choice prob/rate sums to find choice + for (i = 0; x >= tot && i < numChoices; i++) { + d = getChoice(i).getProbabilitySum(); + tot += d; + } + ref.i = i - 1; + // Pick transition within choice + choice = getChoice(i - 1); + if (choice.size() > 1) { + ref.offset = choice.getIndexByProbabilitySum(tot - d); + } else { + ref.offset = 0; + } + } + // Access to transition info // get prob (or rate) of ith transition @@ -136,8 +201,14 @@ public class TransitionList public String toString() { String s = ""; - for (Choice tr : choices) + boolean first = true; + for (Choice tr : choices) { + if (first) + first = false; + else + s += ", "; s += tr.toString(); + } return s; } } diff --git a/prism/src/simulator/Updater.java b/prism/src/simulator/Updater.java index b4af509e..70408da2 100644 --- a/prism/src/simulator/Updater.java +++ b/prism/src/simulator/Updater.java @@ -141,6 +141,7 @@ public class Updater } // Case where there are multiple choices else { + // TODO throw new PrismLangException("Don't handle local nondet yet"); } System.out.println("prod" + j + ": " + prod); @@ -202,10 +203,7 @@ public class Updater // For DTMCs, need to randomise - //System.out.println(transitionList.transitionTotal); - System.out.println(transitionList.choices); - //System.out.println(transitionList.transitionIndices); - //System.out.println(transitionList.transitionOffsets); + System.out.println(transitionList); }