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"
9 #include <xbt/asserts.h>
12 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_api, mc, "Logging specific to MC Fasade APIs ");
17 void mc_api::initialize(char** argv)
19 simgrid::mc::session = new simgrid::mc::Session([argv] {
21 while (argv[i] != nullptr && argv[i][0] == '-')
23 xbt_assert(argv[i] != nullptr,
24 "Unable to find a binary to exec on the command line. Did you only pass config flags?");
25 execvp(argv[i], argv + i);
26 xbt_die("The model-checked process failed to exec(): %s", strerror(errno));
30 std::vector<simgrid::mc::ActorInformation>& mc_api::get_actors() const
32 return mc_model_checker->get_remote_simulation().actors();
35 bool mc_api::actor_is_enabled(aid_t pid) const
37 return session->actor_is_enabled(pid);
40 unsigned long mc_api::get_maxpid() const
42 return MC_smx_get_maxpid();
45 void mc_api::s_initialize() const
47 session->initialize();
50 ModelChecker* mc_api::get_model_checker() const
52 return mc_model_checker;
55 void mc_api::mc_inc_visited_states() const
57 mc_model_checker->visited_states++;
60 void mc_api::mc_inc_executed_trans() const
62 mc_model_checker->executed_transitions++;
65 unsigned long mc_api::mc_get_visited_states() const
67 return mc_model_checker->visited_states;
70 unsigned long mc_api::mc_get_executed_trans() const
72 return mc_model_checker->executed_transitions;
75 bool mc_api::mc_check_deadlock() const
77 return mc_model_checker->checkDeadlock();
80 void mc_api::mc_show_deadlock() const
85 smx_actor_t mc_api::mc_smx_simcall_get_issuer(s_smx_simcall const* req) const
87 return MC_smx_simcall_get_issuer(req);
90 bool mc_api::mc_is_null() const
92 auto is_null = (mc_model_checker == nullptr) ? true : false;
96 Checker* mc_api::mc_get_checker() const
98 return mc_model_checker->getChecker();
101 RemoteSimulation& mc_api::mc_get_remote_simulation() const
103 return mc_model_checker->get_remote_simulation();
106 void mc_api::handle_simcall(Transition const& transition) const
108 mc_model_checker->handle_simcall(transition);
111 void mc_api::mc_wait_for_requests() const
113 mc_model_checker->wait_for_requests();
116 void mc_api::mc_exit(int status) const
118 mc_model_checker->exit(status);
121 std::string const& mc_api::mc_get_host_name(std::string const& hostname) const
123 return mc_model_checker->get_host_name(hostname);
126 void mc_api::mc_dump_record_path() const
128 simgrid::mc::dumpRecordPath();
131 smx_simcall_t mc_api::mc_state_choose_request(simgrid::mc::State* state) const
133 return MC_state_choose_request(state);
136 bool mc_api::request_depend(smx_simcall_t req1, smx_simcall_t req2) const
138 return simgrid::mc::request_depend(req1, req2);
141 std::string mc_api::request_to_string(smx_simcall_t req, int value, RequestType request_type) const
143 return simgrid::mc::request_to_string(req, value, request_type).c_str();
146 std::string mc_api::request_get_dot_output(smx_simcall_t req, int value) const
148 return simgrid::mc::request_get_dot_output(req, value);
151 const char* mc_api::simix_simcall_name(e_smx_simcall_t kind) const
153 return SIMIX_simcall_name(kind);
156 bool mc_api::snapshot_equal(const Snapshot* s1, const Snapshot* s2) const
158 return simgrid::mc::snapshot_equal(s1, s2);
161 simgrid::mc::Snapshot* mc_api::take_snapshot(int num_state) const
163 auto snapshot = new simgrid::mc::Snapshot(num_state);
167 void mc_api::s_close() const
172 void mc_api::s_restore_initial_state() const
174 session->restore_initial_state();
177 void mc_api::execute(Transition const& transition)
179 session->execute(transition);
182 void mc_api::s_log_state() const
184 session->log_state();
188 } // namespace simgrid