Browse Source
Re-factoring of GUI simulator code.
Re-factoring of GUI simulator code.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3443 bbc10eb1-c90d-0410-af57-cb519fbb1720master
Dave Parker
15 years ago
6 changed files with 2261 additions and 2261 deletions
-
1303prism/src/userinterface/simulator/GUISimulator.java
-
438prism/src/userinterface/simulator/GUISimulatorPathTable.java
-
610prism/src/userinterface/simulator/GUISimulatorPathTableModel.java
-
235prism/src/userinterface/simulator/GUITimeDialog.java
-
1277prism/src/userinterface/simulator/GUIViewDialog.java
-
659prism/src/userinterface/simulator/SimulationView.java
1303
prism/src/userinterface/simulator/GUISimulator.java
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
@ -0,0 +1,610 @@ |
|||
//============================================================================== |
|||
// |
|||
// Copyright (c) 2002- |
|||
// Authors: |
|||
// * Andrew Hinton <ug60axh@cs.bham.ac.uk> (University of Birmingham) |
|||
// * Mark Kattenbelt <mark.kattenbelt@comlab.ox.ac.uk> (University of Oxford, formerly University of Birmingham) |
|||
// * Dave Parker <david.parker@comlab.ox.ac.uk> (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<Variable> vars = view.getVisibleVariables(); |
|||
Set<String> varNames = new HashSet<String>(); |
|||
|
|||
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<Variable> vars = view.getVisibleVariables(); |
|||
Set<String> varNames = new HashSet<String>(); |
|||
|
|||
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<Variable> vars = view.getVisibleVariables(); |
|||
Set<String> varNames = new HashSet<String>(); |
|||
|
|||
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<Variable> vars = view.getVisibleVariables(); |
|||
Set<String> varNames = new HashSet<String>(); |
|||
|
|||
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); |
|||
} |
|||
} |
|||
1277
prism/src/userinterface/simulator/GUIViewDialog.java
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
@ -0,0 +1,659 @@ |
|||
//============================================================================== |
|||
// |
|||
// Copyright (c) 2002- |
|||
// Authors: |
|||
// * Andrew Hinton <ug60axh@cs.bham.ac.uk> (University of Birmingham) |
|||
// * Mark Kattenbelt <mark.kattenbelt@comlab.ox.ac.uk> (University of Oxford, formerly University of Birmingham) |
|||
// * Dave Parker <david.parker@comlab.ox.ac.uk> (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<Variable> visibleVariables; |
|||
private ArrayList<Variable> hiddenVariables; |
|||
|
|||
private ArrayList<RewardStructureColumn> visibleRewardColumns; |
|||
private ArrayList<RewardStructure> 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<Variable>(); |
|||
this.hiddenVariables = new ArrayList<Variable>(); |
|||
|
|||
this.visibleRewardColumns = new ArrayList<RewardStructureColumn>(); |
|||
this.rewards = new ArrayList<RewardStructure>(); |
|||
|
|||
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<Variable> getVisibleVariables() |
|||
{ |
|||
return visibleVariables; |
|||
} |
|||
|
|||
public ArrayList<Variable> getHiddenVariables() |
|||
{ |
|||
return hiddenVariables; |
|||
} |
|||
|
|||
public void setVariableVisibility(ArrayList<Variable> visibleVariables, ArrayList<Variable> hiddenVariables) |
|||
{ |
|||
this.visibleVariables = visibleVariables; |
|||
this.hiddenVariables = hiddenVariables; |
|||
|
|||
this.setChanged(); |
|||
this.notifyObservers(); |
|||
} |
|||
|
|||
public ArrayList<RewardStructureColumn> getVisibleRewardColumns() |
|||
{ |
|||
return visibleRewardColumns; |
|||
} |
|||
|
|||
public void setVisibleRewardListItems(ArrayList<RewardListItem> visibleRewardListItems) |
|||
{ |
|||
ArrayList<RewardStructureColumn> visibleRewardColumns = new ArrayList<RewardStructureColumn>(); |
|||
|
|||
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<RewardStructure> 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<String> allVarNames = new TreeSet<String>(); |
|||
|
|||
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<RewardStructure> allrew = new ArrayList<RewardStructure>(); |
|||
|
|||
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) + ": <unnamed>"; |
|||
} |
|||
} |
|||
|
|||
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; |
|||
} |
|||
} |
|||
} |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue