log_state has nothing to do in RemoteApp, it belongs to the exploration

diff --git a/MANIFEST.in b/MANIFEST.in
index e6cd446..60fb437 100644 (file)
--- a/MANIFEST.in
+++ b/MANIFEST.in
@@ -2291,6 +2291,7 @@ include src/mc/compare.cpp
 include src/mc/explo/CommunicationDeterminismChecker.cpp
 include src/mc/explo/DFSExplorer.cpp
 include src/mc/explo/DFSExplorer.hpp
+include src/mc/explo/Exploration.cpp
 include src/mc/explo/Exploration.hpp
 include src/mc/explo/LivenessChecker.cpp
 include src/mc/explo/LivenessChecker.hpp

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index d09a9ad..47f9dd0 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -141,7 +141,7 @@ static void MC_report_crash(Exploration* explorer, int status)
     for (auto const& s : explorer->get_textual_trace())
       XBT_INFO("  %s", s.c_str());
     XBT_INFO("Path = %s", explorer->get_record_trace().to_string().c_str());
-    explorer->get_remote_app().log_state();
+    explorer->log_state();
     if (xbt_log_no_loc) {
       XBT_INFO("Stack trace not displayed because you passed --log=no_loc");
     } else {
@@ -233,7 +233,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
       for (auto const& s : get_exploration()->get_textual_trace())
         XBT_INFO("  %s", s.c_str());
       XBT_INFO("Path = %s", get_exploration()->get_record_trace().to_string().c_str());
-      exploration_->get_remote_app().log_state();
+      exploration_->log_state();
 
       this->exit(SIMGRID_MC_EXIT_SAFETY);
 

diff --git a/src/mc/api/RemoteApp.cpp b/src/mc/api/RemoteApp.cpp
index d4c8961..259716f 100644 (file)
--- a/src/mc/api/RemoteApp.cpp
+++ b/src/mc/api/RemoteApp.cpp
@@ -110,21 +110,6 @@ void RemoteApp::restore_initial_state() const
   this->initial_snapshot_->restore(&model_checker_->get_remote_process());
 }
 
-void RemoteApp::log_state() const
-{
-  model_checker_->get_exploration()->log_state();
-
-  if (not _sg_mc_dot_output_file.get().empty()) {
-    fprintf(dot_output, "}\n");
-    fclose(dot_output);
-  }
-  if (getenv("SIMGRID_MC_SYSTEM_STATISTICS")) {
-    int ret = system("free");
-    if (ret != 0)
-      XBT_WARN("Call to system(free) did not return 0, but %d", ret);
-  }
-}
-
 unsigned long RemoteApp::get_maxpid() const
 {
   return model_checker_->get_remote_process().get_maxpid();
@@ -175,7 +160,7 @@ void RemoteApp::check_deadlock() const
     for (auto const& frame : model_checker_->get_exploration()->get_textual_trace())
       XBT_CINFO(mc_global, "  %s", frame.c_str());
     XBT_CINFO(mc_global, "Path = %s", model_checker_->get_exploration()->get_record_trace().to_string().c_str());
-    log_state();
+    model_checker_->get_exploration()->log_state();
     throw DeadlockError();
   }
 }

diff --git a/src/mc/api/RemoteApp.hpp b/src/mc/api/RemoteApp.hpp
index e88c168..4201cfd 100644 (file)
--- a/src/mc/api/RemoteApp.hpp
+++ b/src/mc/api/RemoteApp.hpp
@@ -49,8 +49,6 @@ public:
   /** Ask to the application to check for a deadlock. If so, do an error message and throw a DeadlockError. */
   void check_deadlock() const;
 
-  void log_state() const;
-
   /** Retrieve the max PID of the running actors */
   unsigned long get_maxpid() const;
 

diff --git a/src/mc/explo/CommunicationDeterminismChecker.cpp b/src/mc/explo/CommunicationDeterminismChecker.cpp
index 24b2227..109a220 100644 (file)
--- a/src/mc/explo/CommunicationDeterminismChecker.cpp
+++ b/src/mc/explo/CommunicationDeterminismChecker.cpp
@@ -207,7 +207,7 @@ void CommDetExtension::enforce_deterministic_pattern(aid_t actor, const PatternC
       XBT_INFO("***** Non-send-deterministic communications pattern *****");
       XBT_INFO("*********************************************************");
       XBT_INFO("%s", send_diff.c_str());
-      exploration_.get_remote_app().log_state();
+      exploration_.log_state();
       mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
     } else if (_sg_mc_comms_determinism && (not send_deterministic && not recv_deterministic)) {
       XBT_INFO("****************************************************");
@@ -217,7 +217,7 @@ void CommDetExtension::enforce_deterministic_pattern(aid_t actor, const PatternC
         XBT_INFO("%s", send_diff.c_str());
       if (not recv_diff.empty())
         XBT_INFO("%s", recv_diff.c_str());
-      exploration_.get_remote_app().log_state();
+      exploration_.log_state();
       mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
     }
   }

diff --git a/src/mc/explo/Exploration.cpp b/src/mc/explo/Exploration.cpp
new file mode 100644 (file)
index 0000000..9dc53d9
--- /dev/null
+++ b/src/mc/explo/Exploration.cpp
@@ -0,0 +1,27 @@
+/* Copyright (c) 2016-2022. The SimGrid Team. All rights reserved.          */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "src/mc/explo/Exploration.hpp"
+#include "src/mc/mc_config.hpp"
+#include "src/mc/mc_private.hpp"
+
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_explo, mc, "Generic exploration algorithm of the model-checker");
+
+namespace simgrid::mc {
+
+void Exploration::log_state()
+{
+  if (not _sg_mc_dot_output_file.get().empty()) {
+    fprintf(dot_output, "}\n");
+    fclose(dot_output);
+  }
+  if (getenv("SIMGRID_MC_SYSTEM_STATISTICS")) {
+    int ret = system("free");
+    if (ret != 0)
+      XBT_WARN("Call to system(free) did not return 0, but %d", ret);
+  }
+}
+
+}; // namespace simgrid::mc

diff --git a/src/mc/explo/Exploration.hpp b/src/mc/explo/Exploration.hpp
index 68f0f97..b5c1948 100644 (file)
--- a/src/mc/explo/Exploration.hpp
+++ b/src/mc/explo/Exploration.hpp
@@ -50,7 +50,7 @@ public:
   virtual std::vector<std::string> get_textual_trace() = 0;
 
   /** Log additional information about the state of the model-checker */
-  virtual void log_state() = 0;
+  virtual void log_state();
 
   RemoteApp& get_remote_app() { return remote_app_; }
 };

diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp
index 455c23b..11bbb87 100644 (file)
--- a/src/mc/explo/LivenessChecker.cpp
+++ b/src/mc/explo/LivenessChecker.cpp
@@ -193,6 +193,7 @@ void LivenessChecker::log_state() // override
   XBT_INFO("Expanded pairs = %lu", expanded_pairs_count_);
   XBT_INFO("Visited pairs = %lu", visited_pairs_count_);
   XBT_INFO("Executed transitions = %lu", Transition::get_executed_transitions());
+  Exploration::log_state();
 }
 
 void LivenessChecker::show_acceptance_cycle(std::size_t depth)

diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp
index 5b4fb8b..308e43c 100644 (file)
--- a/src/mc/explo/UdporChecker.cpp
+++ b/src/mc/explo/UdporChecker.cpp
@@ -26,7 +26,10 @@ std::vector<std::string> UdporChecker::get_textual_trace()
   return trace;
 }
 
-void UdporChecker::log_state() {}
+void UdporChecker::log_state()
+{
+  Exploration::log_state();
+}
 
 Exploration* create_udpor_checker(RemoteApp& remote_app)
 {

diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake
index 9596c7e..f1b2fa5 100644 (file)
--- a/tools/cmake/DefinePackages.cmake
+++ b/tools/cmake/DefinePackages.cmake
@@ -576,6 +576,7 @@ set(MC_SRC
   src/mc/explo/CommunicationDeterminismChecker.cpp
   src/mc/explo/DFSExplorer.cpp
   src/mc/explo/DFSExplorer.hpp
+  src/mc/explo/Exploration.cpp
   src/mc/explo/Exploration.hpp
   src/mc/explo/LivenessChecker.cpp
   src/mc/explo/LivenessChecker.hpp