Reduce the amount of MC locations reading the memory of the App

[simgrid.git] / src / mc / explo / LivenessChecker.cpp

diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp
index c467eee..64d9f36 100644 (file)
--- a/src/mc/explo/LivenessChecker.cpp
+++ b/src/mc/explo/LivenessChecker.cpp
@@ -27,7 +27,7 @@ VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state,
   if (not this->graph_state->get_system_state())
     this->graph_state->set_system_state(std::make_shared<Snapshot>(pair_num));
   this->heap_bytes_used     = Api::get().get_remote_heap_bytes();
-  this->actors_count        = Api::get().get_actors().size();
+  this->actors_count        = mc_model_checker->get_remote_process().actors().size();
   this->other_num           = -1;
   this->atomic_propositions = std::move(atomic_propositions);
 }
@@ -224,18 +224,16 @@ std::shared_ptr<Pair> LivenessChecker::create_pair(const Pair* current_pair, xbt
   ++expanded_pairs_count_;
   auto next_pair                 = std::make_shared<Pair>(expanded_pairs_count_);
   next_pair->automaton_state     = state;
-  next_pair->graph_state         = std::make_shared<State>();
+  next_pair->graph_state         = std::make_shared<State>(get_session());
   next_pair->atomic_propositions = std::move(propositions);
   if (current_pair)
     next_pair->depth = current_pair->depth + 1;
   else
     next_pair->depth = 1;
   /* Add all enabled actors to the interleave set of the initial state */
-  for (auto& act : Api::get().get_actors()) {
-    auto actor = act.copy.get_buffer();
-    if (get_session().actor_is_enabled(actor->get_pid()))
-      next_pair->graph_state->mark_todo(actor->get_pid());
-  }
+  for (auto const& [aid, _] : next_pair->graph_state->get_actors_list())
+    if (next_pair->graph_state->is_actor_enabled(aid))
+      next_pair->graph_state->mark_todo(aid);
 
   next_pair->requests = next_pair->graph_state->count_todo();
   /* FIXME : get search_cycle value for each accepting state */