added timeout to search mode, set via --searchtimeout parameter

Author: sicco

source/main.cpp

@@ -162,6 +162,7 @@ int main(int argc, char *argv[]){
     app.add_option("--searchlocal", SEARCH_LOCAL, "Search using the local heuristic from the evaluation function. Default=0.");
     app.add_option("--searchglobal", SEARCH_GLOBAL, "Search using the global heuristic from the evaluation function. Default=0.");
     app.add_option("--searchpartial", SEARCH_PARTIAL, "Search using the partial heuristic from the evaluation function. Default=0.");
+    app.add_option("--searchtimeout", SEARCH_TIME_OUT, "Timeout in seconds for the search process. When exceeded, the search will finish the current run and return the best discovered solution. Default=600. Set to -1 to use no timeout.");
 
     app.add_option("--predictreset", PREDICT_RESET, "When predicting and there is no outgoing transition, the model is reset to the root state. This works well when using sliding windows. Default=0.");
     app.add_option("--predictremain", PREDICT_REMAIN, "When predicting and there is no outgoing transition, the model is looped back into the current state. Default=0.");

source/parameters.cpp

@@ -169,3 +169,5 @@ std::string POSTGRESQL_TBLNAME = "";
 bool POSTGRESQL_DROPTBLS = true;
 
 std::string PRINT_MODEL_PREFIX = ""; // TODO: delete this one
+
+int SEARCH_TIME_OUT = 600;

source/parameters.h

@@ -198,4 +198,6 @@ extern int DFA_SIZE_BOUND;
 extern int APTA_SIZE_BOUND;
 extern bool SAT_RUN_GREEDY;
 
+extern int SEARCH_TIME_OUT;
+
 #endif

source/running_modes/search_mode.cpp

@@ -14,6 +14,7 @@
 #include "common.h"
 
 #include <queue>
+#include <chrono>
 
 using namespace std;
 
@@ -160,7 +161,8 @@ void change_refinement_list(state_merger* merger, refinement_list* new_list){
 }
 
 int search_mode::run(){
-	start_size = merger->get_final_apta_size();
+    auto time_start = std::chrono::high_resolution_clock::now();
+    start_size = merger->get_final_apta_size();
     best_solution = -1;
     current_run = new refinement_list();
 
@@ -177,19 +179,23 @@ int search_mode::run(){
         MERGE_SINKS_WITH_CORE = temp_merge_sinks_core;
     }
 
-	add_to_q(merger);
+    add_to_q(merger);
 
     cerr << Q.size() << endl;
 
-	while(!Q.empty()){
-		pair<double, refinement_list*> next_refinements = Q.top();
-		change_refinement_list(merger, next_refinements.second);
-		Q.pop();
+    while(!Q.empty()){
+	pair<double, refinement_list*> next_refinements = Q.top();
+	change_refinement_list(merger, next_refinements.second);
+	Q.pop();
 
-		cerr << Q.size() << " " << current_refinements->size() << " " << next_refinements.first << endl;
+	cerr << Q.size() << " " << current_refinements->size() << " " << next_refinements.first << endl;
 
         add_to_q(merger);
-	}
+
+        if (SEARCH_TIME_OUT != -1 && std::chrono::high_resolution_clock::now() - time_start > std::chrono::seconds(SEARCH_TIME_OUT)) {
+            break;
+        }
+    }
 
     return EXIT_SUCCESS;
 }