diff --git a/prism/include/SimulatorEngine.h b/prism/include/SimulatorEngine.h index 32e2b095..a663d911 100644 --- a/prism/include/SimulatorEngine.h +++ b/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 diff --git a/prism/include/simengine.h b/prism/include/simengine.h index c9b3c58a..aabaf554 100644 --- a/prism/include/simengine.h +++ b/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); diff --git a/prism/include/simpath.h b/prism/include/simpath.h index dcb1d56e..70ebeb15 100644 --- a/prism/include/simpath.h +++ b/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. diff --git a/prism/src/simulator/SimulatorEngine.cc b/prism/src/simulator/SimulatorEngine.cc index ef2e930e..27819c0d 100644 --- a/prism/src/simulator/SimulatorEngine.cc +++ b/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) { diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index ebfc22ef..39cb2466 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/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 diff --git a/prism/src/simulator/simpath.cc b/prism/src/simulator/simpath.cc index 6884b979..f4e268b7 100644 --- a/prism/src/simulator/simpath.cc +++ b/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. diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java index f292baeb..11833a3a 100644 --- a/prism/src/userinterface/simulator/GUISimulator.java +++ b/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) {