SafetyChecker::check_non_termination() uses mc_api

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index 5751271..5a2b24e 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -37,16 +37,17 @@ namespace mc {
 void SafetyChecker::check_non_termination(const State* current_state)
 {
   for (auto state = stack_.rbegin(); state != stack_.rend(); ++state)
-    if (snapshot_equal((*state)->system_state_.get(), current_state->system_state_.get())) {
+    if (mcapi::get().snapshot_equal((*state)->system_state_.get(), current_state->system_state_.get())) {
       XBT_INFO("Non-progressive cycle: state %d -> state %d", (*state)->num_, current_state->num_);
       XBT_INFO("******************************************");
       XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
       XBT_INFO("******************************************");
       XBT_INFO("Counter-example execution trace:");
-      for (auto const& s : mc_model_checker->getChecker()->get_textual_trace())
+      auto checker = mcapi::get().mc_get_checker();
+      for (auto const& s : checker->get_textual_trace())
         XBT_INFO("  %s", s.c_str());
-      dumpRecordPath();
-      session->log_state();
+      mcapi::get().mc_dump_record_path();
+      mcapi::get().s_log_state();
 
       throw TerminationError();
     }

diff --git a/src/mc/mc_api.cpp b/src/mc/mc_api.cpp
index d78f38b..8b9fd4f 100644 (file)
--- a/src/mc/mc_api.cpp
+++ b/src/mc/mc_api.cpp
@@ -2,8 +2,9 @@
 
 #include "src/mc/Session.hpp"
 #include "src/mc/mc_private.hpp"
-#include "src/mc/remote/RemoteSimulation.hpp"
 #include "src/mc/mc_smx.hpp"
+#include "src/mc/remote/RemoteSimulation.hpp"
+#include "src/mc/mc_record.hpp"
 
 #include <xbt/asserts.h>
 #include <xbt/log.h>
@@ -33,7 +34,7 @@ void mc_api::s_initialize() const
 
 ModelChecker* mc_api::get_model_checker() const
 {
-    return mc_model_checker;
+  return mc_model_checker;
 }
 
 void mc_api::mc_inc_visited_states() const
@@ -122,7 +123,7 @@ void mc_api::mc_exit(int status) const
 
 std::string const& mc_api::mc_get_host_name(std::string const& hostname) const
 {
-  return mc_model_checker->get_host_name(hostname); 
+  return mc_model_checker->get_host_name(hostname);
 }
 
 PageStore& mc_api::mc_page_store() const
@@ -130,8 +131,9 @@ PageStore& mc_api::mc_page_store() const
   return mc_model_checker->page_store();
 }
 
-void mc_api::mc_cleanup()
+void mc_api::mc_dump_record_path() const
 {
+  simgrid::mc::dumpRecordPath();
 }
 
 bool mc_api::request_depend(smx_simcall_t req1, smx_simcall_t req2) const
@@ -144,11 +146,16 @@ std::string mc_api::request_to_string(smx_simcall_t req, int value, RequestType
   return simgrid::mc::request_to_string(req, value, request_type).c_str();
 }
 
-const char * mc_api::simix_simcall_name(e_smx_simcall_t kind) const
+const char* mc_api::simix_simcall_name(e_smx_simcall_t kind) const
 {
   return SIMIX_simcall_name(kind);
 }
 
+bool mc_api::snapshot_equal(const Snapshot* s1, const Snapshot* s2) const
+{
+  return simgrid::mc::snapshot_equal(s1, s2);
+}
+
 void mc_api::s_close() const
 {
   session->close();

diff --git a/src/mc/mc_api.hpp b/src/mc/mc_api.hpp
index b9d439f..971bbf3 100644 (file)
--- a/src/mc/mc_api.hpp
+++ b/src/mc/mc_api.hpp
@@ -57,13 +57,16 @@ public:
   void mc_exit(int status) const;
   std::string const& mc_get_host_name(std::string const& hostname) const;
   PageStore& mc_page_store() const;
-  void mc_cleanup();
+  void mc_dump_record_path() const;
 
   // SIMCALL FUNCTIONS
   bool request_depend(smx_simcall_t req1, smx_simcall_t req2) const;
   std::string request_to_string(smx_simcall_t req, int value, RequestType request_type) const;
   const char *simix_simcall_name(e_smx_simcall_t kind) const;
 
+  // SNAPSHOT FUNCTIONS
+  bool snapshot_equal(const Snapshot* s1, const Snapshot* s2) const;
+
   // SESSION FUNCTIONS
   void s_initialize() const;
   void s_close() const;