Move dot_label() from Observer to Transition (+ some reorgs)

diff --git a/src/kernel/actor/SimcallObserver.cpp b/src/kernel/actor/SimcallObserver.cpp
index aa457e4..b816e92 100644 (file)
--- a/src/kernel/actor/SimcallObserver.cpp
+++ b/src/kernel/actor/SimcallObserver.cpp
@@ -28,9 +28,9 @@ bool RandomSimcall::depends(SimcallObserver* other)
 {
   return get_issuer() == other->get_issuer();
 }
-void RandomSimcall::serialize(Simcall& type, std::stringstream& stream)
+void RandomSimcall::serialize(mc::Transition::Type& type, std::stringstream& stream)
 {
-  type = Simcall::RANDOM;
+  type = mc::Transition::Type::RANDOM;
   stream << min_ << ' ' << max_;
 }
 
@@ -57,25 +57,6 @@ bool MutexSimcall::depends(SimcallObserver* other)
   return true; // Depend on things we don't know for sure that they are independent
 }
 
-/*
-std::string SimcallObserver::to_string(int) const
-{
-  return simgrid::xbt::string_printf("[(%ld)%s (%s)] ", issuer_->get_pid(), issuer_->get_host()->get_cname(),
-                                     issuer_->get_cname());
-}*/
-
-std::string SimcallObserver::dot_label(int /*times_considered*/) const
-{
-  if (issuer_->get_host())
-    return xbt::string_printf("[(%ld)%s] ", issuer_->get_pid(), issuer_->get_host()->get_cname());
-  return xbt::string_printf("[(%ld)] ", issuer_->get_pid());
-}
-
-std::string RandomSimcall::dot_label(int times_considered) const
-{
-  return SimcallObserver::dot_label(times_considered) + "MC_RANDOM(" + std::to_string(next_value_) + ")";
-}
-
 void RandomSimcall::prepare(int times_considered)
 {
   next_value_ = min_ + times_considered;
@@ -87,11 +68,6 @@ int RandomSimcall::get_max_consider() const
   return max_ - min_ + 1;
 }
 
-std::string MutexUnlockSimcall::dot_label(int times_considered) const
-{
-  return SimcallObserver::dot_label(times_considered) + "Mutex UNLOCK";
-}
-
 /*
 std::string MutexLockSimcall::to_string(int times_considered) const
 {
@@ -103,21 +79,11 @@ std::string MutexLockSimcall::to_string(int times_considered) const
   return res;
 }*/
 
-std::string MutexLockSimcall::dot_label(int times_considered) const
-{
-  return SimcallObserver::dot_label(times_considered) + (blocking_ ? "Mutex LOCK" : "Mutex TRYLOCK");
-}
-
 bool MutexLockSimcall::is_enabled() const
 {
   return not blocking_ || get_mutex()->get_owner() == nullptr || get_mutex()->get_owner() == get_issuer();
 }
 
-std::string ConditionWaitSimcall::dot_label(int times_considered) const
-{
-  return SimcallObserver::dot_label(times_considered) + "Condition WAIT";
-}
-
 bool ConditionWaitSimcall::is_enabled() const
 {
   static bool warned = false;
@@ -128,11 +94,6 @@ bool ConditionWaitSimcall::is_enabled() const
   return true;
 }
 
-std::string SemAcquireSimcall::dot_label(int times_considered) const
-{
-  return SimcallObserver::dot_label(times_considered) + "Sem ACQUIRE";
-}
-
 bool SemAcquireSimcall::is_enabled() const
 {
   static bool warned = false;
@@ -172,17 +133,6 @@ std::string ActivityTestanySimcall::to_string(int times_considered) const
   return res;
 }*/
 
-std::string ActivityTestanySimcall::dot_label(int times_considered) const
-{
-  std::string res = SimcallObserver::dot_label(times_considered) + "TestAny ";
-  if (times_considered == -1) {
-    res += "FALSE";
-  } else {
-    res += xbt::string_printf("TRUE [%d of %zu]", times_considered + 1, activities_.size());
-  }
-  return res;
-}
-
 bool ActivityTestSimcall::depends(SimcallObserver* other)
 {
   if (get_issuer() == other->get_issuer())
@@ -224,17 +174,17 @@ bool ActivityTestSimcall::depends(SimcallObserver* other)
 
   return true;
 }
-void ActivityWaitSimcall::serialize(Simcall& type, std::stringstream& stream)
+void ActivityWaitSimcall::serialize(mc::Transition::Type& type, std::stringstream& stream)
 {
   if (auto* comm = dynamic_cast<activity::CommImpl*>(activity_)) {
-    type = Simcall::COMM_WAIT;
+    type = mc::Transition::Type::COMM_WAIT;
     stream << (timeout_ > 0) << ' ' << comm;
     stream << ' ' << (comm->src_actor_ != nullptr ? comm->src_actor_->get_pid() : -1);
     stream << ' ' << (comm->dst_actor_ != nullptr ? comm->dst_actor_->get_pid() : -1);
     stream << ' ' << comm->get_mailbox_id();
     stream << ' ' << (void*)comm->src_buff_ << ' ' << (void*)comm->dst_buff_ << ' ' << comm->src_buff_size_;
   } else {
-    type = Simcall::UNKNOWN;
+    type = mc::Transition::Type::UNKNOWN;
   }
 }
 
@@ -263,18 +213,6 @@ std::string ActivityTestSimcall::to_string(int times_considered) const
   return res;
 }*/
 
-std::string ActivityTestSimcall::dot_label(int times_considered) const
-{
-  std::string res  = SimcallObserver::dot_label(times_considered) + "Test ";
-  const auto* comm = dynamic_cast<activity::CommImpl*>(activity_);
-  if (comm && (comm->src_actor_.get() == nullptr || comm->dst_actor_.get() == nullptr)) {
-    res += "FALSE";
-  } else {
-    res += "TRUE";
-  }
-  return res;
-}
-
 bool ActivityWaitSimcall::is_enabled() const
 {
   /* FIXME: check also that src and dst processes are not suspended */
@@ -294,28 +232,6 @@ bool ActivityWaitSimcall::is_enabled() const
   return (comm->src_actor_ && comm->dst_actor_);
 }
 
-std::string ActivityWaitSimcall::dot_label(int times_considered) const
-{
-  std::string res = SimcallObserver::dot_label(times_considered);
-  res += (times_considered == -1) ? "WaitTimeout " : "Wait ";
-
-  const auto* comm = dynamic_cast<activity::CommImpl*>(activity_);
-  if (comm) {
-    auto src = comm->src_actor_;
-    auto dst = comm->dst_actor_;
-    res += " [(" + std::to_string(src ? src->get_pid() : 0) + ")";
-    res += "->(" + std::to_string(dst ? dst->get_pid() : 0) + ")]";
-  } else
-    xbt_die("Only Comms are supported here for now");
-  return res;
-}
-
-std::string ActivityWaitanySimcall::dot_label(int times_considered) const
-{
-  return SimcallObserver::dot_label(times_considered) +
-         xbt::string_printf("WaitAny [%d of %zu]", times_considered + 1, activities_.size());
-}
-
 bool ActivityWaitanySimcall::is_enabled() const
 {
   // FIXME: deal with other kind of activities (Exec and I/Os)
@@ -345,16 +261,16 @@ void ActivityWaitanySimcall::prepare(int times_considered)
   next_value_ = times_considered;
 }
 
-void CommIsendSimcall::serialize(Simcall& type, std::stringstream& stream)
+void CommIsendSimcall::serialize(mc::Transition::Type& type, std::stringstream& stream)
 {
-  type = Simcall::ISEND;
+  type = mc::Transition::Type::ISEND;
   stream << mbox_->get_id() << ' ' << (void*)src_buff_ << ' ' << src_buff_size_;
   XBT_DEBUG("SendObserver mbox:%u buff:%p size:%zu", mbox_->get_id(), src_buff_, src_buff_size_);
 }
 
-void CommIrecvSimcall::serialize(Simcall& type, std::stringstream& stream)
+void CommIrecvSimcall::serialize(mc::Transition::Type& type, std::stringstream& stream)
 {
-  type = Simcall::IRECV;
+  type = mc::Transition::Type::IRECV;
   stream << mbox_->get_id() << dst_buff_;
 }
 

diff --git a/src/kernel/actor/SimcallObserver.hpp b/src/kernel/actor/SimcallObserver.hpp
index 002d36f..18ce979 100644 (file)
--- a/src/kernel/actor/SimcallObserver.hpp
+++ b/src/kernel/actor/SimcallObserver.hpp
@@ -7,8 +7,8 @@
 #define SIMGRID_MC_SIMCALL_OBSERVER_HPP
 
 #include "simgrid/forward.h"
+#include "src/mc/api/Transition.hpp"
 #include "xbt/asserts.h"
-#include "xbt/utility.hpp"
 
 #include <string>
 
@@ -20,8 +20,6 @@ class SimcallObserver {
   ActorImpl* const issuer_;
 
 public:
-  XBT_DECLARE_ENUM_CLASS(Simcall, UNKNOWN, RANDOM, ISEND, IRECV, COMM_WAIT, COMM_TEST);
-
   explicit SimcallObserver(ActorImpl* issuer) : issuer_(issuer) {}
   ActorImpl* get_issuer() const { return issuer_; }
   /** Whether this transition can currently be taken without blocking.
@@ -56,12 +54,14 @@ public:
   virtual bool depends(SimcallObserver* other);
 
   /** Serialize to the given string buffer */
-  virtual void serialize(Simcall& type, std::stringstream& stream) { type = Simcall::UNKNOWN; }
+  virtual void serialize(mc::Transition::Type& type, std::stringstream& stream)
+  {
+    type = mc::Transition::Type::UNKNOWN;
+  }
 
   /** Some simcalls may only be observable under some conditions.
    * Most simcalls are not visible from the MC because they don't have an observer at all. */
   virtual bool is_visible() const { return true; }
-  virtual std::string dot_label(int times_considered) const = 0;
 };
 
 template <class T> class ResultingSimcall : public SimcallObserver {
@@ -84,10 +84,9 @@ public:
   {
     xbt_assert(min < max);
   }
-  void serialize(Simcall& type, std::stringstream& stream) override;
+  void serialize(mc::Transition::Type& type, std::stringstream& stream) override;
   int get_max_consider() const override;
   void prepare(int times_considered) override;
-  std::string dot_label(int times_considered) const override;
   int get_value() const { return next_value_; }
   bool depends(SimcallObserver* other) override;
 };
@@ -103,9 +102,6 @@ public:
 
 class MutexUnlockSimcall : public MutexSimcall {
   using MutexSimcall::MutexSimcall;
-
-public:
-  std::string dot_label(int times_considered) const override;
 };
 
 class MutexLockSimcall : public MutexSimcall {
@@ -117,7 +113,6 @@ public:
   {
   }
   bool is_enabled() const override;
-  std::string dot_label(int times_considered) const override;
 };
 
 class ConditionWaitSimcall : public ResultingSimcall<bool> {
@@ -133,7 +128,6 @@ public:
   }
   bool is_enabled() const override;
   bool is_visible() const override { return false; }
-  std::string dot_label(int times_considered) const override;
   activity::ConditionVariableImpl* get_cond() const { return cond_; }
   activity::MutexImpl* get_mutex() const { return mutex_; }
   double get_timeout() const { return timeout_; }
@@ -150,7 +144,6 @@ public:
   }
   bool is_enabled() const override;
   bool is_visible() const override { return false; }
-  std::string dot_label(int times_considered) const override;
   activity::SemaphoreImpl* get_sem() const { return sem_; }
   double get_timeout() const { return timeout_; }
 };
@@ -165,7 +158,6 @@ public:
   }
   bool is_visible() const override { return true; }
   bool depends(SimcallObserver* other) override;
-  std::string dot_label(int times_considered) const override;
   activity::ActivityImpl* get_activity() const { return activity_; }
 };
 
@@ -181,7 +173,6 @@ public:
   bool is_visible() const override { return true; }
   int get_max_consider() const override;
   void prepare(int times_considered) override;
-  std::string dot_label(int times_considered) const override;
   const std::vector<activity::ActivityImpl*>& get_activities() const { return activities_; }
   int get_value() const { return next_value_; }
 };
@@ -195,10 +186,9 @@ public:
       : ResultingSimcall(actor, false), activity_(activity), timeout_(timeout)
   {
   }
-  void serialize(Simcall& type, std::stringstream& stream) override;
+  void serialize(mc::Transition::Type& type, std::stringstream& stream) override;
   bool is_visible() const override { return true; }
   bool is_enabled() const override;
-  std::string dot_label(int times_considered) const override;
   activity::ActivityImpl* get_activity() const { return activity_; }
   void set_activity(activity::ActivityImpl* activity) { activity_ = activity; }
   double get_timeout() const { return timeout_; }
@@ -218,7 +208,6 @@ public:
   bool is_visible() const override { return true; }
   void prepare(int times_considered) override;
   int get_max_consider() const override;
-  std::string dot_label(int times_considered) const override;
   const std::vector<activity::ActivityImpl*>& get_activities() const { return activities_; }
   double get_timeout() const { return timeout_; }
   int get_value() const { return next_value_; }
@@ -256,12 +245,8 @@ public:
       , copy_data_fun_(copy_data_fun)
   {
   }
-  void serialize(Simcall& type, std::stringstream& stream) override;
+  void serialize(mc::Transition::Type& type, std::stringstream& stream) override;
   bool is_visible() const override { return true; }
-  std::string dot_label(int times_considered) const override
-  {
-    return SimcallObserver::dot_label(times_considered) + "iSend";
-  }
   activity::MailboxImpl* get_mailbox() const { return mbox_; }
   double get_payload_size() const { return payload_size_; }
   double get_rate() const { return rate_; }
@@ -295,12 +280,8 @@ public:
       , copy_data_fun_(copy_data_fun)
   {
   }
-  void serialize(Simcall& type, std::stringstream& stream) override;
+  void serialize(mc::Transition::Type& type, std::stringstream& stream) override;
   bool is_visible() const override { return true; }
-  std::string dot_label(int times_considered) const override
-  {
-    return SimcallObserver::dot_label(times_considered) + "iRecv";
-  }
   activity::MailboxImpl* get_mailbox() const { return mbox_; }
   double get_rate() const { return rate_; }
   unsigned char* get_dst_buff() const { return dst_buff_; }

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index 4d74699..fdae4fe 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -361,30 +361,6 @@ bool ModelChecker::simcall_is_visible(aid_t aid)
   return answer.value;
 }
 
-std::string ModelChecker::simcall_dot_label(aid_t aid, int times_considered)
-{
-  xbt_assert(mc_model_checker != nullptr, "This should be called from the checker side");
-
-  s_mc_message_simcall_to_string_t m;
-  memset(&m, 0, sizeof(m));
-  m.type            = MessageType::SIMCALL_DOT_LABEL;
-  m.aid             = aid;
-  m.time_considered = times_considered;
-  checker_side_.get_channel().send(m);
-
-  s_mc_message_simcall_to_string_answer_t answer;
-  ssize_t s = checker_side_.get_channel().receive(answer);
-  xbt_assert(s != -1, "Could not receive message");
-  xbt_assert(s == sizeof(answer) && answer.type == MessageType::SIMCALL_DOT_LABEL_ANSWER,
-             "Received unexpected message %s (%i, size=%i) "
-             "expected MessageType::SIMCALL_TO_STRING_ANSWER (%i, size=%i)",
-             to_c_str(answer.type), (int)answer.type, (int)s, (int)MessageType::SIMCALL_DOT_LABEL_ANSWER,
-             (int)sizeof(answer));
-
-  XBT_DEBUG("dot_label(%ld) is returning %s", aid, answer.value);
-  return answer.value;
-}
-
 void ModelChecker::finalize_app(bool terminate_asap)
 {
   s_mc_message_int_t m;

diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp
index daee1b9..ab99ea5 100644 (file)
--- a/src/mc/ModelChecker.hpp
+++ b/src/mc/ModelChecker.hpp
@@ -56,7 +56,6 @@ public:
 
   /* Interactions with the simcall observer */
   bool simcall_is_visible(aid_t aid);
-  std::string simcall_dot_label(aid_t aid, int times_considered);
 
   XBT_ATTRIB_NORETURN void exit(int status);
 

diff --git a/src/mc/api.cpp b/src/mc/api.cpp
index c99d687..09764e4 100644 (file)
--- a/src/mc/api.cpp
+++ b/src/mc/api.cpp
@@ -351,11 +351,10 @@ void Api::mc_exit(int status) const
   mc_model_checker->exit(status);
 }
 
-std::string Api::request_get_dot_output(aid_t aid, int value) const
+std::string Api::request_get_dot_output(const Transition* t) const
 {
-  const char* color = get_color(aid - 1);
-  return "label = \"" + mc_model_checker->simcall_dot_label(aid, value) + "\", color = " + color +
-         ", fontcolor = " + color;
+  const char* color = get_color(t->aid_ - 1);
+  return "label = \"" + t->dot_label() + "\", color = " + color + ", fontcolor = " + color;
 }
 
 #if HAVE_SMPI

diff --git a/src/mc/api.hpp b/src/mc/api.hpp
index c7fd769..9da3c6d 100644 (file)
--- a/src/mc/api.hpp
+++ b/src/mc/api.hpp
@@ -101,7 +101,7 @@ public:
   XBT_ATTRIB_NORETURN void mc_exit(int status) const;
 
   // SIMCALL APIs
-  std::string request_get_dot_output(aid_t aid, int value) const;
+  std::string request_get_dot_output(const Transition* t) const;
   smx_actor_t simcall_get_issuer(s_smx_simcall const* req) const;
   RemotePtr<kernel::activity::MailboxImpl> get_mbox_remote_addr(smx_simcall_t const req) const;
   RemotePtr<kernel::activity::ActivityImpl> get_comm_remote_addr(smx_simcall_t const req) const;

diff --git a/src/mc/api/Transition.cpp b/src/mc/api/Transition.cpp
index 229e546..0af324b 100644 (file)
--- a/src/mc/api/Transition.cpp
+++ b/src/mc/api/Transition.cpp
@@ -24,14 +24,13 @@ unsigned long Transition::replayed_transitions_ = 0;
 // Do not move this to the header, to ensure that we have a vtable for Transition
 Transition::~Transition() = default;
 
-std::string Transition::to_string(bool)
+std::string Transition::to_string(bool) const
 {
-  return textual_;
+  return "";
 }
-const char* Transition::to_cstring(bool verbose)
+std::string Transition::dot_label() const
 {
-  to_string(verbose);
-  return textual_.c_str();
+  return xbt::string_printf("[(%ld)] %s", aid_, Transition::to_c_str(type_));
 }
 void Transition::replay() const
 {
@@ -42,17 +41,21 @@ void Transition::replay() const
   mc_model_checker->wait_for_requests();
 #endif
 }
-std::string RandomTransition::to_string(bool verbose)
+std::string RandomTransition::to_string(bool verbose) const
 {
   return xbt::string_printf("Random([%d;%d] ~> %d)", min_, max_, times_considered_);
 }
 
 RandomTransition::RandomTransition(aid_t issuer, int times_considered, char* buffer)
-    : Transition(issuer, times_considered)
+    : Transition(Type::RANDOM, issuer, times_considered)
 {
   std::stringstream stream(buffer);
   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/api/Transition.hpp b/src/mc/api/Transition.hpp
index 416241b..1db0101 100644 (file)
--- a/src/mc/api/Transition.hpp
+++ b/src/mc/api/Transition.hpp
@@ -8,6 +8,7 @@
 #define SIMGRID_MC_TRANSITION_HPP
 
 #include "simgrid/forward.h" // aid_t
+#include "xbt/utility.hpp"   // XBT_DECLARE_ENUM_CLASS
 
 #include <string>
 
@@ -29,10 +30,10 @@ class Transition {
 
   friend State; // FIXME remove this once we have a proper class to handle the statistics
 
-protected:
-  std::string textual_ = "";
-
 public:
+  XBT_DECLARE_ENUM_CLASS(Type, UNKNOWN, RANDOM, ISEND, IRECV, COMM_WAIT, COMM_TEST);
+  Type type_ = Type::UNKNOWN;
+
   aid_t aid_ = 0;
 
   /* Which transition was executed for this simcall
@@ -46,11 +47,14 @@ public:
   int times_considered_ = 0;
 
   Transition() = default;
+  Transition(Type type, aid_t issuer, int times_considered)
+      : type_(type), aid_(issuer), times_considered_(times_considered)
+  {
+  }
   virtual ~Transition();
-  Transition(aid_t issuer, int times_considered) : aid_(issuer), times_considered_(times_considered) {}
 
-  virtual std::string to_string(bool verbose = false);
-  const char* to_cstring(bool verbose = false);
+  virtual std::string to_string(bool verbose = false) const;
+  virtual std::string dot_label() const;
 
   /* Moves the application toward a path that was already explored, but don't change the current transition */
   void replay() const;
@@ -68,7 +72,8 @@ class RandomTransition : public Transition {
   int max_;
 
 public:
-  std::string to_string(bool verbose) override;
+  std::string to_string(bool verbose) const override;
+  std::string dot_label() const override;
   RandomTransition(aid_t issuer, int times_considered, char* buffer);
   bool depends(const Transition* other) const override { return false; } // Independent with any other transition
 };

diff --git a/src/mc/api/TransitionComm.cpp b/src/mc/api/TransitionComm.cpp
index 6fa6730..da627c5 100644 (file)
--- a/src/mc/api/TransitionComm.cpp
+++ b/src/mc/api/TransitionComm.cpp
@@ -21,23 +21,23 @@ namespace simgrid {
 namespace mc {
 
 CommWaitTransition::CommWaitTransition(aid_t issuer, int times_considered, char* buffer)
-    : Transition(issuer, times_considered)
+    : Transition(Type::COMM_WAIT, issuer, times_considered)
 {
   std::stringstream stream(buffer);
   stream >> timeout_ >> comm_ >> sender_ >> receiver_ >> mbox_ >> src_buff_ >> dst_buff_ >> size_;
   XBT_DEBUG("CommWaitTransition %s comm:%p, sender:%ld receiver:%ld mbox:%u sbuff:%p rbuff:%p size:%zu",
             (timeout_ ? "timeout" : "no-timeout"), comm_, sender_, receiver_, mbox_, src_buff_, dst_buff_, size_);
 }
-std::string CommWaitTransition::to_string(bool verbose)
+std::string CommWaitTransition::to_string(bool verbose) const
 {
-  textual_ = xbt::string_printf("%ld: WaitComm(from %ld to %ld, mbox=%u, %s", aid_, sender_, receiver_, mbox_,
+  auto res = xbt::string_printf("%ld: WaitComm(from %ld to %ld, mbox=%u, %s", aid_, sender_, receiver_, mbox_,
                                 (timeout_ ? "timeout" : "no timeout"));
   if (verbose) {
-    textual_ += ", src_buff=" + xbt::string_printf("%p", src_buff_) + ", size=" + std::to_string(size_);
-    textual_ += ", dst_buff=" + xbt::string_printf("%p", dst_buff_);
+    res += ", src_buff=" + xbt::string_printf("%p", src_buff_) + ", size=" + std::to_string(size_);
+    res += ", dst_buff=" + xbt::string_printf("%p", dst_buff_);
   }
-  textual_ += ")";
-  return textual_;
+  res += ")";
+  return res;
 }
 bool CommWaitTransition::depends(const Transition* other) const
 {
@@ -69,18 +69,18 @@ bool CommWaitTransition::depends(const Transition* other) const
 }
 
 CommRecvTransition::CommRecvTransition(aid_t issuer, int times_considered, char* buffer)
-    : Transition(issuer, times_considered)
+    : Transition(Type::IRECV, issuer, times_considered)
 {
   std::stringstream stream(buffer);
   stream >> mbox_ >> dst_buff_;
 }
-std::string CommRecvTransition::to_string(bool verbose)
+std::string CommRecvTransition::to_string(bool verbose) const
 {
-  textual_ = xbt::string_printf("%ld: iRecv(mbox=%u", aid_, mbox_);
+  auto res = xbt::string_printf("%ld: iRecv(mbox=%u", aid_, mbox_);
   if (verbose)
-    textual_ += ", buff=" + xbt::string_printf("%p", dst_buff_);
-  textual_ += ")";
-  return textual_;
+    res += ", buff=" + xbt::string_printf("%p", dst_buff_);
+  res += ")";
+  return res;
 }
 bool CommRecvTransition::depends(const Transition* other) const
 {
@@ -118,20 +118,21 @@ bool CommRecvTransition::depends(const Transition* other) const
 }
 
 CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, char* buffer)
-    : Transition(issuer, times_considered)
+    : Transition(Type::ISEND, issuer, times_considered)
 {
   std::stringstream stream(buffer);
   stream >> mbox_ >> src_buff_ >> size_;
   XBT_DEBUG("SendTransition mbox:%u buff:%p size:%zu", mbox_, src_buff_, size_);
 }
-std::string CommSendTransition::to_string(bool verbose = false)
+std::string CommSendTransition::to_string(bool verbose = false) const
 {
-  textual_ = xbt::string_printf("%ld: iSend(mbox=%u", aid_, mbox_);
+  auto res = xbt::string_printf("%ld: iSend(mbox=%u", aid_, mbox_);
   if (verbose)
-    textual_ += ", buff=" + xbt::string_printf("%p", src_buff_) + ", size=" + std::to_string(size_);
-  textual_ += ")";
-  return textual_;
+    res += ", buff=" + xbt::string_printf("%p", src_buff_) + ", size=" + std::to_string(size_);
+  res += ")";
+  return res;
 }
+
 bool CommSendTransition::depends(const Transition* other) const
 {
   if (aid_ == other->aid_)
@@ -167,24 +168,23 @@ bool CommSendTransition::depends(const Transition* other) const
   return true;
 }
 
-Transition* recv_transition(aid_t issuer, int times_considered, kernel::actor::SimcallObserver::Simcall simcall,
-                            char* buffer)
+Transition* recv_transition(aid_t issuer, int times_considered, Transition::Type simcall, char* buffer)
 {
   switch (simcall) {
-    case kernel::actor::SimcallObserver::Simcall::COMM_WAIT:
+    case Transition::Type::COMM_WAIT:
       return new CommWaitTransition(issuer, times_considered, buffer);
-    case kernel::actor::SimcallObserver::Simcall::IRECV:
+    case Transition::Type::IRECV:
       return new CommRecvTransition(issuer, times_considered, buffer);
-    case kernel::actor::SimcallObserver::Simcall::ISEND:
+    case Transition::Type::ISEND:
       return new CommSendTransition(issuer, times_considered, buffer);
 
-    case kernel::actor::SimcallObserver::Simcall::RANDOM:
+    case Transition::Type::RANDOM:
       return new RandomTransition(issuer, times_considered, buffer);
 
-    case kernel::actor::SimcallObserver::Simcall::UNKNOWN:
-      return new Transition(issuer, times_considered);
+    case Transition::Type::UNKNOWN:
+      return new Transition(Transition::Type::UNKNOWN, issuer, times_considered);
     default:
-      xbt_die("recv_transition of type %s unimplemented", kernel::actor::SimcallObserver::to_c_str(simcall));
+      xbt_die("recv_transition of type %s unimplemented", Transition::to_c_str(simcall));
   }
 }
 

diff --git a/src/mc/api/TransitionComm.hpp b/src/mc/api/TransitionComm.hpp
index e2103fa..3e83dca 100644 (file)
--- a/src/mc/api/TransitionComm.hpp
+++ b/src/mc/api/TransitionComm.hpp
@@ -32,7 +32,7 @@ class CommWaitTransition : public Transition {
 
 public:
   CommWaitTransition(aid_t issuer, int times_considered, char* buffer);
-  std::string to_string(bool verbose) override;
+  std::string to_string(bool verbose) const override;
   bool depends(const Transition* other) const override;
 };
 
@@ -42,7 +42,7 @@ class CommRecvTransition : public Transition {
 
 public:
   CommRecvTransition(aid_t issuer, int times_considered, char* buffer);
-  std::string to_string(bool verbose) override;
+  std::string to_string(bool verbose) const override;
   bool depends(const Transition* other) const override;
 };
 
@@ -53,13 +53,12 @@ class CommSendTransition : public Transition {
 
 public:
   CommSendTransition(aid_t issuer, int times_considered, char* buffer);
-  std::string to_string(bool verbose) override;
+  std::string to_string(bool verbose) const override;
   bool depends(const Transition* other) const override;
 };
 
 /** Make a new transition from serialized description */
-Transition* recv_transition(aid_t issuer, int times_considered, kernel::actor::SimcallObserver::Simcall simcall,
-                            char* buffer);
+Transition* recv_transition(aid_t issuer, int times_considered, Transition::Type simcall, char* buffer);
 
 } // namespace mc
 } // namespace simgrid

diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp
index 388e9e2..249d869 100644 (file)
--- a/src/mc/checker/CommunicationDeterminismChecker.cpp
+++ b/src/mc/checker/CommunicationDeterminismChecker.cpp
@@ -420,15 +420,14 @@ void CommunicationDeterminismChecker::real_run()
     if (next_transition >= 0 && visited_state == nullptr) {
       cur_state->execute_next(next_transition);
 
-      aid_t aid         = cur_state->get_transition()->aid_;
       int req_num       = cur_state->get_transition()->times_considered_;
       smx_simcall_t req = &cur_state->executed_req_;
 
-      XBT_DEBUG("Execute: %s", cur_state->get_transition()->to_cstring());
+      XBT_DEBUG("Execute: %s", cur_state->get_transition()->to_string().c_str());
 
       std::string req_str;
       if (dot_output != nullptr)
-        req_str = api::get().request_get_dot_output(aid, req_num);
+        req_str = api::get().request_get_dot_output(cur_state->get_transition());
 
       /* TODO : handle test and testany simcalls */
       CallType call = CallType::NONE;

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index e8f39c1..41a4c2f 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -123,7 +123,7 @@ void LivenessChecker::replay()
 
     if (pair->exploration_started) {
       state->get_transition()->replay();
-      XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, state->get_transition()->to_cstring(), state.get());
+      XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, state->get_transition()->to_string().c_str(), state.get());
     }
 
     /* Update statistics */
@@ -333,13 +333,8 @@ void LivenessChecker::run()
       }
     }
 
-    int next = current_pair->graph_state->next_transition();
-
-    current_pair->graph_state->execute_next(next);
-
-    aid_t aid   = current_pair->graph_state->get_transition()->aid_;
-    int req_num = current_pair->graph_state->get_transition()->times_considered_;
-    XBT_DEBUG("Execute: %s", current_pair->graph_state->get_transition()->to_cstring());
+    current_pair->graph_state->execute_next(current_pair->graph_state->next_transition());
+    XBT_DEBUG("Execute: %s", current_pair->graph_state->get_transition()->to_string().c_str());
 
     if (dot_output != nullptr) {
       if (this->previous_pair_ != 0 && this->previous_pair_ != current_pair->num) {
@@ -348,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(aid, req_num);
+      this->previous_request_ = api::get().request_get_dot_output(current_pair->graph_state->get_transition());
       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 5a8c938..c79f384 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -128,12 +128,11 @@ void SafetyChecker::run()
 
     // If there are processes to interleave and the maximum depth has not been
     // reached then perform one step of the exploration algorithm.
-    XBT_DEBUG("Execute: %s", state->get_transition()->to_cstring());
+    XBT_DEBUG("Execute: %s", state->get_transition()->to_string().c_str());
 
     std::string req_str;
     if (dot_output != nullptr)
-      req_str =
-          api::get().request_get_dot_output(state->get_transition()->aid_, state->get_transition()->times_considered_);
+      req_str = api::get().request_get_dot_output(state->get_transition());
 
     /* Create the new expanded state (copy the state of MCed into our MCer data) */
     auto next_state              = std::make_unique<State>();
@@ -193,13 +192,13 @@ void SafetyChecker::backtrack()
       for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
         State* prev_state = i->get();
         if (state->get_transition()->aid_ == prev_state->get_transition()->aid_) {
-          XBT_DEBUG("Simcall >>%s<< and >>%s<< with same issuer %ld", state->get_transition()->to_cstring(),
-                    prev_state->get_transition()->to_cstring(), issuer_id);
+          XBT_DEBUG("Simcall >>%s<< and >>%s<< with same issuer %ld", state->get_transition()->to_string().c_str(),
+                    prev_state->get_transition()->to_string().c_str(), issuer_id);
           break;
         } else if (prev_state->get_transition()->depends(state->get_transition())) {
           XBT_VERB("Dependent Transitions:");
-          XBT_VERB("  %s (state=%ld)", prev_state->get_transition()->to_cstring(), prev_state->num_);
-          XBT_VERB("  %s (state=%ld)", state->get_transition()->to_cstring(), state->num_);
+          XBT_VERB("  %s (state=%ld)", prev_state->get_transition()->to_string().c_str(), prev_state->num_);
+          XBT_VERB("  %s (state=%ld)", state->get_transition()->to_string().c_str(), state->num_);
 
           if (not prev_state->actor_states_[issuer_id].is_done())
             prev_state->mark_todo(issuer_id);
@@ -208,8 +207,8 @@ void SafetyChecker::backtrack()
           break;
         } else {
           XBT_VERB("INDEPENDENT Transitions:");
-          XBT_VERB("  %s (state=%ld)", prev_state->get_transition()->to_cstring(), prev_state->num_);
-          XBT_VERB("  %s (state=%ld)", state->get_transition()->to_cstring(), state->num_);
+          XBT_VERB("  %s (state=%ld)", prev_state->get_transition()->to_string().c_str(), prev_state->num_);
+          XBT_VERB("  %s (state=%ld)", state->get_transition()->to_string().c_str(), state->num_);
         }
       }
     }

diff --git a/src/mc/mc_record.cpp b/src/mc/mc_record.cpp
index 2e330d6..c33e7e0 100644 (file)
--- a/src/mc/mc_record.cpp
+++ b/src/mc/mc_record.cpp
@@ -65,7 +65,7 @@ simgrid::mc::RecordTrace::RecordTrace(const char* data)
 
     if(count != 2 && count != 1)
       throw std::invalid_argument("Could not parse record path");
-    push_back(new simgrid::mc::Transition(aid, times_considered));
+    push_back(new simgrid::mc::Transition(simgrid::mc::Transition::Type::UNKNOWN, aid, times_considered));
 
     // Find next chunk:
     const char* end = std::strchr(current, ';');

diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp
index e0026c0..3517fe1 100644 (file)
--- a/src/mc/remote/AppSide.cpp
+++ b/src/mc/remote/AppSide.cpp
@@ -110,11 +110,11 @@ void AppSide::handle_simcall_execute(const s_mc_message_simcall_execute_t* messa
                "The serialized simcall is too large for the buffer. Please fix the code.");
     strncpy(answer.buffer, stream.str().c_str(), SIMCALL_SERIALIZATION_BUFFER_SIZE);
   } else {
-    answer.simcall = kernel::actor::SimcallObserver::Simcall::UNKNOWN;
+    answer.simcall = mc::Transition::Type::UNKNOWN;
   }
 
-  XBT_DEBUG("send SIMCALL_EXECUTE_ANSWER(%s) ~> %s '%s'", actor->get_cname(),
-            simgrid::kernel::actor::SimcallObserver::to_c_str(answer.simcall), answer.buffer);
+  XBT_DEBUG("send SIMCALL_EXECUTE_ANSWER(%s) ~> %s '%s'", actor->get_cname(), mc::Transition::to_c_str(answer.simcall),
+            answer.buffer);
   xbt_assert(channel_.send(answer) == 0, "Could not send response");
 
   // The client may send some messages to the server while processing the transition
@@ -176,24 +176,6 @@ void AppSide::handle_messages() const
         break;
       }
 
-      case MessageType::SIMCALL_DOT_LABEL: {
-        assert_msg_size("SIMCALL_DOT_LABEL", s_mc_message_simcall_to_string_t);
-        auto msg_simcall                      = (s_mc_message_simcall_to_string_t*)message_buffer.data();
-        const kernel::actor::ActorImpl* actor = kernel::actor::ActorImpl::by_pid(msg_simcall->aid);
-        xbt_assert(actor != nullptr, "Invalid pid %ld", msg_simcall->aid);
-        std::string value = "";
-        if (actor->simcall_.observer_ != nullptr)
-          value = actor->simcall_.observer_->dot_label(msg_simcall->time_considered);
-        else
-          value = "UNIMPLEMENTED";
-
-        // Send result:
-        s_mc_message_simcall_to_string_answer_t answer{MessageType::SIMCALL_DOT_LABEL_ANSWER, {0}};
-        value.copy(answer.value, (sizeof answer.value) - 1); // last byte was set to '\0' by initialization above
-        xbt_assert(channel_.send(answer) == 0, "Could not send response");
-        break;
-      }
-
       case MessageType::ACTOR_ENABLED:
         assert_msg_size("ACTOR_ENABLED", s_mc_message_actor_enabled_t);
         handle_actor_enabled((s_mc_message_actor_enabled_t*)message_buffer.data());

diff --git a/src/mc/remote/mc_protocol.h b/src/mc/remote/mc_protocol.h
index 8def3da..d8915e5 100644 (file)
--- a/src/mc/remote/mc_protocol.h
+++ b/src/mc/remote/mc_protocol.h
@@ -32,8 +32,8 @@ namespace mc {
 
 XBT_DECLARE_ENUM_CLASS(MessageType, NONE, INITIAL_ADDRESSES, CONTINUE, IGNORE_HEAP, UNIGNORE_HEAP, IGNORE_MEMORY,
                        STACK_REGION, REGISTER_SYMBOL, DEADLOCK_CHECK, DEADLOCK_CHECK_REPLY, WAITING, SIMCALL_EXECUTE,
-                       SIMCALL_EXECUTE_ANSWER, SIMCALL_IS_VISIBLE, SIMCALL_IS_VISIBLE_ANSWER, SIMCALL_DOT_LABEL,
-                       SIMCALL_DOT_LABEL_ANSWER, ASSERTION_FAILED, ACTOR_ENABLED, ACTOR_ENABLED_REPLY, FINALIZE);
+                       SIMCALL_EXECUTE_ANSWER, SIMCALL_IS_VISIBLE, SIMCALL_IS_VISIBLE_ANSWER, ASSERTION_FAILED,
+                       ACTOR_ENABLED, ACTOR_ENABLED_REPLY, FINALIZE);
 
 #define SIMCALL_SERIALIZATION_BUFFER_SIZE 2048
 
@@ -105,7 +105,7 @@ struct s_mc_message_simcall_execute_t {
 };
 struct s_mc_message_simcall_execute_answer_t {
   simgrid::mc::MessageType type;
-  simgrid::kernel::actor::SimcallObserver::Simcall simcall;
+  simgrid::mc::Transition::Type simcall;
   char buffer[SIMCALL_SERIALIZATION_BUFFER_SIZE];
 };
 
@@ -129,15 +129,5 @@ struct s_mc_message_simcall_is_visible_answer_t { // MessageType::SIMCALL_IS_VIS
   bool value;
 };
 
-struct s_mc_message_simcall_to_string_t { // MessageType::SIMCALL_DOT_LABEL
-  simgrid::mc::MessageType type;
-  aid_t aid;
-  int time_considered;
-};
-struct s_mc_message_simcall_to_string_answer_t { // MessageType::SIMCALL_DOT_LABEL_ANSWER
-  simgrid::mc::MessageType type;
-  char value[1024];
-};
-
 #endif // __cplusplus
 #endif