From 72551d7248e8a8f187456f1c764e1774a421bc1c Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 11 Aug 2011 11:25:56 +0000 Subject: [PATCH] Refactoring: detach GUI simulator path table from SimulatorEngine and attach to PathFull. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3445 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/simulator/SimulatorEngine.java | 10 ++++ .../userinterface/simulator/GUISimulator.java | 5 +- .../simulator/GUISimulatorPathTableModel.java | 56 ++++++++++--------- .../simulator/SimulationView.java | 31 +++++++--- 4 files changed, 65 insertions(+), 37 deletions(-) diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index ec9a27a9..8e4d0439 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -977,6 +977,16 @@ public class SimulatorEngine // Querying of current path (full paths only) // ------------------------------------------------------------------------------ + /** + * Get access to the {@code PathFull} object storing the current path. + * (Not applicable for on-the-fly paths) + * This object is only valid until the next time {@link #createNewPath} is called. + */ + public PathFull getPathFull() + { + return (PathFull) path; + } + /** * Get the value of a variable at a given step of the path. * (Not applicable for on-the-fly paths) diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java index c4403909..766eb3bb 100644 --- a/prism/src/userinterface/simulator/GUISimulator.java +++ b/prism/src/userinterface/simulator/GUISimulator.java @@ -82,7 +82,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect this.engine = gui.getPrism().getSimulator(); view = new SimulationView(this, gui.getPrism().getSettings()); - pathTableModel = new GUISimulatorPathTableModel(this, engine, view); + pathTableModel = new GUISimulatorPathTableModel(this, view); updateTableModel = new UpdateTableModel(); @@ -114,7 +114,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect pathTablePlaceHolder.addMouseListener(this); - view.refreshToDefaultView(engine, pathActive, parsedModel); + view.refreshToDefaultView(pathActive, parsedModel); setPathActive(false); doEnables(); @@ -360,6 +360,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect // Create a new path in the simulator and add labels/properties engine.createNewPath(parsedModel); + pathTableModel.setPath(engine.getPathFull()); setPathActive(true); engine.initialisePath(initialState == null ? null : new parser.State(initialState, parsedModel)); repopulateFormulae(pf); diff --git a/prism/src/userinterface/simulator/GUISimulatorPathTableModel.java b/prism/src/userinterface/simulator/GUISimulatorPathTableModel.java index 03ea660d..bd0e3104 100644 --- a/prism/src/userinterface/simulator/GUISimulatorPathTableModel.java +++ b/prism/src/userinterface/simulator/GUISimulatorPathTableModel.java @@ -31,7 +31,7 @@ package userinterface.simulator; import java.util.*; import javax.swing.table.AbstractTableModel; -import simulator.SimulatorEngine; +import simulator.PathFull; import userinterface.simulator.SimulationView.*; import userinterface.util.GUIGroupedTableModel; import parser.ast.*; @@ -41,21 +41,20 @@ public class GUISimulatorPathTableModel extends AbstractTableModel implements GU private static final long serialVersionUID = 1L; private GUISimulator simulator; - private SimulatorEngine engine; private SimulationView view; private boolean pathActive; private ModulesFile parsedModel; + private PathFull path; private RewardStructureValue rewardStructureValue; private VariableValue variableValue; private TimeValue timeValue; private ActionValue actionValue; - public GUISimulatorPathTableModel(GUISimulator simulator, SimulatorEngine engine, SimulationView view) + public GUISimulatorPathTableModel(GUISimulator simulator, SimulationView view) { this.simulator = simulator; - this.engine = engine; this.view = view; this.view.addObserver(this); @@ -68,6 +67,11 @@ public class GUISimulatorPathTableModel extends AbstractTableModel implements GU this.pathActive = pathActive; } + public void setPath(PathFull path) + { + this.path = path; + } + public void setParsedModel(ModulesFile parsedModel) { this.parsedModel = parsedModel; @@ -395,7 +399,7 @@ public class GUISimulatorPathTableModel extends AbstractTableModel implements GU public int getRowCount() { // Return current path size if there is an active path. - return (pathActive ? engine.getPathSize() + 1 : 0); + return (pathActive ? path.size() + 1 : 0); } public boolean shouldColourRow(int row) @@ -499,7 +503,7 @@ public class GUISimulatorPathTableModel extends AbstractTableModel implements GU // The action column if (actionStart <= columnIndex && columnIndex < stepStart) { - actionValue = view.new ActionValue(rowIndex == 0 ? "" : engine.getModuleOrActionOfPathStep(rowIndex - 1)); + actionValue = view.new ActionValue(rowIndex == 0 ? "" : path.getModuleOrAction(rowIndex - 1)); actionValue.setActionValueUnknown(false); return actionValue; } @@ -509,23 +513,23 @@ public class GUISimulatorPathTableModel extends AbstractTableModel implements GU } // Cumulative time column else if (cumulativeTimeStart <= columnIndex && columnIndex < timeStart) { - timeValue = view.new TimeValue(engine.getCumulativeTimeUpToPathStep(rowIndex), true); - timeValue.setTimeValueUnknown(rowIndex > engine.getPathSize()); // Never unknown + timeValue = view.new TimeValue(path.getCumulativeTime(rowIndex), true); + timeValue.setTimeValueUnknown(rowIndex > path.size()); // Never unknown return timeValue; } // Time column else if (timeStart <= columnIndex && columnIndex < varStart) { - timeValue = view.new TimeValue(engine.getTimeSpentInPathStep(rowIndex), false); - timeValue.setTimeValueUnknown(rowIndex >= engine.getPathSize()); + timeValue = view.new TimeValue(path.getTime(rowIndex), false); + timeValue.setTimeValueUnknown(rowIndex >= path.size()); return timeValue; } // A variable column else if (varStart <= columnIndex && columnIndex < rewardStart) { - Variable var = ((Variable) view.getVisibleVariables().get(columnIndex - varStart)); - Object result = engine.getVariableValueOfPathStep(rowIndex, var.getIndex()); + Variable var = view.getVisibleVariables().get(columnIndex - varStart); + Object result = path.getState(rowIndex).varValues[var.getIndex()]; variableValue.setVariable(var); variableValue.setValue(result); - variableValue.setChanged(rowIndex == 0 || !engine.getVariableValueOfPathStep(rowIndex - 1, var.getIndex()).equals(result)); + variableValue.setChanged(rowIndex == 0 || !path.getState(rowIndex - 1).varValues[var.getIndex()].equals(result)); return variableValue; } // A reward column @@ -535,27 +539,27 @@ public class GUISimulatorPathTableModel extends AbstractTableModel implements GU rewardStructureValue.setRewardValueUnknown(false); // A state reward column if (rewardColumn.isStateReward()) { - double value = engine.getStateRewardOfPathStep(rowIndex, rewardColumn.getRewardStructure().getIndex()); + double value = path.getStateReward(rowIndex, rewardColumn.getRewardStructure().getIndex()); rewardStructureValue.setChanged(rowIndex == 0 - || value != engine.getStateRewardOfPathStep(rowIndex - 1, rewardColumn.getRewardStructure().getIndex())); + || value != path.getStateReward(rowIndex - 1, rewardColumn.getRewardStructure().getIndex())); rewardStructureValue.setRewardValue(new Double(value)); - rewardStructureValue.setRewardValueUnknown(rowIndex > engine.getPathSize()); // Never unknown + rewardStructureValue.setRewardValueUnknown(rowIndex > path.size()); // Never unknown } // A transition reward column else if (rewardColumn.isTransitionReward()) { - double value = engine.getTransitionRewardOfPathStep(rowIndex, rewardColumn.getRewardStructure().getIndex()); + double value = path.getTransitionReward(rowIndex, rewardColumn.getRewardStructure().getIndex()); rewardStructureValue.setChanged(rowIndex == 0 - || value != engine.getTransitionRewardOfPathStep(rowIndex - 1, rewardColumn.getRewardStructure().getIndex())); + || value != path.getTransitionReward(rowIndex - 1, rewardColumn.getRewardStructure().getIndex())); rewardStructureValue.setRewardValue(new Double(value)); - rewardStructureValue.setRewardValueUnknown(rowIndex >= engine.getPathSize()); + rewardStructureValue.setRewardValueUnknown(rowIndex >= path.size()); } // A cumulative reward column else { - double value = engine.getCumulativeRewardUpToPathStep(rowIndex, rewardColumn.getRewardStructure().getIndex()); + double value = path.getCumulativeReward(rowIndex, rewardColumn.getRewardStructure().getIndex()); rewardStructureValue.setChanged(rowIndex == 0 - || value != (engine.getCumulativeRewardUpToPathStep(rowIndex - 1, rewardColumn.getRewardStructure().getIndex()))); + || value != (path.getCumulativeReward(rowIndex - 1, rewardColumn.getRewardStructure().getIndex()))); rewardStructureValue.setRewardValue(new Double(value)); - rewardStructureValue.setRewardValueUnknown(rowIndex > engine.getPathSize()); // Never unknown + rewardStructureValue.setRewardValueUnknown(rowIndex > path.size()); // Never unknown } return rewardStructureValue; } @@ -570,7 +574,7 @@ public class GUISimulatorPathTableModel extends AbstractTableModel implements GU */ public void restartPathTable() { - view.refreshToDefaultView(engine, pathActive, parsedModel); + view.refreshToDefaultView(pathActive, parsedModel); } /** @@ -583,17 +587,17 @@ public class GUISimulatorPathTableModel extends AbstractTableModel implements GU public boolean isPathLooping() { - return engine.isPathLooping(); + return path.isLooping(); } public int getLoopStart() { - return engine.loopStart(); + return path.loopStart(); } public int getLoopEnd() { - return engine.loopEnd(); + return path.loopEnd(); } public SimulationView getView() diff --git a/prism/src/userinterface/simulator/SimulationView.java b/prism/src/userinterface/simulator/SimulationView.java index 579d2920..28cdabb7 100644 --- a/prism/src/userinterface/simulator/SimulationView.java +++ b/prism/src/userinterface/simulator/SimulationView.java @@ -33,7 +33,6 @@ import java.util.*; import parser.ast.*; import parser.type.Type; import prism.PrismSettings; -import simulator.SimulatorEngine; import userinterface.simulator.GUIViewDialog.RewardListItem; /** @@ -189,7 +188,7 @@ public class SimulationView extends Observable } } - public void refreshToDefaultView(SimulatorEngine engine, boolean pathActive, ModulesFile parsedModel) + public void refreshToDefaultView(boolean pathActive, ModulesFile parsedModel) { // First see if we can get away with using current settings... boolean canUseCurrentView = true; @@ -212,13 +211,18 @@ public class SimulationView extends Observable for (Variable var : hiddenVariables) allVarNames.add(var.getName()); - for (int i = 0; i < engine.getNumVariables(); i++) { - if (allVarNames.contains(engine.getVariableName(i))) - allVarNames.remove(engine.getVariableName(i)); - else - // Cannot use current view if a variable is not there. + // Cannot use current view if a variable is not there. + for (int g = 0; g < parsedModel.getNumGlobals(); g++) { + if (!allVarNames.remove(parsedModel.getGlobal(g).getName())) canUseCurrentView = false; } + for (int m = 0; m < parsedModel.getNumModules(); m++) { + Module module = parsedModel.getModule(m); + for (int v = 0; v < module.getNumDeclarations(); v++) { + if (!allVarNames.remove(module.getDeclaration(v).getName())) + canUseCurrentView = false; + } + } // Cannot use current view if we have too many variables. if (allVarNames.size() > 0) @@ -265,8 +269,17 @@ public class SimulationView extends Observable rewards.clear(); { - for (int i = 0; i < engine.getNumVariables(); i++) { - visibleVariables.add(new Variable(i, engine.getVariableName(i), engine.getVariableType(i))); + int i = 0; + for (int g = 0; g < parsedModel.getNumGlobals(); g++) { + visibleVariables.add(new Variable(i, parsedModel.getGlobal(g).getName(), parsedModel.getGlobal(g).getType())); + i++; + } + for (int m = 0; m < parsedModel.getNumModules(); m++) { + Module module = parsedModel.getModule(m); + for (int v = 0; v < module.getNumDeclarations(); v++) { + visibleVariables.add(new Variable(i, module.getDeclaration(v).getName(), module.getDeclaration(v).getType())); + i++; + } } for (int r = 0; r < parsedModel.getNumRewardStructs(); r++) {