Stop copying transitions around since that would shorten the virtual methods

[simgrid.git] / src / mc / api.cpp

diff --git a/src/mc/api.cpp b/src/mc/api.cpp
index be6c716625dca4a70ce2ee4a7c21d1b81114ee14..2c40c20069475aa97e8b4bfe2acc3eb32560b9dd 100644 (file)
--- a/src/mc/api.cpp
+++ b/src/mc/api.cpp
@@ -67,14 +67,6 @@ simgrid::mc::ActorInformation* Api::actor_info_cast(smx_actor_t actor) const
   return process_info;
 }
 
-bool Api::requests_are_dependent(RemotePtr<kernel::actor::SimcallObserver> obs1,
-                                 RemotePtr<kernel::actor::SimcallObserver> obs2) const
-{
-  xbt_assert(mc_model_checker != nullptr, "Must be called from MCer");
-
-  return mc_model_checker->requests_are_dependent(obs1, obs2);
-}
-
 xbt::string const& Api::get_actor_host_name(smx_actor_t actor) const
 {
   if (mc_model_checker == nullptr)
@@ -289,21 +281,11 @@ void Api::mc_inc_visited_states() const
   mc_model_checker->visited_states++;
 }
 
-void Api::mc_inc_executed_trans() const
-{
-  mc_model_checker->executed_transitions++;
-}
-
 unsigned long Api::mc_get_visited_states() const
 {
   return mc_model_checker->visited_states;
 }
 
-unsigned long Api::mc_get_executed_trans() const
-{
-  return mc_model_checker->executed_transitions;
-}
-
 void Api::mc_check_deadlock() const
 {
   if (mc_model_checker->checkDeadlock()) {
@@ -364,88 +346,16 @@ RemotePtr<kernel::activity::ActivityImpl> Api::get_comm_remote_addr(smx_simcall_
   THROW_IMPOSSIBLE;
 }
 
-void Api::handle_simcall(Transition const& transition) const
-{
-  mc_model_checker->handle_simcall(transition);
-}
-
-void Api::mc_wait_for_requests() const
-{
-  mc_model_checker->wait_for_requests();
-}
-
 void Api::mc_exit(int status) const
 {
   mc_model_checker->exit(status);
 }
 
-void Api::dump_record_path() const
+std::string Api::request_get_dot_output(aid_t aid, int value) const
 {
-  simgrid::mc::dumpRecordPath();
-}
-
-/* Search for an enabled transition amongst actors
- *
- * This is the first actor marked TODO by the checker, and currently enabled in the application.
- *
- * Once we found it, prepare its execution (increase the times_considered of its observer and remove it as done on need)
- *
- * If we can't find any actor, return false
- */
-
-bool Api::mc_state_choose_request(simgrid::mc::State* state) const
-{
-  RemoteProcess& process = mc_model_checker->get_remote_process();
-  XBT_DEBUG("Search for an actor to run. %zu actors to consider", process.actors().size());
-  for (auto& actor_info : process.actors()) {
-    auto actor                           = actor_info.copy.get_buffer();
-    simgrid::mc::ActorState* actor_state = &state->actor_states_[actor->get_pid()];
-
-    /* Only consider actors (1) marked as interleaving by the checker and (2) currently enabled in the application*/
-    if (not actor_state->is_todo() || not simgrid::mc::actor_is_enabled(actor))
-      continue;
-
-    /* This actor is ready to be executed. Prepare its execution when simcall_handle will be called on it */
-    if (actor->simcall_.observer_ != nullptr) {
-      state->transition_.times_considered_ = actor_state->get_times_considered_and_inc();
-      if (actor->simcall_.mc_max_consider_ <= actor_state->get_times_considered())
-        actor_state->set_done();
-    } else {
-      state->transition_.times_considered_ = 0;
-      actor_state->set_done();
-    }
-
-    state->transition_.aid_ = actor->get_pid();
-    state->executed_req_    = actor->simcall_;
-
-    XBT_DEBUG("Let's run actor %ld, going for transition %s", actor->get_pid(),
-              SIMIX_simcall_name(state->executed_req_));
-    return true;
-  }
-  return false;
-}
-
-std::string Api::request_to_string(smx_simcall_t req, int value) const
-{
-  xbt_assert(mc_model_checker != nullptr, "Must be called from MCer");
-
-  smx_actor_t issuer = simcall_get_issuer(req);
-
-  if (issuer->simcall_.observer_ != nullptr)
-    return mc_model_checker->simcall_to_string(issuer->get_pid(), value);
-  else
-    return "[" + get_actor_string(issuer) + "] " + SIMIX_simcall_name(*req) + "(unknown?)";
-}
-
-std::string Api::request_get_dot_output(smx_simcall_t req, int value) const
-{
-  if (req->observer_ != nullptr) {
-    const smx_actor_t issuer = simcall_get_issuer(req);
-    const char* color        = get_color(issuer->get_pid() - 1);
-    return "label = \"" + mc_model_checker->simcall_dot_label(issuer->get_pid(), value) + "\", color = " + color +
-           ", fontcolor = " + color;
-  } else
-    return "UNIMPLEMENTED";
+  const char* color = get_color(aid - 1);
+  return "label = \"" + mc_model_checker->simcall_dot_label(aid, value) + "\", color = " + color +
+         ", fontcolor = " + color;
 }
 
 #if HAVE_SMPI
@@ -488,16 +398,12 @@ void Api::s_close() const
   session_singleton->close();
 }
 
-RemotePtr<simgrid::kernel::actor::SimcallObserver> Api::execute(Transition& transition, smx_simcall_t simcall) const
-{
-  /* FIXME: once all simcalls have observers, kill the simcall parameter and use mc_model_checker->simcall_to_string() */
-  transition.textual = request_to_string(simcall, transition.times_considered_);
-  return session_singleton->execute(transition);
-}
-
 void Api::automaton_load(const char* file) const
 {
-  MC_automaton_load(file);
+  if (simgrid::mc::property_automaton == nullptr)
+    simgrid::mc::property_automaton = xbt_automaton_new();
+
+  xbt_automaton_load(simgrid::mc::property_automaton, file);
 }
 
 std::vector<int> Api::automaton_propositional_symbol_evaluate() const