Refactoring: detach GUI simulator path table from SimulatorEngine and attach to PathFull.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3445 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/simulator/SimulatorEngine.java

@@ -977,6 +977,16 @@ public class SimulatorEngine
 	// Querying of current path (full paths only)
 	// ------------------------------------------------------------------------------
 
+	/**
+	 * Get access to the {@code PathFull} object storing the current path.
+	 * (Not applicable for on-the-fly paths)
+	 * This object is only valid until the next time {@link #createNewPath} is called. 
+	 */
+	public PathFull getPathFull()
+	{
+		return (PathFull) path;
+	}
+	
 	/**
 	 * Get the value of a variable at a given step of the path.
 	 * (Not applicable for on-the-fly paths)

prism/src/userinterface/simulator/GUISimulator.java

@@ -82,7 +82,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 		this.engine = gui.getPrism().getSimulator();
 
 		view = new SimulationView(this, gui.getPrism().getSettings());
-		pathTableModel = new GUISimulatorPathTableModel(this, engine, view);
+		pathTableModel = new GUISimulatorPathTableModel(this, view);
 
 		updateTableModel = new UpdateTableModel();
 
@@ -114,7 +114,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 
 		pathTablePlaceHolder.addMouseListener(this);
 
-		view.refreshToDefaultView(engine, pathActive, parsedModel);
+		view.refreshToDefaultView(pathActive, parsedModel);
 
 		setPathActive(false);
 		doEnables();
@@ -360,6 +360,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 
 			// Create a new path in the simulator and add labels/properties 
 			engine.createNewPath(parsedModel);
+			pathTableModel.setPath(engine.getPathFull());
 			setPathActive(true);
 			engine.initialisePath(initialState == null ? null : new parser.State(initialState, parsedModel));
 			repopulateFormulae(pf);

prism/src/userinterface/simulator/GUISimulatorPathTableModel.java

@@ -31,7 +31,7 @@ package userinterface.simulator;
 import java.util.*;
 import javax.swing.table.AbstractTableModel;
 
-import simulator.SimulatorEngine;
+import simulator.PathFull;
 import userinterface.simulator.SimulationView.*;
 import userinterface.util.GUIGroupedTableModel;
 import parser.ast.*;
@@ -41,21 +41,20 @@ public class GUISimulatorPathTableModel extends AbstractTableModel implements GU
 	private static final long serialVersionUID = 1L;
 
 	private GUISimulator simulator;
-	private SimulatorEngine engine;
 	private SimulationView view;
 
 	private boolean pathActive;
 	private ModulesFile parsedModel;
+	private PathFull path; 
 
 	private RewardStructureValue rewardStructureValue;
 	private VariableValue variableValue;
 	private TimeValue timeValue;
 	private ActionValue actionValue;
 
-	public GUISimulatorPathTableModel(GUISimulator simulator, SimulatorEngine engine, SimulationView view)
+	public GUISimulatorPathTableModel(GUISimulator simulator, SimulationView view)
 	{
 		this.simulator = simulator;
-		this.engine = engine;
 		this.view = view;
 		this.view.addObserver(this);
 
@@ -68,6 +67,11 @@ public class GUISimulatorPathTableModel extends AbstractTableModel implements GU
 		this.pathActive = pathActive;
 	}
 
+	public void setPath(PathFull path)
+	{
+		this.path = path;
+	}
+
 	public void setParsedModel(ModulesFile parsedModel)
 	{
 		this.parsedModel = parsedModel;
@@ -395,7 +399,7 @@ public class GUISimulatorPathTableModel extends AbstractTableModel implements GU
 	public int getRowCount()
 	{
 		// Return current path size if there is an active path.
-		return (pathActive ? engine.getPathSize() + 1 : 0);
+		return (pathActive ? path.size() + 1 : 0);
 	}
 
 	public boolean shouldColourRow(int row)
@@ -499,7 +503,7 @@ public class GUISimulatorPathTableModel extends AbstractTableModel implements GU
 
 			// The action column
 			if (actionStart <= columnIndex && columnIndex < stepStart) {
-				actionValue = view.new ActionValue(rowIndex == 0 ? "" : engine.getModuleOrActionOfPathStep(rowIndex - 1));
+				actionValue = view.new ActionValue(rowIndex == 0 ? "" : path.getModuleOrAction(rowIndex - 1));
 				actionValue.setActionValueUnknown(false);
 				return actionValue;
 			}
@@ -509,23 +513,23 @@ public class GUISimulatorPathTableModel extends AbstractTableModel implements GU
 			}
 			// Cumulative time column
 			else if (cumulativeTimeStart <= columnIndex && columnIndex < timeStart) {
-				timeValue = view.new TimeValue(engine.getCumulativeTimeUpToPathStep(rowIndex), true);
-				timeValue.setTimeValueUnknown(rowIndex > engine.getPathSize()); // Never unknown
+				timeValue = view.new TimeValue(path.getCumulativeTime(rowIndex), true);
+				timeValue.setTimeValueUnknown(rowIndex > path.size()); // Never unknown
 				return timeValue;
 			}
 			// Time column
 			else if (timeStart <= columnIndex && columnIndex < varStart) {
-				timeValue = view.new TimeValue(engine.getTimeSpentInPathStep(rowIndex), false);
-				timeValue.setTimeValueUnknown(rowIndex >= engine.getPathSize());
+				timeValue = view.new TimeValue(path.getTime(rowIndex), false);
+				timeValue.setTimeValueUnknown(rowIndex >= path.size());
 				return timeValue;
 			}
 			// A variable column
 			else if (varStart <= columnIndex && columnIndex < rewardStart) {
-				Variable var = ((Variable) view.getVisibleVariables().get(columnIndex - varStart));
-				Object result = engine.getVariableValueOfPathStep(rowIndex, var.getIndex());
+				Variable var = view.getVisibleVariables().get(columnIndex - varStart);
+				Object result = path.getState(rowIndex).varValues[var.getIndex()];
 				variableValue.setVariable(var);
 				variableValue.setValue(result);
-				variableValue.setChanged(rowIndex == 0 || !engine.getVariableValueOfPathStep(rowIndex - 1, var.getIndex()).equals(result));
+				variableValue.setChanged(rowIndex == 0 || !path.getState(rowIndex - 1).varValues[var.getIndex()].equals(result));
 				return variableValue;
 			}
 			// A reward column
@@ -535,27 +539,27 @@ public class GUISimulatorPathTableModel extends AbstractTableModel implements GU
 				rewardStructureValue.setRewardValueUnknown(false);
 				// A state reward column
 				if (rewardColumn.isStateReward()) {
-					double value = engine.getStateRewardOfPathStep(rowIndex, rewardColumn.getRewardStructure().getIndex());
+					double value = path.getStateReward(rowIndex, rewardColumn.getRewardStructure().getIndex());
 					rewardStructureValue.setChanged(rowIndex == 0
-							|| value != engine.getStateRewardOfPathStep(rowIndex - 1, rewardColumn.getRewardStructure().getIndex()));
+							|| value != path.getStateReward(rowIndex - 1, rewardColumn.getRewardStructure().getIndex()));
 					rewardStructureValue.setRewardValue(new Double(value));
-					rewardStructureValue.setRewardValueUnknown(rowIndex > engine.getPathSize()); // Never unknown
+					rewardStructureValue.setRewardValueUnknown(rowIndex > path.size()); // Never unknown
 				}
 				// A transition reward column
 				else if (rewardColumn.isTransitionReward()) {
-					double value = engine.getTransitionRewardOfPathStep(rowIndex, rewardColumn.getRewardStructure().getIndex());
+					double value = path.getTransitionReward(rowIndex, rewardColumn.getRewardStructure().getIndex());
 					rewardStructureValue.setChanged(rowIndex == 0
-							|| value != engine.getTransitionRewardOfPathStep(rowIndex - 1, rewardColumn.getRewardStructure().getIndex()));
+							|| value != path.getTransitionReward(rowIndex - 1, rewardColumn.getRewardStructure().getIndex()));
 					rewardStructureValue.setRewardValue(new Double(value));
-					rewardStructureValue.setRewardValueUnknown(rowIndex >= engine.getPathSize());
+					rewardStructureValue.setRewardValueUnknown(rowIndex >= path.size());
 				}
 				// A cumulative reward column
 				else {
-					double value = engine.getCumulativeRewardUpToPathStep(rowIndex, rewardColumn.getRewardStructure().getIndex());
+					double value = path.getCumulativeReward(rowIndex, rewardColumn.getRewardStructure().getIndex());
 					rewardStructureValue.setChanged(rowIndex == 0
-							|| value != (engine.getCumulativeRewardUpToPathStep(rowIndex - 1, rewardColumn.getRewardStructure().getIndex())));
+							|| value != (path.getCumulativeReward(rowIndex - 1, rewardColumn.getRewardStructure().getIndex())));
 					rewardStructureValue.setRewardValue(new Double(value));
-					rewardStructureValue.setRewardValueUnknown(rowIndex > engine.getPathSize()); // Never unknown
+					rewardStructureValue.setRewardValueUnknown(rowIndex > path.size()); // Never unknown
 				}
 				return rewardStructureValue;
 			}
@@ -570,7 +574,7 @@ public class GUISimulatorPathTableModel extends AbstractTableModel implements GU
 	 */
 	public void restartPathTable()
 	{
-		view.refreshToDefaultView(engine, pathActive, parsedModel);
+		view.refreshToDefaultView(pathActive, parsedModel);
 	}
 
 	/** 
@@ -583,17 +587,17 @@ public class GUISimulatorPathTableModel extends AbstractTableModel implements GU
 
 	public boolean isPathLooping()
 	{
-		return engine.isPathLooping();
+		return path.isLooping();
 	}
 
 	public int getLoopStart()
 	{
-		return engine.loopStart();
+		return path.loopStart();
 	}
 
 	public int getLoopEnd()
 	{
-		return engine.loopEnd();
+		return path.loopEnd();
 	}
 
 	public SimulationView getView()

prism/src/userinterface/simulator/SimulationView.java

@@ -33,7 +33,6 @@ import java.util.*;
 import parser.ast.*;
 import parser.type.Type;
 import prism.PrismSettings;
-import simulator.SimulatorEngine;
 import userinterface.simulator.GUIViewDialog.RewardListItem;
 
 /**
@@ -189,7 +188,7 @@ public class SimulationView extends Observable
 		}
 	}
 
-	public void refreshToDefaultView(SimulatorEngine engine, boolean pathActive, ModulesFile parsedModel)
+	public void refreshToDefaultView(boolean pathActive, ModulesFile parsedModel)
 	{
 		// First see if we can get away with using current settings...
 		boolean canUseCurrentView = true;
@@ -212,13 +211,18 @@ public class SimulationView extends Observable
 			for (Variable var : hiddenVariables)
 				allVarNames.add(var.getName());
 
-			for (int i = 0; i < engine.getNumVariables(); i++) {
-				if (allVarNames.contains(engine.getVariableName(i)))
-					allVarNames.remove(engine.getVariableName(i));
-				else
-					// Cannot use current view if a variable is not there.
+			// Cannot use current view if a variable is not there.
+			for (int g = 0; g < parsedModel.getNumGlobals(); g++) {
+				if (!allVarNames.remove(parsedModel.getGlobal(g).getName()))
 					canUseCurrentView = false;
 			}
+			for (int m = 0; m < parsedModel.getNumModules(); m++) {
+				Module module = parsedModel.getModule(m);
+				for (int v = 0; v < module.getNumDeclarations(); v++) {
+					if (!allVarNames.remove(module.getDeclaration(v).getName()))
+						canUseCurrentView = false;
+				}
+			}
 
 			// Cannot use current view if we have too many variables.
 			if (allVarNames.size() > 0)
@@ -265,8 +269,17 @@ public class SimulationView extends Observable
 			rewards.clear();
 
 			{
-				for (int i = 0; i < engine.getNumVariables(); i++) {
-					visibleVariables.add(new Variable(i, engine.getVariableName(i), engine.getVariableType(i)));
+				int i = 0;
+				for (int g = 0; g < parsedModel.getNumGlobals(); g++) {
+					visibleVariables.add(new Variable(i, parsedModel.getGlobal(g).getName(), parsedModel.getGlobal(g).getType()));
+					i++;
+				}
+				for (int m = 0; m < parsedModel.getNumModules(); m++) {
+					Module module = parsedModel.getModule(m);
+					for (int v = 0; v < module.getNumDeclarations(); v++) {
+						visibleVariables.add(new Variable(i, module.getDeclaration(v).getName(), module.getDeclaration(v).getType()));
+						i++;
+					}
 				}
 
 				for (int r = 0; r < parsedModel.getNumRewardStructs(); r++) {