Backport some changes from feature branch, such as making the flaw se…

…arch complete.
jendrikseipp · Dec 10, 2023 · 9ec1210 · 9ec1210
1 parent db5cd29
commit 9ec1210
Show file tree

Hide file tree

Showing 5 changed files with 14 additions and 19 deletions.
diff --git a/misc/style/run-clang-tidy.py b/misc/style/run-clang-tidy.py
@@ -54,6 +54,7 @@ def check_search_code_with_clang_tidy():
         "readability-avoid-const-params-in-decls",
         # "readability-braces-around-statements",
         "readability-container-size-empty",
+        "readability-const-return-type",
         "readability-delete-null-pointer",
         "readability-deleted-default",
         # "readability-else-after-return",

diff --git a/src/search/cartesian_abstractions/cegar.cc b/src/search/cartesian_abstractions/cegar.cc
@@ -53,10 +53,10 @@ CEGAR::CEGAR(
 
     if (log.is_at_least_normal()) {
         log << "Start building abstraction." << endl;
-        log << "Time limit: " << timer.get_remaining_time() << endl;
         log << "Maximum number of states: " << max_states << endl;
         log << "Maximum number of transitions: "
             << max_non_looping_transitions << endl;
+        log << "Maximum time: " << timer.get_remaining_time() << endl;
     }
 
     refinement_loop();

diff --git a/src/search/cartesian_abstractions/cost_saturation.cc b/src/search/cartesian_abstractions/cost_saturation.cc
@@ -258,8 +258,8 @@ void CostSaturation::print_statistics(utils::Duration init_time) const {
         log << "Done initializing additive Cartesian heuristic" << endl;
         log << "Time for initializing additive Cartesian heuristic: "
             << init_time << endl;
-        log << "Cartesian abstractions built: " << heuristic_functions.size() << endl;
-        log << "Cartesian states: " << num_states << endl;
+        log << "Cartesian abstractions: " << heuristic_functions.size() << endl;
+        log << "Total number of Cartesian states: " << num_states << endl;
         log << "Total number of non-looping transitions: "
             << num_non_looping_transitions << endl;
         log << endl;

diff --git a/src/search/cartesian_abstractions/flaw_search.cc b/src/search/cartesian_abstractions/flaw_search.cc
@@ -383,18 +383,10 @@ SearchStatus FlawSearch::search_for_flaws(const utils::CountdownTimer &cegar_tim
 
         int current_num_expanded_states = num_overall_expanded_concrete_states -
             num_expansions_in_prev_searches;
-        if (current_num_expanded_states >= max_state_expansions) {
-            // Expansion limit reached.
-            if (flawed_states.num_abstract_states() == 0) {
-                // No flaw found.
-                // TODO: Why release memory padding here?
-                utils::release_extra_memory_padding();
-                log << "Expansion limit reached with no flaw." << endl;
-                search_status = TIMEOUT;
-            } else {
-                log << "Expansion limit reached with flaws." << endl;
-                search_status = FAILED;
-            }
+        // To remain complete, only take the expansions limit into account once at least one flaw has been found.
+        if (current_num_expanded_states >= max_state_expansions && flawed_states.num_abstract_states() > 0) {
+            log << "Expansion limit reached with flaws." << endl;
+            search_status = FAILED;
             break;
         }
         search_status = step();
@@ -425,7 +417,6 @@ SearchStatus FlawSearch::search_for_flaws(const utils::CountdownTimer &cegar_tim
 unique_ptr<Split> FlawSearch::get_single_split(const utils::CountdownTimer &cegar_timer) {
     auto search_status = search_for_flaws(cegar_timer);
 
-    // Memory padding
     if (search_status == TIMEOUT)
         return nullptr;
 
@@ -499,7 +490,6 @@ FlawSearch::get_min_h_batch_split(const utils::CountdownTimer &cegar_timer) {
         }
     }
 
-    // Memory padding
     if (search_status == TIMEOUT)
         return nullptr;
 

diff --git a/src/search/cartesian_abstractions/transition.h b/src/search/cartesian_abstractions/transition.h
@@ -30,9 +30,13 @@ struct Transition {
         return op_id == other.op_id && target_id == other.target_id;
     }
 
+    bool operator!=(const Transition &other) const {
+        return !(*this == other);
+    }
+
     bool operator<(const Transition &other) const {
-        return op_id < other.op_id ||
-               (op_id == other.op_id && target_id < other.target_id);
+        return std::tie(op_id, target_id)
+               < std::tie(other.op_id, other.target_id);
     }
 
     friend std::ostream &operator<<(std::ostream &os, const Transition &t) {