[mc] Move some liveness code in the liveness file (private/static)

[simgrid.git] / src / mc / mc_visited.cpp

diff --git a/src/mc/mc_visited.cpp b/src/mc/mc_visited.cpp
index 19a9e2e..f030a59 100644 (file)
--- a/src/mc/mc_visited.cpp
+++ b/src/mc/mc_visited.cpp
@@ -28,7 +28,6 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc,
 namespace simgrid {
 namespace mc {
 
-xbt_dynar_t visited_pairs;
 std::vector<std::unique_ptr<simgrid::mc::VisitedState>> visited_states;
 
 static int is_exploration_stack_state(simgrid::mc::VisitedState* state){
@@ -391,92 +390,5 @@ std::unique_ptr<simgrid::mc::VisitedState> is_visited_state(mc_state_t graph_sta
     return nullptr;
 }
 
-/**
- * \brief Checks whether a given pair has already been visited by the algorithm.
- */
-int is_visited_pair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* pair) {
-
-  if (_sg_mc_visited == 0)
-    return -1;
-
-  simgrid::mc::VisitedPair* new_visited_pair = nullptr;
-  if (visited_pair == nullptr)
-    new_visited_pair = new simgrid::mc::VisitedPair(
-      pair->num, pair->automaton_state, pair->atomic_propositions.get(),
-      pair->graph_state);
-  else
-    new_visited_pair = visited_pair;
-
-  if (xbt_dynar_is_empty(visited_pairs)) {
-    xbt_dynar_push(visited_pairs, &new_visited_pair);
-    return -1;
-  }
-
-    int min = -1, max = -1, index;
-    //int res;
-    simgrid::mc::VisitedPair* pair_test;
-    int cursor;
-
-    index = get_search_interval(visited_pairs, new_visited_pair, &min, &max);
-
-    if (min != -1 && max != -1) {       // Visited pair with same number of processes and same heap bytes used exists
-      cursor = min;
-      while (cursor <= max) {
-        pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(visited_pairs, cursor, simgrid::mc::VisitedPair*);
-        if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
-          if (xbt_automaton_propositional_symbols_compare_value(
-              pair_test->atomic_propositions.get(),
-              new_visited_pair->atomic_propositions.get()) == 0) {
-            if (snapshot_compare(pair_test, new_visited_pair) == 0) {
-              if (pair_test->other_num == -1)
-                new_visited_pair->other_num = pair_test->num;
-              else
-                new_visited_pair->other_num = pair_test->other_num;
-              if (dot_output == nullptr)
-                XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
-              else
-                XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_visited_pair->num, pair_test->num, new_visited_pair->other_num);
-              xbt_dynar_remove_at(visited_pairs, cursor, &pair_test);
-              xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_pair);
-              pair_test->visited_removed = 1;
-              if (!pair_test->acceptance_pair
-                  || pair_test->acceptance_removed == 1)
-                delete pair_test;
-              return new_visited_pair->other_num;
-            }
-          }
-        }
-        cursor++;
-      }
-      xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair);
-    } else {
-      pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(visited_pairs, index, simgrid::mc::VisitedPair*);
-      if (pair_test->nb_processes < new_visited_pair->nb_processes)
-        xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
-      else if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used)
-        xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
-      else
-        xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair);
-    }
-
-    if ((ssize_t) xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
-      int min2 = mc_stats->expanded_pairs;
-      unsigned int cursor2 = 0;
-      unsigned int index2 = 0;
-      xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
-        if (!mc_model_checker->is_important_snapshot(*pair_test->graph_state->system_state)
-            && pair_test->num < min2) {
-          index2 = cursor2;
-          min2 = pair_test->num;
-        }
-      }
-      xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
-      pair_test->visited_removed = 1;
-      if (!pair_test->acceptance_pair || pair_test->acceptance_removed)
-        delete pair_test;
-    }
-  return -1;
-}
-
 }
 }
\ No newline at end of file