src/mc/Transition.cpp

   1 /* Copyright (c) 2015-2022. The SimGrid Team. All rights reserved.          */
   2
   3 /* This program is free software; you can redistribute it and/or modify it
   4  * under the terms of the license (GNU LGPL) which comes with this package. */
   5
   6 #include "src/mc/Transition.hpp"
   7 #include "src/mc/ModelChecker.hpp"
   8 #include "src/mc/Session.hpp"
   9 #include "src/mc/mc_state.hpp"
  10 #include "src/mc/remote/RemoteProcess.hpp"
  11 #include "xbt/asserts.h"
  12
  13 #include <sstream>
  14
  15 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_transition, mc, "Logging specific to MC transitions");
  16
  17 namespace simgrid {
  18 namespace mc {
  19 unsigned long Transition::executed_transitions_ = 0;
  20 unsigned long Transition::replayed_transitions_ = 0;
  21
  22 std::string Transition::to_string(bool verbose)
  23 {
  24   xbt_assert(mc_model_checker != nullptr, "Must be called from MCer");
  25
  26   return textual_;
  27 }
  28 const char* Transition::to_cstring(bool verbose)
  29 {
  30   xbt_assert(mc_model_checker != nullptr, "Must be called from MCer");
  31
  32   to_string();
  33   return textual_.c_str();
  34 }
  35 void Transition::init(aid_t aid, int times_considered)
  36 {
  37   aid_              = aid;
  38   times_considered_ = times_considered;
  39 }
  40 void Transition::replay() const
  41 {
  42   replayed_transitions_++;
  43
  44   mc_model_checker->handle_simcall(*this, false);
  45   mc_model_checker->wait_for_requests();
  46 }
  47
  48 CommWaitTransition::CommWaitTransition(aid_t issuer, int times_considered, char* buffer)
  49     : Transition(issuer, times_considered)
  50 {
  51   std::stringstream stream(buffer);
  52   stream >> timeout_ >> comm_ >> sender_ >> receiver_ >> mbox_ >> src_buff_ >> dst_buff_ >> size_;
  53 }
  54 std::string CommWaitTransition::to_string(bool verbose)
  55 {
  56   textual_ = Transition::to_string(verbose);
  57   textual_ += xbt::string_printf("[src=%ld -> dst=%ld, mbox=%u, tout=%f", sender_, receiver_, mbox_, timeout_);
  58   if (verbose) {
  59     textual_ += ", src_buff=" + xbt::string_printf("%p", src_buff_) + ", size=" + std::to_string(size_);
  60     textual_ += ", dst_buff=" + xbt::string_printf("%p", dst_buff_);
  61   }
  62   textual_ += "]";
  63   return textual_;
  64 }
  65
  66 CommRecvTransition::CommRecvTransition(aid_t issuer, int times_considered, char* buffer)
  67     : Transition(issuer, times_considered)
  68 {
  69   std::stringstream stream(buffer);
  70   stream >> mbox_ >> dst_buff_;
  71 }
  72 std::string CommRecvTransition::to_string(bool verbose)
  73 {
  74   textual_ = xbt::string_printf("iRecv(recver=%ld mbox=%u", aid_, mbox_);
  75   if (verbose)
  76     textual_ += ", buff=" + xbt::string_printf("%p", dst_buff_);
  77   textual_ += ")";
  78   return textual_;
  79 }
  80 CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, char* buffer)
  81     : Transition(issuer, times_considered)
  82 {
  83   std::stringstream stream(buffer);
  84   stream >> mbox_ >> src_buff_ >> size_;
  85 }
  86 std::string CommSendTransition::to_string(bool verbose = false)
  87 {
  88   textual_ = xbt::string_printf("iSend(sender=%ld mbox=%u", aid_, mbox_);
  89   if (verbose)
  90     textual_ += ", buff=" + xbt::string_printf("%p", src_buff_) + ", size=" + std::to_string(size_);
  91   textual_ += ")";
  92   return textual_;
  93 }
  94
  95 Transition* recv_transition(aid_t issuer, int times_considered, kernel::actor::SimcallObserver::Simcall simcall,
  96                             char* buffer)
  97 {
  98   switch (simcall) {
  99     case kernel::actor::SimcallObserver::Simcall::COMM_WAIT:
 100       return new CommWaitTransition(issuer, times_considered, buffer);
 101     case kernel::actor::SimcallObserver::Simcall::IRECV:
 102       return new CommRecvTransition(issuer, times_considered, buffer);
 103     case kernel::actor::SimcallObserver::Simcall::ISEND:
 104       return new CommSendTransition(issuer, times_considered, buffer);
 105     case kernel::actor::SimcallObserver::Simcall::UNKNOWN:
 106       return new Transition(issuer, times_considered);
 107     default:
 108       xbt_die("recv_transition of type %s unimplemented", kernel::actor::SimcallObserver::to_c_str(simcall));
 109   }
 110 }
 111
 112 } // namespace mc
 113 } // namespace simgrid