From cd36ad544fa85daea5e2ab2a081b5d419c9b66c7 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 13 Jul 2010 15:05:40 +0000 Subject: [PATCH] Simulator updates, including local nondet (untested). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1982 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/simulator/ChoiceListFlexi.java | 64 +++++-- prism/src/simulator/Updater.java | 207 +++++++++-------------- 2 files changed, 130 insertions(+), 141 deletions(-) diff --git a/prism/src/simulator/ChoiceListFlexi.java b/prism/src/simulator/ChoiceListFlexi.java index 0d6f5542..8d368340 100644 --- a/prism/src/simulator/ChoiceListFlexi.java +++ b/prism/src/simulator/ChoiceListFlexi.java @@ -34,18 +34,21 @@ import prism.PrismLangException; public class ChoiceListFlexi implements Choice { - // TODO: need mult actions - //protected String action; - + // Module/action info, encoded as an integer. + // For an independent (non-synchronous) choice, this is -i, + // where i is the 1-indexed module index. + // For a synchronous choice, this is the 1-indexed action index. protected int moduleOrActionIndex; // List of multiple targets and associated info // Size of list is stored implicitly in target.length - // TODO: convert to arrays? protected List> updates; protected List probability; protected List command; + /** + * Create empty choice. + */ public ChoiceListFlexi() { updates = new ArrayList>(); @@ -55,19 +58,32 @@ public class ChoiceListFlexi implements Choice // Set methods + /** + * Set the module/action for this choice, encoded as an integer + * (-i for independent in ith module, i for synchronous on ith action) + * (in both cases, modules/actions are 1-indexed) + */ public void setModuleOrActionIndex(int moduleOrActionIndex) { this.moduleOrActionIndex = moduleOrActionIndex; } - public void add(String action, double probability, List ups, Command command) + /** + * Add a transition to this choice. + * @param probability Probability (or rate) of the transition + * @param ups List of Update objects defining transition + * @param command Corresponding Command object + */ + public void add(double probability, List ups, Command command) { - //this.action = action; this.updates.add(ups); this.probability.add(probability); this.command.add(command); } + /** + * Scale probability/rate of all transitions, multiplying by d. + */ public void scaleProbabilitiesBy(double d) { int i, n; @@ -77,6 +93,9 @@ public class ChoiceListFlexi implements Choice } } + /** + * Modify this choice, constructing product of it with another. + */ public void productWith(ChoiceListFlexi ch) { List list; @@ -98,7 +117,7 @@ public class ChoiceListFlexi implements Choice for (Update u : ch.updates.get(i)) { list.add(u); } - add("?", pi * getProbability(j), list, null); + add(pi * getProbability(j), list, null); } } // Modify elements of current choice to get (0,j) elements of product @@ -113,11 +132,20 @@ public class ChoiceListFlexi implements Choice // Get methods + /** + * Get the module/action for this choice, as an integer index + * (-i for independent in ith module, i for synchronous on ith action) + * (in both cases, modules/actions are 1-indexed) + */ public int getModuleOrActionIndex() { return moduleOrActionIndex; } + /** + * Get the module/action for this choice, as a string + * (form is "module" or "[action]") + */ public String getModuleOrAction() { Update u = updates.get(0).get(0); @@ -128,11 +156,17 @@ public class ChoiceListFlexi implements Choice return "[" + c.getSynch() + "]"; } + /** + * Get the number of transitions in this choice. + */ public int size() { return probability.size(); } + /** + * Get the updates of the ith transition, as a string. + */ public String getUpdateString(int i) { String s = "("; @@ -142,6 +176,9 @@ public class ChoiceListFlexi implements Choice return s; } + /** + * Compute the target for the ith transition, based on a current state. + */ public State computeTarget(int i, State oldState) throws PrismLangException { if (i < 0 || i >= size()) @@ -152,6 +189,9 @@ public class ChoiceListFlexi implements Choice return newState; } + /** + * Compute the target for the ith transition, based on a current state, store in a State. + */ public void computeTarget(int i, State oldState, State newState) throws PrismLangException { if (i < 0 || i >= size()) @@ -170,11 +210,6 @@ public class ChoiceListFlexi implements Choice computeTarget(0, oldState, newState); } - public double getProbability() - { - return getProbability(0); - } - public double getProbability(int i) { if (i < 0 || i >= size()) @@ -183,6 +218,11 @@ public class ChoiceListFlexi implements Choice return probability.get(i); } + public double getProbability() + { + return getProbability(0); + } + public double getProbabilitySum() { double sum = 0.0; diff --git a/prism/src/simulator/Updater.java b/prism/src/simulator/Updater.java index df94f9b2..3526bb6a 100644 --- a/prism/src/simulator/Updater.java +++ b/prism/src/simulator/Updater.java @@ -50,23 +50,22 @@ public class Updater protected int numRewardStructs; // Temporary storage: - + // Element i,j of updateLists is a list of the updates from module i labelled with action j // (where j=0 denotes independent, otherwise 1-indexed action label) protected List>> updateLists; // Bit j of enabledSynchs is set iff action j is currently enabled // (where j=0 denotes independent, otherwise 1-indexed action label) protected BitSet enabledSynchs; - // Element j of enabledSynchs is BitSet showing modules which enable action j + // Element j of enabledModules is a BitSet showing modules which enable action j // (where j=0 denotes independent, otherwise 1-indexed action label) protected BitSet enabledModules[]; - // TODO: apply optimiseForFast or assume called? public Updater(SimulatorEngine simulator, ModulesFile modulesFile) { int i, j; String s; - + // Get info from simulator/model this.simulator = simulator; prism = simulator.getPrism(); @@ -76,7 +75,7 @@ public class Updater synchs = modulesFile.getSynchs(); numSynchs = synchs.size(); numRewardStructs = modulesFile.getNumRewardStructs(); - + // Compute count of number of modules using each synch action synchModuleCounts = new int[numSynchs]; for (j = 0; j < numSynchs; j++) { @@ -87,7 +86,7 @@ public class Updater synchModuleCounts[j]++; } } - + // Build lists/bitsets for later use updateLists = new ArrayList>>(numModules); for (i = 0; i < numModules; i++) { @@ -110,13 +109,9 @@ public class Updater */ public void calculateTransitions(State state, TransitionList transitionList) throws PrismException { - Module module; - ChoiceListFlexi prod; - int i, j, n, count, n2, n3; - double p; + List chs; + int i, j, k, l, n, count; - //System.out.println("Synchs: " + synchs); - //System.out.println("Calc updates for " + state); // Clear lists/bitsets transitionList.clear(); for (i = 0; i < numModules; i++) { @@ -128,122 +123,95 @@ public class Updater for (i = 0; i < numSynchs + 1; i++) { enabledModules[i].clear(); } + // Calculate the available updates for each module/action + // (update information in updateLists, enabledSynchs and enabledModules) for (i = 0; i < numModules; i++) { calculateUpdatesForModule(i, state); } //System.out.println("updateLists: " + updateLists); - // Combination of updates depends on model type - /*switch (modelType) { - - case DTMC: - case CTMC:*/ - n = 0; - // Independent choices for each (enabled) module - for (i = enabledModules[0].nextSetBit(0); i >= 0; i = enabledModules[0].nextSetBit(i + 1)) { - for (Updates ups : updateLists.get(i).get(0)) { - /*processUpdatesAndAddToSum(ups, state, ch); - n++;*/ - transitionList.add(processUpdatesAndCreateNewChoice(-(i + 1), ups, state)); - } + // Add independent transitions for each (enabled) module to list + for (i = enabledModules[0].nextSetBit(0); i >= 0; i = enabledModules[0].nextSetBit(i + 1)) { + for (Updates ups : updateLists.get(i).get(0)) { + transitionList.add(processUpdatesAndCreateNewChoice(-(i + 1), ups, state)); } - // Add synchronous transitions to list - for (i = enabledSynchs.nextSetBit(1); i >= 0; i = enabledSynchs.nextSetBit(i + 1)) { - // Check counts to see if this action is blocked by some module - if (enabledModules[i].cardinality() < synchModuleCounts[i - 1]) - continue; - // If not, proceed... - prod = null; - for (j = enabledModules[i].nextSetBit(0); j >= 0; j = enabledModules[i].nextSetBit(j + 1)) { - count = updateLists.get(j).get(i).size(); - // Case where there is 1 choice - if (count == 1) { - // Case where this is the first Updates added - if (prod == null) { - for (Updates ups : updateLists.get(j).get(i)) { - prod = processUpdatesAndCreateNewChoice(i, ups, state); - } - } else { - processUpdatesAndAddToProduct(updateLists.get(j).get(i).get(0), state, prod); - } + } + // Add synchronous transitions to list + chs = new ArrayList(); + for (i = enabledSynchs.nextSetBit(1); i >= 0; i = enabledSynchs.nextSetBit(i + 1)) { + chs.clear(); + // Check counts to see if this action is blocked by some module + if (enabledModules[i].cardinality() < synchModuleCounts[i - 1]) + continue; + // If not, proceed... + for (j = enabledModules[i].nextSetBit(0); j >= 0; j = enabledModules[i].nextSetBit(j + 1)) { + count = updateLists.get(j).get(i).size(); + // Case where there is only 1 Updates for this module + if (count == 1) { + Updates ups = updateLists.get(j).get(i).get(0); + // Case where this is the first Choice created + if (chs.size() == 0) { + chs.add(processUpdatesAndCreateNewChoice(i, ups, state)); } - // Case where there are multiple choices + // Case where there are existing Choices else { - // TODO - throw new PrismLangException("Don't handle local nondet yet"); + // Product with all existing choices + for (ChoiceListFlexi ch : chs) { + processUpdatesAndAddToProduct(ups, state, ch); + } } - //System.out.println("prod" + j + ": " + prod); } - transitionList.add(prod); - n++; - } - - /*if (n > 1) - ch.scaleProbabilitiesBy(1.0 / n); - transitionList.add(ch);*/ - //break; - - //case MDP: - /* - // Add independent transitions to list - for (i = 0; i < numModules; i++) { - for (Updates ups : updateLists.get(i).get(0)) { - transitionList.add(calculateTransitionsForUpdates(ups, state)); - } - } - // Add synchronous transitions to list - for (i = 0; i < numSynchs; i++) { - prod = new ArrayList(); - for (j = 0; j < numModules; j++) { - // Skip modules not using this action - if (!modulesFile.getModule(j).usesSynch(synchs.get(i))) - continue; - // Case where module blocks - if (updateLists.get(j).get(i).size() == 0) { - prod.clear(); - break; - } - // Case where this is the first Updates added - if (prod.isEmpty()) { + // Case where there are multiple Updates (i.e. local nondeterminism) + else { + // Case where there are no existing choices + if (chs.size() == 0) { for (Updates ups : updateLists.get(j).get(i)) { - // TODO: avoid so much copying for efficiency? - prod.add((Updates) ups.deepCopy()); + chs.add(processUpdatesAndCreateNewChoice(i, ups, state)); } } - // Case where there is 1 choice - else if (updateLists.get(j).get(i).size() == 1) { - } - // Case where there are multiple choices + // Case where there are existing Choices else { - // TODO - //for (Choice tr : choiceLists.get(j).get(i)) { + // Duplicate (count-1 copies of) current Choice list + n = chs.size(); + for (k = 0; k < count - 1; k++) + for (l = 0; l < n; l++) + chs.add(chs.get(l)); + // Products with existing choices + for (k = 0; k < count; k++) { + Updates ups = updateLists.get(j).get(i).get(k); + for (l = 0; l < n; l++) + processUpdatesAndAddToProduct(ups, state, chs.get(k * n + l)); + } } } - for (Updates ups : prod) { - transitionList.add(calculateTransitionsForUpdates(ups, state)); - } - }*/ - /*break; - - default: - throw new PrismException("Unhandled model type \"" + modelType + "\""); - }*/ - - // For DTMCs, need to randomise + } + // Add all new choices to transition list + for (ChoiceListFlexi ch : chs) { + transitionList.add(ch); + } + } //System.out.println(transitionList); - } + // Private helpers + + /** + * Create a new Choice object (currently ChoiceListFlexi) based on an Updates object + * and a (global) state. If appropriate, check probabilities sum to 1 too. + * @param moduleOrActionIndex Module/action for the choice, encoded as an integer (see Choice) + * @param ups The Updates object + * @param state Global state + */ private ChoiceListFlexi processUpdatesAndCreateNewChoice(int moduleOrActionIndex, Updates ups, State state) throws PrismLangException { - // TODO: use sum function? ChoiceListFlexi ch; List list; int i, n; double p, sum; + // Create choice and add all info ch = new ChoiceListFlexi(); ch.setModuleOrActionIndex(moduleOrActionIndex); n = ups.getNumUpdates(); @@ -253,7 +221,7 @@ public class Updater sum += p; list = new ArrayList(); list.add(ups.getUpdate(i)); - ch.add("", p, list, ups.getParent()); + ch.add(p, list, ups.getParent()); } // Check distribution sums to 1 (if required) if (modelType.choicesSumToOne() && Math.abs(sum - 1) > prism.getSumRoundOff()) { @@ -263,28 +231,14 @@ public class Updater return ch; } - private void processUpdatesAndAddToSum(Updates ups, State state, ChoiceListFlexi ch) throws PrismLangException - { - List list; - int i, n; - double p, sum; - - n = ups.getNumUpdates(); - sum = 0; - for (i = 0; i < n; i++) { - p = ups.getProbabilityInState(i, state); - sum += p; - list = new ArrayList(); - list.add(ups.getUpdate(i)); - ch.add("", p, list, ups.getParent()); - } - // Check distribution sums to 1 (if required) - if (modelType.choicesSumToOne() && Math.abs(sum - 1) > prism.getSumRoundOff()) { - throw new PrismLangException("Probabilities sum to " + sum + " in state " + state); - } - - } - + /** + * Create a new Choice object (currently ChoiceListFlexi) based on the product + * of an existing ChoiceListFlexi and an Updates object, for some (global) state. + * If appropriate, check probabilities sum to 1 too. + * @param ups The Updates object + * @param state Global state + * @param ch The existing Choices object + */ private void processUpdatesAndAddToProduct(Updates ups, State state, ChoiceListFlexi ch) throws PrismLangException { // Create new choice (action index is 0 - not needed) @@ -293,22 +247,17 @@ public class Updater ch.productWith(chNew); } - // Model exploration methods (e.g. for simulation) - /** * Determine the enabled updates for the 'm'th module from (global) state 'state'. - * Update information in ... TODO + * Update information in updateLists, enabledSynchs and enabledModules. * @param m The module index * @param state State from which to explore - * @param ... - * TODO */ private void calculateUpdatesForModule(int m, State state) throws PrismLangException { Module module; Command command; int i, j, n; - String s; module = modulesFile.getModule(m); n = module.getNumCommands();