Finalize passing transitions during model checking

Transitions are now serialized and sent to the
checker side whenever a new State instance is
created (when the ACTOR_STATUS message is sent
by the checker). Transition serialization is the
first step before the work on the UDPOR branch(es)
can be integrated into Mc SimGrid.

diff --git a/include/xbt/utility.hpp b/include/xbt/utility.hpp
index 34dc34e..6a3b542 100644 (file)
--- a/include/xbt/utility.hpp
+++ b/include/xbt/utility.hpp
@@ -25,6 +25,10 @@
     constexpr std::array<const char*, _XBT_COUNT_ARGS(__VA_ARGS__)> names{{_XBT_STRINGIFY_ARGS(__VA_ARGS__)}};         \
     return names.at(static_cast<int>(value));                                                                          \
   }                                                                                                                    \
+  static constexpr bool is_valid_##EnumType(int raw_value)                                                             \
+  {                                                                                                                    \
+    return raw_value < _XBT_COUNT_ARGS(__VA_ARGS__);                                                                   \
+  }                                                                                                                    \
   enum class EnumType { __VA_ARGS__ } /* defined here to handle trailing semicolon */
 
 namespace simgrid {
@@ -76,6 +80,6 @@ template <class List, class Elem> inline void intrusive_erase(List& list, Elem&
   list.erase(list.iterator_to(elem));
 }
 
-}
-}
+} // namespace xbt
+} // namespace simgrid
 #endif

diff --git a/src/mc/api/RemoteApp.cpp b/src/mc/api/RemoteApp.cpp
index b56d54d..d2a2b61 100644 (file)
--- a/src/mc/api/RemoteApp.cpp
+++ b/src/mc/api/RemoteApp.cpp
@@ -215,14 +215,14 @@ void RemoteApp::get_actors_status(std::map<aid_t, ActorState>& whereto) const
                "(currently %d), but only %d transition(s) was/were said to be encoded",
                actor.max_considered, actor.n_transitions);
 
-    std::stringstream stream((*action_pool_iter).buffer.data());
-    auto actor_transitions = std::vector<std::unique_ptr<Transition>>(actor.max_considered);
-
-    for (int times_considered = 0; times_considered < actor.max_considered; times_considered++, action_pool_iter++) {
+    auto actor_transitions = std::vector<std::unique_ptr<Transition>>(actor.n_transitions);
+    for (int times_considered = 0; times_considered < actor.n_transitions; times_considered++, action_pool_iter++) {
+      std::stringstream stream((*action_pool_iter).buffer.data());
       auto transition = std::unique_ptr<Transition>(deserialize_transition(actor.aid, times_considered, stream));
-      actor_transitions.push_back(std::move(transition));
+      actor_transitions[times_considered] = std::move(transition);
     }
 
+    XBT_DEBUG("Received %d transitions for actor %ld", actor.n_transitions, actor.aid);
     whereto.try_emplace(actor.aid, actor.aid, actor.enabled, actor.max_considered, std::move(actor_transitions));
   }
 }

diff --git a/src/mc/remote/Channel.cpp b/src/mc/remote/Channel.cpp
index b7e70bf..60d5989 100644 (file)
--- a/src/mc/remote/Channel.cpp
+++ b/src/mc/remote/Channel.cpp
@@ -26,23 +26,34 @@ Channel::~Channel()
 /** @brief Send a message; returns 0 on success or errno on failure */
 int Channel::send(const void* message, size_t size) const
 {
-  XBT_DEBUG("Send %s", to_c_str(*(MessageType*)message));
   while (::send(this->socket_, message, size, 0) == -1) {
     if (errno != EINTR) {
       XBT_ERROR("Channel::send failure: %s", strerror(errno));
       return errno;
     }
   }
+
+  if (is_valid_MessageType(*(int*)message)) {
+    XBT_DEBUG("Sending %s (%lu bytes sent)", to_c_str(*(MessageType*)message), size);
+  } else {
+    XBT_DEBUG("Sending bytes directly (from address %p) (%lu bytes sent)", message, size);
+  }
+
   return 0;
 }
 
 ssize_t Channel::receive(void* message, size_t size, bool block) const
 {
   ssize_t res = recv(this->socket_, message, size, block ? 0 : MSG_DONTWAIT);
-  if (res != -1)
-    XBT_DEBUG("Receive %s (requested %lu bytes to be sent; received %lu)", to_c_str(*(MessageType*)message), size, res);
-  else
+  if (res != -1) {
+    if (is_valid_MessageType(*(int*)message)) {
+      XBT_DEBUG("Receive %s (requested %lu; received %lu)", to_c_str(*(MessageType*)message), size, res);
+    } else {
+      XBT_DEBUG("Receive %lu bytes", res);
+    }
+  } else {
     XBT_ERROR("Channel::receive failure: %s", strerror(errno));
+  }
   return res;
 }
 } // namespace simgrid::mc