diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index 77666d81..eaffe88d 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -330,6 +330,16 @@ public class SimulatorEngine * @param initialState Initial state (if null, is selected randomly) */ public void initialisePath(Values initialState) throws PrismException + { + // TODO: need this method? + initialisePath(new State(initialState)); + } + + /** + * Initialise (or re-initialise) the simulation path, starting with a specific (or random) initial state. + * @param initialState Initial state (if null, is selected randomly) + */ + public void initialisePath(State initialState) throws PrismException { // Store a copy of passed in state if (initialState != null) { @@ -470,66 +480,6 @@ public class SimulatorEngine throw new PrismException(getLastErrorMessage());*/ } - /** - * Execute a transition from the current transition list and update path (if being stored). - * 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 - * @param offset Index within choice of transition to execute - * @param index (Optionally) index of transition within whole list (-1 if unknown) - */ - private void executeTransition(int i, int offset, int index) throws PrismException - { - // Get corresponding choice - Choice choice = transitionList.getChoice(i); - // Remember last state and compute next one (and its state rewards) - lastState.copy(currentState); - choice.computeTarget(offset, lastState, currentState); - updater.calculateStateRewards(currentState, currentStateRewards); - // Store path info (if necessary) - if (!onTheFly) { - if (index == -1) - index = transitionList.getTotalIndexOfTransition(i, offset); - path.addStep(index, choice.getAction(), currentStateRewards, currentState, currentStateRewards); - // TODO: first currentStateRewards in above should be new *trans* rewards! - } - // Generate updates for next state - updater.calculateTransitions(currentState, transitionList); - } - - /** - * Execute a (timed) transition from the current transition list and update path (if being stored). - * 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 - * should be specified. If -1, this is picked randomly. - * [continuous-time models only] - * @param i Index of choice containing transition to execute - * @param offset Index within choice of transition to execute - * @param time Time for transition - * @param index (Optionally) index of transition within whole list (-1 if unknown) - */ - private void executeTimedTransition(int i, int offset, double time, int index) throws PrismException - { - // Get corresponding choice - Choice choice = transitionList.getChoice(i); - // Remember last state and compute next one (and its state rewards) - lastState.copy(currentState); - choice.computeTarget(offset, lastState, currentState); - updater.calculateStateRewards(currentState, currentStateRewards); - // Store path info (if necessary) - if (!onTheFly) { - if (index == -1) - index = transitionList.getTotalIndexOfTransition(i, offset); - path.addStep(time, index, choice.getAction(), currentStateRewards, currentState, currentStateRewards); - // TODO: first currentStateRewards in above should be new *trans* rewards! - } - // Generate updates for next state - updater.calculateTransitions(currentState, transitionList); - } - /** * This function backtracks the current path to the state of the given index * @@ -660,6 +610,66 @@ public class SimulatorEngine labels = new ArrayList(); } + /** + * Execute a transition from the current transition list and update path (if being stored). + * 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 + * @param offset Index within choice of transition to execute + * @param index (Optionally) index of transition within whole list (-1 if unknown) + */ + private void executeTransition(int i, int offset, int index) throws PrismException + { + // Get corresponding choice + Choice choice = transitionList.getChoice(i); + // Remember last state and compute next one (and its state rewards) + lastState.copy(currentState); + choice.computeTarget(offset, lastState, currentState); + updater.calculateStateRewards(currentState, currentStateRewards); + // Store path info (if necessary) + if (!onTheFly) { + if (index == -1) + index = transitionList.getTotalIndexOfTransition(i, offset); + path.addStep(index, choice.getAction(), currentStateRewards, currentState, currentStateRewards); + // TODO: first currentStateRewards in above should be new *trans* rewards! + } + // Generate updates for next state + updater.calculateTransitions(currentState, transitionList); + } + + /** + * Execute a (timed) transition from the current transition list and update path (if being stored). + * 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 + * should be specified. If -1, this is picked randomly. + * [continuous-time models only] + * @param i Index of choice containing transition to execute + * @param offset Index within choice of transition to execute + * @param time Time for transition + * @param index (Optionally) index of transition within whole list (-1 if unknown) + */ + private void executeTimedTransition(int i, int offset, double time, int index) throws PrismException + { + // Get corresponding choice + Choice choice = transitionList.getChoice(i); + // Remember last state and compute next one (and its state rewards) + lastState.copy(currentState); + choice.computeTarget(offset, lastState, currentState); + updater.calculateStateRewards(currentState, currentStateRewards); + // Store path info (if necessary) + if (!onTheFly) { + if (index == -1) + index = transitionList.getTotalIndexOfTransition(i, offset); + path.addStep(time, index, choice.getAction(), currentStateRewards, currentState, currentStateRewards); + // TODO: first currentStateRewards in above should be new *trans* rewards! + } + // Generate updates for next state + updater.calculateTransitions(currentState, transitionList); + } + // ------------------------------------------------------------------------------ // Queries regarding model // ------------------------------------------------------------------------------ @@ -722,7 +732,7 @@ public class SimulatorEngine } // ------------------------------------------------------------------------------ - // State/Transitions querying + // State/Choice/Transition querying // ------------------------------------------------------------------------------ /** @@ -734,13 +744,65 @@ public class SimulatorEngine } /** - * Returns the current number of available transitions. + * Returns the current number of available choices. + */ + public int getNumChoices() + { + return transitionList.getNumChoices(); + } + + /** + * Returns the current (total) number of available transitions. */ public int getNumTransitions() { return transitionList.getNumTransitions(); } + /** + * Returns the current number of available transitions in choice i. + */ + public int getNumTransitions(int i) + { + return transitionList.getChoice(i).size(); + } + + /** + * Get the probability/rate of a transition within a choice, specified by its index/offset. + */ + public double getTransitionProbability(int i, int offset) throws PrismException + { + double p = transitionList.getChoice(i).getProbability(offset); + // For DTMCs, we need to normalise (over choices) + return (modelType == ModelType.DTMC ? p / transitionList.getNumChoices() : p); + } + + /** + * Get the probability/rate of a transition, specified by its index. + */ + public double getTransitionProbability(int index) throws PrismException + { + double p = transitionList.getTransitionProbability(index); + // For DTMCs, we need to normalise (over choices) + return (modelType == ModelType.DTMC ? p / transitionList.getNumChoices() : p); + } + + /** + * Get the target (as a new State object) of a transition within a choice, specified by its index/offset. + */ + public State computeTransitionTarget(int i, int offset) throws PrismLangException + { + return transitionList.getChoice(i).computeTarget(offset, currentState); + } + + /** + * Get the target of a transition (as a new State object), specified by its index. + */ + public State computeTransitionTarget(int index) throws PrismLangException + { + return transitionList.computeTransitionTarget(index, currentState); + } + /** * Returns the action label of a transition in the list of those currently available. * An empty string denotes an unlabelled (asynchronous) transition. @@ -766,28 +828,6 @@ public class SimulatorEngine return transitionList.getTransitionActionString(index); } - /** - * Returns the probability/rate of the update at the given index - * - * @param i - * the index of the update of interest. - * @return the probability/rate of the update at the given index. - */ - public double getTransitionProbability(int index) throws PrismException - { - double p = transitionList.getTransitionProbability(index); - return (modelType == ModelType.DTMC ? p / transitionList.getNumChoices() : p); - } - - public State computeTransitionTarget(int index) throws PrismLangException - { - // 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); - } - /** * Returns a string representation of the assignments for the current update at the given index. * diff --git a/prism/src/simulator/TransitionList.java b/prism/src/simulator/TransitionList.java index d3cf4286..ec911d3d 100644 --- a/prism/src/simulator/TransitionList.java +++ b/prism/src/simulator/TransitionList.java @@ -110,29 +110,29 @@ public class TransitionList } /** - * Get the choice containing the ith transition. + * Get the choice containing a transition of a given index. */ - public Choice getChoiceOfTransition(int i) + public Choice getChoiceOfTransition(int index) { - return choices.get(transitionIndices.get(i)); + return choices.get(transitionIndices.get(index)); } // Get index/offset info /** - * Get the index of the choice containing the ith transition. + * Get the index of the choice containing a transition of a given index. */ - public int getChoiceIndexOfTransition(int i) + public int getChoiceIndexOfTransition(int index) { - return transitionIndices.get(i); + return transitionIndices.get(index); } /** - * Get the offset of the ith transition within its containing choice. + * Get the offset of a transition within its containing choice. */ - public int getChoiceOffsetOfTransition(int i) + public int getChoiceOffsetOfTransition(int index) { - return transitionOffsets.get(i); + return transitionOffsets.get(index); } /** @@ -173,28 +173,32 @@ public class TransitionList } } - // Access to transition info + // Direct access to transition info - // get prob (or rate) of ith transition - public double getTransitionProbability(int i) + /** + * Get the probability/rate of a transition, specified by its index. + */ + public double getTransitionProbability(int index) { - return getChoiceOfTransition(i).getProbability(transitionOffsets.get(i)); + return getChoiceOfTransition(index).getProbability(transitionOffsets.get(index)); } - public String getTransitionActionString(int i) + /** + * Get the target of a transition (as a new State object), specified by its index. + */ + public State computeTransitionTarget(int index, State oldState) throws PrismLangException { - return getChoiceOfTransition(i).getAction(); + return getChoiceOfTransition(index).computeTarget(transitionOffsets.get(index), oldState); } - public String getTransitionUpdateString(int i) + public String getTransitionActionString(int index) { - return getChoiceOfTransition(i).getUpdateString(transitionOffsets.get(i)); + return getChoiceOfTransition(index).getAction(); } - // compute target of ith transition - public State computeTransitionTarget(int i, State oldState) throws PrismLangException + public String getTransitionUpdateString(int index) { - return getChoiceOfTransition(i).computeTarget(transitionOffsets.get(i), oldState); + return getChoiceOfTransition(index).getUpdateString(transitionOffsets.get(index)); } @Override diff --git a/prism/src/simulator/Updater.java b/prism/src/simulator/Updater.java index 70408da2..a34ad8fd 100644 --- a/prism/src/simulator/Updater.java +++ b/prism/src/simulator/Updater.java @@ -45,6 +45,7 @@ public class Updater // Synchronising action info protected Vector synchs; protected int numSynchs; + protected int synchModuleCounts[]; // Model info/stats protected int numRewardStructs; @@ -56,6 +57,10 @@ public class Updater // 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(); this.modulesFile = modulesFile; @@ -64,17 +69,30 @@ 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++) { + synchModuleCounts[j] = 0; + s = synchs.get(j); + for (i = 0; i < numModules; i++) { + if (modulesFile.getModule(i).usesSynch(s)) + synchModuleCounts[j]++; + } + } + + // Build lists/bitsets for later use updateLists = new ArrayList>>(numModules); - for (int i = 0; i < numModules; i++) { + for (i = 0; i < numModules; i++) { updateLists.add(new ArrayList>(numSynchs + 1)); - for (int j = 0; j < numSynchs + 1; j++) { + for (j = 0; j < numSynchs + 1; j++) { updateLists.get(i).add(new ArrayList()); } } enabledSynchs = new BitSet(numSynchs + 1); enabledModules = new BitSet[numSynchs + 1]; - for (int i = 0; i < numSynchs + 1; i++) { - enabledModules[i] = new BitSet(numModules); + for (j = 0; j < numSynchs + 1; j++) { + enabledModules[j] = new BitSet(numModules); } } @@ -87,9 +105,10 @@ public class Updater { Module module; ChoiceListFlexi ch, prod; - int i, j, n, n2, n3; + int i, j, n, count, n2, n3; double p; + System.out.println("Synchs: " + synchs); System.out.println("Calc updates for " + state); // Clear lists/bitsets transitionList.clear(); @@ -109,10 +128,10 @@ public class Updater System.out.println("updateLists: " + updateLists); // Combination of updates depends on model type - switch (modelType) { + /*switch (modelType) { case DTMC: - case CTMC: + case CTMC:*/ ch = new ChoiceListFlexi(); n = 0; // Independent choices for each (enabled) module @@ -125,11 +144,15 @@ public class Updater } // 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)) { - // TODO: Case where module blocks (CHECK COUNT?) + count = updateLists.get(j).get(i).size(); // Case where there is 1 choice - if (updateLists.get(j).get(i).size() == 1) { + if (count == 1) { // Case where this is the first Updates added if (prod == null) { for (Updates ups : updateLists.get(j).get(i)) { @@ -153,9 +176,9 @@ public class Updater /*if (n > 1) ch.scaleProbabilitiesBy(1.0 / n); transitionList.add(ch);*/ - break; + //break; - case MDP: + //case MDP: /* // Add independent transitions to list for (i = 0; i < numModules; i++) { @@ -195,11 +218,11 @@ public class Updater transitionList.add(calculateTransitionsForUpdates(ups, state)); } }*/ - break; + /*break; default: throw new PrismException("Unhandled model type \"" + modelType + "\""); - } + }*/ // For DTMCs, need to randomise