Define and use a Transition::to_cstring()

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

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index 4ef8cc5..f91565d 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -52,7 +52,7 @@ RecordTrace SafetyChecker::get_record_trace() // override
 {
   RecordTrace res;
   for (auto const& state : stack_)
-    res.push_back(state->get_transition());
+    res.push_back(*state->get_transition());
   return res;
 }
 
@@ -60,7 +60,7 @@ std::vector<std::string> SafetyChecker::get_textual_trace() // override
 {
   std::vector<std::string> trace;
   for (auto const& state : stack_)
-    trace.push_back(state->transition_.textual);
+    trace.push_back(state->get_transition()->to_string());
   return trace;
 }
 
@@ -68,7 +68,7 @@ void SafetyChecker::log_state() // override
 {
   XBT_INFO("Expanded states = %lu", expanded_states_count_);
   XBT_INFO("Visited states = %lu", api::get().mc_get_visited_states());
-  XBT_INFO("Executed transitions = %lu", api::get().mc_get_executed_trans());
+  XBT_INFO("Executed transitions = %lu", Transition::get_executed_transitions());
 }
 
 void SafetyChecker::run()
@@ -109,12 +109,11 @@ void SafetyChecker::run()
       continue;
     }
 
-    // Search an enabled transition in the current state; backtrack if the interleave set is empty
-    // get_request also sets state.transition to be the one corresponding to the returned req
-    smx_simcall_t req = api::get().mc_state_choose_request(state);
-    // req is now the transition of the process that was selected to be executed
+    // Search for the next transition
+    int next = state->next_transition();
+
+    if (next < 0) { // If there is no more transition in the current state, backtrack.
 
-    if (req == nullptr) {
       XBT_DEBUG("There remains %zu actors, but none to interleave (depth %zu).",
                 mc_model_checker->get_remote_process().actors().size(), stack_.size() + 1);
 
@@ -124,19 +123,17 @@ void SafetyChecker::run()
       continue;
     }
 
+    /* Actually answer the request: let execute the selected request (MCed does one step) */
+    auto remote_observer = state->execute_next(next);
+
     // If there are processes to interleave and the maximum depth has not been
     // reached then perform one step of the exploration algorithm.
-    XBT_DEBUG("Execute: %s", api::get().request_to_string(req, state->transition_.times_considered_).c_str());
+    XBT_DEBUG("Execute: %s", state->get_transition()->to_cstring());
 
     std::string req_str;
     if (dot_output != nullptr)
-      req_str = api::get().request_get_dot_output(req, state->transition_.times_considered_);
-
-    api::get().mc_inc_executed_trans();
-
-    /* Actually answer the request: let execute the selected request (MCed does one step) */
-    RemotePtr<simgrid::kernel::actor::SimcallObserver> remote_observer =
-        api::get().execute(state->transition_, &state->executed_req_);
+      req_str =
+          api::get().request_get_dot_output(state->get_transition()->aid_, state->get_transition()->times_considered_);
 
     /* Create the new expanded state (copy the state of MCed into our MCer data) */
     ++expanded_states_count_;
@@ -157,7 +154,7 @@ void SafetyChecker::run()
       for (auto& remoteActor : actors) {
         auto actor = remoteActor.copy.get_buffer();
         if (get_session().actor_is_enabled(actor->get_pid())) {
-          next_state->mark_todo(actor);
+          next_state->mark_todo(actor->get_pid());
           if (reductionMode_ == ReductionMode::dpor)
             break; // With DPOR, we take the first enabled transition
         }
@@ -193,34 +190,31 @@ void SafetyChecker::backtrack()
     std::unique_ptr<State> state = std::move(stack_.back());
     stack_.pop_back();
     if (reductionMode_ == ReductionMode::dpor) {
-      kernel::actor::ActorImpl* issuer = api::get().simcall_get_issuer(&state->executed_req_);
+      aid_t issuer_id = state->get_transition()->aid_;
       for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
         State* prev_state = i->get();
-        if (state->executed_req_.issuer_ == prev_state->executed_req_.issuer_) {
-          XBT_DEBUG("Simcall %s and %s with same issuer", SIMIX_simcall_name(state->executed_req_),
-                    SIMIX_simcall_name(prev_state->executed_req_));
+        if (state->get_transition()->aid_ == prev_state->get_transition()->aid_) {
+          XBT_DEBUG("Simcall >>%s<< and >>%s<< with same issuer %ld", state->get_transition()->to_cstring(),
+                    prev_state->get_transition()->to_cstring(), issuer_id);
           break;
         } else if (api::get().requests_are_dependent(prev_state->remote_observer_, state->remote_observer_)) {
           if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
             XBT_DEBUG("Dependent Transitions:");
-            int value              = prev_state->transition_.times_considered_;
-            smx_simcall_t prev_req = &prev_state->executed_req_;
-            XBT_DEBUG("%s (state=%d)", api::get().request_to_string(prev_req, value).c_str(), prev_state->num_);
-            value    = state->transition_.times_considered_;
-            prev_req = &state->executed_req_;
-            XBT_DEBUG("%s (state=%d)", api::get().request_to_string(prev_req, value).c_str(), state->num_);
+            XBT_DEBUG("  %s (state=%d)", prev_state->get_transition()->to_cstring(), prev_state->num_);
+            XBT_DEBUG("  %s (state=%d)", state->get_transition()->to_cstring(), state->num_);
           }
 
-          if (not prev_state->actor_states_[issuer->get_pid()].is_done())
-            prev_state->mark_todo(issuer);
+          if (not prev_state->actor_states_[issuer_id].is_done())
+            prev_state->mark_todo(issuer_id);
           else
-            XBT_DEBUG("Actor %s %ld is in done set", api::get().get_actor_name(issuer).c_str(), issuer->get_pid());
+            XBT_DEBUG("Actor %ld is in done set", issuer_id);
           break;
         } else {
-          const kernel::actor::ActorImpl* previous_issuer = api::get().simcall_get_issuer(&prev_state->executed_req_);
-          XBT_DEBUG("Simcall %s, process %ld (state %d) and simcall %s, process %ld (state %d) are independent",
-                    SIMIX_simcall_name(state->executed_req_), issuer->get_pid(), state->num_,
-                    SIMIX_simcall_name(prev_state->executed_req_), previous_issuer->get_pid(), prev_state->num_);
+          if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
+            XBT_DEBUG("INDEPENDENT Transitions:");
+            XBT_DEBUG("  %s (state=%d)", prev_state->get_transition()->to_cstring(), prev_state->num_);
+            XBT_DEBUG("  %s (state=%d)", state->get_transition()->to_cstring(), state->num_);
+          }
         }
       }
     }
@@ -253,10 +247,9 @@ void SafetyChecker::restore_state()
   for (std::unique_ptr<State> const& state : stack_) {
     if (state == stack_.back())
       break;
-    api::get().execute(state->transition_, &state->executed_req_);
+    state->get_transition()->replay();
     /* Update statistics */
     api::get().mc_inc_visited_states();
-    api::get().mc_inc_executed_trans();
   }
 }
 
@@ -287,15 +280,17 @@ SafetyChecker::SafetyChecker(Session* session) : Checker(session)
   /* Get an enabled actor and insert it in the interleave set of the initial state */
   auto actors = api::get().get_actors();
   XBT_DEBUG("Initial state. %zu actors to consider", actors.size());
-  for (auto& actor : actors)
-    if (get_session().actor_is_enabled(actor.copy.get_buffer()->get_pid())) {
-      initial_state->mark_todo(actor.copy.get_buffer());
+  for (auto& actor : actors) {
+    aid_t aid = actor.copy.get_buffer()->get_pid();
+    if (get_session().actor_is_enabled(aid)) {
+      initial_state->mark_todo(aid);
       if (reductionMode_ == ReductionMode::dpor) {
-        XBT_DEBUG("Actor %ld is TODO, DPOR is ON so let's go for this one.", actor.copy.get_buffer()->get_pid());
+        XBT_DEBUG("Actor %ld is TODO, DPOR is ON so let's go for this one.", aid);
         break;
       }
-      XBT_DEBUG("Actor %ld is TODO", actor.copy.get_buffer()->get_pid());
+      XBT_DEBUG("Actor %ld is TODO", aid);
     }
+  }
 
   stack_.push_back(std::move(initial_state));
 }