src/mc/mc_api.cpp

   1 #include "mc_api.hpp"
   2
   3 #include "src/mc/Session.hpp"
   4 #include "src/mc/mc_private.hpp"
   5 #include "src/mc/remote/RemoteSimulation.hpp"
   6 #include <xbt/asserts.h>
   7 #include <xbt/log.h>
   8
   9 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_api, mc, "Logging specific to MC Fasade APIs ");
  10
  11 namespace simgrid {
  12 namespace mc {
  13
  14 void mc_api::initialize(char** argv)
  15 {
  16   simgrid::mc::session = new simgrid::mc::Session([argv] {
  17     int i = 1;
  18     while (argv[i] != nullptr && argv[i][0] == '-')
  19       i++;
  20     xbt_assert(argv[i] != nullptr,
  21                "Unable to find a binary to exec on the command line. Did you only pass config flags?");
  22     execvp(argv[i], argv + i);
  23     xbt_die("The model-checked process failed to exec(): %s", strerror(errno));
  24   });
  25 }
  26
  27 void mc_api::s_initialize() const
  28 {
  29   session->initialize();
  30 }
  31
  32 void mc_api::create_model_checker(std::unique_ptr<RemoteSimulation> remote_simulation, int sockfd)
  33 {
  34
  35 }
  36
  37 ModelChecker* mc_api::get_model_checker() const
  38 {
  39     return mc_model_checker;
  40 }
  41
  42 void mc_api::mc_inc_visited_states() const
  43 {
  44   mc_model_checker->visited_states++;
  45 }
  46
  47 void mc_api::mc_inc_executed_trans() const
  48 {
  49   mc_model_checker->executed_transitions++;
  50 }
  51
  52 unsigned long mc_api::mc_get_visited_states() const
  53 {
  54   return mc_model_checker->visited_states;
  55 }
  56
  57 unsigned long mc_api::mc_get_executed_trans() const
  58 {
  59   return mc_model_checker->executed_transitions;
  60 }
  61
  62 bool mc_api::mc_check_deadlock() const
  63 {
  64   return mc_model_checker->checkDeadlock();
  65 }
  66
  67 std::vector<simgrid::mc::ActorInformation>& mc_api::get_actors() const
  68 {
  69   return mc_model_checker->get_remote_simulation().actors();
  70 }
  71
  72 bool mc_api::actor_is_enabled(aid_t pid) const
  73 {
  74   return session->actor_is_enabled(pid);
  75 }
  76
  77 void mc_api::mc_assert(bool notNull, const char* message) const
  78 {
  79   if (notNull)
  80     xbt_assert(mc_model_checker == nullptr, message);
  81   else
  82     xbt_assert(mc_model_checker != nullptr, message);
  83 }
  84
  85 bool mc_api::mc_is_null() const
  86 {
  87   auto is_null = (mc_model_checker == nullptr) ? true : false;
  88   return is_null;
  89 }
  90
  91 Checker* mc_api::mc_get_checker() const
  92 {
  93   return mc_model_checker->getChecker();
  94 }
  95
  96 RemoteSimulation& mc_api::mc_get_remote_simulation() const
  97 {
  98   return mc_model_checker->get_remote_simulation();
  99 }
 100
 101 void mc_api::handle_simcall(Transition const& transition) const
 102 {
 103   mc_model_checker->handle_simcall(transition);
 104 }
 105
 106 void mc_api::mc_wait_for_requests() const
 107 {
 108   mc_model_checker->wait_for_requests();
 109 }
 110
 111 void mc_api::mc_exit(int status) const
 112 {
 113   mc_model_checker->exit(status);
 114 }
 115
 116 std::string const& mc_api::mc_get_host_name(std::string const& hostname) const
 117 {
 118   return mc_model_checker->get_host_name(hostname);
 119 }
 120
 121 PageStore& mc_api::mc_page_store() const
 122 {
 123   return mc_model_checker->page_store();
 124 }
 125
 126 void mc_api::mc_cleanup()
 127 {
 128 }
 129
 130 void mc_api::s_close() const
 131 {
 132   session->close();
 133 }
 134
 135 void mc_api::s_restore_initial_state() const
 136 {
 137   session->restore_initial_state();
 138 }
 139
 140 void mc_api::execute(Transition const& transition)
 141 {
 142   session->execute(transition);
 143 }
 144
 145 void mc_api::s_log_state() const
 146 {
 147   session->log_state();
 148 }
 149
 150 } // namespace mc
 151 } // namespace simgrid