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 edb3cf5..64d9f36 100644 (file)
--- a/src/mc/explo/LivenessChecker.cpp
+++ b/src/mc/explo/LivenessChecker.cpp
@@ -16,8 +16,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc, "Logging specific to algorithms
 
 /********* Static functions *********/
 
-namespace simgrid {
-namespace mc {
+namespace simgrid::mc {
 
 VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state,
                          std::shared_ptr<const std::vector<int>> atomic_propositions,
@@ -28,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);
 }
@@ -64,10 +63,10 @@ std::shared_ptr<VisitedPair> LivenessChecker::insert_acceptance_pair(simgrid::mc
   auto new_pair =
       std::make_shared<VisitedPair>(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
 
-  auto res = boost::range::equal_range(acceptance_pairs_, new_pair.get(), Api::get().compare_pair());
+  auto [res_begin, res_end] = boost::range::equal_range(acceptance_pairs_, new_pair.get(), Api::get().compare_pair());
 
   if (pair->search_cycle)
-    for (auto i = res.first; i != res.second; ++i) {
+    for (auto i = res_begin; i != res_end; ++i) {
       std::shared_ptr<simgrid::mc::VisitedPair> const& pair_test = *i;
       if (xbt_automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) != 0 ||
           *(pair_test->atomic_propositions) != *(new_pair->atomic_propositions) ||
@@ -82,7 +81,7 @@ std::shared_ptr<VisitedPair> LivenessChecker::insert_acceptance_pair(simgrid::mc
       return nullptr;
     }
 
-  acceptance_pairs_.insert(res.first, new_pair);
+  acceptance_pairs_.insert(res_begin, new_pair);
   return new_pair;
 }
 
@@ -102,7 +101,7 @@ void LivenessChecker::replay()
   /* Intermediate backtracking */
   if (_sg_mc_checkpoint > 0) {
     const Pair* pair = exploration_stack_.back().get();
-    if (auto* system_state = pair->graph_state->get_system_state()) {
+    if (const auto* system_state = pair->graph_state->get_system_state()) {
       Api::get().restore_state(system_state);
       return;
     }
@@ -142,9 +141,10 @@ int LivenessChecker::insert_visited_pair(std::shared_ptr<VisitedPair> visited_pa
     visited_pair =
         std::make_shared<VisitedPair>(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
 
-  auto range = boost::range::equal_range(visited_pairs_, visited_pair.get(), Api::get().compare_pair());
+  auto [range_begin, range_end] =
+      boost::range::equal_range(visited_pairs_, visited_pair.get(), Api::get().compare_pair());
 
-  for (auto i = range.first; i != range.second; ++i) {
+  for (auto i = range_begin; i != range_end; ++i) {
     const VisitedPair* pair_test = i->get();
     if (xbt_automaton_state_compare(pair_test->automaton_state, visited_pair->automaton_state) != 0 ||
         *(pair_test->atomic_propositions) != *(visited_pair->atomic_propositions) ||
@@ -164,7 +164,7 @@ int LivenessChecker::insert_visited_pair(std::shared_ptr<VisitedPair> visited_pa
     return (*i)->other_num;
   }
 
-  visited_pairs_.insert(range.first, std::move(visited_pair));
+  visited_pairs_.insert(range_begin, std::move(visited_pair));
   this->purge_visited_pairs();
   return -1;
 }
@@ -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 */
@@ -359,8 +357,9 @@ void LivenessChecker::run()
     // For each enabled transition in the property automaton, push a
     // (application_state, automaton_state) pair to the exploration stack:
     for (int i = xbt_dynar_length(current_pair->automaton_state->out) - 1; i >= 0; i--) {
-      auto transition_succ_label = Api::get().get_automaton_transition_label(current_pair->automaton_state->out, i);
-      auto transition_succ_dst   = Api::get().get_automaton_transition_dst(current_pair->automaton_state->out, i);
+      const auto* transition_succ_label =
+          Api::get().get_automaton_transition_label(current_pair->automaton_state->out, i);
+      auto* transition_succ_dst = Api::get().get_automaton_transition_dst(current_pair->automaton_state->out, i);
       if (evaluate_label(transition_succ_label, *prop_values))
         exploration_stack_.push_back(this->create_pair(current_pair.get(), transition_succ_dst, prop_values));
     }
@@ -375,5 +374,4 @@ Exploration* create_liveness_checker(Session* session)
   return new LivenessChecker(session);
 }
 
-} // namespace mc
-} // namespace simgrid
+} // namespace simgrid::mc