X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/b5f291a286dc3084e91889db196fa6e1f69fc4b8..9a51b791dab55275bffc183f8dfe9c26b6feaa57:/src/mc/ModelChecker.cpp?ds=sidebyside

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index e5c642f89f..141400a9e8 100644
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -1,4 +1,4 @@
-/* Copyright (c) 2008-2020. The SimGrid Team. All rights reserved.          */
+/* Copyright (c) 2008-2021. The SimGrid Team. All rights reserved.          */
 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
@@ -308,13 +308,74 @@ void ModelChecker::handle_simcall(Transition const& transition)
   s_mc_message_simcall_handle_t m;
   memset(&m, 0, sizeof(m));
   m.type  = MessageType::SIMCALL_HANDLE;
-  m.pid   = transition.pid_;
-  m.value = transition.argument_;
+  m.pid_              = transition.pid_;
+  m.times_considered_ = transition.times_considered_;
   checker_side_.get_channel().send(m);
   this->remote_simulation_->clear_cache();
   if (this->remote_simulation_->running())
     checker_side_.dispatch();
 }
+bool ModelChecker::simcall_is_visible(int aid)
+{
+  xbt_assert(mc_model_checker != nullptr, "This should be called from the checker side");
+
+  s_mc_message_simcall_is_visible_t m;
+  memset(&m, 0, sizeof(m));
+  m.type = MessageType::SIMCALL_IS_VISIBLE;
+  m.aid  = aid;
+  checker_side_.get_channel().send(m);
+
+  s_mc_message_simcall_is_visible_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_IS_VISIBLE_ANSWER,
+             "Received unexpected message %s (%i, size=%i) "
+             "expected MessageType::SIMCALL_IS_VISIBLE_ANSWER (%i, size=%i)",
+             to_c_str(answer.type), (int)answer.type, (int)s, (int)MessageType::SIMCALL_IS_VISIBLE_ANSWER,
+             (int)sizeof(answer));
+
+  XBT_DEBUG("is_visible(%d) is returning %s", aid, answer.value ? "true" : "false");
+
+  this->remote_simulation_->clear_cache();
+  return answer.value;
+}
+
+std::string ModelChecker::simcall_to_string(MessageType type, int 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            = type;
+  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_TO_STRING_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_TO_STRING_ANSWER,
+             (int)sizeof(answer));
+
+  return std::string(answer.value);
+}
+
+std::string ModelChecker::simcall_to_string(int aid, int times_considered)
+{
+  std::string answer = simcall_to_string(MessageType::SIMCALL_TO_STRING, aid, times_considered);
+  XBT_DEBUG("to_string(%d) is returning %s", aid, answer.c_str());
+  return answer;
+}
+
+std::string ModelChecker::simcall_dot_label(int aid, int times_considered)
+{
+  std::string answer = simcall_to_string(MessageType::SIMCALL_DOT_LABEL, aid, times_considered);
+  XBT_DEBUG("dot_label(%d) is returning %s", aid, answer.c_str());
+  return answer;
+}
 
 bool ModelChecker::checkDeadlock()
 {
@@ -326,7 +387,7 @@ bool ModelChecker::checkDeadlock()
   xbt_assert(s == sizeof(message) && message.type == MessageType::DEADLOCK_CHECK_REPLY,
              "Received unexpected message %s (%i, size=%i) "
              "expected MessageType::DEADLOCK_CHECK_REPLY (%i, size=%i)",
-             MC_message_type_name(message.type), (int)message.type, (int)s, (int)MessageType::DEADLOCK_CHECK_REPLY,
+             to_c_str(message.type), (int)message.type, (int)s, (int)MessageType::DEADLOCK_CHECK_REPLY,
              (int)sizeof(message));
   return message.value != 0;
 }