+void Session::check_deadlock() const
+{
+ xbt_assert(model_checker_->channel().send(MessageType::DEADLOCK_CHECK) == 0, "Could not check deadlock state");
+ s_mc_message_int_t message;
+ ssize_t s = model_checker_->channel().receive(message);
+ xbt_assert(s != -1, "Could not receive message");
+ 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)",
+ to_c_str(message.type), (int)message.type, (int)s, (int)MessageType::DEADLOCK_CHECK_REPLY,
+ (int)sizeof(message));
+
+ if (message.value != 0) {
+ XBT_CINFO(mc_global, "**************************");
+ XBT_CINFO(mc_global, "*** DEADLOCK DETECTED ***");
+ XBT_CINFO(mc_global, "**************************");
+ XBT_CINFO(mc_global, "Counter-example execution trace:");
+ for (auto const& frame : model_checker_->get_exploration()->get_textual_trace())
+ XBT_CINFO(mc_global, " %s", frame.c_str());
+ XBT_CINFO(mc_global, "Path = %s", model_checker_->get_exploration()->get_record_trace().to_string().c_str());
+ log_state();
+ throw DeadlockError();
+ }