Added time-bounded backtracking. Does not work well when backtracking should be to the first state.

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

prism/include/SimulatorEngine.h

@@ -284,9 +284,17 @@ JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_doAutomaticChoices__DZ
  * Method:    doBacktrack
  * Signature: (I)I
  */
-JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_doBacktrack
+JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_doBacktrack__I
   (JNIEnv *, jclass, jint);
 
+/*
+ * Class:     simulator_SimulatorEngine
+ * Method:    doBacktrack
+ * Signature: (D)I
+ */
+JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_doBacktrack__D
+  (JNIEnv *, jclass, jdouble);
+
 /*
  * Class:     simulator_SimulatorEngine
  * Method:    doRemovePrecedingStates

prism/include/simengine.h

@@ -138,6 +138,7 @@ int Engine_Do_Automatic_Choices(double time);
 int Engine_Do_Automatic_Choices(double time, bool detect);
 
 int Engine_Do_Backtrack(int step);
+int Engine_Do_Backtrack(double time);
 
 int Engine_Do_Remove_Preceding_States(int step);
 

prism/include/simpath.h

@@ -128,6 +128,12 @@ void Automatic_Choices(double time, bool detect);
  */
 void Backtrack(int index);
 
+/*
+ *	Removes all states upto some given cumulative time
+ *	the path and sets the state_variables to that state.
+ */
+void Backtrack(double time);
+
 /*
  *	Removes all states preceding the given index from
  *	the path.

prism/src/simulator/SimulatorEngine.cc

@@ -393,12 +393,28 @@ JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_doAutomaticChoices__DZ
 	return 0;
 }
 
-JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_doBacktrack
+JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_doBacktrack__I
 (JNIEnv *env, jclass cls, jint step)
 {
 	try
 	{
-		Backtrack(step);
+		Backtrack((int)step);
+	}
+	catch(string str)
+	{
+		cout << str << endl;
+		return simulator_SimulatorEngine_ERROR;
+	}   
+	return 0;
+	
+}
+
+JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_doBacktrack__D
+(JNIEnv *env, jclass cls, jdouble time)
+{
+	try
+	{
+		Backtrack((double)time);
 	}
 	catch(string str)
 	{

prism/src/simulator/SimulatorEngine.java

@@ -1269,12 +1269,31 @@ public class SimulatorEngine
 			throw new SimulatorException(getLastErrorMessage());
 	}
 	
+	/**
+	 * This function backtracks the current path to a state where
+	 * the cumulative time is equal to the time parameter.
+	 * @param time the cumulative time to backtrack to.
+	 * @throws SimulatorException is something goes wrong when backtracking.
+	 */
+	public void backtrack(double time) throws SimulatorException
+	{
+		int result = doBacktrack(time);
+		if(result == ERROR)
+			throw new SimulatorException(getLastErrorMessage());
+	}
+	
 	/**
 	 *	Asks the c++ engine to backtrack to the given step.
 	 *	Returns OUTOFRANGE (=-1) if step is out of range
 	 */
 	private static native int doBacktrack(int step);
 	
+	/**
+	 *	Asks the c++ engine to backtrack to some given time of the path.
+	 *	Returns OUTOFRANGE (=-1) if time is out of range
+	 */
+	private static native int doBacktrack(double time);
+	
 	/**
 	 * This function removes states of the path that precede those of the given
 	 * index

prism/src/simulator/simpath.cc

@@ -502,6 +502,63 @@ void Backtrack(int step)
 	loop_detection->Backtrack(step);
 }
 
+/*
+*	Removes all states upto some given cumulative time.
+*	the path and sets the state_variables to that state.
+*/
+void Backtrack(double time)
+{
+	int errorCount = 0;
+	
+	// No need to do anything.
+	if (path_timer <= time)
+		return;
+	
+	// We want to find the state to backtrack to
+	// Find state by binary search (search between upper and lower inclusive)
+		
+	int upper, lower;
+	
+	upper = current_index - 1;
+	lower = 0;
+	
+	int target_index;
+	
+	while (true && errorCount++ < 100)
+	{
+		target_index = (upper - lower)/2 + lower;
+		
+		// Termination case
+		if (upper == lower)
+			break;		
+		
+		if (stored_path[target_index]->cumulative_time_spent_in_state > time)
+		{
+			// need to search lower
+			upper = target_index - 1;
+		}
+		else
+		{
+			// this is our target unless there is a later state that also satisfies <= time
+			if (upper - lower == 1)
+			{
+				// make sure we terminate in this case.
+				target_index = (stored_path[upper]->cumulative_time_spent_in_state <= time) ? upper : lower;
+					break;
+			}
+			else
+			{
+				lower = target_index;
+			}
+		}	
+	}
+	if (errorCount < 90)
+	{
+		if (target_index + 2 < current_index)
+			Backtrack(target_index + 2);
+	}
+}
+
 /*
 *	Removes all states preceding the given index from
 *	the path.

prism/src/userinterface/simulator/GUISimulator.java

@@ -304,11 +304,11 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 			typeBacktrackCombo.addItem("Steps");
 			typeBacktrackCombo.addItem("Back to step");
 			
-			/*if (mf != null && mf.getType() == ModulesFile.STOCHASTIC)
+			if (mf != null && mf.getType() == ModulesFile.STOCHASTIC)
 			{
 				typeBacktrackCombo.addItem("Time");
 				typeBacktrackCombo.addItem("Back to time");
-			}*/
+			}
 		}
 		catch(SimulatorException e)
 		{
@@ -535,7 +535,23 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 		}
 	}	
 	
-	
+	/** Backtracks to a certain time. */	
+	public void a_backTrack(double time) throws SimulatorException
+	{
+		setComputing(true);
+		
+		engine.backtrack(time);
+		
+		pathTableModel.updatePathTable();
+		updateTableModel.updateUpdatesTable();
+		
+		totalTimeLabel.setText(PrismUtils.formatDouble(this.getPrism().getSettings(), engine.getTotalPathTime()));
+		pathLengthLabel.setText(""+(engine.getPathSize()-1));
+		stateLabelList.repaint();
+		pathFormulaeList.repaint();
+		
+		setComputing(false);
+	}
 	
 	/** Backtracks to a certain step. */	
 	public void a_backTrack(int step) throws SimulatorException
@@ -1425,7 +1441,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 						noSteps = engine.getPathSize() - 1;
 					
 					if (noSteps < 0)
-						throw new SimulatorException("Cannot backtrack a negative number of steps, use explore instead");
+						throw new NumberFormatException();
 					else if (noSteps == 0)
 						return;				
 
@@ -1433,7 +1449,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 				}
 				catch (NumberFormatException nfe)
 				{
-					throw new SimulatorException("The \"Num. steps\" parameter is invalid.\nThe current input (\""+inputBacktrackField.getText().trim()+"\") is not a valid positive integer");
+					throw new SimulatorException("The \"Steps\" parameter is invalid, it must be a positive integer smaller than the current path length (which is "+engine.getPathSize()+")");
 				}
 			}
 			else if (typeBacktrackCombo.getSelectedIndex() == 1)
@@ -1448,15 +1464,60 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 					toState = Integer.parseInt(inputBacktrackField.getText().trim());
 					
 					if (toState < 0 || toState >= engine.getPathSize())
-						throw new SimulatorException("State with index \"" + toState + "\" does not exist in the current path");
+						throw new NumberFormatException();
 					
 					a_backTrack(toState);
 				}
 				catch (NumberFormatException nfe)
 				{
-					throw new SimulatorException("The \"Num. steps\" parameter is invalid.\nThe current input (\""+inputBacktrackField.getText().trim()+"\") is not a valid positive integer");
+					throw new SimulatorException("The \"Steps\" parameter is invalid, it must be a positive integer smaller than the current path length (which is "+engine.getPathSize()+")");
 				}
-			}			
+			}	
+			else if (typeBacktrackCombo.getSelectedIndex() == 2)
+			{		
+				double time;
+				
+				try
+				{
+					if (inputBacktrackField.getText().trim().length() == 0)
+						throw new NumberFormatException();
+					
+					time = Double.parseDouble(inputBacktrackField.getText().trim());
+										
+					if (time < 0) 
+						throw new NumberFormatException();
+					
+					if  (time >= engine.getTotalPathTime())
+						a_backTrack(0.0d);
+					else
+						a_backTrack(engine.getTotalPathTime() - time);
+				}
+				catch (NumberFormatException nfe)
+				{
+					throw new SimulatorException("The \"Time\" parameter is invalid, it must be a positive double smaller than the cumulative path time (which is "+engine.getTotalPathTime()+")");
+				}
+			}	
+			else if (typeBacktrackCombo.getSelectedIndex() == 3)
+			{
+				double time;
+				
+				try
+				{
+					if (inputBacktrackField.getText().trim().length() == 0)
+						throw new NumberFormatException();
+					
+					time = Double.parseDouble(inputBacktrackField.getText().trim());
+					
+					if (time < 0 || time >= engine.getTotalPathTime()) 
+						throw new NumberFormatException();
+					
+					a_backTrack(time);
+				}
+				catch (NumberFormatException nfe)
+				{
+					throw new SimulatorException("The \"Back to time\" parameter is invalid, it must be a positive double smaller than the cumulative path time (which is "+engine.getTotalPathTime()+")");
+				}
+			}	
     	}
     	catch (SimulatorException se)
     	{