X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/b9f8f01f1e31a9cec9df207ad241e9c732790cc1..22de1606d048d8ad200f93643bc80434644acea7:/src/mc/ModelChecker.cpp

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index 93400edaf8..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. */
@@ -208,14 +208,15 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
       xbt_assert(size == sizeof(message), "Broken message");
       memcpy(&message, buffer, sizeof(message));
       xbt_assert(not message.callback, "Support for client-side function proposition is not implemented.");
-      XBT_DEBUG("Received symbol: %s", message.name);
+      XBT_DEBUG("Received symbol: %s", message.name.data());
 
       if (property_automaton == nullptr)
         property_automaton = xbt_automaton_new();
 
       const RemoteSimulation* process = &this->get_remote_simulation();
       RemotePtr<int> address          = remote((int*)message.data);
-      xbt::add_proposition(property_automaton, message.name, [process, address]() { return process->read(address); });
+      xbt::add_proposition(property_automaton, message.name.data(),
+                           [process, address]() { return process->read(address); });
 
       break;
     }
@@ -307,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()
 {
@@ -325,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;
 }