Added time-bound exploration option to the simulator. Needs make clean!

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

prism/include/SimulatorEngine.h

@@ -268,9 +268,17 @@ JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_makeManualUpdate__ID
  * Method:    doAutomaticChoices
  * Signature: (IZ)I
  */
-JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_doAutomaticChoices
+JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_doAutomaticChoices__IZ
   (JNIEnv *, jclass, jint, jboolean);
 
+/*
+ * Class:     simulator_SimulatorEngine
+ * Method:    doAutomaticChoices
+ * Signature: (DZ)I
+ */
+JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_doAutomaticChoices__DZ
+  (JNIEnv *, jclass, jdouble, jboolean);
+
 /*
  * Class:     simulator_SimulatorEngine
  * Method:    doBacktrack

prism/include/simengine.h

@@ -134,6 +134,9 @@ int Engine_Make_Manual_Update(int index, double time_in_state);
 int Engine_Do_Automatic_Choices(int n);
 int Engine_Do_Automatic_Choices(int n, bool detect);
 
+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_Remove_Preceding_States(int step);

prism/include/simpath.h

@@ -116,6 +116,12 @@ void Manual_Update(int, double time_in_state);
 void Automatic_Choices(int n);
 void Automatic_Choices(int n, bool detect);
 
+/*
+ *	Make automatic updates untill time is passed, and stores the path.
+ */
+void Automatic_Choices(double time);
+void Automatic_Choices(double time, bool detect);
+
 /*
  *	Removes all states following the given index from
  *	the path and sets the state_variables to that state.

prism/src/simulator/SimulatorEngine.cc

@@ -363,8 +363,8 @@ JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_makeManualUpdate__ID
 	return 0;
 }
 
-JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_doAutomaticChoices
-(JNIEnv *env, jclass cls, jint n, jboolean detect)
+JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_doAutomaticChoices__IZ
+  (JNIEnv *, jclass, jint n, jboolean detect)
 {
 	try
 	{
@@ -378,6 +378,21 @@ JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_doAutomaticChoices
 	return 0;
 }
 
+JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_doAutomaticChoices__DZ
+  (JNIEnv *, jclass, jdouble time, jboolean detect)
+{
+	try
+	{
+		Automatic_Choices((double)time, (bool)detect);
+	}
+	catch(string str)
+	{
+		cout << str << endl;
+		return simulator_SimulatorEngine_ERROR;
+	}  
+	return 0;
+}
+
 JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_doBacktrack
 (JNIEnv *env, jclass cls, jint step)
 {

prism/src/simulator/SimulatorEngine.java

@@ -1221,11 +1221,41 @@ public class SimulatorEngine
 			throw new SimulatorException(getLastErrorMessage());
 	}
 	
+	/**
+	 * This function makes a number of automatic choices of updates to the global
+	 * state, untill `time' has passed.
+	 * @param time is the length of time to pass.
+	 * @throws SimulatorException if something goes wrong when updating the state.
+	 */
+	public void automaticChoices(double time) throws SimulatorException
+	{
+		automaticChoices(time, true);
+	}
+		
+	/**
+	 * This function makes n automatic choices of updates to the global
+	 * state, untill `time' has passed.
+	 * @param time is the length of time to pass.
+	 * @param detect whether to employ loop detection.
+	 * @throws SimulatorException if something goes wrong when updating the state.
+	 */
+	public void automaticChoices(double time, boolean detect) throws SimulatorException
+	{
+		int result = doAutomaticChoices(time, detect);
+		if(result == ERROR)
+			throw new SimulatorException(getLastErrorMessage());
+	}
+	
 	/**
 	 *	Ask c++ engine to make n automatic updates to the global state.
 	 */
 	private static native int doAutomaticChoices(int n, boolean detect);
 	
+	/**
+	 *	Ask c++ engine to make some automatic updates to the global state, up to some time.
+	 */
+	private static native int doAutomaticChoices(double time, boolean detect);
+	
 	/**
 	 * This function backtracks the current path to the state of the
 	 * given index

prism/src/simulator/simengine.cc

@@ -360,6 +360,24 @@ int Engine_Do_Automatic_Choices(int n, bool detect)
 	return 0;
 }
 
+int Engine_Do_Automatic_Choices(double time)
+{
+	return Engine_Do_Automatic_Choices(time, true);
+}
+
+int Engine_Do_Automatic_Choices(double time, bool detect)
+{
+	try
+	{
+		Automatic_Choices(time, detect);
+	}
+	catch(char* str)
+	{
+		return ERROR;
+	}  
+	return 0;
+}
+
 int Engine_Do_Backtrack(int step)
 {
 	try

prism/src/simulator/simpath.cc

@@ -385,6 +385,71 @@ void Automatic_Choices(int n, bool detect)
 	}
 }
 
+/*
+*	Make choices untill time has passed and update the path.
+*/
+void Automatic_Choices(double time){ Automatic_Choices(time, true); }
+
+void Automatic_Choices(double time, bool detect)
+{
+	if (model_type != STOCHASTIC)
+		Automatic_Choices((int)ceil(time), detect);
+	else
+	{				
+		double startTime = path_timer;
+		double currentTime = startTime;
+			
+		while (currentTime - startTime < time)
+		{	
+			/* Break when looping. */
+			if (detect && loop_detection->Is_Proven_Looping()) 
+				break;
+				
+			/* Break when deadlocking. */
+			if (loop_detection->Is_Deadlock()) 
+				break;
+					
+			double probability = 0.0;
+			Automatic_Update(loop_detection, probability);
+			
+			// Because we cannot guarantee that we know the selected index, we have to show this.
+			stored_path[current_index]->choice_made = PATH_NO_CHOICE_MADE;
+			stored_path[current_index]->probability = probability;
+			
+			// Unless requested not to (detect==false), this function will stop exploring when a loop is detected.
+			// Because Automatic_Update() checks for loops before making a transition, we overshoot.
+			// Hence at this point if we are looping we step back a state,
+			// i.e. reset state_variables and don't add new state to the path.
+			
+			if (detect && loop_detection->Is_Proven_Looping()) 
+			{
+				stored_path[current_index]->Make_Current_State_This();
+			}
+			else 
+			{						
+				// Add state to path (unless we have stayed in the same state because of deadlock).
+				if (!loop_detection->Is_Deadlock()) 
+					Add_Current_State_To_Path();	
+				currentTime = path_timer;
+			}
+			
+			Calculate_State_Reward(state_variables);
+		}
+		
+		Calculate_Updates(state_variables);
+		
+		// check for looping
+		if(Are_Updates_Deterministic())
+		{
+			loop_detection->Notify_Deterministic_State(false);
+		}
+		else
+		{
+			loop_detection->Notify_Deterministic_Path_End();
+		}
+	}
+}
+
 /*
 *	Removes all states following the given index from
 *	the path and sets the state_variables to that state.

prism/src/userinterface/simulator/GUISimulator.java

@@ -292,11 +292,11 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 			typeExploreCombo.addItem("Steps");
 			typeExploreCombo.addItem("Up to step");
 			
-			/*if (mf != null && mf.getType() == ModulesFile.STOCHASTIC)
+			if (mf != null && mf.getType() == ModulesFile.STOCHASTIC)
 			{
 				typeExploreCombo.addItem("Time");
 				typeExploreCombo.addItem("Up to time");
-			}*/
+			}
 					
 			typeBacktrackCombo.setEnabled(pathActive);
 			typeBacktrackCombo.removeAllItems();
@@ -453,7 +453,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 		}
 	}
 	
-	/** Backtracks a number of steps. */
+	/** Explore a number of steps. */
 	public void a_autoStep(int noSteps)
 	{		
 		try
@@ -494,6 +494,49 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 		}
 	}	
 	
+	/** Explore an amount of time. */
+	public void a_autoStep(double time)
+	{		
+		try
+		{										
+			if (displayPathLoops && pathTableModel.isPathLooping())
+			{
+				if (questionYesNo("A loop in the path has been detected. Do you wish to disable loop detection and extend the path?") == 0) 
+				{
+					displayPathLoops = false;
+					pathTable.repaint();
+				}
+				else return;
+			}
+				
+			setComputing(true);
+				
+			if(isOldUpdate())
+			{
+				engine.finishedWithOldUpdates();
+			}
+			
+			engine.automaticChoices(time, displayPathLoops);		
+												
+			pathTableModel.updatePathTable();
+			updateTableModel.updateUpdatesTable();
+			pathTable.scrollRectToVisible(new Rectangle(0, (int)pathTable.getPreferredSize().getHeight() - 10, (int)pathTable.getPreferredSize().getWidth(), (int)pathTable.getPreferredSize().getHeight()) );
+			
+			totalTimeLabel.setText(PrismUtils.formatDouble(this.getPrism().getSettings(), engine.getTotalPathTime()));
+			pathLengthLabel.setText(""+(engine.getPathSize()-1));
+			
+			stateLabelList.repaint();
+			pathFormulaeList.repaint();
+			setComputing(false);
+		}		
+		catch(SimulatorException e)
+		{
+			this.error(e.getMessage());
+		}
+	}	
+	
+	
+	
 	/** Backtracks to a certain step. */	
 	public void a_backTrack(int step) throws SimulatorException
 	{
@@ -1565,18 +1608,18 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 				try
 				{
 					if (inputExploreField.getText().trim().length() == 0)
-							throw new SimulatorException("The \"Num. steps\" parameter is invalid.\nIt must be a positive integer, but it is currently empty");
+						throw new NumberFormatException();
 					
 					noSteps = Integer.parseInt(inputExploreField.getText().trim());
 					
 					if (noSteps <= 0) 
-								throw new SimulatorException("The \"Num. steps\" parameter is invalid.\nIt must be a positive integer");
+						throw new NumberFormatException();
 
 					a_autoStep(noSteps);
 				}
 				catch (NumberFormatException nfe)
 				{
-						throw new SimulatorException("The \"Num. steps\" parameter is invalid.\nThe current input (\""+inputExploreField.getText().trim()+"\") is not a valid positive integer");
+					throw new SimulatorException("The \"Steps\" parameter is invalid, it must be a positive integer.");
 				}
 			}
 			/* Update upto some state. */
@@ -1587,20 +1630,64 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 				try
 				{
 					if (inputExploreField.getText().trim().length() == 0)
-							throw new SimulatorException("The \"To state\" parameter is invalid.\nIt must be a positive integer larger than the index of the current state ("+(engine.getPathSize()-1)+"), but it is currently empty");
+						throw new NumberFormatException();
 					
 					uptoState = Integer.parseInt(inputExploreField.getText().trim());
 					
 					if (uptoState < engine.getPathSize()) 
-								throw new SimulatorException("The \"To state\" parameter is invalid.\nIt must be a positive integer larger than the index of the current state ("+(engine.getPathSize()-1)+")");
+						throw new NumberFormatException();
 
 					a_autoStep(uptoState - engine.getPathSize() + 1);
 				}
 				catch (NumberFormatException nfe)
 				{
-						throw new SimulatorException("The \"To state\" parameter is invalid.\nThe current input (\""+inputExploreField.getText().trim()+"\") is not a valid positive integer");
+					throw new SimulatorException("The \"Up to state\" parameter is invalid, it must be a positive integer larger than the index of the current state (which is "+ (engine.getPathSize()-1)+")");
 				}
 			}
+			else if (typeExploreCombo.getSelectedIndex() == 2)
+			{
+				double time;
+				
+				try
+				{
+					if (inputExploreField.getText().trim().length() == 0)
+						throw new NumberFormatException();
+					
+					time = Double.parseDouble(inputExploreField.getText().trim());
+					
+					if (time < 0.0d) 
+						throw new NumberFormatException();
+
+					a_autoStep(time);
+				}
+				catch (NumberFormatException nfe)
+				{
+					throw new SimulatorException("The \"Time\" parameter is invalid, it must be a positive double");
+				}
+			}
+			else if (typeExploreCombo.getSelectedIndex() == 3)
+			{
+				double time;
+				double currentTime = engine.getTotalPathTime();
+				
+				try
+				{
+					if (inputExploreField.getText().trim().length() == 0)
+						throw new NumberFormatException();
+					
+					time = Double.parseDouble(inputExploreField.getText().trim());
+					
+					if (time <= currentTime) 
+						throw new NumberFormatException();
+
+					a_autoStep(time-currentTime);
+				}
+				catch (NumberFormatException nfe)
+				{
+					throw new SimulatorException("The \"Time\" parameter is invalid, it must be a positive double larger than the cumulative path time (which is currently " + currentTime+")");
+				}
+			}
+			
     	}
     	catch (SimulatorException se)
     	{