Move the dot_output global into ModelChecker

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index 9e24ee2..17e2bce 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -67,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();
 
@@ -88,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", "*"),

diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp
index 87b1e0e..8f80eae 100644 (file)
--- a/src/mc/ModelChecker.hpp
+++ b/src/mc/ModelChecker.hpp
@@ -28,6 +28,8 @@ class ModelChecker {
   std::unique_ptr<RemoteProcess> remote_process_;
   Exploration* exploration_ = nullptr;
 
+  FILE* dot_output_ = nullptr;
+
   unsigned long visited_states_ = 0;
 
 public:
@@ -63,6 +65,18 @@ public:
   unsigned long get_visited_states() const { return visited_states_; }
   void inc_visited_states() { visited_states_++; }
 
+  void dot_output(const char* fmt, ...);
+  void dot_output_flush()
+  {
+    if (dot_output_ != nullptr)
+      fflush(dot_output_);
+  }
+  void dot_output_close()
+  {
+    if (dot_output_ != nullptr)
+      fclose(dot_output_);
+  }
+
 private:
   void setup_ignore();
   bool handle_message(const char* buffer, ssize_t size);

diff --git a/src/mc/VisitedState.cpp b/src/mc/VisitedState.cpp
index 5e45f71..fa2302a 100644 (file)
--- a/src/mc/VisitedState.cpp
+++ b/src/mc/VisitedState.cpp
@@ -63,11 +63,8 @@ VisitedStates::addVisitedState(unsigned long state_number, simgrid::mc::State* g
         else // I'm the copy of a copy
           new_state->original_num = old_state->original_num;
 
-        if (dot_output == nullptr)
-          XBT_DEBUG("State %ld already visited ! (equal to state %ld)", new_state->num, old_state->num);
-        else
-          XBT_DEBUG("State %ld already visited ! (equal to state %ld (state %ld in dot_output))", new_state->num,
-                    old_state->num, new_state->original_num);
+        XBT_DEBUG("State %ld already visited ! (equal to state %ld (state %ld in dot_output))", new_state->num,
+                  old_state->num, new_state->original_num);
 
         /* Replace the old state with the new one (with a bigger num)
            (when the max number of visited states is reached,  the oldest

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index 3ad1173..1bd4125 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -169,14 +169,14 @@ void DFSExplorer::run()
         }
       }
 
-      if (dot_output != nullptr)
-        std::fprintf(dot_output, "\"%ld\" -> \"%ld\" [%s];\n", state->get_num(), next_state->get_num(),
-                     state->get_transition()->dot_string().c_str());
-
-    } else if (dot_output != nullptr)
-      std::fprintf(dot_output, "\"%ld\" -> \"%ld\" [%s];\n", state->get_num(),
-                   visited_state_->original_num == -1 ? visited_state_->num : visited_state_->original_num,
-                   state->get_transition()->dot_string().c_str());
+      mc_model_checker->dot_output("\"%ld\" -> \"%ld\" [%s];\n", state->get_num(), next_state->get_num(),
+                                   state->get_transition()->dot_string().c_str());
+
+    } else
+      mc_model_checker->dot_output("\"%ld\" -> \"%ld\" [%s];\n", state->get_num(),
+                                   visited_state_->original_num == -1 ? visited_state_->num
+                                                                      : visited_state_->original_num,
+                                   state->get_transition()->dot_string().c_str());
 
     stack_.push_back(std::move(next_state));
   }

diff --git a/src/mc/explo/Exploration.cpp b/src/mc/explo/Exploration.cpp
index d50266c..e23d38c 100644 (file)
--- a/src/mc/explo/Exploration.cpp
+++ b/src/mc/explo/Exploration.cpp
@@ -19,8 +19,8 @@ Exploration::Exploration(const std::vector<char*>& args) : remote_app_(std::make
 void Exploration::log_state()
 {
   if (not _sg_mc_dot_output_file.get().empty()) {
-    fprintf(dot_output, "}\n");
-    fclose(dot_output);
+    mc_model_checker->dot_output("}\n");
+    mc_model_checker->dot_output_close();
   }
   if (getenv("SIMGRID_MC_SYSTEM_STATISTICS")) {
     int ret = system("free");

diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp
index 3b61b6b..3d45e8d 100644 (file)
--- a/src/mc/explo/LivenessChecker.cpp
+++ b/src/mc/explo/LivenessChecker.cpp
@@ -74,9 +74,8 @@ std::shared_ptr<VisitedPair> LivenessChecker::insert_acceptance_pair(simgrid::mc
         continue;
       XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num);
       exploration_stack_.pop_back();
-      if (dot_output != nullptr)
-        fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, pair_test->num,
-                this->previous_request_.c_str());
+      mc_model_checker->dot_output("\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, pair_test->num,
+                                   this->previous_request_.c_str());
       return nullptr;
     }
 
@@ -154,11 +153,8 @@ int LivenessChecker::insert_visited_pair(std::shared_ptr<VisitedPair> visited_pa
       visited_pair->other_num = pair_test->num;
     else
       visited_pair->other_num = pair_test->other_num;
-    if (dot_output == nullptr)
-      XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", visited_pair->num, pair_test->num);
-    else
-      XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", visited_pair->num,
-                pair_test->num, visited_pair->other_num);
+    XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", visited_pair->num, pair_test->num,
+              visited_pair->other_num);
     (*i) = std::move(visited_pair);
     return (*i)->other_num;
   }
@@ -388,11 +384,10 @@ void LivenessChecker::run()
     if (not current_pair->exploration_started) {
       int visited_num = this->insert_visited_pair(reached_pair, current_pair.get());
       if (visited_num != -1) {
-        if (dot_output != nullptr) {
-          fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, visited_num,
-                  this->previous_request_.c_str());
-          fflush(dot_output);
-        }
+        mc_model_checker->dot_output("\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, visited_num,
+                                     this->previous_request_.c_str());
+        mc_model_checker->dot_output_flush();
+
         XBT_DEBUG("Pair already visited (equal to pair %d), exploration on the current path stopped.", visited_num);
         current_pair->requests = 0;
         this->backtrack();
@@ -403,18 +398,17 @@ void LivenessChecker::run()
     current_pair->app_state_->execute_next(current_pair->app_state_->next_transition());
     XBT_DEBUG("Execute: %s", current_pair->app_state_->get_transition()->to_string().c_str());
 
-    if (dot_output != nullptr) {
-      if (this->previous_pair_ != 0 && this->previous_pair_ != current_pair->num) {
-        fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, current_pair->num,
-                this->previous_request_.c_str());
-        this->previous_request_.clear();
-      }
-      this->previous_pair_    = current_pair->num;
-      this->previous_request_ = current_pair->app_state_->get_transition()->dot_string();
-      if (current_pair->search_cycle)
-        fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num);
-      fflush(dot_output);
+    /* Update the dot output */
+    if (this->previous_pair_ != 0 && this->previous_pair_ != current_pair->num) {
+      mc_model_checker->dot_output("\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, current_pair->num,
+                                   this->previous_request_.c_str());
+      this->previous_request_.clear();
     }
+    this->previous_pair_    = current_pair->num;
+    this->previous_request_ = current_pair->app_state_->get_transition()->dot_string();
+    if (current_pair->search_cycle)
+      mc_model_checker->dot_output("%d [shape=doublecircle];\n", current_pair->num);
+    mc_model_checker->dot_output_flush();
 
     if (not current_pair->exploration_started)
       visited_pairs_count_++;

diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index dacf7e4..e58176f 100644 (file)
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -39,23 +39,8 @@ std::vector<double> processes_time;
 
 #if SIMGRID_HAVE_MC
 
-/* Dot output */
-FILE *dot_output = nullptr;
-
-void MC_init_dot_output()
-{
-  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");
-}
-
 namespace simgrid::mc {
 
-/* Liveness */
-xbt_automaton_t property_automaton = nullptr;
-
 /*******************************  Core of MC *******************************/
 /**************************************************************************/
 void dumpStack(FILE* file, unw_cursor_t* cursor)

diff --git a/src/mc/mc_private.hpp b/src/mc/mc_private.hpp
index 969d5fe..b3168d1 100644 (file)
--- a/src/mc/mc_private.hpp
+++ b/src/mc/mc_private.hpp
@@ -12,12 +12,6 @@
 #include "src/mc/mc_forward.hpp"
 #include "src/xbt/memory_map.hpp"
 
-/********************************* MC Global **********************************/
-
-XBT_PRIVATE void MC_init_dot_output();
-
-XBT_PRIVATE extern FILE* dot_output;
-
 /********************************** Miscellaneous **********************************/
 namespace simgrid::mc {