Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Inline another stupid function
authorMartin Quinson <martin.quinson@ens-rennes.fr>
Fri, 11 Feb 2022 20:47:52 +0000 (21:47 +0100)
committerMartin Quinson <martin.quinson@ens-rennes.fr>
Fri, 11 Feb 2022 20:47:52 +0000 (21:47 +0100)
src/mc/ModelChecker.cpp
src/mc/api.cpp
src/mc/checker/LivenessChecker.cpp
src/mc/checker/SafetyChecker.cpp
src/mc/mc_record.cpp
src/mc/mc_record.hpp

index a7f0a6d..5341513 100644 (file)
@@ -139,7 +139,7 @@ static void MC_report_crash(int status)
   XBT_INFO("Counter-example execution trace:");
   for (auto const& s : mc_model_checker->getChecker()->get_textual_trace())
     XBT_INFO("  %s", s.c_str());
-  dumpRecordPath();
+  XBT_INFO("Path = %s", mc_model_checker->getChecker()->get_record_trace().to_string().c_str());
   session_singleton->log_state();
   if (xbt_log_no_loc) {
     XBT_INFO("Stack trace not displayed because you passed --log=no_loc");
@@ -230,7 +230,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
       XBT_INFO("Counter-example execution trace:");
       for (auto const& s : getChecker()->get_textual_trace())
         XBT_INFO("  %s", s.c_str());
-      dumpRecordPath();
+      XBT_INFO("Path = %s", getChecker()->get_record_trace().to_string().c_str());
       session_singleton->log_state();
 
       this->exit(SIMGRID_MC_EXIT_SAFETY);
index 2c40c20..8b5dc8f 100644 (file)
@@ -295,7 +295,7 @@ void Api::mc_check_deadlock() const
     XBT_CINFO(mc_global, "Counter-example execution trace:");
     for (auto const& s : mc_model_checker->getChecker()->get_textual_trace())
       XBT_CINFO(mc_global, "  %s", s.c_str());
-    simgrid::mc::dumpRecordPath();
+    XBT_INFO("Path = %s", mc_model_checker->getChecker()->get_record_trace().to_string().c_str());
     simgrid::mc::session_singleton->log_state();
     throw DeadlockError();
   }
index 7a9806d..1927cc4 100644 (file)
@@ -206,7 +206,7 @@ void LivenessChecker::show_acceptance_cycle(std::size_t depth)
   XBT_INFO("Counter-example that violates formula:");
   for (auto const& s : this->get_textual_trace())
     XBT_INFO("  %s", s.c_str());
-  simgrid::mc::dumpRecordPath();
+  XBT_INFO("Path = %s", get_record_trace().to_string().c_str());
   api::get().log_state();
   XBT_INFO("Counter-example depth: %zu", depth);
 }
index 8fd5f95..77a35ea 100644 (file)
@@ -41,7 +41,7 @@ void SafetyChecker::check_non_termination(const State* current_state)
       XBT_INFO("Counter-example execution trace:");
       for (auto const& s : get_textual_trace())
         XBT_INFO("  %s", s.c_str());
-      simgrid::mc::dumpRecordPath();
+      XBT_INFO("Path = %s", get_record_trace().to_string().c_str());
       api::get().log_state();
 
       throw TerminationError();
index 0db71d0..2e330d6 100644 (file)
@@ -91,11 +91,6 @@ std::string simgrid::mc::RecordTrace::to_string() const
   return stream.str();
 }
 
-void dumpRecordPath()
-{
-  XBT_INFO("Path = %s", mc_model_checker->getChecker()->get_record_trace().to_string().c_str());
-}
-
 #endif
 
 }
index 1f4ec51..5b162d6 100644 (file)
@@ -45,8 +45,6 @@ public:
   static void replay(const std::string& trace);
 };
 
-XBT_PRIVATE void dumpRecordPath();
-
 }
 }