objectification of MC simcall achieved -- many tests still failing

[simgrid.git] / src / mc / remote / AppSide.cpp

diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp
index 3cd49b2..665da7d 100644 (file)
--- a/src/mc/remote/AppSide.cpp
+++ b/src/mc/remote/AppSide.cpp
@@ -6,6 +6,7 @@
 #include "src/mc/remote/AppSide.hpp"
 #include "src/internal_config.h"
 #include "src/kernel/actor/ActorImpl.hpp"
+#include "src/mc/checker/SimcallInspector.hpp"
 #include <simgrid/modelchecker.h>
 
 #include <cerrno>
@@ -135,6 +136,64 @@ void AppSide::handle_messages() const
         handle_simcall((s_mc_message_simcall_handle_t*)message_buffer.data());
         break;
 
+      case MessageType::SIMCALL_IS_PENDING: {
+        assert_msg_size("SIMCALL_IS_PENDING", s_mc_message_simcall_is_pending_t);
+        auto msg_simcall                = (s_mc_message_simcall_is_pending_t*)message_buffer.data();
+        kernel::actor::ActorImpl* actor = kernel::actor::ActorImpl::by_PID(msg_simcall->aid);
+        xbt_assert(actor != nullptr, "Invalid pid %d", msg_simcall->aid);
+        xbt_assert(actor->simcall_.inspector_, "The transition of %s has no inspector", actor->get_cname());
+        bool value = actor->simcall_.inspector_->is_pending(msg_simcall->time_considered);
+
+        // Send result:
+        s_mc_message_simcall_is_pending_answer_t answer{MessageType::SIMCALL_IS_PENDING_ANSWER, value};
+        xbt_assert(channel_.send(answer) == 0, "Could not send response");
+        break;
+      }
+
+      case MessageType::SIMCALL_IS_VISIBLE: {
+        assert_msg_size("SIMCALL_IS_VISIBLE", s_mc_message_simcall_is_visible_t);
+        auto msg_simcall                = (s_mc_message_simcall_is_visible_t*)message_buffer.data();
+        kernel::actor::ActorImpl* actor = kernel::actor::ActorImpl::by_PID(msg_simcall->aid);
+        xbt_assert(actor != nullptr, "Invalid pid %d", msg_simcall->aid);
+        xbt_assert(actor->simcall_.inspector_, "The transition of %s has no inspector", actor->get_cname());
+        bool value = actor->simcall_.inspector_->is_visible();
+
+        // Send result:
+        s_mc_message_simcall_is_visible_answer_t answer{MessageType::SIMCALL_IS_VISIBLE_ANSWER, value};
+        xbt_assert(channel_.send(answer) == 0, "Could not send response");
+        break;
+      }
+
+      case MessageType::SIMCALL_TO_STRING: {
+        assert_msg_size("SIMCALL_TO_STRING", s_mc_message_simcall_to_string_t);
+        auto msg_simcall                = (s_mc_message_simcall_to_string_t*)message_buffer.data();
+        kernel::actor::ActorImpl* actor = kernel::actor::ActorImpl::by_PID(msg_simcall->aid);
+        xbt_assert(actor != nullptr, "Invalid pid %d", msg_simcall->aid);
+        xbt_assert(actor->simcall_.inspector_, "The transition of %s has no inspector", actor->get_cname());
+        std::string value = actor->simcall_.inspector_->to_string(msg_simcall->time_considered);
+
+        // Send result:
+        s_mc_message_simcall_to_string_answer_t answer{MessageType::SIMCALL_TO_STRING_ANSWER, 0};
+        strcat(answer.value, value.c_str());
+        xbt_assert(channel_.send(answer) == 0, "Could not send response");
+        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();
+        kernel::actor::ActorImpl* actor = kernel::actor::ActorImpl::by_PID(msg_simcall->aid);
+        xbt_assert(actor != nullptr, "Invalid pid %d", msg_simcall->aid);
+        xbt_assert(actor->simcall_.inspector_, "The transition of %s has no inspector", actor->get_cname());
+        std::string value = actor->simcall_.inspector_->dot_label();
+
+        // Send result:
+        s_mc_message_simcall_to_string_answer_t answer{MessageType::SIMCALL_TO_STRING_ANSWER, 0};
+        strcat(answer.value, value.c_str());
+        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());