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 8b8dcb8..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,10 +109,10 @@ void SafetyChecker::run()
       continue;
     }
 
-    // Search for the next transition. If found, state is modified accordingly (transition and executed_req are set)
-    // If there is no more transition in the current state, backtrack.
+    // Search for the next transition
+    int next = state->next_transition();
 
-    if (not api::get().mc_state_choose_request(state)) {
+    if (next < 0) { // If there is no more transition in the current state, backtrack.
 
       XBT_DEBUG("There remains %zu actors, but none to interleave (depth %zu).",
                 mc_model_checker->get_remote_process().actors().size(), stack_.size() + 1);
@@ -124,17 +124,16 @@ void SafetyChecker::run()
     }
 
     /* Actually answer the request: let execute the selected request (MCed does one step) */
-    auto remote_observer = api::get().execute(state->transition_);
+    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", state->transition_.textual.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(state->transition_.aid_, state->transition_.times_considered_);
-
-    api::get().mc_inc_executed_trans();
+      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_;
@@ -191,18 +190,18 @@ void SafetyChecker::backtrack()
     std::unique_ptr<State> state = std::move(stack_.back());
     stack_.pop_back();
     if (reductionMode_ == ReductionMode::dpor) {
-      aid_t issuer_id = state->transition_.aid_;
+      aid_t issuer_id = state->get_transition()->aid_;
       for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
         State* prev_state = i->get();
-        if (state->transition_.aid_ == prev_state->transition_.aid_) {
-          XBT_DEBUG("Simcall >>%s<< and >>%s<< with same issuer %ld", state->transition_.textual.c_str(),
-                    prev_state->transition_.textual.c_str(), issuer_id);
+        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:");
-            XBT_DEBUG("  %s (state=%d)", prev_state->transition_.textual.c_str(), prev_state->num_);
-            XBT_DEBUG("  %s (state=%d)", state->transition_.textual.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_id].is_done())
@@ -213,8 +212,8 @@ void SafetyChecker::backtrack()
         } else {
           if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
             XBT_DEBUG("INDEPENDENT Transitions:");
-            XBT_DEBUG("  %s (state=%d)", prev_state->transition_.textual.c_str(), prev_state->num_);
-            XBT_DEBUG("  %s (state=%d)", state->transition_.textual.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_);
           }
         }
       }
@@ -248,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->get_transition()->replay();
     /* Update statistics */
     api::get().mc_inc_visited_states();
-    api::get().mc_inc_executed_trans();
   }
 }