diff --git a/prism/src/simulator/Choice.java b/prism/src/simulator/Choice.java index 5ce81963..caabfa47 100644 --- a/prism/src/simulator/Choice.java +++ b/prism/src/simulator/Choice.java @@ -27,11 +27,8 @@ package simulator; import parser.*; -import parser.ast.*; import prism.*; -import java.util.*; - public interface Choice { // public void setAction(String action); diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index 97e43d00..8c6557cf 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -98,9 +98,6 @@ public class SimulatorEngine private VarList varList; private int numVars; private Map varIndices; - // Synchronising action info - private Vector synchs; - private int numSynchs; // Constant definitions from model file private Values mfConstants; @@ -109,22 +106,18 @@ public class SimulatorEngine private List properties; private List propertySamplers; - // Current path info - protected Path path; - protected boolean onTheFly; - - // TODO: remove these now can get from path? - protected State previousState; - protected State currentState; - - // TODO: just temp storage? - // (if so, remove 'current', 'prev' from names?) - protected double currentStateRewards[]; - protected double previousTransitionRewards[]; + // Temporary storage for manipulating states/rewards + protected State tmpState; + protected double tmpStateRewards[]; + protected double tmpTransitionRewards[]; // List of currently available transitions protected TransitionList transitionList; + // Current path info + protected Path path; + protected boolean onTheFly; + // Updater object for model protected Updater updater; @@ -205,22 +198,22 @@ public class SimulatorEngine */ public void initialisePath(State initialState) throws PrismException { - // Store a copy of passed in state + // Store a temporary copy of passed in state if (initialState != null) { - currentState.copy(new State(initialState)); + tmpState.copy(new State(initialState)); } // Or pick a random one else { throw new PrismException("Random initial start state not yet supported"); } - updater.calculateStateRewards(currentState, currentStateRewards); + updater.calculateStateRewards(tmpState, tmpStateRewards); // Initialise stored path if necessary - path.initialise(currentState, currentStateRewards); + path.initialise(tmpState, tmpStateRewards); // Reset and then update samplers for any loaded properties resetSamplers(); updateSamplers(); // Generate updates for initial state - updater.calculateTransitions(currentState, transitionList); + updater.calculateTransitions(tmpState, transitionList); } /** @@ -269,7 +262,7 @@ public class SimulatorEngine numChoices = transitionList.getNumChoices(); if (numChoices == 0) return false; - //throw new PrismException("Deadlock found at state " + currentState.toString(modulesFile)); + //throw new PrismException("Deadlock found at state " + path.getCurrentState().toString(modulesFile)); switch (modelType) { case DTMC: @@ -357,16 +350,10 @@ public class SimulatorEngine } // Back track in path ((PathFull) path).backtrack(step); - // Update previous/current state info - if (step == 0) - previousState.clear(); - else - previousState.copy(path.getPreviousState()); - currentState.copy(path.getCurrentState()); // Recompute samplers for any loaded properties recomputeSamplers(); // Generate updates for new current state - updater.calculateTransitions(currentState, transitionList); + updater.calculateTransitions(path.getCurrentState(), transitionList); } /** @@ -412,10 +399,6 @@ public class SimulatorEngine } // Modify path ((PathFull) path).removePrecedingStates(step); - // Update previous state info (if required) - // (No need to update current state info) - if (path.size() == 1) - previousState.clear(); // Recompute samplers for any loaded properties recomputeSamplers(); // (No need to re-generate updates for new current state) @@ -438,7 +421,7 @@ public class SimulatorEngine */ public void computeTransitionsForCurrentState() throws PrismException { - updater.calculateTransitions(currentState, transitionList); + updater.calculateTransitions(path.getCurrentState(), transitionList); } // ------------------------------------------------------------------------------ @@ -613,18 +596,13 @@ public class SimulatorEngine varIndices.put(varList.getName(i), i); } - // Get list of synchronising actions - synchs = modulesFile.getSynchs(); - numSynchs = synchs.size(); - // Evaluate constants and optimise (a copy of) modules file for simulation modulesFile = (ModulesFile) modulesFile.deepCopy().replaceConstants(mfConstants).simplify(); - // Create state/transition storage - previousState = new State(numVars); - currentState = new State(numVars); - currentStateRewards = new double[modulesFile.getNumRewardStructs()]; - previousTransitionRewards = new double[modulesFile.getNumRewardStructs()]; + // Create temporary state/transition storage + tmpState = new State(numVars); + tmpStateRewards = new double[modulesFile.getNumRewardStructs()]; + tmpTransitionRewards = new double[modulesFile.getNumRewardStructs()]; transitionList = new TransitionList(); // Create updater for model @@ -652,17 +630,16 @@ public class SimulatorEngine if (!onTheFly && index == -1) index = transitionList.getTotalIndexOfTransition(i, offset); // Compute its transition rewards - updater.calculateTransitionRewards(currentState, choice, previousTransitionRewards); - // Remember last state and compute next one (and its state rewards) - previousState.copy(currentState); - choice.computeTarget(offset, previousState, currentState); - updater.calculateStateRewards(currentState, currentStateRewards); + updater.calculateTransitionRewards(path.getCurrentState(), choice, tmpTransitionRewards); + // Compute next state (and its state rewards) + choice.computeTarget(offset, path.getCurrentState(), tmpState); + updater.calculateStateRewards(tmpState, tmpStateRewards); // Update path - path.addStep(index, choice.getModuleOrActionIndex(), previousTransitionRewards, currentState, currentStateRewards); + path.addStep(index, choice.getModuleOrActionIndex(), tmpTransitionRewards, tmpState, tmpStateRewards); // Update samplers for any loaded properties updateSamplers(); // Generate updates for next state - updater.calculateTransitions(currentState, transitionList); + updater.calculateTransitions(tmpState, transitionList); } /** @@ -684,17 +661,16 @@ public class SimulatorEngine if (!onTheFly && index == -1) index = transitionList.getTotalIndexOfTransition(i, offset); // Compute its transition rewards - updater.calculateTransitionRewards(currentState, choice, previousTransitionRewards); - // Remember last state and compute next one (and its state rewards) - previousState.copy(currentState); - choice.computeTarget(offset, previousState, currentState); - updater.calculateStateRewards(currentState, currentStateRewards); + updater.calculateTransitionRewards(path.getCurrentState(), choice, tmpTransitionRewards); + // Compute next state (and its state rewards) + choice.computeTarget(offset, path.getCurrentState(), tmpState); + updater.calculateStateRewards(tmpState, tmpStateRewards); // Update path - path.addStep(time, index, choice.getModuleOrActionIndex(), previousTransitionRewards, currentState, currentStateRewards); + path.addStep(time, index, choice.getModuleOrActionIndex(), tmpTransitionRewards, tmpState, tmpStateRewards); // Update samplers for any loaded properties updateSamplers(); // Generate updates for next state - updater.calculateTransitions(currentState, transitionList); + updater.calculateTransitions(tmpState, transitionList); } /** @@ -774,15 +750,6 @@ public class SimulatorEngine return varList.getIndex(name); } - /** - * Returns the index of an action name, as stored by the simulator for the current model. - * Returns -1 if the action name does not exist. - */ - public int getIndexOfAction(String name) - { - return synchs.indexOf(name); - } - // ------------------------------------------------------------------------------ // Querying of current state and its available choices/transitions // ------------------------------------------------------------------------------ @@ -860,7 +827,7 @@ public class SimulatorEngine */ public State computeTransitionTarget(int i, int offset) throws PrismLangException { - return transitionList.getChoice(i).computeTarget(offset, currentState); + return transitionList.getChoice(i).computeTarget(offset, path.getCurrentState()); } /** @@ -868,7 +835,7 @@ public class SimulatorEngine */ public State computeTransitionTarget(int index) throws PrismLangException { - return transitionList.computeTransitionTarget(index, currentState); + return transitionList.computeTransitionTarget(index, path.getCurrentState()); } // ------------------------------------------------------------------------------ diff --git a/prism/src/simulator/Updater.java b/prism/src/simulator/Updater.java index 3526bb6a..50b09725 100644 --- a/prism/src/simulator/Updater.java +++ b/prism/src/simulator/Updater.java @@ -195,8 +195,81 @@ public class Updater //System.out.println(transitionList); } + /** + * Calculate the state rewards for a given state. + * @param state The state to compute rewards for + * @param store An array in which to store the rewards + */ + public void calculateStateRewards(State state, double[] store) throws PrismLangException + { + int i, j, n; + double d; + RewardStruct rw; + for (i = 0; i < numRewardStructs; i++) { + rw = modulesFile.getRewardStruct(i); + n = rw.getNumItems(); + d = 0.0; + for (j = 0; j < n; j++) { + if (!rw.getRewardStructItem(j).isTransitionReward()) + if (rw.getStates(j).evaluateBoolean(state)) + d += rw.getReward(j).evaluateDouble(state); + } + store[i] = d; + } + } + + /** + * Calculate the transition rewards for a given state and outgoing choice. + * @param state The state to compute rewards for + * @param ch The choice from the state to compute rewards for + * @param store An array in which to store the rewards + */ + public void calculateTransitionRewards(State state, Choice ch, double[] store) throws PrismLangException + { + int i, j, n; + double d; + RewardStruct rw; + for (i = 0; i < numRewardStructs; i++) { + rw = modulesFile.getRewardStruct(i); + n = rw.getNumItems(); + d = 0.0; + for (j = 0; j < n; j++) { + if (rw.getRewardStructItem(j).isTransitionReward()) + if (rw.getRewardStructItem(j).getSynchIndex() == Math.max(0, ch.getModuleOrActionIndex())) + if (rw.getStates(j).evaluateBoolean(state)) + d += rw.getReward(j).evaluateDouble(state); + } + store[i] = d; + } + } + // Private helpers + /** + * Determine the enabled updates for the 'm'th module from (global) state 'state'. + * Update information in updateLists, enabledSynchs and enabledModules. + * @param m The module index + * @param state State from which to explore + */ + private void calculateUpdatesForModule(int m, State state) throws PrismLangException + { + Module module; + Command command; + int i, j, n; + + module = modulesFile.getModule(m); + n = module.getNumCommands(); + for (i = 0; i < n; i++) { + command = module.getCommand(i); + if (command.getGuard().evaluateBoolean(state)) { + j = command.getSynchIndex(); + updateLists.get(m).get(j).add(command.getUpdates()); + enabledSynchs.set(j); + enabledModules[j].set(m); + } + } + } + /** * Create a new Choice object (currently ChoiceListFlexi) based on an Updates object * and a (global) state. If appropriate, check probabilities sum to 1 too. @@ -246,119 +319,4 @@ public class Updater // Build product with existing ch.productWith(chNew); } - - /** - * Determine the enabled updates for the 'm'th module from (global) state 'state'. - * Update information in updateLists, enabledSynchs and enabledModules. - * @param m The module index - * @param state State from which to explore - */ - private void calculateUpdatesForModule(int m, State state) throws PrismLangException - { - Module module; - Command command; - int i, j, n; - - module = modulesFile.getModule(m); - n = module.getNumCommands(); - for (i = 0; i < n; i++) { - command = module.getCommand(i); - if (command.getGuard().evaluateBoolean(state)) { - j = command.getSynchIndex(); - updateLists.get(m).get(j).add(command.getUpdates()); - enabledSynchs.set(j); - enabledModules[j].set(m); - } - } - } - - /*private Choice calculateTransitionsForUpdates(Updates ups, State state) throws PrismLangException - { - int i, n; - State newState; - - n = ups.getNumUpdates(); - if (n == 1) { - ChoiceSingleton chSingle = null; - chSingle = new ChoiceSingleton(); - newState = calculateTransitionsForUpdate(ups.getUpdate(0), state); - chSingle.setTarget(newState); - chSingle.setProbability(ups.getProbabilityInState(0, state)); - return chSingle; - } else { - ChoiceList chList; - chList = new ChoiceList(n); - for (i = 0; i < n; i++) { - newState = calculateTransitionsForUpdate(ups.getUpdate(i), state); - chList.addTarget(newState); - chList.addProbability(ups.getProbabilityInState(i, state)); - } - return chList; - } - }*/ - - // TODO: do we really need to evaluate dest State at this point? - // maybe just store pointer to Update object for efficiency - private State calculateTransitionsForUpdate(Update up, State state) throws PrismLangException - { - State newState; - int i, n; - - // Copy current state, then apply updates - newState = new State(state); - n = up.getNumElements(); - for (i = 0; i < n; i++) { - newState.varValues[up.getVarIndex(i)] = up.getExpression(i).evaluate(state); - } - - return newState; - } - - /** - * Calculate the state rewards for a given state. - * @param state The state to compute rewards for - * @param store An array in which to store the rewards - */ - public void calculateStateRewards(State state, double[] store) throws PrismLangException - { - int i, j, n; - double d; - RewardStruct rw; - for (i = 0; i < numRewardStructs; i++) { - rw = modulesFile.getRewardStruct(i); - n = rw.getNumItems(); - d = 0.0; - for (j = 0; j < n; j++) { - if (!rw.getRewardStructItem(j).isTransitionReward()) - if (rw.getStates(j).evaluateBoolean(state)) - d += rw.getReward(j).evaluateDouble(state); - } - store[i] = d; - } - } - - /** - * Calculate the transition rewards for a given state and outgoing choice. - * @param state The state to compute rewards for - * @param ch The choice from the state to compute rewards for - * @param store An array in which to store the rewards - */ - public void calculateTransitionRewards(State state, Choice ch, double[] store) throws PrismLangException - { - int i, j, n; - double d; - RewardStruct rw; - for (i = 0; i < numRewardStructs; i++) { - rw = modulesFile.getRewardStruct(i); - n = rw.getNumItems(); - d = 0.0; - for (j = 0; j < n; j++) { - if (rw.getRewardStructItem(j).isTransitionReward()) - if (rw.getRewardStructItem(j).getSynchIndex() == Math.max(0, ch.getModuleOrActionIndex())) - if (rw.getStates(j).evaluateBoolean(state)) - d += rw.getReward(j).evaluateDouble(state); - } - store[i] = d; - } - } }