[mc] Use std::list for LivenessChecker::visited_pairs

diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp
index b2d9553..c34552d 100644 (file)
--- a/src/mc/LivenessChecker.cpp
+++ b/src/mc/LivenessChecker.cpp
@@ -42,7 +42,7 @@ namespace mc {
 
 std::list<VisitedPair*> LivenessChecker::acceptance_pairs;
 std::list<Pair*> LivenessChecker::liveness_stack;
 
 std::list<VisitedPair*> LivenessChecker::acceptance_pairs;
 std::list<Pair*> LivenessChecker::liveness_stack;

-xbt_dynar_t LivenessChecker::visited_pairs;
+std::list<VisitedPair*> LivenessChecker::visited_pairs;

 
 VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, std::shared_ptr<simgrid::mc::State> graph_state)
 {
 
 VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, std::shared_ptr<simgrid::mc::State> graph_state)
 {


@@ -188,9 +188,9 @@ void LivenessChecker::prepare(void)
 {
   simgrid::mc::Pair* initial_pair = nullptr;
   mc_model_checker->wait_for_requests();
 {
   simgrid::mc::Pair* initial_pair = nullptr;
   mc_model_checker->wait_for_requests();

+

   acceptance_pairs.clear();
   acceptance_pairs.clear();

-  if(_sg_mc_visited > 0)
-    LivenessChecker::visited_pairs = xbt_dynar_new(sizeof(simgrid::mc::VisitedPair*), nullptr);
+  visited_pairs.clear();

 
   initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
   initial_global_state->prev_pair = 0;
 
   initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
   initial_global_state->prev_pair = 0;


@@ -298,14 +298,11 @@ int LivenessChecker::insertVisitedPair(simgrid::mc::VisitedPair* visited_pair, s
   else
     new_visited_pair = visited_pair;
 
   else
     new_visited_pair = visited_pair;
 

-  auto visited_pairs = simgrid::xbt::range<simgrid::mc::VisitedPair*>(LivenessChecker::visited_pairs);
-

   auto range = std::equal_range(visited_pairs.begin(), visited_pairs.end(),
     new_visited_pair, simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
 
   for (auto i = range.first; i != range.second; ++i) {
     simgrid::mc::VisitedPair* pair_test = *i;
   auto range = std::equal_range(visited_pairs.begin(), visited_pairs.end(),
     new_visited_pair, simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
 
   for (auto i = range.first; i != range.second; ++i) {
     simgrid::mc::VisitedPair* pair_test = *i;

-    std::size_t cursor = i - visited_pairs.begin();

     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(),
     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(),


@@ -319,8 +316,7 @@ int LivenessChecker::insertVisitedPair(simgrid::mc::VisitedPair* visited_pair, s
             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_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(LivenessChecker::visited_pairs, cursor, &pair_test);
-          xbt_dynar_insert_at(LivenessChecker::visited_pairs, cursor, &new_visited_pair);
+          *i = new_visited_pair;

           pair_test->visited_removed = 1;
           if (!pair_test->acceptance_pair
               || pair_test->acceptance_removed == 1)
           pair_test->visited_removed = 1;
           if (!pair_test->acceptance_pair
               || pair_test->acceptance_removed == 1)


@@ -331,20 +327,21 @@ int LivenessChecker::insertVisitedPair(simgrid::mc::VisitedPair* visited_pair, s
     }
   }
 
     }
   }
 

-  xbt_dynar_insert_at(LivenessChecker::visited_pairs, range.first - visited_pairs.begin(), &new_visited_pair);
+  visited_pairs.insert(range.first, new_visited_pair);

 
 

-  if ((ssize_t) visited_pairs.size() > _sg_mc_visited) {
+  if (visited_pairs.size() > (std::size_t) _sg_mc_visited) {

     int min2 = mc_stats->expanded_pairs;
     int min2 = mc_stats->expanded_pairs;

-    unsigned int index2 = 0;
-    for (std::size_t i = 0; i != (std::size_t) visited_pairs.size(); ++i) {
-      simgrid::mc::VisitedPair* pair_test = visited_pairs[i];
-      if (pair_test->num < min2) {
+
+    std::list<VisitedPair*>::iterator index2;
+    for (auto i = visited_pairs.begin(); i != visited_pairs.end(); ++i) {
+      if ((*i)->num < min2) {

         index2 = i;
         index2 = i;

-        min2 = pair_test->num;
+        min2 = (*i)->num;

       }
     }
       }
     }

-    simgrid::mc::VisitedPair* pair_test = nullptr;
-    xbt_dynar_remove_at(LivenessChecker::visited_pairs, index2, &pair_test);
+
+    simgrid::mc::VisitedPair* pair_test = *index2;
+    visited_pairs.erase(index2);

     pair_test->visited_removed = 1;
     if (!pair_test->acceptance_pair || pair_test->acceptance_removed)
       delete pair_test;
     pair_test->visited_removed = 1;
     if (!pair_test->acceptance_pair || pair_test->acceptance_removed)
       delete pair_test;

diff --git a/src/mc/LivenessChecker.hpp b/src/mc/LivenessChecker.hpp
index 6175f02..6f0cbff 100644 (file)
--- a/src/mc/LivenessChecker.hpp
+++ b/src/mc/LivenessChecker.hpp
@@ -85,7 +85,7 @@ private:
 public: // (non-static wannabe) fields
   static std::list<VisitedPair*> acceptance_pairs;
   static std::list<Pair*> liveness_stack;
 public: // (non-static wannabe) fields
   static std::list<VisitedPair*> acceptance_pairs;
   static std::list<Pair*> liveness_stack;

-  static xbt_dynar_t visited_pairs;
+  static std::list<VisitedPair*> visited_pairs;

 };
 
 }
 };
 
 }