diff --git a/prism/src/simulator/Path.java b/prism/src/simulator/Path.java index 71e658b1..d25371f9 100644 --- a/prism/src/simulator/Path.java +++ b/prism/src/simulator/Path.java @@ -49,6 +49,7 @@ public class Path public State state; public double stateRewards[]; public double time; + public double timeCumul; public int choice; public String action; public double transitionRewards[]; @@ -58,6 +59,8 @@ public class Path protected SimulatorEngine engine; // Model to which the path corresponds protected ModulesFile modulesFile; + // Does model use continuous time? + protected boolean continuousTime; // Model info/stats protected int numRewardStructs; // The path, i.e. list of states, etc. @@ -98,6 +101,11 @@ public class Path return path.get(i).time; } + public double getCumulativeTime(int i) + { + return path.get(i).timeCumul; + } + public int getChoice(int i) { return path.get(i).choice; @@ -122,6 +130,7 @@ public class Path this.engine = engine; // Store model and info this.modulesFile = modulesFile; + continuousTime = modulesFile.getModelType().continuousTime(); numRewardStructs = modulesFile.getNumRewardStructs(); // Create arrays to store totals totalReward = new double[numRewardStructs]; @@ -163,13 +172,28 @@ public class Path } /** - * Add step... + * Add a step to the path. */ public void addStep(int choice, String action, double[] transRewards, State newState, double[] newStateRewards) + { + addStep(0, choice, action, transRewards, newState, newStateRewards); + } + + /** + * Add a (timed) step to the path. + */ + public void addStep(double time, int choice, String action, double[] transRewards, State newState, + double[] newStateRewards) { Step step; // Add info to last existing step step = path.get(path.size() - 1); + if (continuousTime) { + step.time = time; + step.timeCumul = time; + if (path.size() > 1) + step.timeCumul += path.get(path.size() - 1).timeCumul; + } step.choice = choice; step.action = action; step.transitionRewards = transRewards.clone(); diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index 1bec3e2a..18c54b3c 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -192,7 +192,7 @@ public class SimulatorEngine protected TransitionList transitionList; protected List labels; - + // ------------------------------------------------------------------------------ // CONSTANTS // ------------------------------------------------------------------------------ @@ -337,6 +337,7 @@ public class SimulatorEngine } // Or pick a random one else { + // TODO //currentState... throw new PrismException("Random initial start state not yet supported"); } @@ -350,30 +351,30 @@ public class SimulatorEngine /** * Execute a transition from the current transition list, specified by its index - * within the (whole) list. + * within the (whole) list. If this is a continuous time model, the time to be spent + * in the state before leaving is picked randomly. */ public void manualUpdate(int index) throws PrismException { - int choice = transitionList.getChoiceIndexOfTransition(index); + int i = transitionList.getChoiceIndexOfTransition(index); int offset = transitionList.getChoiceOffsetOfTransition(index); - executeTransition(choice, offset); + if (modelType.continuousTime()) + executeTimedTransition(i, offset, -1, index); + else + executeTransition(i, offset, index); } /** - * This function applies the index update of the current list of updates to the model. The time spent in the last - * state is also given (for ctmcs). Use -1.0 for this parameter if an automatically generated time is required. - * - * @param index - * the index of the selected update to be applied. - * @param time_in_state - * the time spent in the last state. Use -1.0 for this parameter if an automatically generated time is - * required. - * @throws PrismException - * if the index is out of range, or there was a problem with performing the update. + * Execute a transition from the current transition list, specified by its index + * within the (whole) list. In addition, specify the amount of time to be spent in + * the current state before this transition occurs. If -1, this is picked randomly. + * [continuous-time models only] */ - public void manualUpdate(int index, double time_in_state) throws PrismException + public void manualUpdate(int index, double time) throws PrismException { - //TODO int result = makeManualUpdate(index, time_in_state); + int i = transitionList.getChoiceIndexOfTransition(index); + int offset = transitionList.getChoiceOffsetOfTransition(index); + executeTimedTransition(i, offset, time, index); } /** @@ -395,12 +396,12 @@ public class SimulatorEngine for (i = 0; i < n; i++) automaticChoice(detect); } - + public void automaticChoice(boolean detect) throws PrismException { // just one for now... - Choice ch; + Choice choice; int numChoices, i, j; double d; @@ -413,11 +414,11 @@ public class SimulatorEngine throw new PrismException("Deadlock found at state " + currentState.toString(modulesFile)); // Pick a random choice i = rng.randomInt(numChoices); - ch = transitionList.getChoice(i); + choice = transitionList.getChoice(i); // Pick a random transition from this choice d = rng.randomDouble(); - j = ch.getIndexByProbSum(d); - executeTransition(i, j); + j = choice.getIndexByProbSum(d); + executeTransition(i, j, -1); break; case CTMC: // TODO: automaticUpdateContinuous(); @@ -458,21 +459,61 @@ public class SimulatorEngine } /** - * Execute a transition from the current transition list, specified by index - * of choice and offset within that choice. Also update path info (if required). + * 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 + * (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 choice, int offset) throws PrismException + private void executeTransition(int i, int offset, int index) throws PrismException { - Choice ch; + // Get corresponding choice + Choice choice = transitionList.getChoice(i); // Remember last state and compute next one (and its state rewards) lastState.copy(currentState); - ch = transitionList.getChoice(choice); - ch.computeTarget(offset, lastState, currentState); + choice.computeTarget(offset, lastState, currentState); updater.calculateStateRewards(currentState, currentStateRewards); - // Stored path info (if necessary) - if (!onTheFly) - // TODO: first currentStateRewards should be new Trans rewards! - path.addStep(offset, ch.getAction(), currentStateRewards, 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 it 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); } @@ -602,7 +643,7 @@ public class SimulatorEngine // Create updater for model updater = new Updater(this, modulesFile); - + // Create storage for labels labels = new ArrayList(); } @@ -800,26 +841,18 @@ public class SimulatorEngine /** * Returns the time spent in the state at the given path index. - * - * @param stateIndex - * the index of the path state of interest - * @return the time spent in the state at the given path index. */ - public double getTimeSpentInPathState(int stateIndex) + public double getTimeSpentInPathState(int index) { - return path.getTime(stateIndex); + return path.getTime(index); } /** - * Returns the cumulative time spent in the states upto a given path index. - * - * @param stateIndex - * the index of the path state of interest - * @return the time spent in the state at the given path index. + * Returns the cumulative time spent in the states up to (and including) a given path index. */ - public double getCumulativeTimeSpentInPathState(int stateIndex) + public double getCumulativeTimeSpentInPathState(int index) { - return 99; + return path.getCumulativeTime(index); } /** @@ -932,15 +965,11 @@ public class SimulatorEngine public static native int loopEnd(); /** - * Returns the index of the update chosen for the precalculated old update set. - * - * @param oldStep - * the old path step of interest - * @return the index of the update chosen for the precalculated old update set. + * Returns the index of the update chosen for an earlier state in the path. */ - public int getChosenIndexOfOldUpdate(int oldStep) + public int getChosenIndexOfOldUpdate(int step) { - return path.getChoice(oldStep); + return path.getChoice(step); } /** @@ -1394,17 +1423,17 @@ public class SimulatorEngine labels.add(label); return labels.size() - 1; } - + public boolean queryLabel(int index) throws PrismLangException { return labels.get(index).evaluateBoolean(currentState); } - + public boolean queryLabel(int index, int step) throws PrismLangException { return labels.get(index).evaluateBoolean(path.getState(step)); } - + /** * For the current state, this returns 1 if it is the same as the initial state for the current path */ diff --git a/prism/src/simulator/TransitionList.java b/prism/src/simulator/TransitionList.java index 8bacb1ae..869a6f23 100644 --- a/prism/src/simulator/TransitionList.java +++ b/prism/src/simulator/TransitionList.java @@ -33,7 +33,7 @@ import prism.*; public class TransitionList { - public ArrayList transitions = new ArrayList(); + public ArrayList choices = new ArrayList(); public ArrayList transitionIndices = new ArrayList(); public ArrayList transitionOffsets = new ArrayList(); public int numChoices = 0; @@ -42,7 +42,7 @@ public class TransitionList public void clear() { - transitions.clear(); + choices.clear(); transitionIndices.clear(); transitionOffsets.clear(); numChoices = 0; @@ -53,10 +53,10 @@ public class TransitionList public void add(Choice tr) { int i, n; - transitions.add(tr); + choices.add(tr); n = tr.size(); for (i = 0; i < n; i++) { - transitionIndices.add(transitions.size() - 1); + transitionIndices.add(choices.size() - 1); transitionOffsets.add(i); } numChoices++; @@ -64,30 +64,52 @@ public class TransitionList probSum += tr.getProbabilitySum(); } - // get ith choice + // Get access to Choice objects + + /** + * Get the ith choice. + */ public Choice getChoice(int i) { - return transitions.get(i); + return choices.get(i); } - // get choice containing ith transition + /** + * Get the choice containing the ith transition. + */ public Choice getChoiceOfTransition(int i) { - return transitions.get(transitionIndices.get(i)); + return choices.get(transitionIndices.get(i)); } - // get index of choice containing ith transition + // Get index/offset info + + /** + * Get the index of the choice containing the ith transition. + */ public int getChoiceIndexOfTransition(int i) { return transitionIndices.get(i); } - // get offset in choice containing ith transition + /** + * Get the offset of the ith transition within its containing choice. + */ public int getChoiceOffsetOfTransition(int i) { return transitionOffsets.get(i); } + /** + * Get the (total) index of a transition from the index of its containing choice and its offset within it. + */ + public int getTotalIndexOfTransition(int i, int offset) + { + return transitionOffsets.get(i); + } + + // Access to transition info + // get prob (or rate) of ith transition public double getTransitionProbability(int i) { @@ -114,7 +136,7 @@ public class TransitionList public String toString() { String s = ""; - for (Choice tr : transitions) + for (Choice tr : choices) s += tr.toString(); return s; } diff --git a/prism/src/simulator/Updater.java b/prism/src/simulator/Updater.java index f0b43c2f..b4af509e 100644 --- a/prism/src/simulator/Updater.java +++ b/prism/src/simulator/Updater.java @@ -40,6 +40,7 @@ public class Updater // Model to which the path corresponds protected ModulesFile modulesFile; + protected ModelType modelType; protected int numModules; // Synchronising action info protected Vector synchs; @@ -58,6 +59,7 @@ public class Updater this.simulator = simulator; prism = simulator.getPrism(); this.modulesFile = modulesFile; + modelType = modulesFile.getModelType(); numModules = modulesFile.getNumModules(); synchs = modulesFile.getSynchs(); numSynchs = synchs.size(); @@ -107,9 +109,10 @@ public class Updater System.out.println("updateLists: " + updateLists); // Combination of updates depends on model type - switch (modulesFile.getModelType()) { + switch (modelType) { case DTMC: + case CTMC: ch = new ChoiceListFlexi(); n = 0; // Independent choices for each (enabled) module @@ -194,13 +197,13 @@ public class Updater break; default: - throw new PrismException("Unhandled model type \"" + modulesFile.getModelType() + "\""); + throw new PrismException("Unhandled model type \"" + modelType + "\""); } // For DTMCs, need to randomise //System.out.println(transitionList.transitionTotal); - System.out.println(transitionList.transitions); + System.out.println(transitionList.choices); //System.out.println(transitionList.transitionIndices); //System.out.println(transitionList.transitionOffsets); @@ -224,8 +227,8 @@ public class Updater list.add(ups.getUpdate(i)); ch.add("", p, list, ups.getParent()); } - // Check distribution sums to 1 - if (Math.abs(sum - 1) > prism.getSumRoundOff()) { + // 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.toString(modulesFile), ups); } @@ -247,8 +250,8 @@ public class Updater list.add(ups.getUpdate(i)); ch.add("", p, list, ups.getParent()); } - // Check distribution sums to 1 - if (Math.abs(sum - 1) > prism.getSumRoundOff()) { + // 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); } diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java index 7ae4fdb7..cb0d60e7 100644 --- a/prism/src/userinterface/simulator/GUISimulator.java +++ b/prism/src/userinterface/simulator/GUISimulator.java @@ -619,6 +619,9 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect public void a_manualUpdate() { try { + if (currentUpdatesTable.getSelectedRow() == -1) + throw new PrismException("No current update is selected"); + if (displayPathLoops && pathTableModel.isPathLooping()) { if (questionYesNo("A loop in the path has been detected. Do you wish to disable loop detection and extend the path?") == 0) { displayPathLoops = false; @@ -638,10 +641,11 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect //Double.parseDouble(stateTimeField.getText()); setComputing(true); - - if (currentUpdatesTable.getSelectedRow() == -1) - throw new PrismException("No current update is selected"); - engine.manualUpdate(currentUpdatesTable.getSelectedRow(), time); + if (time == -1) { + engine.manualUpdate(currentUpdatesTable.getSelectedRow()); + } else { + engine.manualUpdate(currentUpdatesTable.getSelectedRow(), time); + } pathTableModel.updatePathTable(); updateTableModel.updateUpdatesTable(); @@ -657,8 +661,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect } else { setComputing(true); - if (currentUpdatesTable.getSelectedRow() == -1) - throw new PrismException("No current update is selected"); + engine.manualUpdate(currentUpdatesTable.getSelectedRow()); pathTableModel.updatePathTable(); @@ -2183,6 +2186,37 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect } } + public class ActionValue + { + private String value; + private boolean actionValueUnknown; + + public ActionValue(String value) + { + this.value = value; + } + + public String getValue() + { + return value; + } + + public void setValue(String value) + { + this.value = value; + } + + public void setActionValueUnknown(boolean unknown) + { + this.actionValueUnknown = unknown; + } + + public boolean isActionValueUnknown() + { + return this.actionValueUnknown; + } + } + public class TimeValue { private Double value; @@ -2714,6 +2748,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect private RewardStructureValue rewardStructureValue; private VariableValue variableValue; private TimeValue timeValue; + private ActionValue actionValue; public PathTableModel(SimulationView view) { @@ -3113,7 +3148,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect // The step column if (stepStart <= columnIndex && columnIndex < actionStart) { - return "Step index"; + return "Index of state in path"; } else if (actionStart <= columnIndex && columnIndex < timeStart) { return "Action label or module name"; } else if (timeStart <= columnIndex && columnIndex < cumulativeTimeStart) { @@ -3159,13 +3194,14 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect } // The action column else if (actionStart <= columnIndex && columnIndex < timeStart) { - return engine.getActionOfPathStep(rowIndex); + actionValue = new ActionValue(engine.getActionOfPathStep(rowIndex)); + actionValue.setActionValueUnknown(rowIndex >= engine.getPathSize() - 1); + return actionValue; } // Time column else if (timeStart <= columnIndex && columnIndex < cumulativeTimeStart) { timeValue = new TimeValue(engine.getTimeSpentInPathState(rowIndex), false); timeValue.setTimeValueUnknown(rowIndex >= engine.getPathSize() - 1); - return timeValue; } // Cumulative time column @@ -3173,30 +3209,24 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect timeValue = new TimeValue((rowIndex == 0) ? 0.0 : engine .getCumulativeTimeSpentInPathState(rowIndex - 1), true); timeValue.setTimeValueUnknown(rowIndex >= engine.getPathSize()); - return timeValue; } // A variable column else if (varStart <= columnIndex && columnIndex < rewardStart) { Variable var = ((Variable) view.getVisibleVariables().get(columnIndex - varStart)); - - Type type = var.getType(); Object result = engine.getPathData(var.getIndex(), rowIndex); variableValue.setVariable(var); variableValue.setValue(result); variableValue.setChanged(rowIndex == 0 || !engine.getPathData(var.getIndex(), rowIndex - 1).equals(result)); - return variableValue; } // A reward column else if (rewardStart <= columnIndex) { RewardStructureColumn rewardColumn = (RewardStructureColumn) view.getVisibleRewardColumns().get( columnIndex - rewardStart); - rewardStructureValue.setRewardStructureColumn(rewardColumn); rewardStructureValue.setRewardValueUnknown(false); - // A state reward column if (rewardColumn.isStateReward()) { double value = engine.getStateRewardOfPathState(rowIndex, rewardColumn.getRewardStructure() @@ -3205,7 +3235,6 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect || value != engine.getStateRewardOfPathState(rowIndex - 1, rewardColumn .getRewardStructure().getIndex())); rewardStructureValue.setRewardValue(new Double(value)); - rewardStructureValue.setRewardValueUnknown(rowIndex > engine.getPathSize() - 1); } // A transition reward column @@ -3216,7 +3245,6 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect || value != engine.getTransitionRewardOfPathState(rowIndex - 1, rewardColumn .getRewardStructure().getIndex())); rewardStructureValue.setRewardValue(new Double(value)); - rewardStructureValue.setRewardValueUnknown(rowIndex >= engine.getPathSize() - 1); } // A cumulative reward column @@ -3241,7 +3269,6 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect rewardStructureValue.setRewardValueUnknown(rowIndex >= engine.getPathSize()); } } - return rewardStructureValue; } } diff --git a/prism/src/userinterface/simulator/GUISimulatorPathTable.java b/prism/src/userinterface/simulator/GUISimulatorPathTable.java index c442a049..7521db18 100644 --- a/prism/src/userinterface/simulator/GUISimulatorPathTable.java +++ b/prism/src/userinterface/simulator/GUISimulatorPathTable.java @@ -275,6 +275,20 @@ public class GUISimulatorPathTable extends GUIGroupedTable stringValue = (String)value; this.setToolTipText("State " + row); } + else if (value instanceof GUISimulator.ActionValue) + { + GUISimulator.ActionValue actionValue = (GUISimulator.ActionValue)value; + if (actionValue.isActionValueUnknown()) + { + stringValue = "?"; + this.setToolTipText("Action label or module name for transition from state " + (row) + " to " + (row + 1) + " (not yet known)"); + } + else + { + stringValue = actionValue.getValue(); + this.setToolTipText("Action label or module name for transition from state " + (row) + " to " + (row + 1)); + } + } else if (value instanceof GUISimulator.TimeValue) { GUISimulator.TimeValue timeValue = (GUISimulator.TimeValue)value; @@ -347,8 +361,8 @@ public class GUISimulatorPathTable extends GUIGroupedTable width = (int)Math.ceil(rect.getWidth()); height = (int)Math.ceil(rect.getHeight()); - // State index - if (value instanceof String) { + // State index/action + if (value instanceof String || value instanceof GUISimulator.ActionValue) { // Position (horiz centred, vert centred) x = (getWidth()/2) - (width/2); y = (getHeight()/2) + (height/2);