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/mc_smx.hpp"
   6 #include "src/mc/remote/RemoteSimulation.hpp"
   7 #include "src/mc/mc_record.hpp"
   8 #include "src/mc/mc_comm_pattern.hpp"
   9
  10 #include <xbt/asserts.h>
  11 #include <xbt/log.h>
  12
  13 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_api, mc, "Logging specific to MC Fasade APIs ");
  14
  15 namespace simgrid {
  16 namespace mc {
  17
  18 void mc_api::initialize(char** argv)
  19 {
  20   simgrid::mc::session = new simgrid::mc::Session([argv] {
  21     int i = 1;
  22     while (argv[i] != nullptr && argv[i][0] == '-')
  23       i++;
  24     xbt_assert(argv[i] != nullptr,
  25                "Unable to find a binary to exec on the command line. Did you only pass config flags?");
  26     execvp(argv[i], argv + i);
  27     xbt_die("The model-checked process failed to exec(): %s", strerror(errno));
  28   });
  29 }
  30
  31 std::vector<simgrid::mc::ActorInformation>& mc_api::get_actors() const
  32 {
  33   return mc_model_checker->get_remote_simulation().actors();
  34 }
  35
  36 bool mc_api::actor_is_enabled(aid_t pid) const
  37 {
  38   return session->actor_is_enabled(pid);
  39 }
  40
  41 unsigned long mc_api::get_maxpid() const
  42 {
  43   return MC_smx_get_maxpid();
  44 }
  45
  46 void mc_api::copy_incomplete_comm_pattern(const simgrid::mc::State* state) const
  47 {
  48   MC_state_copy_incomplete_communications_pattern((simgrid::mc::State*)state);
  49 }
  50
  51 void mc_api::copy_index_comm_pattern(const simgrid::mc::State* state) const
  52 {
  53   MC_state_copy_index_communications_pattern((simgrid::mc::State*)state);
  54 }
  55
  56 void mc_api::s_initialize() const
  57 {
  58   session->initialize();
  59 }
  60
  61 ModelChecker* mc_api::get_model_checker() const
  62 {
  63   return mc_model_checker;
  64 }
  65
  66 void mc_api::mc_inc_visited_states() const
  67 {
  68   mc_model_checker->visited_states++;
  69 }
  70
  71 void mc_api::mc_inc_executed_trans() const
  72 {
  73   mc_model_checker->executed_transitions++;
  74 }
  75
  76 unsigned long mc_api::mc_get_visited_states() const
  77 {
  78   return mc_model_checker->visited_states;
  79 }
  80
  81 unsigned long mc_api::mc_get_executed_trans() const
  82 {
  83   return mc_model_checker->executed_transitions;
  84 }
  85
  86 bool mc_api::mc_check_deadlock() const
  87 {
  88   return mc_model_checker->checkDeadlock();
  89 }
  90
  91 void mc_api::mc_show_deadlock() const
  92 {
  93   MC_show_deadlock();
  94 }
  95
  96 smx_actor_t mc_api::mc_smx_simcall_get_issuer(s_smx_simcall const* req) const
  97 {
  98   return MC_smx_simcall_get_issuer(req);
  99 }
 100
 101 bool mc_api::mc_is_null() const
 102 {
 103   auto is_null = (mc_model_checker == nullptr) ? true : false;
 104   return is_null;
 105 }
 106
 107 Checker* mc_api::mc_get_checker() const
 108 {
 109   return mc_model_checker->getChecker();
 110 }
 111
 112 RemoteSimulation& mc_api::mc_get_remote_simulation() const
 113 {
 114   return mc_model_checker->get_remote_simulation();
 115 }
 116
 117 void mc_api::handle_simcall(Transition const& transition) const
 118 {
 119   mc_model_checker->handle_simcall(transition);
 120 }
 121
 122 void mc_api::mc_wait_for_requests() const
 123 {
 124   mc_model_checker->wait_for_requests();
 125 }
 126
 127 void mc_api::mc_exit(int status) const
 128 {
 129   mc_model_checker->exit(status);
 130 }
 131
 132 std::string const& mc_api::mc_get_host_name(std::string const& hostname) const
 133 {
 134   return mc_model_checker->get_host_name(hostname);
 135 }
 136
 137 void mc_api::mc_dump_record_path() const
 138 {
 139   simgrid::mc::dumpRecordPath();
 140 }
 141
 142 smx_simcall_t mc_api::mc_state_choose_request(simgrid::mc::State* state) const
 143 {
 144   return MC_state_choose_request(state);
 145 }
 146
 147 bool mc_api::request_depend(smx_simcall_t req1, smx_simcall_t req2) const
 148 {
 149   return simgrid::mc::request_depend(req1, req2);
 150 }
 151
 152 std::string mc_api::request_to_string(smx_simcall_t req, int value, RequestType request_type) const
 153 {
 154   return simgrid::mc::request_to_string(req, value, request_type).c_str();
 155 }
 156
 157 std::string mc_api::request_get_dot_output(smx_simcall_t req, int value) const
 158 {
 159   return simgrid::mc::request_get_dot_output(req, value);
 160 }
 161
 162 const char* mc_api::simix_simcall_name(e_smx_simcall_t kind) const
 163 {
 164   return SIMIX_simcall_name(kind);
 165 }
 166
 167 bool mc_api::snapshot_equal(const Snapshot* s1, const Snapshot* s2) const
 168 {
 169   return simgrid::mc::snapshot_equal(s1, s2);
 170 }
 171
 172 simgrid::mc::Snapshot* mc_api::take_snapshot(int num_state) const
 173 {
 174   auto snapshot = new simgrid::mc::Snapshot(num_state);
 175   return snapshot;
 176 }
 177
 178 void mc_api::s_close() const
 179 {
 180   session->close();
 181 }
 182
 183 void mc_api::s_restore_initial_state() const
 184 {
 185   session->restore_initial_state();
 186 }
 187
 188 void mc_api::execute(Transition const& transition)
 189 {
 190   session->execute(transition);
 191 }
 192
 193 void mc_api::s_log_state() const
 194 {
 195   session->log_state();
 196 }
 197
 198 } // namespace mc
 199 } // namespace simgrid