From 0b65c69a6b3bd4ba60c55e2158ce7ae29f4b72da Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Sat, 13 Aug 2011 15:12:17 +0000
Subject: [PATCH] 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      | 37 +++++++++++++++++++
 .../userinterface/simulator/GUISimulator.java | 28 ++++++++++++++
 2 files changed, 65 insertions(+)

diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java
index 62c1a730..d8eb772d 100644
--- a/prism/src/simulator/SimulatorEngine.java
+++ b/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
 	// ------------------------------------------------------------------------------
diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java
index 21b16bb2..3cf5e2ac 100644
--- a/prism/src/userinterface/simulator/GUISimulator.java
+++ b/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 {