diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java index ee5d1aab..c4403909 100644 --- a/prism/src/userinterface/simulator/GUISimulator.java +++ b/prism/src/userinterface/simulator/GUISimulator.java @@ -28,7 +28,6 @@ package userinterface.simulator; -import java.util.*; import java.awt.*; import java.awt.event.*; import javax.swing.*; @@ -39,7 +38,6 @@ import simulator.*; import simulator.networking.*; import parser.*; import parser.ast.*; -import parser.type.*; import prism.*; import userinterface.*; import userinterface.util.*; @@ -49,6 +47,8 @@ import userinterface.simulator.networking.*; public class GUISimulator extends GUIPlugin implements MouseListener, ListSelectionListener, PrismSettingsListener { + private static final long serialVersionUID = 1L; + //ATTRIBUTES private GUIPrism gui; //reference to the gui private GUIMultiProperties guiProp; //reference to the properties information @@ -59,10 +59,10 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect private JPopupMenu pathPopupMenu; //Current State - private ModulesFile parsedModel; private boolean pathActive; + private ModulesFile parsedModel; - private PathTableModel pathTableModel; + private GUISimulatorPathTableModel pathTableModel; private UpdateTableModel updateTableModel; private Values lastConstants, lastPropertyConstants, lastInitialState; @@ -79,11 +79,10 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect public GUISimulator(GUIPrism gui) { super(gui, true); - this.gui = gui; this.engine = gui.getPrism().getSimulator(); - view = new SimulationView(); - pathTableModel = new PathTableModel(view); + view = new SimulationView(this, gui.getPrism().getSettings()); + pathTableModel = new GUISimulatorPathTableModel(this, engine, view); updateTableModel = new UpdateTableModel(); @@ -115,12 +114,11 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect pathTablePlaceHolder.addMouseListener(this); - view.refreshToDefaultView(); + view.refreshToDefaultView(engine, pathActive, parsedModel); - pathActive = false; + setPathActive(false); doEnables(); - //verifyAllPropertiesAtOnce = true; //options = new GUISimulatorOptions(this); currentUpdatesTable.setModel(updateTableModel); @@ -203,6 +201,11 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect this.guiProp = guiProp; } + public JList getStateLabelList() + { + return stateLabelList; + } + public String getTotalRewardLabelString() { int i, n; @@ -222,7 +225,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect { tableScroll.setViewportView(pathTablePlaceHolder); - pathActive = false; + setPathActive(false); pathTableModel.restartPathTable(); ((GUISimLabelList) stateLabelList).clearLabels(); @@ -231,8 +234,8 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect public void a_loadModulesFile(ModulesFile mf) { - this.parsedModel = mf; - pathActive = false; + setParsedModel(mf); + setPathActive(false); pathTableModel.restartPathTable(); updateTableModel.restartUpdatesTable(); @@ -302,7 +305,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect if (parsedModel.getInitialStates() != null) { throw new PrismException("The simulator does not not yet handle models with multiple states"); } - + // do we need to ask for an initial state for simulation? // no: just use default/random if (!chooseInitialState) { @@ -311,7 +314,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect // yes: else { // first, pick default values for chooser dialog - + // default initial state if none specified previously if (lastInitialState == null) { lastInitialState = new Values(parsedModel.getDefaultInitialState(), parsedModel); @@ -342,7 +345,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect lastInitialState = new Values(parsedModel.getDefaultInitialState(), parsedModel); } } - + initialState = null; initialState = GUIInitialStatePicker.defineInitalValuesWithDialog(getGUI(), lastInitialState, parsedModel); // if user clicked cancel from dialog, bail out @@ -357,7 +360,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect // Create a new path in the simulator and add labels/properties engine.createNewPath(parsedModel); - pathActive = true; + setPathActive(true); engine.initialisePath(initialState == null ? null : new parser.State(initialState, parsedModel)); repopulateFormulae(pf); @@ -380,7 +383,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect lastInitialState = initialState; if (getPrism().getSettings().getBoolean(PrismSettings.SIMULATOR_NEW_PATH_ASK_VIEW)) { - new GUIViewDialog(gui, pathTableModel.getView()); + new GUIViewDialog(gui, pathTableModel.getView(), pathTableModel); } } catch (PrismException e) { @@ -642,7 +645,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect public void a_configureView() { - new GUIViewDialog(gui, pathTableModel.getView()); + new GUIViewDialog(gui, pathTableModel.getView(), pathTableModel); } /** @@ -784,30 +787,6 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect { } - //ACCESS METHODS - - /** - * Getter for property verifyAllPropertiesAtOnce. - * @return Value of property verifyAllPropertiesAtOnce. - */ - public boolean isVerifyAllPropertiesAtOnce() - { - return getPrism().getSettings().getBoolean(PrismSettings.SIMULATOR_SIMULTANEOUS); - //return verifyAllPropertiesAtOnce; - } - - //UPDATE METHODS - - /** - * Setter for property verifyAllPropertiesAtOnce. - * @param verifyAllPropertiesAtOnce New value of property verifyAllPropertiesAtOnce. - */ - public void setVerifyAllPropertiesAtOnce(boolean verifyAllPropertiesAtOnce) throws PrismException - { - getPrism().getSettings().set(PrismSettings.SIMULATOR_SIMULTANEOUS, verifyAllPropertiesAtOnce); - //this.verifyAllPropertiesAtOnce = verifyAllPropertiesAtOnce; - } - protected void doEnables() { newPath.setEnabled(parsedModel != null && !computing); @@ -1671,7 +1650,17 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect public void setPathActive(boolean pathActive) { this.pathActive = pathActive; - doEnables(); + pathTableModel.setPathActive(pathActive); + } + + /** + * Setter for property parsedModel. + * @param pathActive New value of property pathActive. + */ + public void setParsedModel(ModulesFile parsedModel) + { + this.parsedModel = parsedModel; + pathTableModel.setParsedModel(parsedModel); } /** @@ -1878,43 +1867,6 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect } - /** - * Getter for property askForInitialState. - * @return Value of property askForInitialState. - */ - public boolean isAskForInitialState() - { - return false; //getPrism().getSettings().getBoolean(PrismSettings.SIMULATOR_NEW_PATH_ASK_INITIAL); - } - - /** - * Setter for property askForInitialState. - * @param askForInitialState New value of property askForInitialState. - */ - public void setAskForInitialState(boolean askForInitialState) throws PrismException - { - //getPrism().getSettings().set(PrismSettings.SIMULATOR_NEW_PATH_ASK_INITIAL, askForInitialState); - } - - /** - * Getter for property maxPathLength. - * @return Value of property maxPathLength. - */ - /*public int getMaxPathLength() - { - return maxPathLength; - }*/ - - /** - * Setter for property maxPathLength. - * @param maxPathLength New value of property maxPathLength. - */ - /*public void setMaxPathLength(int maxPathLength) - { - this.maxPathLength = maxPathLength; - engine.setMaximumPathLength(maxPathLength); - }*/ - /** * Getter for property displayPathLoops. * @return Value of property displayPathLoops. @@ -2027,1195 +1979,6 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect // End of variables declaration//GEN-END:variables - /** - * Represents a variable in the model. - */ - public class Variable - { - private int index; - private String name; - private Type type; - - public Variable(int index, String name, Type type) - { - this.index = index; - this.name = name; - this.type = type; - } - - public int getIndex() - { - return index; - } - - public String getName() - { - return name; - } - - public Type getType() - { - return type; - } - - public String toString() - { - return name; - } - - public boolean equals(Object o) - { - return (o instanceof Variable && ((Variable) o).getIndex() == index); - } - } - - public class VariableValue - { - private Variable variable; - private Object value; - private boolean hasChanged; - - public VariableValue(Variable variable, Object value) - { - this.variable = variable; - this.value = value; - this.hasChanged = true; - } - - public Object getValue() - { - return value; - } - - public void setValue(Object value) - { - this.value = value; - } - - public Variable getVariable() - { - return variable; - } - - public void setVariable(Variable variable) - { - this.variable = variable; - } - - public boolean hasChanged() - { - return hasChanged; - } - - public void setChanged(boolean hasChanged) - { - this.hasChanged = hasChanged; - } - } - - 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; - private boolean timeValueUnknown; - private boolean isCumulative; - - public TimeValue(Double value, boolean isCumulative) - { - this.value = value; - this.isCumulative = isCumulative; - } - - public Double getValue() - { - return value; - } - - public void setValue(Double value) - { - this.value = value; - } - - public void setTimeValueUnknown(boolean unknown) - { - this.timeValueUnknown = unknown; - } - - public boolean isTimeValueUnknown() - { - return this.timeValueUnknown; - } - - public boolean isCumulative() - { - return isCumulative; - } - - public void setCumulative(boolean isCumulative) - { - this.isCumulative = isCumulative; - } - } - - /** - * Represents a reward structure in the model. - */ - public class RewardStructure - { - private int index; - private String name; - - private boolean stateEmpty; - private boolean transitionEmpty; - - public RewardStructure(int index, String name, boolean stateEmpty, boolean transitionEmpty) - { - this.index = index; - this.name = name; - this.stateEmpty = stateEmpty; - this.transitionEmpty = transitionEmpty; - } - - public int getIndex() - { - return index; - } - - public String getName() - { - return name; - } - - public String getColumnName() - { - if (name == null) { - return "" + (index + 1); - } else { - return "\"" + name + "\""; - } - } - - public boolean isStateEmpty() - { - return stateEmpty; - } - - public boolean isTransitionEmpty() - { - return transitionEmpty; - } - - public boolean isCumulative() - { - return false; - } - - public String toString() - { - if (name != null) { - return "" + (index + 1) + ": \"" + name + "\""; - } else { - return "" + (index + 1) + ": "; - } - } - - public boolean equals(Object o) - { - return (o instanceof RewardStructure && ((RewardStructure) o).getIndex() == index && ((RewardStructure) o).isCumulative() == isCumulative()); - } - } - - public class RewardStructureColumn - { - public static final int STATE_REWARD = 0; - public static final int TRANSITION_REWARD = 1; - public static final int CUMULATIVE_REWARD = 2; - - private RewardStructure rewardStructure; - private int type; - - public RewardStructureColumn(RewardStructure rewardStructure, int type) - { - this.rewardStructure = rewardStructure; - this.type = type; - } - - public String getColumnName() - { - switch (type) { - case (STATE_REWARD): - return rewardStructure.getColumnName(); - case (TRANSITION_REWARD): - return "[ " + rewardStructure.getColumnName() + " ]"; - case (CUMULATIVE_REWARD): - return rewardStructure.getColumnName() + " (+)"; - } - return ""; - } - - public RewardStructure getRewardStructure() - { - return rewardStructure; - } - - public void setRewardStructure(RewardStructure rewardStructure) - { - this.rewardStructure = rewardStructure; - } - - public String toString() - { - return getColumnName(); - } - - public boolean isStateReward() - { - return this.type == RewardStructureColumn.STATE_REWARD; - } - - public boolean isTransitionReward() - { - return this.type == RewardStructureColumn.TRANSITION_REWARD; - } - - public boolean isCumulativeReward() - { - return this.type == RewardStructureColumn.CUMULATIVE_REWARD; - } - - public void setStateReward() - { - this.type = RewardStructureColumn.STATE_REWARD; - } - - public void setTransitionReward() - { - this.type = RewardStructureColumn.TRANSITION_REWARD; - } - - public void setCumulativeReward() - { - this.type = RewardStructureColumn.CUMULATIVE_REWARD; - } - } - - public class RewardStructureValue - { - private RewardStructureColumn rewardStructureColumn; - private Double rewardValue; - private boolean hasChanged; - - private boolean rewardValueUnknown; - - public RewardStructureValue(RewardStructureColumn rewardStructureColumn, Double rewardValue) - { - this.rewardStructureColumn = rewardStructureColumn; - this.rewardValue = rewardValue; - this.hasChanged = true; - - this.rewardValueUnknown = false; - } - - public RewardStructureColumn getRewardStructureColumn() - { - return rewardStructureColumn; - } - - public void setRewardStructureColumn(RewardStructureColumn rewardStructureColumn) - { - this.rewardStructureColumn = rewardStructureColumn; - } - - public Double getRewardValue() - { - return rewardValue; - } - - public void setRewardValue(Double rewardValue) - { - this.rewardValue = rewardValue; - } - - public void setRewardValueUnknown(boolean unknown) - { - this.rewardValueUnknown = unknown; - } - - public boolean isRewardValueUnknown() - { - return this.rewardValueUnknown; - } - - public boolean hasChanged() - { - return hasChanged; - } - - public void setChanged(boolean hasChanged) - { - this.hasChanged = hasChanged; - } - } - - public class SimulationView extends Observable - { - private ArrayList visibleVariables; - private ArrayList hiddenVariables; - - private ArrayList visibleRewardColumns; - private ArrayList rewards; - - private boolean stepsVisible; - private boolean actionsVisible; - private boolean showTime; - private boolean showCumulativeTime; - private boolean useChangeRenderer; - - private boolean initialRun = true; - - public SimulationView() - { - this.visibleVariables = new ArrayList(); - this.hiddenVariables = new ArrayList(); - - this.visibleRewardColumns = new ArrayList(); - this.rewards = new ArrayList(); - - this.stepsVisible = true; - this.actionsVisible = true; - this.showTime = false; - this.showCumulativeTime = true; - - useChangeRenderer = (gui.getPrism().getSettings().getInteger(PrismSettings.SIMULATOR_RENDER_ALL_VALUES) == 0); - - } - - public boolean showSteps() - { - return stepsVisible; - } - - public void showSteps(boolean stepsVisible) - { - this.stepsVisible = stepsVisible; - - this.setChanged(); - this.notifyObservers(); - } - - public boolean showActions() - { - return actionsVisible; - } - - public void showActions(boolean actionsVisible) - { - this.actionsVisible = actionsVisible; - - this.setChanged(); - this.notifyObservers(); - } - - public boolean showTime() - { - return showTime; - } - - public boolean showCumulativeTime() - { - return showCumulativeTime; - } - - public boolean canShowTime() - { - return parsedModel.getModelType() == ModelType.CTMC; - } - - public void showTime(boolean showTime) - { - this.showTime = showTime; - - this.setChanged(); - this.notifyObservers(); - } - - public void showCumulativeTime(boolean showCumulativeTime) - { - this.showCumulativeTime = showCumulativeTime; - - this.setChanged(); - this.notifyObservers(); - } - - public ArrayList getVisibleVariables() - { - return visibleVariables; - } - - public ArrayList getHiddenVariables() - { - return hiddenVariables; - } - - public void setVariableVisibility(ArrayList visibleVariables, ArrayList hiddenVariables) - { - this.visibleVariables = visibleVariables; - this.hiddenVariables = hiddenVariables; - - this.setChanged(); - this.notifyObservers(); - } - - public ArrayList getVisibleRewardColumns() - { - return visibleRewardColumns; - } - - public void setVisibleRewardListItems(ArrayList visibleRewardListItems) - { - ArrayList visibleRewardColumns = new ArrayList(); - - for (Object obj : visibleRewardListItems) { - GUIViewDialog.RewardListItem item = (GUIViewDialog.RewardListItem) obj; - if (item.isCumulative()) - visibleRewardColumns.add(new RewardStructureColumn(item.getRewardStructure(), GUISimulator.RewardStructureColumn.CUMULATIVE_REWARD)); - else { - if (!item.getRewardStructure().isStateEmpty()) - visibleRewardColumns.add(new RewardStructureColumn(item.getRewardStructure(), GUISimulator.RewardStructureColumn.STATE_REWARD)); - if (!item.getRewardStructure().isTransitionEmpty()) - visibleRewardColumns.add(new RewardStructureColumn(item.getRewardStructure(), GUISimulator.RewardStructureColumn.TRANSITION_REWARD)); - } - } - - this.visibleRewardColumns = visibleRewardColumns; - - this.setChanged(); - this.notifyObservers(); - } - - public ArrayList getRewards() - { - return this.rewards; - } - - public SimulatorEngine getEngine() - { - return engine; - } - - public boolean isChangeRenderer() - { - return useChangeRenderer; - } - - public void setRenderer(boolean isChangeRenderer) - { - if (useChangeRenderer != isChangeRenderer) { - useChangeRenderer = isChangeRenderer; - - GUISimulator.this.setRenderer(useChangeRenderer); - } - } - - public void refreshToDefaultView() - { - // First see if we can get away with using current settings... - boolean canUseCurrentView = true; - - if (!pathActive) - canUseCurrentView = false; - else { - if (useChangeRenderer != usingChangeRenderer()) { - GUISimulator.this.setRenderer(useChangeRenderer); - } - - // Time-wise we have a problem. - if (parsedModel.getModelType() != ModelType.CTMC && (showTime || showCumulativeTime)) - canUseCurrentView = false; - - // Make a set of all variable names. - TreeSet allVarNames = new TreeSet(); - - for (Object var : visibleVariables) - allVarNames.add(((Variable) var).getName()); - for (Object var : hiddenVariables) - allVarNames.add(((Variable) 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. - canUseCurrentView = false; - } - - // Cannot use current view if we have too many variables. - if (allVarNames.size() > 0) - canUseCurrentView = false; - - // Make a list of all reward structures - ArrayList allrew = new ArrayList(); - - for (Object rew : rewards) { - allrew.add((RewardStructure) rew); - } - - for (int r = 0; r < parsedModel.getNumRewardStructs(); r++) { - RewardStruct rewardStruct = parsedModel.getRewardStruct(r); - String rewardName = rewardStruct.getName(); - - boolean hasStates = parsedModel.getRewardStruct(r).getNumStateItems() != 0; - boolean hasTrans = parsedModel.getRewardStruct(r).getNumTransItems() != 0; - - boolean foundReward = false; - - for (Object rewobj : rewards) { - RewardStructure rew = (RewardStructure) rewobj; - if (rew.isStateEmpty() == !hasStates && rew.isTransitionEmpty() == !hasTrans - && ((rew.getName() == null && rewardName.equals("")) || (rew.getName() != null && rew.getName().equals(rewardName)))) { - allrew.remove(rew); - foundReward = true; - } - } - - if (!foundReward) - canUseCurrentView = false; - } - - if (allrew.size() > 0) - canUseCurrentView = false; - - } - - if (!canUseCurrentView && pathActive) { - visibleVariables.clear(); - hiddenVariables.clear(); - visibleRewardColumns.clear(); - - rewards.clear(); - - { - for (int i = 0; i < engine.getNumVariables(); i++) { - visibleVariables.add(new Variable(i, engine.getVariableName(i), engine.getVariableType(i))); - } - - for (int r = 0; r < parsedModel.getNumRewardStructs(); r++) { - RewardStruct rewardStruct = parsedModel.getRewardStruct(r); - String rewardName = rewardStruct.getName(); - - if (rewardName.trim().length() == 0) { - rewardName = null; - } - - RewardStructure rewardStructure = new RewardStructure(r, rewardName, parsedModel.getRewardStruct(r).getNumStateItems() == 0, - parsedModel.getRewardStruct(r).getNumTransItems() == 0); - - if (!rewardStructure.isStateEmpty() || !rewardStructure.isTransitionEmpty()) - rewards.add(rewardStructure); - - if (!rewardStructure.isStateEmpty()) - visibleRewardColumns.add(new RewardStructureColumn(rewardStructure, RewardStructureColumn.STATE_REWARD)); - - if (!rewardStructure.isTransitionEmpty()) - visibleRewardColumns.add(new RewardStructureColumn(rewardStructure, RewardStructureColumn.TRANSITION_REWARD)); - } - - } - } - initialRun = false; - this.setChanged(); - this.notifyObservers(); - - } - } - - class PathTableModel extends AbstractTableModel implements GUIGroupedTableModel, Observer - { - private SimulationView view; - private RewardStructureValue rewardStructureValue; - private VariableValue variableValue; - private TimeValue timeValue; - private ActionValue actionValue; - - public PathTableModel(SimulationView view) - { - this.view = view; - this.view.addObserver(this); - - rewardStructureValue = new RewardStructureValue(null, null); - variableValue = new VariableValue(null, null); - } - - public int getGroupCount() - { - if (!pathActive) { - return 0; - } else { - int groupCount = 0; - - if (view.showActions() || view.showSteps()) { - groupCount++; - } - - if (view.canShowTime() && (view.showTime() || view.showCumulativeTime())) { - groupCount++; - } - - ArrayList vars = view.getVisibleVariables(); - Set varNames = new HashSet(); - - for (Object var : vars) { - Variable variable = (Variable) var; - varNames.add(variable.getName()); - } - - for (int g = 0; g < parsedModel.getNumGlobals(); g++) { - if (varNames.contains(parsedModel.getGlobal(g).getName())) { - groupCount++; - break; - } - } - - for (int m = 0; m < parsedModel.getNumModules(); m++) { - Module module = parsedModel.getModule(m); - for (int v = 0; v < module.getNumDeclarations(); v++) { - if (varNames.contains(module.getDeclaration(v).getName())) { - groupCount++; - break; - } - } - } - - if (view.getVisibleRewardColumns().size() > 0) { - groupCount++; - } - - return groupCount; - } - } - - public void update(Observable o, Object arg) - { - if (o == view) { - fireTableStructureChanged(); - - //Sort out the minimum widths for each column - sortOutColumnSizes(); - } - } - - public String getGroupName(int groupIndex) - { - if (!pathActive) { - return ""; - } else { - int groupCount = 0; - - if (view.showActions() || view.showSteps()) { - if (groupCount == groupIndex) { - return "Step"; - } - - groupCount++; - } - - if (view.canShowTime() && (view.showTime() || view.showCumulativeTime())) { - if (groupCount == groupIndex) { - return "Time"; - } - - groupCount++; - } - - if (view.getVisibleVariables().size() > 0) { - ArrayList vars = view.getVisibleVariables(); - Set varNames = new HashSet(); - - for (Object var : vars) { - Variable variable = (Variable) var; - varNames.add(variable.getName()); - } - - for (int g = 0; g < parsedModel.getNumGlobals(); g++) { - if (varNames.contains(parsedModel.getGlobal(g).getName())) { - if (groupCount == groupIndex) { - return "Globals"; - } - - groupCount++; - break; - } - } - - for (int m = 0; m < parsedModel.getNumModules(); m++) { - Module module = parsedModel.getModule(m); - for (int v = 0; v < module.getNumDeclarations(); v++) { - if (varNames.contains(module.getDeclaration(v).getName())) { - if (groupCount == groupIndex) { - return "" + parsedModel.getModuleName(m) + ""; - } - - groupCount++; - break; - } - } - } - } - - // Add state and transitions rewards for each reward structure. - if (view.getVisibleRewardColumns().size() > 0) { - if (groupCount == groupIndex) { - return "Rewards"; - } - - groupCount++; - } - - return "Undefined Group"; - } - } - - public String getGroupToolTip(int groupIndex) - { - ArrayList vars = view.getVisibleVariables(); - Set varNames = new HashSet(); - - for (Object var : vars) { - Variable variable = (Variable) var; - varNames.add(variable.getName()); - } - - int groupCount = 0; - - if (view.showActions() || view.showSteps()) { - if (groupCount == groupIndex) { - return null; - } - - groupCount++; - } - - if (view.canShowTime() && (view.showTime() || view.showCumulativeTime())) { - if (groupCount == groupIndex) { - return null; - } - - groupCount++; - } - - for (int g = 0; g < parsedModel.getNumGlobals(); g++) { - if (varNames.contains(parsedModel.getGlobal(g).getName())) { - if (groupCount == groupIndex) { - return "Global variables"; - } - - groupCount++; - break; - } - } - - for (int m = 0; m < parsedModel.getNumModules(); m++) { - Module module = parsedModel.getModule(m); - for (int v = 0; v < module.getNumDeclarations(); v++) { - if (varNames.contains(module.getDeclaration(v).getName())) { - if (groupCount == groupIndex) { - return "Variables of module \"" + parsedModel.getModuleName(m) + "\""; - } - - groupCount++; - break; - } - } - } - - // Add state and transitions rewards for each reward structure. - if (view.getVisibleRewardColumns().size() > 0) { - if (groupCount == groupIndex) { - return "State, transition and cumulative rewards"; - } - - groupCount++; - } - - return null; - } - - public int getLastColumnOfGroup(int groupIndex) - { - int stepStart = 0; - int timeStart = stepStart + (view.showActions() ? 1 : 0) + (view.showSteps() ? 1 : 0); - int varStart = timeStart + (view.canShowTime() && view.showCumulativeTime() ? 1 : 0) + (view.canShowTime() && view.showTime() ? 1 : 0); - int rewardStart = varStart + view.getVisibleVariables().size(); - - int groupCount = 0; - - if (view.showActions() || view.showSteps()) { - if (groupCount == groupIndex) { - if (view.showActions() && view.showSteps()) - return stepStart + 1; - else - return stepStart; - } - - groupCount++; - } - - if (view.canShowTime() && (view.showCumulativeTime() || view.showTime())) { - if (groupCount == groupIndex) { - if (view.showCumulativeTime() && view.showTime()) - return timeStart + 1; - else - return timeStart; - } - - groupCount++; - } - - if (view.getVisibleVariables().size() > 0) { - int visVarCount = 0; - - ArrayList vars = view.getVisibleVariables(); - Set varNames = new HashSet(); - - for (Object var : vars) { - Variable variable = (Variable) var; - varNames.add(variable.getName()); - } - - boolean atLeastOneGlobal = false; - - for (int g = 0; g < parsedModel.getNumGlobals(); g++) { - boolean contained = varNames.contains(parsedModel.getGlobal(g).getName()); - - if (!atLeastOneGlobal && contained) { - atLeastOneGlobal = true; - } - - if (contained) - visVarCount++; - } - - if (atLeastOneGlobal && groupCount == groupIndex) { - return varStart + visVarCount - 1; - } - - if (atLeastOneGlobal) { - groupCount++; - } - - for (int m = 0; m < parsedModel.getNumModules(); m++) { - Module module = parsedModel.getModule(m); - boolean atLeastOne = false; - - for (int v = 0; v < module.getNumDeclarations(); v++) { - boolean contained = varNames.contains(module.getDeclaration(v).getName()); - if (!atLeastOne && contained) { - atLeastOne = true; - } - - if (contained) - visVarCount++; - } - - if (atLeastOne && groupCount == groupIndex) { - return varStart + visVarCount - 1; - } - - if (atLeastOne) { - groupCount++; - } - } - } - - // Add state and transitions rewards for each reward structure. - if (view.getVisibleRewardColumns().size() > 0) { - if (groupCount == groupIndex) { - return rewardStart + view.getVisibleRewardColumns().size() - 1; - } - - groupCount++; - } - - return 0; - } - - /** - * Returns the number of columns. - * @see javax.swing.table.TableModel#getColumnCount() - */ - public int getColumnCount() - { - if (!pathActive) { - return 0; - } else { - int colCount = 0; - - colCount += (view.showActions() ? 1 : 0); - colCount += (view.showSteps() ? 1 : 0); - colCount += (view.canShowTime() && view.showCumulativeTime() ? 1 : 0) + (view.canShowTime() && view.showTime() ? 1 : 0); - colCount += view.getVisibleVariables().size(); - colCount += view.getVisibleRewardColumns().size(); - - return colCount; - } - } - - /** - * Returns the number of rows. - * @see javax.swing.table.TableModel#getRowCount() - */ - public int getRowCount() - { - // Return current path size if there is an active path. - return (pathActive ? engine.getPathSize() + 1 : 0); - } - - public boolean shouldColourRow(int row) - { - int selection = stateLabelList.getSelectedIndex(); - if (selection != -1) { - GUISimLabelList.SimLabel label = (GUISimLabelList.SimLabel) stateLabelList.getModel().getElementAt(selection); - if (row == getRowCount() - 1) { - if (label.getResult() == 1) - return true; - } else { - if (label.getResult(row) == 1) - return true; - } - } - - return false; - } - - public String getColumnName(int columnIndex) - { - if (pathActive) { - int actionStart = 0; - int stepStart = actionStart + (view.showActions() ? 1 : 0); - int cumulativeTimeStart = stepStart + (view.showSteps() ? 1 : 0); - int timeStart = cumulativeTimeStart + (view.canShowTime() && view.showCumulativeTime() ? 1 : 0); - int varStart = timeStart + (view.canShowTime() && view.showTime() ? 1 : 0); - int rewardStart = varStart + view.getVisibleVariables().size(); - - // The step column - if (actionStart <= columnIndex && columnIndex < stepStart) { - return "Action"; - } else if (stepStart <= columnIndex && columnIndex < cumulativeTimeStart) { - return "#"; - } else if (cumulativeTimeStart <= columnIndex && columnIndex < timeStart) { - return "Time (+)"; - } else if (timeStart <= columnIndex && columnIndex < varStart) { - return "Time"; - } - // A variable column - else if (varStart <= columnIndex && columnIndex < rewardStart) { - return ((Variable) view.getVisibleVariables().get(columnIndex - varStart)).toString(); - } - - else if (rewardStart <= columnIndex) { - return ((RewardStructureColumn) view.getVisibleRewardColumns().get(columnIndex - rewardStart)).getColumnName(); - } - } - return "Undefined Column"; - } - - public String getColumnToolTip(int columnIndex) - { - if (pathActive) { - int actionStart = 0; - int stepStart = actionStart + (view.showActions() ? 1 : 0); - int cumulativeTimeStart = stepStart + (view.showSteps() ? 1 : 0); - int timeStart = cumulativeTimeStart + (view.canShowTime() && view.showCumulativeTime() ? 1 : 0); - int varStart = timeStart + (view.canShowTime() && view.showTime() ? 1 : 0); - int rewardStart = varStart + view.getVisibleVariables().size(); - - // The step column - if (actionStart <= columnIndex && columnIndex < stepStart) { - return "Module name or [action] label"; - } else if (stepStart <= columnIndex && columnIndex < cumulativeTimeStart) { - return "Index of state in path"; - } else if (cumulativeTimeStart <= columnIndex && columnIndex < timeStart) { - return "Cumulative time"; - } else if (timeStart <= columnIndex && columnIndex < varStart) { - return "Time spent in state"; - } - // A variable column - else if (varStart <= columnIndex && columnIndex < rewardStart) { - return "Values of variable \"" + ((Variable) view.getVisibleVariables().get(columnIndex - varStart)).toString() + "\""; - } - - else if (rewardStart <= columnIndex) { - RewardStructureColumn column = ((RewardStructureColumn) view.getVisibleRewardColumns().get(columnIndex - rewardStart)); - String rewardName = column.getRewardStructure().getColumnName(); - - if (column.isStateReward()) - return "State reward of reward structure " + rewardName; - if (column.isTransitionReward()) - return "Transition reward of reward structure " + rewardName; - if (column.isCumulativeReward()) - return "Cumulative reward of reward structure " + rewardName; - } - } - return "Undefined Column"; - } - - public Object getValueAt(int rowIndex, int columnIndex) - { - if (pathActive) { - int actionStart = 0; - int stepStart = actionStart + (view.showActions() ? 1 : 0); - int cumulativeTimeStart = stepStart + (view.showSteps() ? 1 : 0); - int timeStart = cumulativeTimeStart + (view.canShowTime() && view.showCumulativeTime() ? 1 : 0); - int varStart = timeStart + (view.canShowTime() && view.showTime() ? 1 : 0); - int rewardStart = varStart + view.getVisibleVariables().size(); - - // The action column - if (actionStart <= columnIndex && columnIndex < stepStart) { - actionValue = new ActionValue(rowIndex == 0 ? "" : engine.getModuleOrActionOfPathStep(rowIndex - 1)); - actionValue.setActionValueUnknown(false); - return actionValue; - } - // The step column - else if (stepStart <= columnIndex && columnIndex < cumulativeTimeStart) { - return "" + rowIndex; - } - // Cumulative time column - else if (cumulativeTimeStart <= columnIndex && columnIndex < timeStart) { - timeValue = new TimeValue(engine.getCumulativeTimeUpToPathStep(rowIndex), true); - timeValue.setTimeValueUnknown(rowIndex > engine.getPathSize()); // Never unknown - return timeValue; - } - // Time column - else if (timeStart <= columnIndex && columnIndex < varStart) { - timeValue = new TimeValue(engine.getTimeSpentInPathStep(rowIndex), false); - timeValue.setTimeValueUnknown(rowIndex >= engine.getPathSize()); - 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()); - variableValue.setVariable(var); - variableValue.setValue(result); - variableValue.setChanged(rowIndex == 0 || !engine.getVariableValueOfPathStep(rowIndex - 1, var.getIndex()).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.getStateRewardOfPathStep(rowIndex, rewardColumn.getRewardStructure().getIndex()); - rewardStructureValue.setChanged(rowIndex == 0 - || value != engine.getStateRewardOfPathStep(rowIndex - 1, rewardColumn.getRewardStructure().getIndex())); - rewardStructureValue.setRewardValue(new Double(value)); - rewardStructureValue.setRewardValueUnknown(rowIndex > engine.getPathSize()); // Never unknown - } - // A transition reward column - else if (rewardColumn.isTransitionReward()) { - double value = engine.getTransitionRewardOfPathStep(rowIndex, rewardColumn.getRewardStructure().getIndex()); - rewardStructureValue.setChanged(rowIndex == 0 - || value != engine.getTransitionRewardOfPathStep(rowIndex - 1, rewardColumn.getRewardStructure().getIndex())); - rewardStructureValue.setRewardValue(new Double(value)); - rewardStructureValue.setRewardValueUnknown(rowIndex >= engine.getPathSize()); - } - // A cumulative reward column - else { - double value = engine.getCumulativeRewardUpToPathStep(rowIndex, rewardColumn.getRewardStructure().getIndex()); - rewardStructureValue.setChanged(rowIndex == 0 - || value != (engine.getCumulativeRewardUpToPathStep(rowIndex - 1, rewardColumn.getRewardStructure().getIndex()))); - rewardStructureValue.setRewardValue(new Double(value)); - rewardStructureValue.setRewardValueUnknown(rowIndex > engine.getPathSize()); // Never unknown - } - return rewardStructureValue; - } - } - - return "Undefined value"; - } - - /** - * Method is called when a new path is created. - * The structure of the path may be for a different model etc. - */ - public void restartPathTable() - { - view.refreshToDefaultView(); - } - - /** - * Method is called whenever a path is modified. - */ - public void updatePathTable() - { - fireTableDataChanged(); - } - - public boolean isPathLooping() - { - return engine.isPathLooping(); - } - - public int getLoopStart() - { - return engine.loopStart(); - } - - public int getLoopEnd() - { - return engine.loopEnd(); - } - - public boolean isDisplayPathLoops() - { - return displayPathLoops; - } - - public SimulationView getView() - { - return view; - } - - public void setView(SimulationView view) - { - this.view.deleteObserver(this); - this.view = view; - this.view.addObserver(this); - } - } - public void sortOutColumnSizes() { int prevWidth = pathTable.getWidth(); diff --git a/prism/src/userinterface/simulator/GUISimulatorPathTable.java b/prism/src/userinterface/simulator/GUISimulatorPathTable.java index 66ce6a95..e0ec0cd5 100644 --- a/prism/src/userinterface/simulator/GUISimulatorPathTable.java +++ b/prism/src/userinterface/simulator/GUISimulatorPathTable.java @@ -28,34 +28,36 @@ package userinterface.simulator; -import simulator.*; -import prism.*; -import userinterface.util.*; - import javax.swing.*; import javax.swing.table.*; import java.awt.*; import java.awt.geom.*; import java.awt.font.*; +import simulator.*; +import userinterface.util.*; +import userinterface.simulator.SimulationView.*; + public class GUISimulatorPathTable extends GUIGroupedTable { - private SimulatorEngine engine; + private static final long serialVersionUID = 1L; + + private SimulatorEngine engine; private GUISimulator simulator; // Table model - private GUISimulator.PathTableModel ptm; + private GUISimulatorPathTableModel ptm; // Component on left hand side to show path loops private JList loopIndicator; private LoopIndicatorListModel loopIndicatorModel; - + /** Creates a new instance of GUISimulatorPathTable */ - public GUISimulatorPathTable(GUISimulator simulator, GUISimulator.PathTableModel ptm, SimulatorEngine engine) + public GUISimulatorPathTable(GUISimulator simulator, GUISimulatorPathTableModel ptm, SimulatorEngine engine) { super(ptm); this.ptm = ptm; this.simulator = simulator; this.engine = engine; - + // Table setColumnSelectionAllowed(false); getSelectionModel().setSelectionMode(ListSelectionModel.SINGLE_SELECTION); @@ -68,49 +70,52 @@ public class GUISimulatorPathTable extends GUIGroupedTable loopIndicator.setFixedCellHeight(getRowHeight()); loopIndicator.setCellRenderer(new LoopIndicatorRenderer(this)); } - - /** Override set font to set row height(s) */ - public void setFont(Font font) - { + + /** Override set font to set row height(s) */ + public void setFont(Font font) + { super.setFont(font); - setRowHeight(getFontMetrics(font).getHeight() + 4); - if (loopIndicator != null) loopIndicator.setFixedCellHeight(getRowHeight()); - } - + setRowHeight(getFontMetrics(font).getHeight() + 4); + if (loopIndicator != null) + loopIndicator.setFixedCellHeight(getRowHeight()); + } + public boolean usingChangeRenderer() { - return ((PathChangeTableRenderer)getDefaultRenderer(Object.class)).onlyShowChange(); + return ((PathChangeTableRenderer) getDefaultRenderer(Object.class)).onlyShowChange(); } - + public void switchToChangeRenderer() { setDefaultRenderer(Object.class, new PathChangeTableRenderer(true)); repaint(); } - + public void switchToBoringRenderer() { setDefaultRenderer(Object.class, new PathChangeTableRenderer(false)); repaint(); } - + public void paintComponent(Graphics g) { super.paintComponent(g); - loopIndicatorModel.updateIndicator(); + loopIndicatorModel.updateIndicator(); } - + public Component getPathLoopIndicator() { return loopIndicator; } - - // Cell renderer for list representing loop indicator (left of path table) - + + // Cell renderer for list representing loop indicator (left of path table) + class LoopIndicatorRenderer extends JPanel implements ListCellRenderer { + private static final long serialVersionUID = 1L; + boolean startLoop, midLoop, endLoop; - + LoopIndicatorRenderer(JTable table) { /*JTableHeader header = table.getTableHeader(); @@ -121,171 +126,147 @@ public class GUISimulatorPathTable extends GUIGroupedTable setBackground(header.getBackground()); setFont(header.getFont());*/ } - + public Component getListCellRendererComponent(JList list, Object value, int index, boolean isSelected, boolean cellHasFocus) { //setText((value == null) ? "" : value.toString()); //setBorder(new LineBorder(Color.black, 1)); - if(ptm.isPathLooping()) - { - if(index == ptm.getLoopEnd() && index == ptm.getLoopStart()) - { + if (ptm.isPathLooping()) { + if (index == ptm.getLoopEnd() && index == ptm.getLoopStart()) { startLoop = true; endLoop = true; midLoop = false; - } - else if(index == ptm.getLoopEnd()) - { + } else if (index == ptm.getLoopEnd()) { startLoop = false; midLoop = false; endLoop = true; - } - else if(index == ptm.getLoopStart()) - { + } else if (index == ptm.getLoopStart()) { startLoop = true; midLoop = false; endLoop = false; - } - else if(index > ptm.getLoopStart() && index < ptm.getLoopEnd()) - { + } else if (index > ptm.getLoopStart() && index < ptm.getLoopEnd()) { startLoop = false; midLoop = true; endLoop = false; - } - else - { + } else { startLoop = false; midLoop = false; endLoop = false; } - } - else - { + } else { startLoop = false; midLoop = false; endLoop = false; } - + return this; } - + public void paintComponent(Graphics g) { Graphics2D g2 = (Graphics2D) g; g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON); - + g2.setColor(getBackground()); - g2.fillRect(0,0,getWidth(), getHeight()); - - if (!ptm.isDisplayPathLoops()) return; - + g2.fillRect(0, 0, getWidth(), getHeight()); + + if (!simulator.isDisplayPathLoops()) + return; + g2.setColor(Color.black); - if(startLoop && endLoop) - { + if (startLoop && endLoop) { GeneralPath gp = new GeneralPath(); - gp.moveTo(getWidth(), (getHeight()/2)+5); - gp.lineTo((getWidth()/2)+5, (getHeight()/2)+5); - gp.quadTo(getWidth()/2, (getHeight()/2)+5, getWidth()/2, (getHeight()/2)); - gp.quadTo(getWidth()/2, (getHeight()/2)-5, (getWidth()/2)+5, (getHeight()/2)-5); - gp.lineTo((getWidth()), (getHeight()/2)-5); + gp.moveTo(getWidth(), (getHeight() / 2) + 5); + gp.lineTo((getWidth() / 2) + 5, (getHeight() / 2) + 5); + gp.quadTo(getWidth() / 2, (getHeight() / 2) + 5, getWidth() / 2, (getHeight() / 2)); + gp.quadTo(getWidth() / 2, (getHeight() / 2) - 5, (getWidth() / 2) + 5, (getHeight() / 2) - 5); + gp.lineTo((getWidth()), (getHeight() / 2) - 5); g2.draw(gp); gp = new GeneralPath(); - gp.moveTo(getWidth(), (getHeight()/2)-5); - gp.lineTo(getWidth()-5, (getHeight()/2) - 8); - gp.lineTo(getWidth()-5, (getHeight()/2) - 2); + gp.moveTo(getWidth(), (getHeight() / 2) - 5); + gp.lineTo(getWidth() - 5, (getHeight() / 2) - 8); + gp.lineTo(getWidth() - 5, (getHeight() / 2) - 2); gp.closePath(); g2.fill(gp); - } - else if(startLoop) - { + } else if (startLoop) { GeneralPath gp = new GeneralPath(); - gp.moveTo(getWidth(), getHeight()/2); - gp.lineTo((getWidth()/2)+5, getHeight()/2); - gp.quadTo(getWidth()/2, getHeight()/2, getWidth()/2, (getHeight()/2)+5); - gp.lineTo(getWidth()/2, getHeight()); + gp.moveTo(getWidth(), getHeight() / 2); + gp.lineTo((getWidth() / 2) + 5, getHeight() / 2); + gp.quadTo(getWidth() / 2, getHeight() / 2, getWidth() / 2, (getHeight() / 2) + 5); + gp.lineTo(getWidth() / 2, getHeight()); g2.draw(gp); gp = new GeneralPath(); - gp.moveTo(getWidth(), getHeight()/2); - gp.lineTo(getWidth()-5, (getHeight()/2) - 3); - gp.lineTo(getWidth()-5, (getHeight()/2) + 3); + gp.moveTo(getWidth(), getHeight() / 2); + gp.lineTo(getWidth() - 5, (getHeight() / 2) - 3); + gp.lineTo(getWidth() - 5, (getHeight() / 2) + 3); gp.closePath(); g2.fill(gp); - } - else if(midLoop) - { - g2.drawLine(getWidth()/2, 0, getWidth()/2, getHeight()); - } - else if(endLoop) - { + } else if (midLoop) { + g2.drawLine(getWidth() / 2, 0, getWidth() / 2, getHeight()); + } else if (endLoop) { GeneralPath gp = new GeneralPath(); - gp.moveTo(getWidth(), getHeight()/2); - gp.lineTo((getWidth()/2)+5, getHeight()/2); - gp.quadTo(getWidth()/2, getHeight()/2, getWidth()/2, (getHeight()/2)-5); - gp.lineTo(getWidth()/2, 0); + gp.moveTo(getWidth(), getHeight() / 2); + gp.lineTo((getWidth() / 2) + 5, getHeight() / 2); + gp.quadTo(getWidth() / 2, getHeight() / 2, getWidth() / 2, (getHeight() / 2) - 5); + gp.lineTo(getWidth() / 2, 0); g2.draw(gp); } } } - - // Model for list representing loop indicator - + + // Model for list representing loop indicator + class LoopIndicatorListModel extends AbstractListModel { - + private static final long serialVersionUID = 1L; + public Object getElementAt(int index) { return ""; } - + public int getSize() { return ptm.getRowCount(); } - + public void updateIndicator() { fireContentsChanged(this, 0, ptm.getRowCount()); } - - } - + + } + // Renderer for cells in path table - - class PathChangeCellRenderer extends JPanel + + class PathChangeCellRenderer extends JPanel { + private static final long serialVersionUID = 1L; + private PathChangeTableRenderer pctr; - + private Object value; private String stringValue; - + private boolean isSelected; - - private int row; - public PathChangeCellRenderer(PathChangeTableRenderer pctr, Object value, boolean isSelected, int row) + public PathChangeCellRenderer(PathChangeTableRenderer pctr, Object value, boolean isSelected, int row) { super(); this.pctr = pctr; this.value = value; this.isSelected = isSelected; - this.row = row; - - if (value instanceof String) - { - stringValue = (String)value; + + if (value instanceof String) { + stringValue = (String) value; this.setToolTipText("State " + row); - } - else if (value instanceof GUISimulator.ActionValue) - { - GUISimulator.ActionValue actionValue = (GUISimulator.ActionValue)value; - if (actionValue.isActionValueUnknown()) - { + } else if (value instanceof ActionValue) { + ActionValue actionValue = (ActionValue) value; + if (actionValue.isActionValueUnknown()) { // unused: stringValue = "?"; this.setToolTipText("Module name or [action] label for transition from state " + (row - 1) + " to " + (row) + " (not yet known)"); - } - else - { + } else { stringValue = actionValue.getValue(); String tooltip; if (row == 0) { @@ -295,54 +276,44 @@ public class GUISimulatorPathTable extends GUIGroupedTable } this.setToolTipText(tooltip); } - } - else if (value instanceof GUISimulator.TimeValue) - { - GUISimulator.TimeValue timeValue = (GUISimulator.TimeValue)value; - if (timeValue.isTimeValueUnknown()) - { + } else if (value instanceof TimeValue) { + TimeValue timeValue = (TimeValue) value; + if (timeValue.isTimeValueUnknown()) { stringValue = "?"; if (timeValue.isCumulative()) this.setToolTipText("Cumulative time up until entering state " + (row) + " (not yet known)"); else this.setToolTipText("Time spent in state " + (row) + " (not yet known)"); - } - else - { - stringValue = (simulator.formatDouble((Double)timeValue.getValue())); + } else { + stringValue = (simulator.formatDouble((Double) timeValue.getValue())); if (timeValue.isCumulative()) this.setToolTipText("Cumulative time up until entering state " + (row)); else this.setToolTipText("Time spent in state " + (row)); } - } - else if (value instanceof GUISimulator.VariableValue) - { - GUISimulator.VariableValue variableValue = (GUISimulator.VariableValue)value; - stringValue = (variableValue.getValue() instanceof Double) ? (simulator.formatDouble(((Double)variableValue.getValue()))) : variableValue.getValue().toString(); - + } else if (value instanceof VariableValue) { + VariableValue variableValue = (VariableValue) value; + stringValue = (variableValue.getValue() instanceof Double) ? (simulator.formatDouble(((Double) variableValue.getValue()))) : variableValue + .getValue().toString(); + this.setToolTipText("Value of variable \"" + variableValue.getVariable().getName() + "\" in state " + (row)); - } - else if (value instanceof GUISimulator.RewardStructureValue) - { - GUISimulator.RewardStructureValue rewardValue = (GUISimulator.RewardStructureValue)value; + } else if (value instanceof RewardStructureValue) { + RewardStructureValue rewardValue = (RewardStructureValue) value; String rewardName = rewardValue.getRewardStructureColumn().getRewardStructure().getColumnName(); - - if (rewardValue.isRewardValueUnknown()) - { - stringValue = "?"; - + + if (rewardValue.isRewardValueUnknown()) { + stringValue = "?"; + if (rewardValue.getRewardStructureColumn().isCumulativeReward()) this.setToolTipText("Cumulative reward of reward structure " + rewardName + " up until state " + (row) + " (not yet known)"); if (rewardValue.getRewardStructureColumn().isStateReward()) this.setToolTipText("State reward of reward structure " + rewardName + " in state " + (row) + " (not yet known)"); if (rewardValue.getRewardStructureColumn().isTransitionReward()) - this.setToolTipText("Transition reward of reward structure " + rewardName + " from state " + (row) + " to " + (row + 1) + " (not yet known)"); - } - else - { - stringValue = simulator.formatDouble(rewardValue.getRewardValue()); - + this.setToolTipText("Transition reward of reward structure " + rewardName + " from state " + (row) + " to " + (row + 1) + + " (not yet known)"); + } else { + stringValue = simulator.formatDouble(rewardValue.getRewardValue()); + if (rewardValue.getRewardStructureColumn().isCumulativeReward()) this.setToolTipText("Cumulative reward of reward structure " + rewardName + " up until state " + (row)); if (rewardValue.getRewardStructureColumn().isStateReward()) @@ -350,203 +321,202 @@ public class GUISimulatorPathTable extends GUIGroupedTable if (rewardValue.getRewardStructureColumn().isTransitionReward()) this.setToolTipText("Transition reward of reward structure " + rewardName + " from state " + (row) + " to " + (row + 1)); } - + } } - + public void paintComponent(Graphics g) { super.paintComponent(g); - - Rectangle rect; - int width, height, x, y; - - // Get graphics context - Graphics2D g2 = (Graphics2D)g; - // Get some info about the string + + Rectangle rect; + int width, height, x, y; + + // Get graphics context + Graphics2D g2 = (Graphics2D) g; + // Get some info about the string rect = getStringBounds(stringValue, g2); - width = (int)Math.ceil(rect.getWidth()); - height = (int)Math.ceil(rect.getHeight()); - + width = (int) Math.ceil(rect.getWidth()); + height = (int) Math.ceil(rect.getHeight()); + // State index/action - if (value instanceof String || value instanceof GUISimulator.ActionValue) { + if (value instanceof String || value instanceof ActionValue) { // Position (horiz centred, vert centred) - x = (getWidth()/2) - (width/2); - y = (getHeight()/2) + (height/2); - // Write value - g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_OFF); + x = (getWidth() / 2) - (width / 2); + y = (getHeight() / 2) + (height / 2); + // Write value + g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_OFF); g2.setColor(Color.black); g2.drawString(stringValue, x, y); } // Variable value - else if (value instanceof GUISimulator.VariableValue) { - GUISimulator.VariableValue variableValue = (GUISimulator.VariableValue)value; + else if (value instanceof VariableValue) { + VariableValue variableValue = (VariableValue) value; // Position (horiz centred, vert centred) - x = (getWidth()/2) - (width/2); - y = (getHeight()/2) + (height/2); - // Prepare box/colour - RoundRectangle2D.Double rec = new RoundRectangle2D.Double(x-5, 2, width+10, getHeight()-5, 8, 8); + x = (getWidth() / 2) - (width / 2); + y = (getHeight() / 2) + (height / 2); + // Prepare box/colour + RoundRectangle2D.Double rec = new RoundRectangle2D.Double(x - 5, 2, width + 10, getHeight() - 5, 8, 8); Color color = (variableValue.hasChanged()) ? (Color.black) : (Color.lightGray); // "Render changes" view if (pctr.onlyShowChange()) { // Vertical line in background g2.setColor(Color.black); - g2.drawLine(getWidth()/2, 0, getWidth()/2, getHeight()); + g2.drawLine(getWidth() / 2, 0, getWidth() / 2, getHeight()); // Only display box/value if there was a change - if (isSelected || variableValue.hasChanged()) { + if (isSelected || variableValue.hasChanged()) { g2.setColor(Color.white); - g2.fill(rec); - g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON); - g2.setColor(color); + g2.fill(rec); + g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON); + g2.setColor(color); g2.draw(rec); - g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_OFF); + g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_OFF); g2.drawString(stringValue, x, y); } } // "Render all values" view else { // Just display value - g2.setColor(color); - g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_OFF); + g2.setColor(color); + g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_OFF); g2.drawString(stringValue, x, y); } } // Reward value - else if (value instanceof GUISimulator.RewardStructureValue) { - GUISimulator.RewardStructureValue rewardValue = (GUISimulator.RewardStructureValue)value; + else if (value instanceof RewardStructureValue) { + RewardStructureValue rewardValue = (RewardStructureValue) value; // Default case (everything except cumulative for CTMCs) - if (!(ptm.getView().canShowTime() && rewardValue.getRewardStructureColumn().isCumulativeReward())) { + if (!(ptm.canShowTime() && rewardValue.getRewardStructureColumn().isCumulativeReward())) { // Position (horiz centred, vert centred) - x = (getWidth()/2) - (width/2); - y = (getHeight()/2) + (height/2); - // Prepare box/colour - RoundRectangle2D.Double rec = new RoundRectangle2D.Double(x-5, 2, width+10, getHeight()-5, 8, 8); + x = (getWidth() / 2) - (width / 2); + y = (getHeight() / 2) + (height / 2); + // Prepare box/colour + RoundRectangle2D.Double rec = new RoundRectangle2D.Double(x - 5, 2, width + 10, getHeight() - 5, 8, 8); Color color = (rewardValue.hasChanged() || rewardValue.isRewardValueUnknown()) ? (Color.black) : (Color.lightGray); // "Render changes" view if (pctr.onlyShowChange()) { // Vertical line in background g2.setColor(Color.black); - g2.drawLine(getWidth()/2, 0, getWidth()/2, getHeight()); + g2.drawLine(getWidth() / 2, 0, getWidth() / 2, getHeight()); // Only display box/value if there was a change if ((isSelected || rewardValue.hasChanged())) { g2.setColor(Color.white); - g2.fill(rec); - g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON); - g2.setColor(color); + g2.fill(rec); + g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON); + g2.setColor(color); g2.draw(rec); - g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_OFF); + g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_OFF); g2.drawString(stringValue, x, y); } } // "Render all values" view else { // Just display value - g2.setColor(color); - g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_OFF); + g2.setColor(color); + g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_OFF); g2.drawString(stringValue, x, y); } } // For cumulative rewards on CTMCs, we left-align (like for display of time) else { // Position (left aligned, vert centred) - x = 3; - y = (getHeight()/2) + (height/2); - // Write text - g2.setColor(Color.black); + x = 3; + y = (getHeight() / 2) + (height / 2); + // Write text + g2.setColor(Color.black); g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_OFF); g2.drawString(stringValue, x, y); - } + } } // Time value - else if (value instanceof GUISimulator.TimeValue) - { + else if (value instanceof TimeValue) { // Position (left aligned, vert centred) - x = 3; - y = (getHeight()/2) + (height/2); - // Write text - g2.setColor(Color.black); + x = 3; + y = (getHeight() / 2) + (height / 2); + // Write text + g2.setColor(Color.black); g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_OFF); - g2.drawString(stringValue, x, y); + g2.drawString(stringValue, x, y); } } } - + class PathChangeTableRenderer implements TableCellRenderer - { + { private boolean onlyShowChange; - + private Color defaultColor; private Color selectedColor; private Color labelColor; private Color selectedLabelColor; - + public PathChangeTableRenderer(boolean onlyShowChange) { super(); - + this.onlyShowChange = onlyShowChange; - + defaultColor = Color.white; - - selectedColor = new Color(defaultColor.getRed()-20, defaultColor.getGreen()-20, defaultColor.getBlue()); - selectedLabelColor = new Color(selectedColor.getRed()-20, selectedColor.getGreen(), selectedColor.getBlue()-20); - labelColor = new Color(defaultColor.getRed()-50, defaultColor.getGreen(), defaultColor.getBlue()-50); - + + selectedColor = new Color(defaultColor.getRed() - 20, defaultColor.getGreen() - 20, defaultColor.getBlue()); + selectedLabelColor = new Color(selectedColor.getRed() - 20, selectedColor.getGreen(), selectedColor.getBlue() - 20); + labelColor = new Color(defaultColor.getRed() - 50, defaultColor.getGreen(), defaultColor.getBlue() - 50); + } - - public Component getTableCellRendererComponent(JTable table, Object value, - boolean isSelected, boolean hasFocus, int row, int column) - { + + public Component getTableCellRendererComponent(JTable table, Object value, boolean isSelected, boolean hasFocus, int row, int column) + { PathChangeCellRenderer pctr = new PathChangeCellRenderer(this, value, isSelected, row); - + boolean shouldColourRow = ptm.shouldColourRow(row); - + Color backGround = defaultColor; - - if(isSelected && !shouldColourRow) + + if (isSelected && !shouldColourRow) backGround = selectedColor; else if (isSelected && shouldColourRow) backGround = selectedLabelColor; else if (!isSelected && shouldColourRow) backGround = labelColor; - + pctr.setBackground(backGround); - + return pctr; - } - + } - public boolean onlyShowChange() + public boolean onlyShowChange() { return onlyShowChange; - } + } } - + /** Method which computes rectangle bounds of a string for a given Graphics2D object */ public static Rectangle getStringBounds(String s, Graphics2D g2) { // catch special cases... // ...TextLayout constructor crashes with null or zero-length string - if (s == null) return new Rectangle(0, 0); - if (s.length() == 0) return new Rectangle(0, 0); + if (s == null) + return new Rectangle(0, 0); + if (s.length() == 0) + return new Rectangle(0, 0); TextLayout layout = new TextLayout(s, g2.getFont(), g2.getFontRenderContext()); return layout.getOutline(new AffineTransform()).getBounds(); } - + /** Method which computes width of a string for a given Graphics2D object */ public static double getStringWidth(String s, Graphics2D g2) { return getStringBounds(s, g2).getWidth(); } - + /** Method which computes height of a string for a given Graphics2D object */ public static double getStringHeight(String s, Graphics2D g2) { return getStringBounds(s, g2).getHeight(); } - + } diff --git a/prism/src/userinterface/simulator/GUISimulatorPathTableModel.java b/prism/src/userinterface/simulator/GUISimulatorPathTableModel.java new file mode 100644 index 00000000..03ea660d --- /dev/null +++ b/prism/src/userinterface/simulator/GUISimulatorPathTableModel.java @@ -0,0 +1,610 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Andrew Hinton (University of Birmingham) +// * Mark Kattenbelt (University of Oxford, formerly University of Birmingham) +// * Dave Parker (University of Oxford, formerly University of Birmingham) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package userinterface.simulator; + +import java.util.*; +import javax.swing.table.AbstractTableModel; + +import simulator.SimulatorEngine; +import userinterface.simulator.SimulationView.*; +import userinterface.util.GUIGroupedTableModel; +import parser.ast.*; + +public class GUISimulatorPathTableModel extends AbstractTableModel implements GUIGroupedTableModel, Observer +{ + private static final long serialVersionUID = 1L; + + private GUISimulator simulator; + private SimulatorEngine engine; + private SimulationView view; + + private boolean pathActive; + private ModulesFile parsedModel; + + private RewardStructureValue rewardStructureValue; + private VariableValue variableValue; + private TimeValue timeValue; + private ActionValue actionValue; + + public GUISimulatorPathTableModel(GUISimulator simulator, SimulatorEngine engine, SimulationView view) + { + this.simulator = simulator; + this.engine = engine; + this.view = view; + this.view.addObserver(this); + + rewardStructureValue = view.new RewardStructureValue(null, null); + variableValue = view.new VariableValue(null, null); + } + + public void setPathActive(boolean pathActive) + { + this.pathActive = pathActive; + } + + public void setParsedModel(ModulesFile parsedModel) + { + this.parsedModel = parsedModel; + } + + public boolean canShowTime() + { + return parsedModel.getModelType().continuousTime(); + } + + public int getGroupCount() + { + if (!pathActive) { + return 0; + } else { + int groupCount = 0; + + if (view.showActions() || view.showSteps()) { + groupCount++; + } + + if (canShowTime() && (view.showTime() || view.showCumulativeTime())) { + groupCount++; + } + + ArrayList vars = view.getVisibleVariables(); + Set varNames = new HashSet(); + + for (Variable variable : vars) { + varNames.add(variable.getName()); + } + + for (int g = 0; g < parsedModel.getNumGlobals(); g++) { + if (varNames.contains(parsedModel.getGlobal(g).getName())) { + groupCount++; + break; + } + } + + for (int m = 0; m < parsedModel.getNumModules(); m++) { + Module module = parsedModel.getModule(m); + for (int v = 0; v < module.getNumDeclarations(); v++) { + if (varNames.contains(module.getDeclaration(v).getName())) { + groupCount++; + break; + } + } + } + + if (view.getVisibleRewardColumns().size() > 0) { + groupCount++; + } + + return groupCount; + } + } + + public void update(Observable o, Object arg) + { + if (o == view) { + fireTableStructureChanged(); + + //Sort out the minimum widths for each column + simulator.sortOutColumnSizes(); + } + } + + public String getGroupName(int groupIndex) + { + if (!pathActive) { + return ""; + } else { + int groupCount = 0; + + if (view.showActions() || view.showSteps()) { + if (groupCount == groupIndex) { + return "Step"; + } + + groupCount++; + } + + if (canShowTime() && (view.showTime() || view.showCumulativeTime())) { + if (groupCount == groupIndex) { + return "Time"; + } + + groupCount++; + } + + if (view.getVisibleVariables().size() > 0) { + ArrayList vars = view.getVisibleVariables(); + Set varNames = new HashSet(); + + for (Variable variable : vars) { + varNames.add(variable.getName()); + } + + for (int g = 0; g < parsedModel.getNumGlobals(); g++) { + if (varNames.contains(parsedModel.getGlobal(g).getName())) { + if (groupCount == groupIndex) { + return "Globals"; + } + + groupCount++; + break; + } + } + + for (int m = 0; m < parsedModel.getNumModules(); m++) { + Module module = parsedModel.getModule(m); + for (int v = 0; v < module.getNumDeclarations(); v++) { + if (varNames.contains(module.getDeclaration(v).getName())) { + if (groupCount == groupIndex) { + return "" + parsedModel.getModuleName(m) + ""; + } + + groupCount++; + break; + } + } + } + } + + // Add state and transitions rewards for each reward structure. + if (view.getVisibleRewardColumns().size() > 0) { + if (groupCount == groupIndex) { + return "Rewards"; + } + + groupCount++; + } + + return "Undefined Group"; + } + } + + public String getGroupToolTip(int groupIndex) + { + ArrayList vars = view.getVisibleVariables(); + Set varNames = new HashSet(); + + for (Variable variable : vars) { + varNames.add(variable.getName()); + } + + int groupCount = 0; + + if (view.showActions() || view.showSteps()) { + if (groupCount == groupIndex) { + return null; + } + + groupCount++; + } + + if (canShowTime() && (view.showTime() || view.showCumulativeTime())) { + if (groupCount == groupIndex) { + return null; + } + + groupCount++; + } + + for (int g = 0; g < parsedModel.getNumGlobals(); g++) { + if (varNames.contains(parsedModel.getGlobal(g).getName())) { + if (groupCount == groupIndex) { + return "Global variables"; + } + + groupCount++; + break; + } + } + + for (int m = 0; m < parsedModel.getNumModules(); m++) { + Module module = parsedModel.getModule(m); + for (int v = 0; v < module.getNumDeclarations(); v++) { + if (varNames.contains(module.getDeclaration(v).getName())) { + if (groupCount == groupIndex) { + return "Variables of module \"" + parsedModel.getModuleName(m) + "\""; + } + + groupCount++; + break; + } + } + } + + // Add state and transitions rewards for each reward structure. + if (view.getVisibleRewardColumns().size() > 0) { + if (groupCount == groupIndex) { + return "State, transition and cumulative rewards"; + } + + groupCount++; + } + + return null; + } + + public int getLastColumnOfGroup(int groupIndex) + { + int stepStart = 0; + int timeStart = stepStart + (view.showActions() ? 1 : 0) + (view.showSteps() ? 1 : 0); + int varStart = timeStart + (canShowTime() && view.showCumulativeTime() ? 1 : 0) + (canShowTime() && view.showTime() ? 1 : 0); + int rewardStart = varStart + view.getVisibleVariables().size(); + + int groupCount = 0; + + if (view.showActions() || view.showSteps()) { + if (groupCount == groupIndex) { + if (view.showActions() && view.showSteps()) + return stepStart + 1; + else + return stepStart; + } + + groupCount++; + } + + if (canShowTime() && (view.showCumulativeTime() || view.showTime())) { + if (groupCount == groupIndex) { + if (view.showCumulativeTime() && view.showTime()) + return timeStart + 1; + else + return timeStart; + } + + groupCount++; + } + + if (view.getVisibleVariables().size() > 0) { + int visVarCount = 0; + + ArrayList vars = view.getVisibleVariables(); + Set varNames = new HashSet(); + + for (Variable variable : vars) { + varNames.add(variable.getName()); + } + + boolean atLeastOneGlobal = false; + + for (int g = 0; g < parsedModel.getNumGlobals(); g++) { + boolean contained = varNames.contains(parsedModel.getGlobal(g).getName()); + + if (!atLeastOneGlobal && contained) { + atLeastOneGlobal = true; + } + + if (contained) + visVarCount++; + } + + if (atLeastOneGlobal && groupCount == groupIndex) { + return varStart + visVarCount - 1; + } + + if (atLeastOneGlobal) { + groupCount++; + } + + for (int m = 0; m < parsedModel.getNumModules(); m++) { + Module module = parsedModel.getModule(m); + boolean atLeastOne = false; + + for (int v = 0; v < module.getNumDeclarations(); v++) { + boolean contained = varNames.contains(module.getDeclaration(v).getName()); + if (!atLeastOne && contained) { + atLeastOne = true; + } + + if (contained) + visVarCount++; + } + + if (atLeastOne && groupCount == groupIndex) { + return varStart + visVarCount - 1; + } + + if (atLeastOne) { + groupCount++; + } + } + } + + // Add state and transitions rewards for each reward structure. + if (view.getVisibleRewardColumns().size() > 0) { + if (groupCount == groupIndex) { + return rewardStart + view.getVisibleRewardColumns().size() - 1; + } + + groupCount++; + } + + return 0; + } + + /** + * Returns the number of columns. + * @see javax.swing.table.TableModel#getColumnCount() + */ + public int getColumnCount() + { + if (!pathActive) { + return 0; + } else { + int colCount = 0; + + colCount += (view.showActions() ? 1 : 0); + colCount += (view.showSteps() ? 1 : 0); + colCount += (canShowTime() && view.showCumulativeTime() ? 1 : 0) + (canShowTime() && view.showTime() ? 1 : 0); + colCount += view.getVisibleVariables().size(); + colCount += view.getVisibleRewardColumns().size(); + + return colCount; + } + } + + /** + * Returns the number of rows. + * @see javax.swing.table.TableModel#getRowCount() + */ + public int getRowCount() + { + // Return current path size if there is an active path. + return (pathActive ? engine.getPathSize() + 1 : 0); + } + + public boolean shouldColourRow(int row) + { + int selection = simulator.getStateLabelList().getSelectedIndex(); + if (selection != -1) { + GUISimLabelList.SimLabel label = (GUISimLabelList.SimLabel) simulator.getStateLabelList().getModel().getElementAt(selection); + if (row == getRowCount() - 1) { + if (label.getResult() == 1) + return true; + } else { + if (label.getResult(row) == 1) + return true; + } + } + + return false; + } + + public String getColumnName(int columnIndex) + { + if (pathActive) { + int actionStart = 0; + int stepStart = actionStart + (view.showActions() ? 1 : 0); + int cumulativeTimeStart = stepStart + (view.showSteps() ? 1 : 0); + int timeStart = cumulativeTimeStart + (canShowTime() && view.showCumulativeTime() ? 1 : 0); + int varStart = timeStart + (canShowTime() && view.showTime() ? 1 : 0); + int rewardStart = varStart + view.getVisibleVariables().size(); + + // The step column + if (actionStart <= columnIndex && columnIndex < stepStart) { + return "Action"; + } else if (stepStart <= columnIndex && columnIndex < cumulativeTimeStart) { + return "#"; + } else if (cumulativeTimeStart <= columnIndex && columnIndex < timeStart) { + return "Time (+)"; + } else if (timeStart <= columnIndex && columnIndex < varStart) { + return "Time"; + } + // A variable column + else if (varStart <= columnIndex && columnIndex < rewardStart) { + return ((Variable) view.getVisibleVariables().get(columnIndex - varStart)).toString(); + } + + else if (rewardStart <= columnIndex) { + return ((RewardStructureColumn) view.getVisibleRewardColumns().get(columnIndex - rewardStart)).getColumnName(); + } + } + return "Undefined Column"; + } + + public String getColumnToolTip(int columnIndex) + { + if (pathActive) { + int actionStart = 0; + int stepStart = actionStart + (view.showActions() ? 1 : 0); + int cumulativeTimeStart = stepStart + (view.showSteps() ? 1 : 0); + int timeStart = cumulativeTimeStart + (canShowTime() && view.showCumulativeTime() ? 1 : 0); + int varStart = timeStart + (canShowTime() && view.showTime() ? 1 : 0); + int rewardStart = varStart + view.getVisibleVariables().size(); + + // The step column + if (actionStart <= columnIndex && columnIndex < stepStart) { + return "Module name or [action] label"; + } else if (stepStart <= columnIndex && columnIndex < cumulativeTimeStart) { + return "Index of state in path"; + } else if (cumulativeTimeStart <= columnIndex && columnIndex < timeStart) { + return "Cumulative time"; + } else if (timeStart <= columnIndex && columnIndex < varStart) { + return "Time spent in state"; + } + // A variable column + else if (varStart <= columnIndex && columnIndex < rewardStart) { + return "Values of variable \"" + ((Variable) view.getVisibleVariables().get(columnIndex - varStart)).toString() + "\""; + } + + else if (rewardStart <= columnIndex) { + RewardStructureColumn column = ((RewardStructureColumn) view.getVisibleRewardColumns().get(columnIndex - rewardStart)); + String rewardName = column.getRewardStructure().getColumnName(); + + if (column.isStateReward()) + return "State reward of reward structure " + rewardName; + if (column.isTransitionReward()) + return "Transition reward of reward structure " + rewardName; + if (column.isCumulativeReward()) + return "Cumulative reward of reward structure " + rewardName; + } + } + return "Undefined Column"; + } + + public Object getValueAt(int rowIndex, int columnIndex) + { + if (pathActive) { + int actionStart = 0; + int stepStart = actionStart + (view.showActions() ? 1 : 0); + int cumulativeTimeStart = stepStart + (view.showSteps() ? 1 : 0); + int timeStart = cumulativeTimeStart + (canShowTime() && view.showCumulativeTime() ? 1 : 0); + int varStart = timeStart + (canShowTime() && view.showTime() ? 1 : 0); + int rewardStart = varStart + view.getVisibleVariables().size(); + + // The action column + if (actionStart <= columnIndex && columnIndex < stepStart) { + actionValue = view.new ActionValue(rowIndex == 0 ? "" : engine.getModuleOrActionOfPathStep(rowIndex - 1)); + actionValue.setActionValueUnknown(false); + return actionValue; + } + // The step column + else if (stepStart <= columnIndex && columnIndex < cumulativeTimeStart) { + return "" + rowIndex; + } + // Cumulative time column + else if (cumulativeTimeStart <= columnIndex && columnIndex < timeStart) { + timeValue = view.new TimeValue(engine.getCumulativeTimeUpToPathStep(rowIndex), true); + timeValue.setTimeValueUnknown(rowIndex > engine.getPathSize()); // 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()); + 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()); + variableValue.setVariable(var); + variableValue.setValue(result); + variableValue.setChanged(rowIndex == 0 || !engine.getVariableValueOfPathStep(rowIndex - 1, var.getIndex()).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.getStateRewardOfPathStep(rowIndex, rewardColumn.getRewardStructure().getIndex()); + rewardStructureValue.setChanged(rowIndex == 0 + || value != engine.getStateRewardOfPathStep(rowIndex - 1, rewardColumn.getRewardStructure().getIndex())); + rewardStructureValue.setRewardValue(new Double(value)); + rewardStructureValue.setRewardValueUnknown(rowIndex > engine.getPathSize()); // Never unknown + } + // A transition reward column + else if (rewardColumn.isTransitionReward()) { + double value = engine.getTransitionRewardOfPathStep(rowIndex, rewardColumn.getRewardStructure().getIndex()); + rewardStructureValue.setChanged(rowIndex == 0 + || value != engine.getTransitionRewardOfPathStep(rowIndex - 1, rewardColumn.getRewardStructure().getIndex())); + rewardStructureValue.setRewardValue(new Double(value)); + rewardStructureValue.setRewardValueUnknown(rowIndex >= engine.getPathSize()); + } + // A cumulative reward column + else { + double value = engine.getCumulativeRewardUpToPathStep(rowIndex, rewardColumn.getRewardStructure().getIndex()); + rewardStructureValue.setChanged(rowIndex == 0 + || value != (engine.getCumulativeRewardUpToPathStep(rowIndex - 1, rewardColumn.getRewardStructure().getIndex()))); + rewardStructureValue.setRewardValue(new Double(value)); + rewardStructureValue.setRewardValueUnknown(rowIndex > engine.getPathSize()); // Never unknown + } + return rewardStructureValue; + } + } + + return "Undefined value"; + } + + /** + * Method is called when a new path is created. + * The structure of the path may be for a different model etc. + */ + public void restartPathTable() + { + view.refreshToDefaultView(engine, pathActive, parsedModel); + } + + /** + * Method is called whenever a path is modified. + */ + public void updatePathTable() + { + fireTableDataChanged(); + } + + public boolean isPathLooping() + { + return engine.isPathLooping(); + } + + public int getLoopStart() + { + return engine.loopStart(); + } + + public int getLoopEnd() + { + return engine.loopEnd(); + } + + public SimulationView getView() + { + return view; + } + + public void setView(SimulationView view) + { + this.view.deleteObserver(this); + this.view = view; + this.view.addObserver(this); + } +} diff --git a/prism/src/userinterface/simulator/GUITimeDialog.java b/prism/src/userinterface/simulator/GUITimeDialog.java index 83eabd7b..79632d40 100644 --- a/prism/src/userinterface/simulator/GUITimeDialog.java +++ b/prism/src/userinterface/simulator/GUITimeDialog.java @@ -34,186 +34,192 @@ import javax.swing.event.DocumentListener; import userinterface.*; public class GUITimeDialog extends JDialog -{ +{ + private static final long serialVersionUID = 1L; + //ATTRIBUTES - private Action okAction; - private Action cancelAction; - - private GUIPrism gui; - private GUISimulator.PathTableModel pathTableModel; - - private GUISimulator.SimulationView view; private double time; private boolean cancelled; - + private static double lastTime = 1.0d; - - // Variables declaration - do not modify//GEN-BEGIN:variables - private javax.swing.JPanel allPanel; - private javax.swing.JPanel bottomPanel; - private javax.swing.JPanel buttonPanel; - private javax.swing.JButton cancelButton; - private javax.swing.JLabel inputLabel; - private javax.swing.JButton okayButton; - private javax.swing.JTextField timeInputField; - private javax.swing.JPanel timeInputPanel; - private javax.swing.JPanel topPanel; - private javax.swing.JLabel warningLabel; - // End of variables declaration//GEN-END:variables - + + // Variables declaration - do not modify//GEN-BEGIN:variables + private javax.swing.JPanel allPanel; + private javax.swing.JPanel bottomPanel; + private javax.swing.JPanel buttonPanel; + private javax.swing.JButton cancelButton; + private javax.swing.JLabel inputLabel; + private javax.swing.JButton okayButton; + private javax.swing.JTextField timeInputField; + private javax.swing.JPanel timeInputPanel; + private javax.swing.JPanel topPanel; + private javax.swing.JLabel warningLabel; + + // End of variables declaration//GEN-END:variables + /** Creates new form GUIConstantsPicker */ private GUITimeDialog(GUIPrism parent, GUISimulator simulator) { super(parent, "Provide a time", true); - + //initialise initComponents(); - + this.getRootPane().setDefaultButton(okayButton); - + this.time = lastTime; this.cancelled = false; - + this.timeInputField.setText("" + time); - - this.warningLabel.setIcon(GUIPrism.getIconFromImage("smallError.png")); + + this.warningLabel.setIcon(GUIPrism.getIconFromImage("smallError.png")); this.warningLabel.setVisible(false); - + this.timeInputField.getDocument().addDocumentListener(new DocumentListener() - { - public void changedUpdate(DocumentEvent e) + { + public void changedUpdate(DocumentEvent e) { - try - { - Double d = Double.parseDouble(timeInputField.getText()); + try { + Double.parseDouble(timeInputField.getText()); GUITimeDialog.this.warningLabel.setVisible(false); GUITimeDialog.this.okayButton.setEnabled(true); - } - catch (NumberFormatException nfe) - { + } catch (NumberFormatException nfe) { GUITimeDialog.this.warningLabel.setVisible(true); GUITimeDialog.this.okayButton.setEnabled(false); - } + } + } + + public void removeUpdate(DocumentEvent e) + { + changedUpdate(e); + } + + public void insertUpdate(DocumentEvent e) + { + changedUpdate(e); } - - public void removeUpdate(DocumentEvent e) {changedUpdate(e);} - public void insertUpdate(DocumentEvent e) {changedUpdate(e);} }); - + super.setBounds(new Rectangle(550, 300)); setResizable(true); setLocationRelativeTo(getParent()); // centre - + this.setVisible(true); } - + /** This method is called from within the constructor to * initialize the form. * WARNING: Do NOT modify this code. The content of this method is * always regenerated by the Form Editor. */ - // //GEN-BEGIN:initComponents - private void initComponents() { - allPanel = new javax.swing.JPanel(); - bottomPanel = new javax.swing.JPanel(); - warningLabel = new javax.swing.JLabel(); - buttonPanel = new javax.swing.JPanel(); - okayButton = new javax.swing.JButton(); - cancelButton = new javax.swing.JButton(); - topPanel = new javax.swing.JPanel(); - timeInputPanel = new javax.swing.JPanel(); - inputLabel = new javax.swing.JLabel(); - timeInputField = new javax.swing.JTextField(); - - addWindowListener(new java.awt.event.WindowAdapter() { - public void windowClosing(java.awt.event.WindowEvent evt) { - closeDialog(evt); - } - }); + // //GEN-BEGIN:initComponents + private void initComponents() + { + allPanel = new javax.swing.JPanel(); + bottomPanel = new javax.swing.JPanel(); + warningLabel = new javax.swing.JLabel(); + buttonPanel = new javax.swing.JPanel(); + okayButton = new javax.swing.JButton(); + cancelButton = new javax.swing.JButton(); + topPanel = new javax.swing.JPanel(); + timeInputPanel = new javax.swing.JPanel(); + inputLabel = new javax.swing.JLabel(); + timeInputField = new javax.swing.JTextField(); + + addWindowListener(new java.awt.event.WindowAdapter() + { + public void windowClosing(java.awt.event.WindowEvent evt) + { + closeDialog(evt); + } + }); - allPanel.setLayout(new java.awt.BorderLayout()); + allPanel.setLayout(new java.awt.BorderLayout()); - allPanel.setBorder(javax.swing.BorderFactory.createEmptyBorder(5, 5, 5, 5)); - bottomPanel.setLayout(new java.awt.BorderLayout()); + allPanel.setBorder(javax.swing.BorderFactory.createEmptyBorder(5, 5, 5, 5)); + bottomPanel.setLayout(new java.awt.BorderLayout()); - warningLabel.setText("Please enter a valid positive double"); - warningLabel.setBorder(javax.swing.BorderFactory.createEmptyBorder(0, 5, 0, 0)); - bottomPanel.add(warningLabel, java.awt.BorderLayout.CENTER); + warningLabel.setText("Please enter a valid positive double"); + warningLabel.setBorder(javax.swing.BorderFactory.createEmptyBorder(0, 5, 0, 0)); + bottomPanel.add(warningLabel, java.awt.BorderLayout.CENTER); - buttonPanel.setLayout(new java.awt.FlowLayout(java.awt.FlowLayout.RIGHT)); + buttonPanel.setLayout(new java.awt.FlowLayout(java.awt.FlowLayout.RIGHT)); - okayButton.setText("Okay"); - okayButton.addActionListener(new java.awt.event.ActionListener() { - public void actionPerformed(java.awt.event.ActionEvent evt) { - okayButtonActionPerformed(evt); - } - }); + okayButton.setText("Okay"); + okayButton.addActionListener(new java.awt.event.ActionListener() + { + public void actionPerformed(java.awt.event.ActionEvent evt) + { + okayButtonActionPerformed(evt); + } + }); - buttonPanel.add(okayButton); + buttonPanel.add(okayButton); - cancelButton.setText("Cancel"); - cancelButton.addActionListener(new java.awt.event.ActionListener() { - public void actionPerformed(java.awt.event.ActionEvent evt) { - cancelButtonActionPerformed(evt); - } - }); + cancelButton.setText("Cancel"); + cancelButton.addActionListener(new java.awt.event.ActionListener() + { + public void actionPerformed(java.awt.event.ActionEvent evt) + { + cancelButtonActionPerformed(evt); + } + }); - buttonPanel.add(cancelButton); + buttonPanel.add(cancelButton); - bottomPanel.add(buttonPanel, java.awt.BorderLayout.EAST); + bottomPanel.add(buttonPanel, java.awt.BorderLayout.EAST); - allPanel.add(bottomPanel, java.awt.BorderLayout.SOUTH); + allPanel.add(bottomPanel, java.awt.BorderLayout.SOUTH); - topPanel.setLayout(new java.awt.BorderLayout()); + topPanel.setLayout(new java.awt.BorderLayout()); - topPanel.setBorder(javax.swing.BorderFactory.createTitledBorder("Time spent in state")); - timeInputPanel.setLayout(new java.awt.GridLayout(1, 2, 5, 5)); + topPanel.setBorder(javax.swing.BorderFactory.createTitledBorder("Time spent in state")); + timeInputPanel.setLayout(new java.awt.GridLayout(1, 2, 5, 5)); - timeInputPanel.setBorder(javax.swing.BorderFactory.createEmptyBorder(5, 5, 5, 5)); - inputLabel.setText("Provide a time:"); - timeInputPanel.add(inputLabel); + timeInputPanel.setBorder(javax.swing.BorderFactory.createEmptyBorder(5, 5, 5, 5)); + inputLabel.setText("Provide a time:"); + timeInputPanel.add(inputLabel); - timeInputField.setText("1.0"); - timeInputPanel.add(timeInputField); + timeInputField.setText("1.0"); + timeInputPanel.add(timeInputField); - topPanel.add(timeInputPanel, java.awt.BorderLayout.NORTH); + topPanel.add(timeInputPanel, java.awt.BorderLayout.NORTH); - allPanel.add(topPanel, java.awt.BorderLayout.CENTER); + allPanel.add(topPanel, java.awt.BorderLayout.CENTER); - getContentPane().add(allPanel, java.awt.BorderLayout.CENTER); + getContentPane().add(allPanel, java.awt.BorderLayout.CENTER); - }// //GEN-END:initComponents + }// //GEN-END:initComponents private void okayButtonActionPerformed(java.awt.event.ActionEvent evt)//GEN-FIRST:event_okayButtonActionPerformed {//GEN-HEADEREND:event_okayButtonActionPerformed - try - { time = Double.parseDouble(timeInputField.getText()); } - catch (NumberFormatException nfe) - { // Shouldn't happen. + try { + time = Double.parseDouble(timeInputField.getText()); + } catch (NumberFormatException nfe) { // Shouldn't happen. cancelled = true; } dispose(); }//GEN-LAST:event_okayButtonActionPerformed - + private void cancelButtonActionPerformed(java.awt.event.ActionEvent evt)//GEN-FIRST:event_cancelButtonActionPerformed {//GEN-HEADEREND:event_cancelButtonActionPerformed cancelled = true; dispose(); }//GEN-LAST:event_cancelButtonActionPerformed - + /** Closes the dialog */ private void closeDialog(java.awt.event.WindowEvent evt)//GEN-FIRST:event_closeDialog { setVisible(false); dispose(); }//GEN-LAST:event_closeDialog - - public boolean isCancelled() + + public boolean isCancelled() { return cancelled; } - public double getTime() + public double getTime() { return time; } @@ -222,17 +228,12 @@ public class GUITimeDialog extends JDialog public static double askTime(GUIPrism prism, GUISimulator simulator) { GUITimeDialog dialog = new GUITimeDialog(prism, simulator); - - if (dialog.isCancelled()) - { + + if (dialog.isCancelled()) { return -1; - } - else - { - GUITimeDialog.lastTime = dialog.time; - return dialog.time; + } else { + GUITimeDialog.lastTime = dialog.time; + return dialog.time; } } } - - diff --git a/prism/src/userinterface/simulator/GUIViewDialog.java b/prism/src/userinterface/simulator/GUIViewDialog.java index 7e759f46..d67199dc 100644 --- a/prism/src/userinterface/simulator/GUIViewDialog.java +++ b/prism/src/userinterface/simulator/GUIViewDialog.java @@ -34,665 +34,673 @@ import java.awt.*; import java.util.*; import java.awt.event.*; import userinterface.*; -import userinterface.simulator.GUISimulator.RewardStructure; +import userinterface.simulator.SimulationView.*; public class GUIViewDialog extends JDialog implements KeyListener -{ +{ + private static final long serialVersionUID = 1L; + //ATTRIBUTES - private boolean cancelled = true; private boolean askOption; - - private Action okAction; - private Action cancelAction; - + private GUIPrism gui; - private GUISimulator.PathTableModel pathTableModel; - - private GUISimulator.SimulationView view; - + + private SimulationView view; + private VariableListModel visibleVariableListModel; private VariableListModel hiddenVariableListModel; private RewardListModel visibleRewardListModel; private RewardListModel hiddenRewardListModel; - - // Variables declaration - do not modify//GEN-BEGIN:variables - private javax.swing.JPanel allPanel; - private javax.swing.JPanel bottomPanel; - private javax.swing.JPanel boxPanel; - private javax.swing.JPanel buttonPanel; - private javax.swing.JButton cancelButton; - private javax.swing.JPanel centerRewardColumn; - private javax.swing.JPanel centerRewardPanel; - private javax.swing.JPanel centerVariableColumn; - private javax.swing.JPanel centerVariablePanel; - private javax.swing.JRadioButton changeRenderingButton; - private javax.swing.JLabel hiddenLabel; - private javax.swing.JList hiddenRewardList; - private javax.swing.JScrollPane hiddenRewardScrollList; - private javax.swing.JList hiddenVariableList; - private javax.swing.JScrollPane hiddenVariableScrollList; - private javax.swing.JPanel innerPathStylePanel; - private javax.swing.JPanel innerTimePanel; - private javax.swing.JPanel leftRewardColumn; - private javax.swing.JPanel leftRewardPanel; - private javax.swing.JPanel leftVariableColumn; - private javax.swing.JPanel leftVariablePanel; - private javax.swing.JButton makeRewardHiddenButton; - private javax.swing.JButton makeRewardVisibleButton; - private javax.swing.JButton makeVariableHiddenButton; - private javax.swing.JButton makeVariableVisibleButton; - private javax.swing.JButton okayButton; - private javax.swing.JCheckBox optionCheckBox; - private javax.swing.JPanel otherTabPanel; - private javax.swing.ButtonGroup pathStyle; - private javax.swing.JPanel pathStylePanel; - private javax.swing.JRadioButton renderAllButton; - private javax.swing.JPanel rewardPanel; - private javax.swing.JPanel rewardTabPanel; - private javax.swing.JPanel rightRewardColumn; - private javax.swing.JPanel rightRewardPanel; - private javax.swing.JPanel rightVariableColumn; - private javax.swing.JPanel rightVariablePanel; - private javax.swing.JButton selectAllHiddenRewardsButton; - private javax.swing.JButton selectAllHiddenVariablesButton; - private javax.swing.JButton selectAllVisibleRewardsButton; - private javax.swing.JButton selectAllVisibleVariablesButton; - private javax.swing.JCheckBox showCumulativeTimeCheckBox; - private javax.swing.JCheckBox showTimeCheckBox; - private javax.swing.JPanel topInnerTimePanel; - private javax.swing.JPanel variablePanel; - private javax.swing.JTabbedPane variableTabPane; - private javax.swing.JPanel variableTabPanel; - private javax.swing.JLabel visibleLabel; - private javax.swing.JList visibleRewardList; - private javax.swing.JScrollPane visibleRewardScrollList; - private javax.swing.JList visibleVariableList; - private javax.swing.JScrollPane visibleVariableScrollList; - // End of variables declaration//GEN-END:variables - - /** Creates new form GUIConstantsPicker */ - public GUIViewDialog(GUIPrism parent, GUISimulator.SimulationView view) + + // Variables declaration - do not modify//GEN-BEGIN:variables + private javax.swing.JPanel allPanel; + private javax.swing.JPanel bottomPanel; + private javax.swing.JPanel boxPanel; + private javax.swing.JPanel buttonPanel; + private javax.swing.JButton cancelButton; + private javax.swing.JPanel centerRewardColumn; + private javax.swing.JPanel centerRewardPanel; + private javax.swing.JPanel centerVariableColumn; + private javax.swing.JPanel centerVariablePanel; + private javax.swing.JRadioButton changeRenderingButton; + private javax.swing.JLabel hiddenLabel; + private javax.swing.JList hiddenRewardList; + private javax.swing.JScrollPane hiddenRewardScrollList; + private javax.swing.JList hiddenVariableList; + private javax.swing.JScrollPane hiddenVariableScrollList; + private javax.swing.JPanel innerPathStylePanel; + private javax.swing.JPanel innerTimePanel; + private javax.swing.JPanel leftRewardColumn; + private javax.swing.JPanel leftRewardPanel; + private javax.swing.JPanel leftVariableColumn; + private javax.swing.JPanel leftVariablePanel; + private javax.swing.JButton makeRewardHiddenButton; + private javax.swing.JButton makeRewardVisibleButton; + private javax.swing.JButton makeVariableHiddenButton; + private javax.swing.JButton makeVariableVisibleButton; + private javax.swing.JButton okayButton; + private javax.swing.JCheckBox optionCheckBox; + private javax.swing.JPanel otherTabPanel; + private javax.swing.ButtonGroup pathStyle; + private javax.swing.JPanel pathStylePanel; + private javax.swing.JRadioButton renderAllButton; + private javax.swing.JPanel rewardPanel; + private javax.swing.JPanel rewardTabPanel; + private javax.swing.JPanel rightRewardColumn; + private javax.swing.JPanel rightRewardPanel; + private javax.swing.JPanel rightVariableColumn; + private javax.swing.JPanel rightVariablePanel; + private javax.swing.JButton selectAllHiddenRewardsButton; + private javax.swing.JButton selectAllHiddenVariablesButton; + private javax.swing.JButton selectAllVisibleRewardsButton; + private javax.swing.JButton selectAllVisibleVariablesButton; + private javax.swing.JCheckBox showCumulativeTimeCheckBox; + private javax.swing.JCheckBox showTimeCheckBox; + private javax.swing.JPanel topInnerTimePanel; + private javax.swing.JPanel variablePanel; + private javax.swing.JTabbedPane variableTabPane; + private javax.swing.JPanel variableTabPanel; + private javax.swing.JLabel visibleLabel; + private javax.swing.JList visibleRewardList; + private javax.swing.JScrollPane visibleRewardScrollList; + private javax.swing.JList visibleVariableList; + private javax.swing.JScrollPane visibleVariableScrollList; + + // End of variables declaration//GEN-END:variables + + /** + * Creates new form GUIViewDialog + */ + public GUIViewDialog(GUIPrism parent, SimulationView view, GUISimulatorPathTableModel pathTableModel) { super(parent, "Configure View for Simulation", true); - + this.gui = parent; this.view = view; - + //initialise initComponents(); - + this.getRootPane().setDefaultButton(okayButton); - + super.setBounds(new Rectangle(550, 300)); setResizable(true); setLocationRelativeTo(getParent()); // centre - - this.askOption = ((GUIPrism)this.getParent()).getPrism().getSettings().getBoolean(PrismSettings.SIMULATOR_NEW_PATH_ASK_VIEW); + + this.askOption = ((GUIPrism) this.getParent()).getPrism().getSettings().getBoolean(PrismSettings.SIMULATOR_NEW_PATH_ASK_VIEW); optionCheckBox.setSelected(this.askOption); - + showTimeCheckBox.setSelected(view.showTime()); - showCumulativeTimeCheckBox.setSelected(view.showCumulativeTime()); - + showCumulativeTimeCheckBox.setSelected(view.showCumulativeTime()); + visibleVariableListModel = new VariableListModel(view.getVisibleVariables()); hiddenVariableListModel = new VariableListModel(view.getHiddenVariables()); - + visibleVariableList.setModel(visibleVariableListModel); - hiddenVariableList.setModel(hiddenVariableListModel); - - ArrayList visibleRewardColumn = new ArrayList(); - ArrayList hiddenRewardColumn = new ArrayList(); - - for (Object obj : view.getRewards()) - { - GUISimulator.RewardStructure reward = (GUISimulator.RewardStructure)obj; - + hiddenVariableList.setModel(hiddenVariableListModel); + + ArrayList visibleRewardColumn = new ArrayList(); + ArrayList hiddenRewardColumn = new ArrayList(); + + for (RewardStructure reward : view.getRewards()) { hiddenRewardColumn.add(new RewardListItem(reward, false)); hiddenRewardColumn.add(new RewardListItem(reward, true)); } - - for (Object obj1 : view.getVisibleRewardColumns()) - { - GUISimulator.RewardStructureColumn rewardColumn = (GUISimulator.RewardStructureColumn)obj1; - - for (Object obj2 : hiddenRewardColumn) - { - RewardListItem rewardListItem = (RewardListItem)obj2; - - if (rewardColumn.getRewardStructure().equals(rewardListItem.getRewardStructure()) && rewardColumn.isCumulativeReward() == rewardListItem.isCumulative()) - { - visibleRewardColumn.add(obj2); - hiddenRewardColumn.remove(obj2); - + + for (RewardStructureColumn rewardColumn : view.getVisibleRewardColumns()) { + for (RewardListItem rewardListItem : hiddenRewardColumn) { + if (rewardColumn.getRewardStructure().equals(rewardListItem.getRewardStructure()) + && rewardColumn.isCumulativeReward() == rewardListItem.isCumulative()) { + visibleRewardColumn.add(rewardListItem); + hiddenRewardColumn.remove(rewardListItem); + break; } - } + } } - + visibleRewardListModel = new RewardListModel(visibleRewardColumn); hiddenRewardListModel = new RewardListModel(hiddenRewardColumn); - + visibleRewardList.setModel(visibleRewardListModel); hiddenRewardList.setModel(hiddenRewardListModel); - - showCumulativeTimeCheckBox.setEnabled(view.canShowTime()); - showTimeCheckBox.setEnabled(view.canShowTime()); - + + showCumulativeTimeCheckBox.setEnabled(pathTableModel.canShowTime()); + showTimeCheckBox.setEnabled(pathTableModel.canShowTime()); + pathStyle.add(renderAllButton); pathStyle.add(changeRenderingButton); - + renderAllButton.setSelected(!view.isChangeRenderer()); changeRenderingButton.setSelected(view.isChangeRenderer()); - + makeVariableHiddenButton.setIcon(GUIPrism.getIconFromImage("smallArrowRight.png")); makeRewardHiddenButton.setIcon(GUIPrism.getIconFromImage("smallArrowRight.png")); - + makeVariableVisibleButton.setIcon(GUIPrism.getIconFromImage("smallArrowLeft.png")); makeRewardVisibleButton.setIcon(GUIPrism.getIconFromImage("smallArrowLeft.png")); - + this.setVisible(true); } - + /** This method is called from within the constructor to * initialize the form. * WARNING: Do NOT modify this code. The content of this method is * always regenerated by the Form Editor. */ - // //GEN-BEGIN:initComponents - private void initComponents() { - java.awt.GridBagConstraints gridBagConstraints; - - visibleLabel = new javax.swing.JLabel(); - hiddenLabel = new javax.swing.JLabel(); - pathStyle = new javax.swing.ButtonGroup(); - allPanel = new javax.swing.JPanel(); - bottomPanel = new javax.swing.JPanel(); - buttonPanel = new javax.swing.JPanel(); - okayButton = new javax.swing.JButton(); - cancelButton = new javax.swing.JButton(); - optionCheckBox = new javax.swing.JCheckBox(); - variableTabPane = new javax.swing.JTabbedPane(); - variableTabPanel = new javax.swing.JPanel(); - variablePanel = new javax.swing.JPanel(); - leftVariableColumn = new javax.swing.JPanel(); - leftVariablePanel = new javax.swing.JPanel(); - visibleVariableScrollList = new javax.swing.JScrollPane(); - visibleVariableList = new javax.swing.JList(); - selectAllVisibleVariablesButton = new javax.swing.JButton(); - centerVariableColumn = new javax.swing.JPanel(); - centerVariablePanel = new javax.swing.JPanel(); - makeVariableVisibleButton = new javax.swing.JButton(); - makeVariableHiddenButton = new javax.swing.JButton(); - rightVariableColumn = new javax.swing.JPanel(); - rightVariablePanel = new javax.swing.JPanel(); - hiddenVariableScrollList = new javax.swing.JScrollPane(); - hiddenVariableList = new javax.swing.JList(); - selectAllHiddenVariablesButton = new javax.swing.JButton(); - rewardTabPanel = new javax.swing.JPanel(); - rewardPanel = new javax.swing.JPanel(); - leftRewardColumn = new javax.swing.JPanel(); - leftRewardPanel = new javax.swing.JPanel(); - visibleRewardScrollList = new javax.swing.JScrollPane(); - visibleRewardList = new javax.swing.JList(); - selectAllVisibleRewardsButton = new javax.swing.JButton(); - centerRewardColumn = new javax.swing.JPanel(); - centerRewardPanel = new javax.swing.JPanel(); - makeRewardVisibleButton = new javax.swing.JButton(); - makeRewardHiddenButton = new javax.swing.JButton(); - rightRewardColumn = new javax.swing.JPanel(); - rightRewardPanel = new javax.swing.JPanel(); - hiddenRewardScrollList = new javax.swing.JScrollPane(); - hiddenRewardList = new javax.swing.JList(); - selectAllHiddenRewardsButton = new javax.swing.JButton(); - otherTabPanel = new javax.swing.JPanel(); - boxPanel = new javax.swing.JPanel(); - innerTimePanel = new javax.swing.JPanel(); - topInnerTimePanel = new javax.swing.JPanel(); - showTimeCheckBox = new javax.swing.JCheckBox(); - showCumulativeTimeCheckBox = new javax.swing.JCheckBox(); - pathStylePanel = new javax.swing.JPanel(); - innerPathStylePanel = new javax.swing.JPanel(); - changeRenderingButton = new javax.swing.JRadioButton(); - renderAllButton = new javax.swing.JRadioButton(); - - visibleLabel.setHorizontalAlignment(javax.swing.SwingConstants.CENTER); - visibleLabel.setText("Visible Variables"); - hiddenLabel.setHorizontalAlignment(javax.swing.SwingConstants.CENTER); - hiddenLabel.setText("Hidden Variables"); - - addWindowListener(new java.awt.event.WindowAdapter() { - public void windowClosing(java.awt.event.WindowEvent evt) { - closeDialog(evt); - } - }); - - allPanel.setLayout(new java.awt.BorderLayout()); - - allPanel.setBorder(javax.swing.BorderFactory.createEmptyBorder(5, 5, 5, 5)); - bottomPanel.setLayout(new java.awt.BorderLayout()); - - buttonPanel.setLayout(new java.awt.FlowLayout(java.awt.FlowLayout.RIGHT)); - - okayButton.setText("Okay"); - okayButton.addActionListener(new java.awt.event.ActionListener() { - public void actionPerformed(java.awt.event.ActionEvent evt) { - okayButtonActionPerformed(evt); - } - }); - - buttonPanel.add(okayButton); - - cancelButton.setText("Cancel"); - cancelButton.addActionListener(new java.awt.event.ActionListener() { - public void actionPerformed(java.awt.event.ActionEvent evt) { - cancelButtonActionPerformed(evt); - } - }); - - buttonPanel.add(cancelButton); - - bottomPanel.add(buttonPanel, java.awt.BorderLayout.EAST); - - optionCheckBox.setText("Always prompt for view configuration on path creation"); - bottomPanel.add(optionCheckBox, java.awt.BorderLayout.WEST); - optionCheckBox.getAccessibleContext().setAccessibleName("optionCheckBox"); - - allPanel.add(bottomPanel, java.awt.BorderLayout.SOUTH); - - getContentPane().add(allPanel, java.awt.BorderLayout.SOUTH); - - variableTabPane.setBorder(javax.swing.BorderFactory.createEmptyBorder(5, 5, 5, 5)); - variableTabPanel.setLayout(new java.awt.BorderLayout()); - - variablePanel.setLayout(new java.awt.GridBagLayout()); - - variablePanel.setBorder(javax.swing.BorderFactory.createEmptyBorder(5, 5, 5, 5)); - leftVariableColumn.setLayout(new java.awt.BorderLayout()); - - leftVariableColumn.setBorder(javax.swing.BorderFactory.createTitledBorder("Visible variables")); - leftVariablePanel.setLayout(new java.awt.BorderLayout(0, 5)); - - leftVariablePanel.setBorder(javax.swing.BorderFactory.createEmptyBorder(5, 5, 5, 5)); - visibleVariableScrollList.setHorizontalScrollBarPolicy(javax.swing.ScrollPaneConstants.HORIZONTAL_SCROLLBAR_NEVER); - visibleVariableScrollList.setViewportView(visibleVariableList); - - leftVariablePanel.add(visibleVariableScrollList, java.awt.BorderLayout.CENTER); - - selectAllVisibleVariablesButton.setText("Select All"); - selectAllVisibleVariablesButton.addActionListener(new java.awt.event.ActionListener() { - public void actionPerformed(java.awt.event.ActionEvent evt) { - selectAllVisibleVariablesButtonActionPerformed(evt); - } - }); - - leftVariablePanel.add(selectAllVisibleVariablesButton, java.awt.BorderLayout.SOUTH); - - leftVariableColumn.add(leftVariablePanel, java.awt.BorderLayout.CENTER); - - gridBagConstraints = new java.awt.GridBagConstraints(); - gridBagConstraints.gridx = 0; - gridBagConstraints.gridy = 0; - gridBagConstraints.gridwidth = 2; - gridBagConstraints.fill = java.awt.GridBagConstraints.BOTH; - gridBagConstraints.weightx = 0.5; - gridBagConstraints.weighty = 1.0; - variablePanel.add(leftVariableColumn, gridBagConstraints); + // //GEN-BEGIN:initComponents + private void initComponents() + { + java.awt.GridBagConstraints gridBagConstraints; + + visibleLabel = new javax.swing.JLabel(); + hiddenLabel = new javax.swing.JLabel(); + pathStyle = new javax.swing.ButtonGroup(); + allPanel = new javax.swing.JPanel(); + bottomPanel = new javax.swing.JPanel(); + buttonPanel = new javax.swing.JPanel(); + okayButton = new javax.swing.JButton(); + cancelButton = new javax.swing.JButton(); + optionCheckBox = new javax.swing.JCheckBox(); + variableTabPane = new javax.swing.JTabbedPane(); + variableTabPanel = new javax.swing.JPanel(); + variablePanel = new javax.swing.JPanel(); + leftVariableColumn = new javax.swing.JPanel(); + leftVariablePanel = new javax.swing.JPanel(); + visibleVariableScrollList = new javax.swing.JScrollPane(); + visibleVariableList = new javax.swing.JList(); + selectAllVisibleVariablesButton = new javax.swing.JButton(); + centerVariableColumn = new javax.swing.JPanel(); + centerVariablePanel = new javax.swing.JPanel(); + makeVariableVisibleButton = new javax.swing.JButton(); + makeVariableHiddenButton = new javax.swing.JButton(); + rightVariableColumn = new javax.swing.JPanel(); + rightVariablePanel = new javax.swing.JPanel(); + hiddenVariableScrollList = new javax.swing.JScrollPane(); + hiddenVariableList = new javax.swing.JList(); + selectAllHiddenVariablesButton = new javax.swing.JButton(); + rewardTabPanel = new javax.swing.JPanel(); + rewardPanel = new javax.swing.JPanel(); + leftRewardColumn = new javax.swing.JPanel(); + leftRewardPanel = new javax.swing.JPanel(); + visibleRewardScrollList = new javax.swing.JScrollPane(); + visibleRewardList = new javax.swing.JList(); + selectAllVisibleRewardsButton = new javax.swing.JButton(); + centerRewardColumn = new javax.swing.JPanel(); + centerRewardPanel = new javax.swing.JPanel(); + makeRewardVisibleButton = new javax.swing.JButton(); + makeRewardHiddenButton = new javax.swing.JButton(); + rightRewardColumn = new javax.swing.JPanel(); + rightRewardPanel = new javax.swing.JPanel(); + hiddenRewardScrollList = new javax.swing.JScrollPane(); + hiddenRewardList = new javax.swing.JList(); + selectAllHiddenRewardsButton = new javax.swing.JButton(); + otherTabPanel = new javax.swing.JPanel(); + boxPanel = new javax.swing.JPanel(); + innerTimePanel = new javax.swing.JPanel(); + topInnerTimePanel = new javax.swing.JPanel(); + showTimeCheckBox = new javax.swing.JCheckBox(); + showCumulativeTimeCheckBox = new javax.swing.JCheckBox(); + pathStylePanel = new javax.swing.JPanel(); + innerPathStylePanel = new javax.swing.JPanel(); + changeRenderingButton = new javax.swing.JRadioButton(); + renderAllButton = new javax.swing.JRadioButton(); + + visibleLabel.setHorizontalAlignment(javax.swing.SwingConstants.CENTER); + visibleLabel.setText("Visible Variables"); + hiddenLabel.setHorizontalAlignment(javax.swing.SwingConstants.CENTER); + hiddenLabel.setText("Hidden Variables"); + + addWindowListener(new java.awt.event.WindowAdapter() + { + public void windowClosing(java.awt.event.WindowEvent evt) + { + closeDialog(evt); + } + }); - centerVariableColumn.setLayout(new java.awt.BorderLayout()); + allPanel.setLayout(new java.awt.BorderLayout()); - centerVariablePanel.setLayout(new java.awt.GridBagLayout()); + allPanel.setBorder(javax.swing.BorderFactory.createEmptyBorder(5, 5, 5, 5)); + bottomPanel.setLayout(new java.awt.BorderLayout()); - makeVariableVisibleButton.addActionListener(new java.awt.event.ActionListener() { - public void actionPerformed(java.awt.event.ActionEvent evt) { - makeVariableVisibleButtonActionPerformed(evt); - } - }); + buttonPanel.setLayout(new java.awt.FlowLayout(java.awt.FlowLayout.RIGHT)); - gridBagConstraints = new java.awt.GridBagConstraints(); - gridBagConstraints.gridx = 0; - gridBagConstraints.gridy = 1; - gridBagConstraints.ipadx = 5; - gridBagConstraints.ipady = 5; - gridBagConstraints.insets = new java.awt.Insets(3, 10, 3, 10); - centerVariablePanel.add(makeVariableVisibleButton, gridBagConstraints); + okayButton.setText("Okay"); + okayButton.addActionListener(new java.awt.event.ActionListener() + { + public void actionPerformed(java.awt.event.ActionEvent evt) + { + okayButtonActionPerformed(evt); + } + }); - makeVariableHiddenButton.addActionListener(new java.awt.event.ActionListener() { - public void actionPerformed(java.awt.event.ActionEvent evt) { - makeVariableHiddenButtonActionPerformed(evt); - } - }); + buttonPanel.add(okayButton); - gridBagConstraints = new java.awt.GridBagConstraints(); - gridBagConstraints.ipadx = 5; - gridBagConstraints.ipady = 5; - gridBagConstraints.insets = new java.awt.Insets(3, 10, 3, 10); - centerVariablePanel.add(makeVariableHiddenButton, gridBagConstraints); + cancelButton.setText("Cancel"); + cancelButton.addActionListener(new java.awt.event.ActionListener() + { + public void actionPerformed(java.awt.event.ActionEvent evt) + { + cancelButtonActionPerformed(evt); + } + }); - centerVariableColumn.add(centerVariablePanel, java.awt.BorderLayout.CENTER); + buttonPanel.add(cancelButton); - gridBagConstraints = new java.awt.GridBagConstraints(); - gridBagConstraints.gridx = 2; - gridBagConstraints.gridy = 0; - gridBagConstraints.fill = java.awt.GridBagConstraints.VERTICAL; - gridBagConstraints.weighty = 1.0; - variablePanel.add(centerVariableColumn, gridBagConstraints); + bottomPanel.add(buttonPanel, java.awt.BorderLayout.EAST); - rightVariableColumn.setLayout(new java.awt.BorderLayout()); + optionCheckBox.setText("Always prompt for view configuration on path creation"); + bottomPanel.add(optionCheckBox, java.awt.BorderLayout.WEST); + optionCheckBox.getAccessibleContext().setAccessibleName("optionCheckBox"); - rightVariableColumn.setBorder(javax.swing.BorderFactory.createTitledBorder("Hidden variables")); - rightVariablePanel.setLayout(new java.awt.BorderLayout(0, 5)); + allPanel.add(bottomPanel, java.awt.BorderLayout.SOUTH); - rightVariablePanel.setBorder(javax.swing.BorderFactory.createEmptyBorder(5, 5, 5, 5)); - hiddenVariableScrollList.setHorizontalScrollBarPolicy(javax.swing.ScrollPaneConstants.HORIZONTAL_SCROLLBAR_NEVER); - hiddenVariableScrollList.setViewportView(hiddenVariableList); + getContentPane().add(allPanel, java.awt.BorderLayout.SOUTH); - rightVariablePanel.add(hiddenVariableScrollList, java.awt.BorderLayout.CENTER); + variableTabPane.setBorder(javax.swing.BorderFactory.createEmptyBorder(5, 5, 5, 5)); + variableTabPanel.setLayout(new java.awt.BorderLayout()); - selectAllHiddenVariablesButton.setText("Select All"); - selectAllHiddenVariablesButton.addActionListener(new java.awt.event.ActionListener() { - public void actionPerformed(java.awt.event.ActionEvent evt) { - selectAllHiddenVariablesButtonActionPerformed(evt); - } - }); + variablePanel.setLayout(new java.awt.GridBagLayout()); - rightVariablePanel.add(selectAllHiddenVariablesButton, java.awt.BorderLayout.SOUTH); + variablePanel.setBorder(javax.swing.BorderFactory.createEmptyBorder(5, 5, 5, 5)); + leftVariableColumn.setLayout(new java.awt.BorderLayout()); - rightVariableColumn.add(rightVariablePanel, java.awt.BorderLayout.CENTER); + leftVariableColumn.setBorder(javax.swing.BorderFactory.createTitledBorder("Visible variables")); + leftVariablePanel.setLayout(new java.awt.BorderLayout(0, 5)); - gridBagConstraints = new java.awt.GridBagConstraints(); - gridBagConstraints.gridx = 3; - gridBagConstraints.gridy = 0; - gridBagConstraints.gridwidth = 2; - gridBagConstraints.fill = java.awt.GridBagConstraints.BOTH; - gridBagConstraints.weightx = 0.5; - gridBagConstraints.weighty = 1.0; - variablePanel.add(rightVariableColumn, gridBagConstraints); + leftVariablePanel.setBorder(javax.swing.BorderFactory.createEmptyBorder(5, 5, 5, 5)); + visibleVariableScrollList.setHorizontalScrollBarPolicy(javax.swing.ScrollPaneConstants.HORIZONTAL_SCROLLBAR_NEVER); + visibleVariableScrollList.setViewportView(visibleVariableList); - variableTabPanel.add(variablePanel, java.awt.BorderLayout.CENTER); + leftVariablePanel.add(visibleVariableScrollList, java.awt.BorderLayout.CENTER); - variableTabPane.addTab("Variable visibility", variableTabPanel); + selectAllVisibleVariablesButton.setText("Select All"); + selectAllVisibleVariablesButton.addActionListener(new java.awt.event.ActionListener() + { + public void actionPerformed(java.awt.event.ActionEvent evt) + { + selectAllVisibleVariablesButtonActionPerformed(evt); + } + }); - rewardTabPanel.setLayout(new java.awt.BorderLayout()); - - rewardPanel.setLayout(new java.awt.GridBagLayout()); - - rewardPanel.setBorder(javax.swing.BorderFactory.createEmptyBorder(5, 5, 5, 5)); - leftRewardColumn.setLayout(new java.awt.BorderLayout()); - - leftRewardColumn.setBorder(javax.swing.BorderFactory.createTitledBorder("Visible reward structures")); - leftRewardPanel.setLayout(new java.awt.BorderLayout(0, 5)); + leftVariablePanel.add(selectAllVisibleVariablesButton, java.awt.BorderLayout.SOUTH); - leftRewardPanel.setBorder(javax.swing.BorderFactory.createEmptyBorder(5, 5, 5, 5)); - visibleRewardScrollList.setHorizontalScrollBarPolicy(javax.swing.ScrollPaneConstants.HORIZONTAL_SCROLLBAR_NEVER); - visibleRewardScrollList.setViewportView(visibleRewardList); + leftVariableColumn.add(leftVariablePanel, java.awt.BorderLayout.CENTER); - leftRewardPanel.add(visibleRewardScrollList, java.awt.BorderLayout.CENTER); + gridBagConstraints = new java.awt.GridBagConstraints(); + gridBagConstraints.gridx = 0; + gridBagConstraints.gridy = 0; + gridBagConstraints.gridwidth = 2; + gridBagConstraints.fill = java.awt.GridBagConstraints.BOTH; + gridBagConstraints.weightx = 0.5; + gridBagConstraints.weighty = 1.0; + variablePanel.add(leftVariableColumn, gridBagConstraints); - selectAllVisibleRewardsButton.setText("Select All"); - selectAllVisibleRewardsButton.addActionListener(new java.awt.event.ActionListener() { - public void actionPerformed(java.awt.event.ActionEvent evt) { - selectAllVisibleRewardsButtonActionPerformed(evt); - } - }); + centerVariableColumn.setLayout(new java.awt.BorderLayout()); - leftRewardPanel.add(selectAllVisibleRewardsButton, java.awt.BorderLayout.SOUTH); + centerVariablePanel.setLayout(new java.awt.GridBagLayout()); - leftRewardColumn.add(leftRewardPanel, java.awt.BorderLayout.CENTER); + makeVariableVisibleButton.addActionListener(new java.awt.event.ActionListener() + { + public void actionPerformed(java.awt.event.ActionEvent evt) + { + makeVariableVisibleButtonActionPerformed(evt); + } + }); - gridBagConstraints = new java.awt.GridBagConstraints(); - gridBagConstraints.gridx = 0; - gridBagConstraints.gridy = 0; - gridBagConstraints.gridwidth = 2; - gridBagConstraints.fill = java.awt.GridBagConstraints.BOTH; - gridBagConstraints.weightx = 0.5; - gridBagConstraints.weighty = 1.0; - rewardPanel.add(leftRewardColumn, gridBagConstraints); + gridBagConstraints = new java.awt.GridBagConstraints(); + gridBagConstraints.gridx = 0; + gridBagConstraints.gridy = 1; + gridBagConstraints.ipadx = 5; + gridBagConstraints.ipady = 5; + gridBagConstraints.insets = new java.awt.Insets(3, 10, 3, 10); + centerVariablePanel.add(makeVariableVisibleButton, gridBagConstraints); - centerRewardColumn.setLayout(new java.awt.BorderLayout()); + makeVariableHiddenButton.addActionListener(new java.awt.event.ActionListener() + { + public void actionPerformed(java.awt.event.ActionEvent evt) + { + makeVariableHiddenButtonActionPerformed(evt); + } + }); + + gridBagConstraints = new java.awt.GridBagConstraints(); + gridBagConstraints.ipadx = 5; + gridBagConstraints.ipady = 5; + gridBagConstraints.insets = new java.awt.Insets(3, 10, 3, 10); + centerVariablePanel.add(makeVariableHiddenButton, gridBagConstraints); - centerRewardPanel.setLayout(new java.awt.GridBagLayout()); + centerVariableColumn.add(centerVariablePanel, java.awt.BorderLayout.CENTER); - makeRewardVisibleButton.addActionListener(new java.awt.event.ActionListener() { - public void actionPerformed(java.awt.event.ActionEvent evt) { - makeRewardVisibleButtonActionPerformed(evt); - } - }); + gridBagConstraints = new java.awt.GridBagConstraints(); + gridBagConstraints.gridx = 2; + gridBagConstraints.gridy = 0; + gridBagConstraints.fill = java.awt.GridBagConstraints.VERTICAL; + gridBagConstraints.weighty = 1.0; + variablePanel.add(centerVariableColumn, gridBagConstraints); - gridBagConstraints = new java.awt.GridBagConstraints(); - gridBagConstraints.gridx = 0; - gridBagConstraints.gridy = 1; - gridBagConstraints.ipadx = 5; - gridBagConstraints.ipady = 5; - gridBagConstraints.insets = new java.awt.Insets(3, 10, 3, 10); - centerRewardPanel.add(makeRewardVisibleButton, gridBagConstraints); + rightVariableColumn.setLayout(new java.awt.BorderLayout()); - makeRewardHiddenButton.addActionListener(new java.awt.event.ActionListener() { - public void actionPerformed(java.awt.event.ActionEvent evt) { - makeRewardHiddenButtonActionPerformed(evt); - } - }); + rightVariableColumn.setBorder(javax.swing.BorderFactory.createTitledBorder("Hidden variables")); + rightVariablePanel.setLayout(new java.awt.BorderLayout(0, 5)); - gridBagConstraints = new java.awt.GridBagConstraints(); - gridBagConstraints.ipadx = 5; - gridBagConstraints.ipady = 5; - gridBagConstraints.insets = new java.awt.Insets(3, 10, 3, 10); - centerRewardPanel.add(makeRewardHiddenButton, gridBagConstraints); + rightVariablePanel.setBorder(javax.swing.BorderFactory.createEmptyBorder(5, 5, 5, 5)); + hiddenVariableScrollList.setHorizontalScrollBarPolicy(javax.swing.ScrollPaneConstants.HORIZONTAL_SCROLLBAR_NEVER); + hiddenVariableScrollList.setViewportView(hiddenVariableList); - centerRewardColumn.add(centerRewardPanel, java.awt.BorderLayout.CENTER); + rightVariablePanel.add(hiddenVariableScrollList, java.awt.BorderLayout.CENTER); - gridBagConstraints = new java.awt.GridBagConstraints(); - gridBagConstraints.gridx = 2; - gridBagConstraints.gridy = 0; - gridBagConstraints.fill = java.awt.GridBagConstraints.VERTICAL; - gridBagConstraints.weighty = 1.0; - rewardPanel.add(centerRewardColumn, gridBagConstraints); + selectAllHiddenVariablesButton.setText("Select All"); + selectAllHiddenVariablesButton.addActionListener(new java.awt.event.ActionListener() + { + public void actionPerformed(java.awt.event.ActionEvent evt) + { + selectAllHiddenVariablesButtonActionPerformed(evt); + } + }); - rightRewardColumn.setLayout(new java.awt.BorderLayout()); + rightVariablePanel.add(selectAllHiddenVariablesButton, java.awt.BorderLayout.SOUTH); - rightRewardColumn.setBorder(javax.swing.BorderFactory.createTitledBorder("Hidden reward structures")); - rightRewardPanel.setLayout(new java.awt.BorderLayout(0, 5)); + rightVariableColumn.add(rightVariablePanel, java.awt.BorderLayout.CENTER); - rightRewardPanel.setBorder(javax.swing.BorderFactory.createEmptyBorder(5, 5, 5, 5)); - hiddenRewardScrollList.setHorizontalScrollBarPolicy(javax.swing.ScrollPaneConstants.HORIZONTAL_SCROLLBAR_NEVER); - hiddenRewardScrollList.setViewportView(hiddenRewardList); + gridBagConstraints = new java.awt.GridBagConstraints(); + gridBagConstraints.gridx = 3; + gridBagConstraints.gridy = 0; + gridBagConstraints.gridwidth = 2; + gridBagConstraints.fill = java.awt.GridBagConstraints.BOTH; + gridBagConstraints.weightx = 0.5; + gridBagConstraints.weighty = 1.0; + variablePanel.add(rightVariableColumn, gridBagConstraints); - rightRewardPanel.add(hiddenRewardScrollList, java.awt.BorderLayout.CENTER); + variableTabPanel.add(variablePanel, java.awt.BorderLayout.CENTER); - selectAllHiddenRewardsButton.setText("Select All"); - selectAllHiddenRewardsButton.addActionListener(new java.awt.event.ActionListener() { - public void actionPerformed(java.awt.event.ActionEvent evt) { - selectAllHiddenRewardsButtonActionPerformed(evt); - } - }); + variableTabPane.addTab("Variable visibility", variableTabPanel); - rightRewardPanel.add(selectAllHiddenRewardsButton, java.awt.BorderLayout.SOUTH); + rewardTabPanel.setLayout(new java.awt.BorderLayout()); - rightRewardColumn.add(rightRewardPanel, java.awt.BorderLayout.CENTER); + rewardPanel.setLayout(new java.awt.GridBagLayout()); + + rewardPanel.setBorder(javax.swing.BorderFactory.createEmptyBorder(5, 5, 5, 5)); + leftRewardColumn.setLayout(new java.awt.BorderLayout()); + + leftRewardColumn.setBorder(javax.swing.BorderFactory.createTitledBorder("Visible reward structures")); + leftRewardPanel.setLayout(new java.awt.BorderLayout(0, 5)); + + leftRewardPanel.setBorder(javax.swing.BorderFactory.createEmptyBorder(5, 5, 5, 5)); + visibleRewardScrollList.setHorizontalScrollBarPolicy(javax.swing.ScrollPaneConstants.HORIZONTAL_SCROLLBAR_NEVER); + visibleRewardScrollList.setViewportView(visibleRewardList); + + leftRewardPanel.add(visibleRewardScrollList, java.awt.BorderLayout.CENTER); + + selectAllVisibleRewardsButton.setText("Select All"); + selectAllVisibleRewardsButton.addActionListener(new java.awt.event.ActionListener() + { + public void actionPerformed(java.awt.event.ActionEvent evt) + { + selectAllVisibleRewardsButtonActionPerformed(evt); + } + }); + + leftRewardPanel.add(selectAllVisibleRewardsButton, java.awt.BorderLayout.SOUTH); + + leftRewardColumn.add(leftRewardPanel, java.awt.BorderLayout.CENTER); + + gridBagConstraints = new java.awt.GridBagConstraints(); + gridBagConstraints.gridx = 0; + gridBagConstraints.gridy = 0; + gridBagConstraints.gridwidth = 2; + gridBagConstraints.fill = java.awt.GridBagConstraints.BOTH; + gridBagConstraints.weightx = 0.5; + gridBagConstraints.weighty = 1.0; + rewardPanel.add(leftRewardColumn, gridBagConstraints); + + centerRewardColumn.setLayout(new java.awt.BorderLayout()); + + centerRewardPanel.setLayout(new java.awt.GridBagLayout()); + + makeRewardVisibleButton.addActionListener(new java.awt.event.ActionListener() + { + public void actionPerformed(java.awt.event.ActionEvent evt) + { + makeRewardVisibleButtonActionPerformed(evt); + } + }); + + gridBagConstraints = new java.awt.GridBagConstraints(); + gridBagConstraints.gridx = 0; + gridBagConstraints.gridy = 1; + gridBagConstraints.ipadx = 5; + gridBagConstraints.ipady = 5; + gridBagConstraints.insets = new java.awt.Insets(3, 10, 3, 10); + centerRewardPanel.add(makeRewardVisibleButton, gridBagConstraints); + + makeRewardHiddenButton.addActionListener(new java.awt.event.ActionListener() + { + public void actionPerformed(java.awt.event.ActionEvent evt) + { + makeRewardHiddenButtonActionPerformed(evt); + } + }); + + gridBagConstraints = new java.awt.GridBagConstraints(); + gridBagConstraints.ipadx = 5; + gridBagConstraints.ipady = 5; + gridBagConstraints.insets = new java.awt.Insets(3, 10, 3, 10); + centerRewardPanel.add(makeRewardHiddenButton, gridBagConstraints); + + centerRewardColumn.add(centerRewardPanel, java.awt.BorderLayout.CENTER); + + gridBagConstraints = new java.awt.GridBagConstraints(); + gridBagConstraints.gridx = 2; + gridBagConstraints.gridy = 0; + gridBagConstraints.fill = java.awt.GridBagConstraints.VERTICAL; + gridBagConstraints.weighty = 1.0; + rewardPanel.add(centerRewardColumn, gridBagConstraints); + + rightRewardColumn.setLayout(new java.awt.BorderLayout()); + + rightRewardColumn.setBorder(javax.swing.BorderFactory.createTitledBorder("Hidden reward structures")); + rightRewardPanel.setLayout(new java.awt.BorderLayout(0, 5)); + + rightRewardPanel.setBorder(javax.swing.BorderFactory.createEmptyBorder(5, 5, 5, 5)); + hiddenRewardScrollList.setHorizontalScrollBarPolicy(javax.swing.ScrollPaneConstants.HORIZONTAL_SCROLLBAR_NEVER); + hiddenRewardScrollList.setViewportView(hiddenRewardList); + + rightRewardPanel.add(hiddenRewardScrollList, java.awt.BorderLayout.CENTER); + + selectAllHiddenRewardsButton.setText("Select All"); + selectAllHiddenRewardsButton.addActionListener(new java.awt.event.ActionListener() + { + public void actionPerformed(java.awt.event.ActionEvent evt) + { + selectAllHiddenRewardsButtonActionPerformed(evt); + } + }); + + rightRewardPanel.add(selectAllHiddenRewardsButton, java.awt.BorderLayout.SOUTH); + + rightRewardColumn.add(rightRewardPanel, java.awt.BorderLayout.CENTER); + + gridBagConstraints = new java.awt.GridBagConstraints(); + gridBagConstraints.gridx = 3; + gridBagConstraints.gridy = 0; + gridBagConstraints.gridwidth = 2; + gridBagConstraints.fill = java.awt.GridBagConstraints.BOTH; + gridBagConstraints.weightx = 0.5; + gridBagConstraints.weighty = 1.0; + rewardPanel.add(rightRewardColumn, gridBagConstraints); + + rewardTabPanel.add(rewardPanel, java.awt.BorderLayout.CENTER); + + variableTabPane.addTab("Reward visibility", rewardTabPanel); + + otherTabPanel.setLayout(new java.awt.BorderLayout()); + + boxPanel.setLayout(new javax.swing.BoxLayout(boxPanel, javax.swing.BoxLayout.Y_AXIS)); + + boxPanel.setBorder(javax.swing.BorderFactory.createEmptyBorder(5, 5, 5, 5)); + innerTimePanel.setLayout(new java.awt.BorderLayout()); + + innerTimePanel.setBorder(javax.swing.BorderFactory.createTitledBorder("Time properties")); + topInnerTimePanel.setLayout(new java.awt.GridLayout(2, 1, 5, 5)); + + topInnerTimePanel.setBorder(javax.swing.BorderFactory.createEmptyBorder(5, 5, 5, 5)); + showTimeCheckBox.setText("Show the time spent in states"); + showTimeCheckBox.setBorder(javax.swing.BorderFactory.createEmptyBorder(0, 0, 0, 0)); + showTimeCheckBox.setMargin(new java.awt.Insets(0, 0, 0, 0)); + topInnerTimePanel.add(showTimeCheckBox); + showTimeCheckBox.getAccessibleContext().setAccessibleName(""); + + showCumulativeTimeCheckBox.setText("Show the cumulative time"); + showCumulativeTimeCheckBox.setBorder(javax.swing.BorderFactory.createEmptyBorder(0, 0, 0, 0)); + showCumulativeTimeCheckBox.setMargin(new java.awt.Insets(0, 0, 0, 0)); + topInnerTimePanel.add(showCumulativeTimeCheckBox); + + innerTimePanel.add(topInnerTimePanel, java.awt.BorderLayout.NORTH); + + boxPanel.add(innerTimePanel); + + pathStylePanel.setLayout(new java.awt.BorderLayout()); + + pathStylePanel.setBorder(javax.swing.BorderFactory.createTitledBorder("Path style")); + innerPathStylePanel.setLayout(new java.awt.GridLayout(2, 1, 5, 5)); + + innerPathStylePanel.setBorder(javax.swing.BorderFactory.createEmptyBorder(5, 5, 5, 5)); + changeRenderingButton.setText("Render changes"); + changeRenderingButton.setBorder(javax.swing.BorderFactory.createEmptyBorder(0, 0, 0, 0)); + changeRenderingButton.setMargin(new java.awt.Insets(0, 0, 0, 0)); + innerPathStylePanel.add(changeRenderingButton); + + renderAllButton.setText("Render all values"); + renderAllButton.setBorder(javax.swing.BorderFactory.createEmptyBorder(0, 0, 0, 0)); + renderAllButton.setMargin(new java.awt.Insets(0, 0, 0, 0)); + innerPathStylePanel.add(renderAllButton); + + pathStylePanel.add(innerPathStylePanel, java.awt.BorderLayout.NORTH); + + boxPanel.add(pathStylePanel); + + otherTabPanel.add(boxPanel, java.awt.BorderLayout.NORTH); + + variableTabPane.addTab("Other", otherTabPanel); + + getContentPane().add(variableTabPane, java.awt.BorderLayout.CENTER); + + }// //GEN-END:initComponents + + private void selectAllHiddenRewardsButtonActionPerformed(java.awt.event.ActionEvent evt) + {//GEN-FIRST:event_selectAllHiddenRewardsButtonActionPerformed + int[] indices = new int[hiddenRewardListModel.getSize()]; + for (int i = 0; i < indices.length; i++) + indices[i] = i; + + hiddenRewardList.setSelectedIndices(indices); + }//GEN-LAST:event_selectAllHiddenRewardsButtonActionPerformed + + private void makeRewardHiddenButtonActionPerformed(java.awt.event.ActionEvent evt) + {//GEN-FIRST:event_makeRewardHiddenButtonActionPerformed + int[] indices = visibleRewardList.getSelectedIndices(); + + for (int i = indices.length - 1; i >= 0; i--) { + RewardListItem rew = (RewardListItem) visibleRewardListModel.get(indices[i]); + + visibleRewardListModel.removeReward(rew); + hiddenRewardListModel.addReward(rew); + } + }//GEN-LAST:event_makeRewardHiddenButtonActionPerformed + + private void makeRewardVisibleButtonActionPerformed(java.awt.event.ActionEvent evt) + {//GEN-FIRST:event_makeRewardVisibleButtonActionPerformed + int[] indices = hiddenRewardList.getSelectedIndices(); + + for (int i = indices.length - 1; i >= 0; i--) { + RewardListItem rew = (RewardListItem) hiddenRewardListModel.get(indices[i]); + + hiddenRewardListModel.removeReward(rew); + visibleRewardListModel.addReward(rew); + } + }//GEN-LAST:event_makeRewardVisibleButtonActionPerformed + + private void selectAllVisibleRewardsButtonActionPerformed(java.awt.event.ActionEvent evt) + {//GEN-FIRST:event_selectAllVisibleRewardsButtonActionPerformed + int[] indices = new int[visibleRewardListModel.getSize()]; + for (int i = 0; i < indices.length; i++) + indices[i] = i; + + visibleRewardList.setSelectedIndices(indices); + }//GEN-LAST:event_selectAllVisibleRewardsButtonActionPerformed + + private void selectAllVisibleVariablesButtonActionPerformed(java.awt.event.ActionEvent evt) + {//GEN-FIRST:event_selectAllVisibleVariablesButtonActionPerformed + int[] indices = new int[visibleVariableListModel.getSize()]; + for (int i = 0; i < indices.length; i++) + indices[i] = i; + + visibleVariableList.setSelectedIndices(indices); + }//GEN-LAST:event_selectAllVisibleVariablesButtonActionPerformed + + private void selectAllHiddenVariablesButtonActionPerformed(java.awt.event.ActionEvent evt) + {//GEN-FIRST:event_selectAllHiddenVariablesButtonActionPerformed + int[] indices = new int[hiddenVariableListModel.getSize()]; + for (int i = 0; i < indices.length; i++) + indices[i] = i; + + hiddenVariableList.setSelectedIndices(indices); + + }//GEN-LAST:event_selectAllHiddenVariablesButtonActionPerformed + + private void makeVariableVisibleButtonActionPerformed(java.awt.event.ActionEvent evt) + {//GEN-FIRST:event_makeVariableVisibleButtonActionPerformed + int[] indices = hiddenVariableList.getSelectedIndices(); + + for (int i = indices.length - 1; i >= 0; i--) { + Variable var = (Variable) hiddenVariableListModel.get(indices[i]); + + hiddenVariableListModel.removeVariable(var); + visibleVariableListModel.addVariable(var); + } + }//GEN-LAST:event_makeVariableVisibleButtonActionPerformed + + private void makeVariableHiddenButtonActionPerformed(java.awt.event.ActionEvent evt) + {//GEN-FIRST:event_makeVariableHiddenButtonActionPerformed + int[] indices = visibleVariableList.getSelectedIndices(); + + for (int i = indices.length - 1; i >= 0; i--) { + Variable var = (Variable) visibleVariableListModel.get(indices[i]); + + visibleVariableListModel.removeVariable(var); + hiddenVariableListModel.addVariable(var); + } + }//GEN-LAST:event_makeVariableHiddenButtonActionPerformed - gridBagConstraints = new java.awt.GridBagConstraints(); - gridBagConstraints.gridx = 3; - gridBagConstraints.gridy = 0; - gridBagConstraints.gridwidth = 2; - gridBagConstraints.fill = java.awt.GridBagConstraints.BOTH; - gridBagConstraints.weightx = 0.5; - gridBagConstraints.weighty = 1.0; - rewardPanel.add(rightRewardColumn, gridBagConstraints); - - rewardTabPanel.add(rewardPanel, java.awt.BorderLayout.CENTER); - - variableTabPane.addTab("Reward visibility", rewardTabPanel); - - otherTabPanel.setLayout(new java.awt.BorderLayout()); - - boxPanel.setLayout(new javax.swing.BoxLayout(boxPanel, javax.swing.BoxLayout.Y_AXIS)); - - boxPanel.setBorder(javax.swing.BorderFactory.createEmptyBorder(5, 5, 5, 5)); - innerTimePanel.setLayout(new java.awt.BorderLayout()); - - innerTimePanel.setBorder(javax.swing.BorderFactory.createTitledBorder("Time properties")); - topInnerTimePanel.setLayout(new java.awt.GridLayout(2, 1, 5, 5)); - - topInnerTimePanel.setBorder(javax.swing.BorderFactory.createEmptyBorder(5, 5, 5, 5)); - showTimeCheckBox.setText("Show the time spent in states"); - showTimeCheckBox.setBorder(javax.swing.BorderFactory.createEmptyBorder(0, 0, 0, 0)); - showTimeCheckBox.setMargin(new java.awt.Insets(0, 0, 0, 0)); - topInnerTimePanel.add(showTimeCheckBox); - showTimeCheckBox.getAccessibleContext().setAccessibleName(""); - - showCumulativeTimeCheckBox.setText("Show the cumulative time"); - showCumulativeTimeCheckBox.setBorder(javax.swing.BorderFactory.createEmptyBorder(0, 0, 0, 0)); - showCumulativeTimeCheckBox.setMargin(new java.awt.Insets(0, 0, 0, 0)); - topInnerTimePanel.add(showCumulativeTimeCheckBox); - - innerTimePanel.add(topInnerTimePanel, java.awt.BorderLayout.NORTH); - - boxPanel.add(innerTimePanel); - - pathStylePanel.setLayout(new java.awt.BorderLayout()); - - pathStylePanel.setBorder(javax.swing.BorderFactory.createTitledBorder("Path style")); - innerPathStylePanel.setLayout(new java.awt.GridLayout(2, 1, 5, 5)); - - innerPathStylePanel.setBorder(javax.swing.BorderFactory.createEmptyBorder(5, 5, 5, 5)); - changeRenderingButton.setText("Render changes"); - changeRenderingButton.setBorder(javax.swing.BorderFactory.createEmptyBorder(0, 0, 0, 0)); - changeRenderingButton.setMargin(new java.awt.Insets(0, 0, 0, 0)); - innerPathStylePanel.add(changeRenderingButton); - - renderAllButton.setText("Render all values"); - renderAllButton.setBorder(javax.swing.BorderFactory.createEmptyBorder(0, 0, 0, 0)); - renderAllButton.setMargin(new java.awt.Insets(0, 0, 0, 0)); - innerPathStylePanel.add(renderAllButton); - - pathStylePanel.add(innerPathStylePanel, java.awt.BorderLayout.NORTH); - - boxPanel.add(pathStylePanel); - - otherTabPanel.add(boxPanel, java.awt.BorderLayout.NORTH); - - variableTabPane.addTab("Other", otherTabPanel); - - getContentPane().add(variableTabPane, java.awt.BorderLayout.CENTER); - - }// //GEN-END:initComponents - - private void selectAllHiddenRewardsButtonActionPerformed(java.awt.event.ActionEvent evt) {//GEN-FIRST:event_selectAllHiddenRewardsButtonActionPerformed - int[] indices = new int[hiddenRewardListModel.getSize()]; - for (int i = 0; i < indices.length; i++) - indices[i] = i; - - hiddenRewardList.setSelectedIndices(indices); - }//GEN-LAST:event_selectAllHiddenRewardsButtonActionPerformed - - private void makeRewardHiddenButtonActionPerformed(java.awt.event.ActionEvent evt) {//GEN-FIRST:event_makeRewardHiddenButtonActionPerformed - int[] indices = visibleRewardList.getSelectedIndices(); - - for (int i = indices.length - 1; i >= 0; i--) - { - RewardListItem rew = (RewardListItem)visibleRewardListModel.get(indices[i]); - - visibleRewardListModel.removeReward(rew); - hiddenRewardListModel.addReward(rew); - } - }//GEN-LAST:event_makeRewardHiddenButtonActionPerformed - - private void makeRewardVisibleButtonActionPerformed(java.awt.event.ActionEvent evt) {//GEN-FIRST:event_makeRewardVisibleButtonActionPerformed - int[] indices = hiddenRewardList.getSelectedIndices(); - - for (int i = indices.length - 1; i >= 0; i--) - { - RewardListItem rew = (RewardListItem)hiddenRewardListModel.get(indices[i]); - - hiddenRewardListModel.removeReward(rew); - visibleRewardListModel.addReward(rew); - } - }//GEN-LAST:event_makeRewardVisibleButtonActionPerformed - - private void selectAllVisibleRewardsButtonActionPerformed(java.awt.event.ActionEvent evt) {//GEN-FIRST:event_selectAllVisibleRewardsButtonActionPerformed - int[] indices = new int[visibleRewardListModel.getSize()]; - for (int i = 0; i < indices.length; i++) - indices[i] = i; - - visibleRewardList.setSelectedIndices(indices); - }//GEN-LAST:event_selectAllVisibleRewardsButtonActionPerformed - - private void selectAllVisibleVariablesButtonActionPerformed(java.awt.event.ActionEvent evt) {//GEN-FIRST:event_selectAllVisibleVariablesButtonActionPerformed - int[] indices = new int[visibleVariableListModel.getSize()]; - for (int i = 0; i < indices.length; i++) - indices[i] = i; - - visibleVariableList.setSelectedIndices(indices); - }//GEN-LAST:event_selectAllVisibleVariablesButtonActionPerformed - - private void selectAllHiddenVariablesButtonActionPerformed(java.awt.event.ActionEvent evt) {//GEN-FIRST:event_selectAllHiddenVariablesButtonActionPerformed - int[] indices = new int[hiddenVariableListModel.getSize()]; - for (int i = 0; i < indices.length; i++) - indices[i] = i; - - hiddenVariableList.setSelectedIndices(indices); - - }//GEN-LAST:event_selectAllHiddenVariablesButtonActionPerformed - - private void makeVariableVisibleButtonActionPerformed(java.awt.event.ActionEvent evt) {//GEN-FIRST:event_makeVariableVisibleButtonActionPerformed - int[] indices = hiddenVariableList.getSelectedIndices(); - - for (int i = indices.length - 1; i >= 0; i--) - { - GUISimulator.Variable var = (GUISimulator.Variable)hiddenVariableListModel.get(indices[i]); - - hiddenVariableListModel.removeVariable(var); - visibleVariableListModel.addVariable(var); - } - }//GEN-LAST:event_makeVariableVisibleButtonActionPerformed - - private void makeVariableHiddenButtonActionPerformed(java.awt.event.ActionEvent evt) {//GEN-FIRST:event_makeVariableHiddenButtonActionPerformed - int[] indices = visibleVariableList.getSelectedIndices(); - - for (int i = indices.length - 1; i >= 0; i--) - { - GUISimulator.Variable var = (GUISimulator.Variable)visibleVariableListModel.get(indices[i]); - - visibleVariableListModel.removeVariable(var); - hiddenVariableListModel.addVariable(var); - } - }//GEN-LAST:event_makeVariableHiddenButtonActionPerformed - - - - public static double log(double base, double x) - { - return Math.log(x) / Math.log(base); - } - - private void okayButtonActionPerformed(java.awt.event.ActionEvent evt)//GEN-FIRST:event_okayButtonActionPerformed {//GEN-HEADEREND:event_okayButtonActionPerformed - - if (optionCheckBox.isSelected() != this.askOption) - { + + if (optionCheckBox.isSelected() != this.askOption) { this.askOption = !this.askOption; - - try - { - ((GUIPrism)this.getParent()).getPrism().getSettings().set(PrismSettings.SIMULATOR_NEW_PATH_ASK_VIEW, this.askOption); + + try { + ((GUIPrism) this.getParent()).getPrism().getSettings().set(PrismSettings.SIMULATOR_NEW_PATH_ASK_VIEW, this.askOption); + } catch (PrismException e) { } - catch (PrismException e) {} } - + view.showTime(showTimeCheckBox.isSelected()); - view.showCumulativeTime(showCumulativeTimeCheckBox.isSelected()); - view.setVariableVisibility(visibleVariableListModel.getVariables(), hiddenVariableListModel.getVariables()); + view.showCumulativeTime(showCumulativeTimeCheckBox.isSelected()); + view.setVariableVisibility(visibleVariableListModel.getVariables(), hiddenVariableListModel.getVariables()); view.setRenderer(changeRenderingButton.isSelected()); view.setVisibleRewardListItems(visibleRewardListModel.getRewards()); - + dispose(); }//GEN-LAST:event_okayButtonActionPerformed - + private void cancelButtonActionPerformed(java.awt.event.ActionEvent evt)//GEN-FIRST:event_cancelButtonActionPerformed {//GEN-HEADEREND:event_cancelButtonActionPerformed dispose(); }//GEN-LAST:event_cancelButtonActionPerformed - + /** Closes the dialog */ private void closeDialog(java.awt.event.WindowEvent evt)//GEN-FIRST:event_closeDialog { @@ -702,88 +710,83 @@ public class GUIViewDialog extends JDialog implements KeyListener public void keyPressed(KeyEvent e) { - } - + } + public void keyReleased(KeyEvent e) { - + } - + public void keyTyped(KeyEvent e) { - + } - + class VariableListModel extends DefaultListModel - { - public VariableListModel(ArrayList variables) + { + private static final long serialVersionUID = 1L; + + public VariableListModel(ArrayList variables) { super(); - for (int i = 0; i < variables.size(); i++) - { - super.add(i, ((GUISimulator.Variable)variables.get(i))); - + for (int i = 0; i < variables.size(); i++) { + super.add(i, variables.get(i)); } } - - public void removeVariable(GUISimulator.Variable variable) + + public void removeVariable(Variable variable) { - for (int i = 0; i < super.getSize(); i++) - { - GUISimulator.Variable var = (GUISimulator.Variable)super.getElementAt(i); - if (var.equals(variable)) - { + for (int i = 0; i < super.getSize(); i++) { + Variable var = (Variable) super.getElementAt(i); + if (var.equals(variable)) { super.remove(i); } - } + } } - - public void addVariable(GUISimulator.Variable variable) + + public void addVariable(Variable variable) { int i = 0; - - while (i < super.getSize() && ((GUISimulator.Variable)super.getElementAt(i)).getIndex() < variable.getIndex()) - { - i++; - } - + + while (i < super.getSize() && ((Variable) super.getElementAt(i)).getIndex() < variable.getIndex()) { + i++; + } + super.add(i, variable); } - - public ArrayList getVariables() + + public ArrayList getVariables() { - ArrayList list = new ArrayList(); - for (int i = 0; i < super.getSize(); i++) - { - list.add(super.getElementAt(i)); + ArrayList list = new ArrayList(); + for (int i = 0; i < super.getSize(); i++) { + list.add((Variable) super.getElementAt(i)); } - + return list; } } - + class RewardListItem { - private GUISimulator.RewardStructure rewardStructure; + private RewardStructure rewardStructure; private boolean isCumulative; - - public RewardListItem(RewardStructure rewardStructure, boolean isCumulative) - { + + public RewardListItem(RewardStructure rewardStructure, boolean isCumulative) + { this.rewardStructure = rewardStructure; this.isCumulative = isCumulative; } - + public String toString() { String res = rewardStructure.toString(); if (isCumulative) return res + " (cumulative)"; - else - { + else { if (!rewardStructure.isStateEmpty() && !rewardStructure.isTransitionEmpty()) return res + " (state and transition)"; else if (!rewardStructure.isStateEmpty()) - return res + " (state)"; + return res + " (state)"; else if (!rewardStructure.isTransitionEmpty()) return res + " (transition)"; else @@ -791,89 +794,83 @@ public class GUIViewDialog extends JDialog implements KeyListener } } - public boolean isCumulative() + public boolean isCumulative() { return isCumulative; } - public void setCumulative(boolean isCumulative) + public void setCumulative(boolean isCumulative) { this.isCumulative = isCumulative; } - - public GUISimulator.RewardStructure getRewardStructure() + + public RewardStructure getRewardStructure() { return rewardStructure; } - public void setRewardStructure(GUISimulator.RewardStructure rewardStructure) + public void setRewardStructure(RewardStructure rewardStructure) { this.rewardStructure = rewardStructure; } - + public boolean equals(Object obj) { - if (obj instanceof RewardListItem) - { - RewardListItem item = (RewardListItem)obj; + if (obj instanceof RewardListItem) { + RewardListItem item = (RewardListItem) obj; return (item.getRewardStructure().equals(this.rewardStructure) && item.isCumulative() == isCumulative); } - + return false; } } - + class RewardListModel extends DefaultListModel - { - public RewardListModel(ArrayList rewardListItems) + { + private static final long serialVersionUID = 1L; + + public RewardListModel(ArrayList rewardListItems) { - for (int i = 0; i < rewardListItems.size(); i++) - { - super.add(i, (RewardListItem)rewardListItems.get(i)); - + for (int i = 0; i < rewardListItems.size(); i++) { + super.add(i, rewardListItems.get(i)); + } } - + public void removeReward(RewardListItem reward) { - for (int i = 0; i < super.getSize(); i++) - { - RewardListItem rew = (RewardListItem)super.getElementAt(i); - if (rew.equals(reward)) - { + for (int i = 0; i < super.getSize(); i++) { + RewardListItem rew = (RewardListItem) super.getElementAt(i); + if (rew.equals(reward)) { super.remove(i); } - } + } } - + public void addReward(RewardListItem reward) { int i = 0; - - while (i < super.getSize() && ((RewardListItem)super.getElementAt(i)).getRewardStructure().getIndex() < reward.getRewardStructure().getIndex()) - { - i++; + + while (i < super.getSize() && ((RewardListItem) super.getElementAt(i)).getRewardStructure().getIndex() < reward.getRewardStructure().getIndex()) { + i++; } - - if (i < super.getSize() && ((RewardListItem)super.getElementAt(i)).getRewardStructure().getIndex() == reward.getRewardStructure().getIndex() && reward.isCumulative()) - { + + if (i < super.getSize() && ((RewardListItem) super.getElementAt(i)).getRewardStructure().getIndex() == reward.getRewardStructure().getIndex() + && reward.isCumulative()) { i++; } - + super.add(i, reward); } - - public ArrayList getRewards() + + public ArrayList getRewards() { - ArrayList list = new ArrayList(); - for (int i = 0; i < super.getSize(); i++) - { - list.add(super.getElementAt(i)); + ArrayList list = new ArrayList(); + for (int i = 0; i < super.getSize(); i++) { + list.add((RewardListItem) super.getElementAt(i)); } - + return list; } } } - - diff --git a/prism/src/userinterface/simulator/SimulationView.java b/prism/src/userinterface/simulator/SimulationView.java new file mode 100644 index 00000000..579d2920 --- /dev/null +++ b/prism/src/userinterface/simulator/SimulationView.java @@ -0,0 +1,659 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Andrew Hinton (University of Birmingham) +// * Mark Kattenbelt (University of Oxford, formerly University of Birmingham) +// * Dave Parker (University of Oxford, formerly University of Birmingham) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package userinterface.simulator; + +import java.util.*; + +import parser.ast.*; +import parser.type.Type; +import prism.PrismSettings; +import simulator.SimulatorEngine; +import userinterface.simulator.GUIViewDialog.RewardListItem; + +/** + * Class storing information about the view configuration for a path in the simulator. + */ +public class SimulationView extends Observable +{ + private GUISimulator simulator; + + private ArrayList visibleVariables; + private ArrayList hiddenVariables; + + private ArrayList visibleRewardColumns; + private ArrayList rewards; + + private boolean stepsVisible; + private boolean actionsVisible; + private boolean showTime; + private boolean showCumulativeTime; + private boolean useChangeRenderer; + + public SimulationView(GUISimulator simulator, PrismSettings settings) + { + this.simulator = simulator; + + this.visibleVariables = new ArrayList(); + this.hiddenVariables = new ArrayList(); + + this.visibleRewardColumns = new ArrayList(); + this.rewards = new ArrayList(); + + this.stepsVisible = true; + this.actionsVisible = true; + this.showTime = false; + this.showCumulativeTime = true; + + useChangeRenderer = (settings.getInteger(PrismSettings.SIMULATOR_RENDER_ALL_VALUES) == 0); + + } + + public boolean showSteps() + { + return stepsVisible; + } + + public void showSteps(boolean stepsVisible) + { + this.stepsVisible = stepsVisible; + + this.setChanged(); + this.notifyObservers(); + } + + public boolean showActions() + { + return actionsVisible; + } + + public void showActions(boolean actionsVisible) + { + this.actionsVisible = actionsVisible; + + this.setChanged(); + this.notifyObservers(); + } + + public boolean showTime() + { + return showTime; + } + + public boolean showCumulativeTime() + { + return showCumulativeTime; + } + + public void showTime(boolean showTime) + { + this.showTime = showTime; + + this.setChanged(); + this.notifyObservers(); + } + + public void showCumulativeTime(boolean showCumulativeTime) + { + this.showCumulativeTime = showCumulativeTime; + + this.setChanged(); + this.notifyObservers(); + } + + public ArrayList getVisibleVariables() + { + return visibleVariables; + } + + public ArrayList getHiddenVariables() + { + return hiddenVariables; + } + + public void setVariableVisibility(ArrayList visibleVariables, ArrayList hiddenVariables) + { + this.visibleVariables = visibleVariables; + this.hiddenVariables = hiddenVariables; + + this.setChanged(); + this.notifyObservers(); + } + + public ArrayList getVisibleRewardColumns() + { + return visibleRewardColumns; + } + + public void setVisibleRewardListItems(ArrayList visibleRewardListItems) + { + ArrayList visibleRewardColumns = new ArrayList(); + + for (RewardListItem item : visibleRewardListItems) { + if (item.isCumulative()) + visibleRewardColumns.add(new RewardStructureColumn(item.getRewardStructure(), RewardStructureColumn.CUMULATIVE_REWARD)); + else { + if (!item.getRewardStructure().isStateEmpty()) + visibleRewardColumns.add(new RewardStructureColumn(item.getRewardStructure(), RewardStructureColumn.STATE_REWARD)); + if (!item.getRewardStructure().isTransitionEmpty()) + visibleRewardColumns.add(new RewardStructureColumn(item.getRewardStructure(), RewardStructureColumn.TRANSITION_REWARD)); + } + } + + this.visibleRewardColumns = visibleRewardColumns; + + this.setChanged(); + this.notifyObservers(); + } + + public ArrayList getRewards() + { + return rewards; + } + + public boolean isChangeRenderer() + { + return useChangeRenderer; + } + + public void setRenderer(boolean isChangeRenderer) + { + if (useChangeRenderer != isChangeRenderer) { + useChangeRenderer = isChangeRenderer; + simulator.setRenderer(useChangeRenderer); + } + } + + public void refreshToDefaultView(SimulatorEngine engine, boolean pathActive, ModulesFile parsedModel) + { + // First see if we can get away with using current settings... + boolean canUseCurrentView = true; + if (!pathActive) { + canUseCurrentView = false; + } else { + if (useChangeRenderer != simulator.usingChangeRenderer()) { + simulator.setRenderer(useChangeRenderer); + } + + // Time-wise we have a problem. + if (!parsedModel.getModelType().continuousTime() && (showTime || showCumulativeTime)) + canUseCurrentView = false; + + // Make a set of all variable names. + TreeSet allVarNames = new TreeSet(); + + for (Variable var : visibleVariables) + allVarNames.add(var.getName()); + 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. + canUseCurrentView = false; + } + + // Cannot use current view if we have too many variables. + if (allVarNames.size() > 0) + canUseCurrentView = false; + + // Make a list of all reward structures + ArrayList allrew = new ArrayList(); + + for (RewardStructure rew : rewards) { + allrew.add(rew); + } + + for (int r = 0; r < parsedModel.getNumRewardStructs(); r++) { + RewardStruct rewardStruct = parsedModel.getRewardStruct(r); + String rewardName = rewardStruct.getName(); + + boolean hasStates = parsedModel.getRewardStruct(r).getNumStateItems() != 0; + boolean hasTrans = parsedModel.getRewardStruct(r).getNumTransItems() != 0; + + boolean foundReward = false; + + for (RewardStructure rew : rewards) { + if (rew.isStateEmpty() == !hasStates && rew.isTransitionEmpty() == !hasTrans + && ((rew.getName() == null && rewardName.equals("")) || (rew.getName() != null && rew.getName().equals(rewardName)))) { + allrew.remove(rew); + foundReward = true; + } + } + + if (!foundReward) + canUseCurrentView = false; + } + + if (allrew.size() > 0) + canUseCurrentView = false; + + } + + if (!canUseCurrentView && pathActive) { + visibleVariables.clear(); + hiddenVariables.clear(); + visibleRewardColumns.clear(); + + rewards.clear(); + + { + for (int i = 0; i < engine.getNumVariables(); i++) { + visibleVariables.add(new Variable(i, engine.getVariableName(i), engine.getVariableType(i))); + } + + for (int r = 0; r < parsedModel.getNumRewardStructs(); r++) { + RewardStruct rewardStruct = parsedModel.getRewardStruct(r); + String rewardName = rewardStruct.getName(); + + if (rewardName.trim().length() == 0) { + rewardName = null; + } + + RewardStructure rewardStructure = new RewardStructure(r, rewardName, parsedModel.getRewardStruct(r).getNumStateItems() == 0, parsedModel + .getRewardStruct(r).getNumTransItems() == 0); + + if (!rewardStructure.isStateEmpty() || !rewardStructure.isTransitionEmpty()) + rewards.add(rewardStructure); + + if (!rewardStructure.isStateEmpty()) + visibleRewardColumns.add(new RewardStructureColumn(rewardStructure, RewardStructureColumn.STATE_REWARD)); + + if (!rewardStructure.isTransitionEmpty()) + visibleRewardColumns.add(new RewardStructureColumn(rewardStructure, RewardStructureColumn.TRANSITION_REWARD)); + } + + } + } + this.setChanged(); + this.notifyObservers(); + + } + + /** + * Represents a variable in the model. + */ + public class Variable + { + private int index; + private String name; + private Type type; + + public Variable(int index, String name, Type type) + { + this.index = index; + this.name = name; + this.type = type; + } + + public int getIndex() + { + return index; + } + + public String getName() + { + return name; + } + + public Type getType() + { + return type; + } + + public String toString() + { + return name; + } + + public boolean equals(Object o) + { + return (o instanceof Variable && ((Variable) o).getIndex() == index); + } + } + + public class VariableValue + { + private Variable variable; + private Object value; + private boolean hasChanged; + + public VariableValue(Variable variable, Object value) + { + this.variable = variable; + this.value = value; + this.hasChanged = true; + } + + public Object getValue() + { + return value; + } + + public void setValue(Object value) + { + this.value = value; + } + + public Variable getVariable() + { + return variable; + } + + public void setVariable(Variable variable) + { + this.variable = variable; + } + + public boolean hasChanged() + { + return hasChanged; + } + + public void setChanged(boolean hasChanged) + { + this.hasChanged = hasChanged; + } + } + + 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; + private boolean timeValueUnknown; + private boolean isCumulative; + + public TimeValue(Double value, boolean isCumulative) + { + this.value = value; + this.isCumulative = isCumulative; + } + + public Double getValue() + { + return value; + } + + public void setValue(Double value) + { + this.value = value; + } + + public void setTimeValueUnknown(boolean unknown) + { + this.timeValueUnknown = unknown; + } + + public boolean isTimeValueUnknown() + { + return this.timeValueUnknown; + } + + public boolean isCumulative() + { + return isCumulative; + } + + public void setCumulative(boolean isCumulative) + { + this.isCumulative = isCumulative; + } + } + + /** + * Represents a reward structure in the model. + */ + public class RewardStructure + { + private int index; + private String name; + + private boolean stateEmpty; + private boolean transitionEmpty; + + public RewardStructure(int index, String name, boolean stateEmpty, boolean transitionEmpty) + { + this.index = index; + this.name = name; + this.stateEmpty = stateEmpty; + this.transitionEmpty = transitionEmpty; + } + + public int getIndex() + { + return index; + } + + public String getName() + { + return name; + } + + public String getColumnName() + { + if (name == null) { + return "" + (index + 1); + } else { + return "\"" + name + "\""; + } + } + + public boolean isStateEmpty() + { + return stateEmpty; + } + + public boolean isTransitionEmpty() + { + return transitionEmpty; + } + + public boolean isCumulative() + { + return false; + } + + public String toString() + { + if (name != null) { + return "" + (index + 1) + ": \"" + name + "\""; + } else { + return "" + (index + 1) + ": "; + } + } + + public boolean equals(Object o) + { + return (o instanceof RewardStructure && ((RewardStructure) o).getIndex() == index && ((RewardStructure) o).isCumulative() == isCumulative()); + } + } + + public class RewardStructureColumn + { + public static final int STATE_REWARD = 0; + public static final int TRANSITION_REWARD = 1; + public static final int CUMULATIVE_REWARD = 2; + + private RewardStructure rewardStructure; + private int type; + + public RewardStructureColumn(RewardStructure rewardStructure, int type) + { + this.rewardStructure = rewardStructure; + this.type = type; + } + + public String getColumnName() + { + switch (type) { + case (STATE_REWARD): + return rewardStructure.getColumnName(); + case (TRANSITION_REWARD): + return "[ " + rewardStructure.getColumnName() + " ]"; + case (CUMULATIVE_REWARD): + return rewardStructure.getColumnName() + " (+)"; + } + return ""; + } + + public RewardStructure getRewardStructure() + { + return rewardStructure; + } + + public void setRewardStructure(RewardStructure rewardStructure) + { + this.rewardStructure = rewardStructure; + } + + public String toString() + { + return getColumnName(); + } + + public boolean isStateReward() + { + return this.type == RewardStructureColumn.STATE_REWARD; + } + + public boolean isTransitionReward() + { + return this.type == RewardStructureColumn.TRANSITION_REWARD; + } + + public boolean isCumulativeReward() + { + return this.type == RewardStructureColumn.CUMULATIVE_REWARD; + } + + public void setStateReward() + { + this.type = RewardStructureColumn.STATE_REWARD; + } + + public void setTransitionReward() + { + this.type = RewardStructureColumn.TRANSITION_REWARD; + } + + public void setCumulativeReward() + { + this.type = RewardStructureColumn.CUMULATIVE_REWARD; + } + } + + public class RewardStructureValue + { + private RewardStructureColumn rewardStructureColumn; + private Double rewardValue; + private boolean hasChanged; + + private boolean rewardValueUnknown; + + public RewardStructureValue(RewardStructureColumn rewardStructureColumn, Double rewardValue) + { + this.rewardStructureColumn = rewardStructureColumn; + this.rewardValue = rewardValue; + this.hasChanged = true; + + this.rewardValueUnknown = false; + } + + public RewardStructureColumn getRewardStructureColumn() + { + return rewardStructureColumn; + } + + public void setRewardStructureColumn(RewardStructureColumn rewardStructureColumn) + { + this.rewardStructureColumn = rewardStructureColumn; + } + + public Double getRewardValue() + { + return rewardValue; + } + + public void setRewardValue(Double rewardValue) + { + this.rewardValue = rewardValue; + } + + public void setRewardValueUnknown(boolean unknown) + { + this.rewardValueUnknown = unknown; + } + + public boolean isRewardValueUnknown() + { + return this.rewardValueUnknown; + } + + public boolean hasChanged() + { + return hasChanged; + } + + public void setChanged(boolean hasChanged) + { + this.hasChanged = hasChanged; + } + } +}