Move another function of mc::api, to Transition

diff --git a/src/mc/api.cpp b/src/mc/api.cpp
index 3aa9b9d..6590c22 100644 (file)
--- a/src/mc/api.cpp
+++ b/src/mc/api.cpp
@@ -157,16 +157,6 @@ void Api::mc_exit(int status) const
   mc_model_checker->exit(status);
 }
 
-std::string Api::request_get_dot_output(const Transition* t) const
-{
-  static constexpr std::array<const char*, 13> colors{{"blue", "red", "green3", "goldenrod", "brown", "purple",
-                                                       "magenta", "turquoise4", "gray25", "forestgreen", "hotpink",
-                                                       "lightblue", "tan"}};
-  const char* color = colors[(t->aid_ - 1) % colors.size()];
-
-  return "label = \"" + t->dot_label() + "\", color = " + color + ", fontcolor = " + color;
-}
-
 void Api::restore_state(std::shared_ptr<simgrid::mc::Snapshot> system_state) const
 {
   system_state->restore(&mc_model_checker->get_remote_process());

diff --git a/src/mc/api.hpp b/src/mc/api.hpp
index f871ee6..180b2dd 100644 (file)
--- a/src/mc/api.hpp
+++ b/src/mc/api.hpp
@@ -81,9 +81,6 @@ public:
   unsigned long mc_get_visited_states() const;
   XBT_ATTRIB_NORETURN void mc_exit(int status) const;
 
-  // SIMCALL APIs
-  std::string request_get_dot_output(const Transition* t) const;
-
   // STATE APIs
   void restore_state(std::shared_ptr<simgrid::mc::Snapshot> system_state) const;
 

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index 36a999d..e268d70 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -343,7 +343,7 @@ void LivenessChecker::run()
         this->previous_request_.clear();
       }
       this->previous_pair_    = current_pair->num;
-      this->previous_request_ = api::get().request_get_dot_output(current_pair->graph_state->get_transition());
+      this->previous_request_ = current_pair->graph_state->get_transition()->dot_string();
       if (current_pair->search_cycle)
         fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num);
       fflush(dot_output);

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index cb6b88e..284acd4 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -147,7 +147,7 @@ void SafetyChecker::run()
 
     std::string req_str;
     if (dot_output != nullptr)
-      req_str = api::get().request_get_dot_output(state->get_transition());
+      req_str = state->get_transition()->dot_string();
 
     /* Create the new expanded state (copy the state of MCed into our MCer data) */
     auto next_state = std::make_unique<State>();

diff --git a/src/mc/transition/Transition.cpp b/src/mc/transition/Transition.cpp
index f29da6f..010e23b 100644 (file)
--- a/src/mc/transition/Transition.cpp
+++ b/src/mc/transition/Transition.cpp
@@ -31,9 +31,15 @@ std::string Transition::to_string(bool) const
 {
   return "";
 }
-std::string Transition::dot_label() const
+std::string Transition::dot_string() const
 {
-  return xbt::string_printf("[(%ld)] %s", aid_, Transition::to_c_str(type_));
+  static constexpr std::array<const char*, 13> colors{{"blue", "red", "green3", "goldenrod", "brown", "purple",
+                                                       "magenta", "turquoise4", "gray25", "forestgreen", "hotpink",
+                                                       "lightblue", "tan"}};
+  const char* color = colors[(aid_ - 1) % colors.size()];
+
+  return xbt::string_printf("label = \"[(%ld)] %s\", color = %s, fontcolor = %s", aid_, Transition::to_c_str(type_),
+                            color, color);
 }
 void Transition::replay() const
 {

diff --git a/src/mc/transition/Transition.hpp b/src/mc/transition/Transition.hpp
index e8b8727..eddd404 100644 (file)
--- a/src/mc/transition/Transition.hpp
+++ b/src/mc/transition/Transition.hpp
@@ -55,8 +55,10 @@ public:
   }
   virtual ~Transition();
 
+  /** Returns a textual representation of the transition. Pointer adresses are omitted if verbose=false */
   virtual std::string to_string(bool verbose = false) const;
-  virtual std::string dot_label() const;
+  /** Returns something like >>label = "desc", color = c<< to describe the transition in dot format */
+  virtual std::string dot_string() const;
 
   /* Moves the application toward a path that was already explored, but don't change the current transition */
   void replay() const;

diff --git a/src/mc/transition/TransitionRandom.cpp b/src/mc/transition/TransitionRandom.cpp
index fb87d0d..79f9932 100644 (file)
--- a/src/mc/transition/TransitionRandom.cpp
+++ b/src/mc/transition/TransitionRandom.cpp
@@ -24,10 +24,5 @@ RandomTransition::RandomTransition(aid_t issuer, int times_considered, std::stri
   xbt_assert(stream >> min_ >> max_);
 }
 
-std::string RandomTransition::dot_label() const
-{
-  return Transition::dot_label() + to_c_str(type_);
-}
-
 } // namespace mc
 } // namespace simgrid

diff --git a/src/mc/transition/TransitionRandom.hpp b/src/mc/transition/TransitionRandom.hpp
index 415a5ee..a47a097 100644 (file)
--- a/src/mc/transition/TransitionRandom.hpp
+++ b/src/mc/transition/TransitionRandom.hpp
@@ -17,7 +17,6 @@ class RandomTransition : public Transition {
 
 public:
   std::string to_string(bool verbose) const override;
-  std::string dot_label() const override;
   RandomTransition(aid_t issuer, int times_considered, std::stringstream& stream);
   bool depends(const Transition* other) const override { return false; } // Independent with any other transition
 };