Added loadPath methods to SimulatorEngine and GUISimulator; not used currently.

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

prism/src/simulator/SimulatorEngine.java

@@ -435,6 +435,43 @@ public class SimulatorEngine
 		transitionListState = null;
 	}
 
+	/**
+	 * Construct a path through a model to match a supplied path,
+	 * specified as a PathFullInfo object.
+	 * Note: All constants in the model must have already been defined.
+	 * @param modulesFile Model for simulation
+	 * @param newPath Path to match
+	 */
+	public void loadPath(ModulesFile modulesFile, PathFullInfo newPath) throws PrismException
+	{
+		int i, j, numSteps, numTrans;
+		boolean found;
+		State state, nextState;
+		createNewPath(modulesFile);
+		numSteps = newPath.size();
+		if (numSteps == 0)
+			return;
+		state = newPath.getState(0);
+		initialisePath(state);
+		for (i = 0; i < numSteps; i++) {
+			nextState = newPath.getState(i + 1);
+			// Find matching transition
+			// (just look at states for now)
+			numTrans = transitionList.getNumTransitions();
+			found = false;
+			for (j = 0; j < numTrans; j++) {
+				if (transitionList.computeTransitionTarget(j, state).equals(nextState)) {
+					found = true;
+					manualTransition(j);
+					break;
+				}
+			}
+			if (!found)
+				throw new PrismException("Path loading failed at step " + (i + 1));
+			state = nextState;
+		}
+	}
+	
 	// ------------------------------------------------------------------------------
 	// Methods for adding/querying labels and properties
 	// ------------------------------------------------------------------------------

prism/src/userinterface/simulator/GUISimulator.java

@@ -602,6 +602,34 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 		}
 	}
 
+	public void a_loadPath(PathFullInfo pathNew)
+	{
+		try {
+			// Insert path table
+			tableScroll.setViewportView(pathTable);
+
+			displayPathLoops = true;
+
+			// Load new path into the simulator 
+			engine.loadPath(parsedModel, pathNew);
+			// Update model/path/tables/lists
+			setPathActive(true);
+			pathTableModel.setPath(engine.getPathFull());
+			pathTableModel.restartPathTable();
+			pathTable.getSelectionModel().setSelectionInterval(0, 0);
+			updateTableModel.restartUpdatesTable();
+			//repopulateFormulae(pf);
+			// Update display
+			repaintLists();
+			updatePathInfoAll(null);
+			doEnables();
+
+		} catch (PrismException e) {
+			this.error(e.getMessage());
+			setComputing(false);
+		}
+	}
+
 	public void a_exportPath()
 	{
 		try {