MC: apply some sonar advices

[simgrid.git] / src / mc / ModelChecker.cpp

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index d09a9ad..17e2bce 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -5,6 +5,7 @@
 
 #include "src/mc/ModelChecker.hpp"
 #include "src/mc/explo/Exploration.hpp"
+#include "src/mc/explo/LivenessChecker.hpp"
 #include "src/mc/mc_config.hpp"
 #include "src/mc/mc_exit.hpp"
 #include "src/mc/mc_private.hpp"
@@ -66,8 +67,13 @@ void ModelChecker::start()
   xbt_assert(waitpid(pid, &status, WAITPID_CHECKED_FLAGS) == pid && WIFSTOPPED(status) && WSTOPSIG(status) == SIGSTOP,
              "Could not wait model-checked process");
 
-  if (not _sg_mc_dot_output_file.get().empty())
-    MC_init_dot_output();
+  if (not _sg_mc_dot_output_file.get().empty()) {
+    dot_output_ = fopen(_sg_mc_dot_output_file.get().c_str(), "w");
+    xbt_assert(dot_output_ != nullptr, "Error open dot output file: %s", strerror(errno));
+
+    fprintf(dot_output_, "digraph graphname{\n fixedsize=true; rankdir=TB; ranksep=.25; edge [fontsize=12]; node "
+                         "[fontsize=10, shape=circle,width=.5 ]; graph [resolution=20, fontsize=10];\n");
+  }
 
   setup_ignore();
 
@@ -87,6 +93,16 @@ void ModelChecker::start()
              errno);
 }
 
+void ModelChecker::dot_output(const char* fmt, ...)
+{
+  if (dot_output_ != nullptr) {
+    va_list ap;
+    va_start(ap, fmt);
+    vfprintf(dot_output_, fmt, ap);
+    va_end(ap);
+  }
+}
+
 static constexpr auto ignored_local_variables = {
     std::make_pair("e", "*"),
     std::make_pair("_log_ev", "*"),
@@ -141,7 +157,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 {
@@ -211,14 +227,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
       xbt_assert(not message.callback, "Support for client-side function proposition is not implemented.");
       XBT_DEBUG("Received symbol: %s", message.name.data());
 
-      if (property_automaton == nullptr)
-        property_automaton = xbt_automaton_new();
-
-      const RemoteProcess* process    = &this->get_remote_process();
-      RemotePtr<int> address          = remote((int*)message.data);
-      xbt::add_proposition(property_automaton, message.name.data(),
-                           [process, address]() { return process->read(address); });
-
+      LivenessChecker::automaton_register_symbol(get_remote_process(), message.name.data(), remote((int*)message.data));
       break;
     }
 
@@ -233,7 +242,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);