Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Inline a function of mc::api
authorMartin Quinson <martin.quinson@ens-rennes.fr>
Fri, 11 Feb 2022 18:04:48 +0000 (19:04 +0100)
committerMartin Quinson <martin.quinson@ens-rennes.fr>
Fri, 11 Feb 2022 18:04:48 +0000 (19:04 +0100)
src/mc/api.cpp
src/mc/api.hpp
src/mc/checker/LivenessChecker.cpp
src/mc/checker/SafetyChecker.cpp

index 6556ab7..ee045bc 100644 (file)
@@ -351,11 +351,6 @@ void Api::mc_exit(int status) const
   mc_model_checker->exit(status);
 }
 
-void Api::dump_record_path() const
-{
-  simgrid::mc::dumpRecordPath();
-}
-
 std::string Api::request_get_dot_output(aid_t aid, int value) const
 {
   const char* color = get_color(aid - 1);
index cd5551d..7a2676b 100644 (file)
@@ -99,7 +99,6 @@ public:
   unsigned long mc_get_visited_states() const;
   void mc_check_deadlock() const;
   XBT_ATTRIB_NORETURN void mc_exit(int status) const;
-  void dump_record_path() const;
 
   // SIMCALL APIs
   std::string request_get_dot_output(aid_t aid, int value) const;
index c4a214a..561d1fd 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());
-  api::get().dump_record_path();
+  simgrid::mc::dumpRecordPath();
   api::get().log_state();
   XBT_INFO("Counter-example depth: %zu", depth);
 }
index 4d2cc15..7362331 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());
-      api::get().dump_record_path();
+      simgrid::mc::dumpRecordPath();
       api::get().log_state();
 
       throw TerminationError();