snake_case some surviving camels

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

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index 3f2030e6eccd248afdf9f45ca7c03eb570b70eac..1b7953ac9fae4f11478797e3c15cb458d1477842 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -4,11 +4,10 @@
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "src/mc/checker/LivenessChecker.hpp"
+#include "src/mc/Session.hpp"
 #include "src/mc/mc_config.hpp"
 #include "src/mc/mc_exit.hpp"
 #include "src/mc/mc_private.hpp"
-#include "src/mc/mc_request.hpp"
-#include "src/mc/mc_smx.hpp"
 
 #include <boost/range/algorithm.hpp>
 #include <cstring>
@@ -117,8 +116,7 @@ void LivenessChecker::replay()
     }
   }
 
-  /* Restore the initial state */
-  api::get().restore_initial_state();
+  get_session().restore_initial_state();
 
   /* Traverse the stack from the initial state and re-execute the transitions */
   int depth = 1;
@@ -140,10 +138,10 @@ void LivenessChecker::replay()
       req                      = &issuer->simcall_;
 
       /* Debug information */
-      XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth,
-                api::get().request_to_string(req, req_num, simgrid::mc::RequestType::simix).c_str(), state.get());
+      XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, api::get().request_to_string(req, req_num).c_str(),
+                state.get());
 
-      api::get().execute(state->transition_);
+      api::get().execute(state->transition_, req);
     }
 
     /* Update statistics */
@@ -203,9 +201,7 @@ void LivenessChecker::purge_visited_pairs()
   }
 }
 
-LivenessChecker::LivenessChecker() : Checker()
-{
-}
+LivenessChecker::LivenessChecker(Session* session) : Checker(session) {}
 
 RecordTrace LivenessChecker::get_record_trace() // override
 {
@@ -242,7 +238,7 @@ std::vector<std::string> LivenessChecker::get_textual_trace() // override
     int req_num       = pair->graph_state->transition_.times_considered_;
     smx_simcall_t req = &pair->graph_state->executed_req_;
     if (req->call_ != simix::Simcall::NONE)
-      trace.push_back(api::get().request_to_string(req, req_num, RequestType::executed));
+      trace.push_back(api::get().request_to_string(req, req_num));
   }
   return trace;
 }
@@ -260,12 +256,14 @@ std::shared_ptr<Pair> LivenessChecker::create_pair(const Pair* current_pair, xbt
     next_pair->depth = current_pair->depth + 1;
   else
     next_pair->depth = 1;
-  /* Get enabled actors and insert them in the interleave set of the next graph_state */
-  auto actors = api::get().get_actors();
-  for (auto& actor : actors)
-    if (api::get().actor_is_enabled(actor.copy.get_buffer()->get_pid()))
-      next_pair->graph_state->add_interleaving_set(actor.copy.get_buffer());
-  next_pair->requests = next_pair->graph_state->interleave_size();
+  /* 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);
+  }
+
+  next_pair->requests = next_pair->graph_state->count_todo();
   /* FIXME : get search_cycle value for each accepting state */
   if (next_pair->automaton_state->type == 1 || (current_pair && current_pair->search_cycle))
     next_pair->search_cycle = true;
@@ -302,7 +300,7 @@ void LivenessChecker::run()
   api::get().automaton_load(_sg_mc_property_file.get().c_str());
 
   XBT_DEBUG("Starting the liveness algorithm");
-  api::get().session_initialize();
+  get_session().take_initial_snapshot();
 
   /* Initialize */
   this->previous_pair_ = 0;
@@ -326,8 +324,8 @@ void LivenessChecker::run()
 
     XBT_DEBUG(
         "********************* ( Depth = %d, search_cycle = %d, interleave size = %zu, pair_num = %d, requests = %d)",
-        current_pair->depth, current_pair->search_cycle, current_pair->graph_state->interleave_size(),
-        current_pair->num, current_pair->requests);
+        current_pair->depth, current_pair->search_cycle, current_pair->graph_state->count_todo(), current_pair->num,
+        current_pair->requests);
 
     if (current_pair->requests == 0) {
       this->backtrack();
@@ -375,7 +373,7 @@ void LivenessChecker::run()
       fflush(dot_output);
     }
 
-    XBT_DEBUG("Execute: %s", api::get().request_to_string(req, req_num, RequestType::simix).c_str());
+    XBT_DEBUG("Execute: %s", api::get().request_to_string(req, req_num).c_str());
 
     /* Update stats */
     api::get().mc_inc_executed_trans();
@@ -409,9 +407,9 @@ void LivenessChecker::run()
   api::get().log_state();
 }
 
-Checker* createLivenessChecker()
+Checker* create_liveness_checker(Session* session)
 {
-  return new LivenessChecker();
+  return new LivenessChecker(session);
 }
 
 } // namespace mc