Define and use a Transition::to_cstring()

diff --git a/src/mc/Transition.cpp b/src/mc/Transition.cpp
index c9ab4b5..61623be 100644 (file)
--- a/src/mc/Transition.cpp
+++ b/src/mc/Transition.cpp
@@ -22,6 +22,12 @@ std::string Transition::to_string() const
 
   return textual_;
 }
+const char* Transition::to_cstring() const
+{
+  xbt_assert(mc_model_checker != nullptr, "Must be called from MCer");
+
+  return textual_.c_str();
+}
 void Transition::init(aid_t aid, int times_considered)
 {
   aid_              = aid;

diff --git a/src/mc/Transition.hpp b/src/mc/Transition.hpp
index 95089a1..3cd9c4c 100644 (file)
--- a/src/mc/Transition.hpp
+++ b/src/mc/Transition.hpp
@@ -43,6 +43,7 @@ public:
   void init(aid_t aid, int times_considered);
 
   std::string to_string() const;
+  const char* to_cstring() const;
 
   /* Moves the application toward a path that was already explored, but don't change the current transition */
   RemotePtr<simgrid::kernel::actor::SimcallObserver> replay() const;

diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp
index df6f25d..4d99e55 100644 (file)
--- a/src/mc/checker/CommunicationDeterminismChecker.cpp
+++ b/src/mc/checker/CommunicationDeterminismChecker.cpp
@@ -429,7 +429,7 @@ void CommunicationDeterminismChecker::real_run()
       int req_num       = cur_state->get_transition()->times_considered_;
       smx_simcall_t req = &cur_state->executed_req_;
 
-      XBT_DEBUG("Execute: %s", cur_state->get_transition()->to_string().c_str());
+      XBT_DEBUG("Execute: %s", cur_state->get_transition()->to_cstring());
 
       std::string req_str;
       if (dot_output != nullptr)

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index 6194f29..06d3efd 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -123,7 +123,7 @@ void LivenessChecker::replay()
 
     if (pair->exploration_started) {
       state->get_transition()->replay();
-      XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, state->get_transition()->to_string().c_str(), state.get());
+      XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, state->get_transition()->to_cstring(), state.get());
     }
 
     /* Update statistics */
@@ -342,7 +342,7 @@ void LivenessChecker::run()
 
     aid_t aid   = current_pair->graph_state->get_transition()->aid_;
     int req_num = current_pair->graph_state->get_transition()->times_considered_;
-    XBT_DEBUG("Execute: %s", current_pair->graph_state->get_transition()->to_string().c_str());
+    XBT_DEBUG("Execute: %s", current_pair->graph_state->get_transition()->to_cstring());
 
     if (dot_output != nullptr) {
       if (this->previous_pair_ != 0 && this->previous_pair_ != current_pair->num) {

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index de95bdd..f91565d 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -128,7 +128,7 @@ void SafetyChecker::run()
 
     // 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->get_transition()->to_string().c_str());
+    XBT_DEBUG("Execute: %s", state->get_transition()->to_cstring());
 
     std::string req_str;
     if (dot_output != nullptr)
@@ -194,14 +194,14 @@ void SafetyChecker::backtrack()
       for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
         State* prev_state = i->get();
         if (state->get_transition()->aid_ == prev_state->get_transition()->aid_) {
-          XBT_DEBUG("Simcall >>%s<< and >>%s<< with same issuer %ld", state->get_transition()->to_string().c_str(),
-                    prev_state->get_transition()->to_string().c_str(), issuer_id);
+          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->get_transition()->to_string().c_str(), prev_state->num_);
-            XBT_DEBUG("  %s (state=%d)", state->get_transition()->to_string().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())
@@ -212,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->get_transition()->to_string().c_str(), prev_state->num_);
-            XBT_DEBUG("  %s (state=%d)", state->get_transition()->to_string().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_);
           }
         }
       }

diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp
index f92aaa1..d5a082d 100644 (file)
--- a/src/mc/mc_state.cpp
+++ b/src/mc/mc_state.cpp
@@ -81,7 +81,7 @@ RemotePtr<simgrid::kernel::actor::SimcallObserver> State::execute_next(int next)
   transition_.init(aid, times_considered);
   executed_req_ = actor->simcall_;
 
-  XBT_DEBUG("Let's run actor %ld, going for transition %s", aid, transition_.to_string().c_str());
+  XBT_DEBUG("Let's run actor %ld, going for transition %s", aid, transition_.to_cstring());
 
   return transition_.replay();
 }