X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/0ad6bd059ce73f4fcad69113644b928daa520af7..162424b0ac640baa56b0ca9bc158ef9743f0c4ac:/src/mc/api.cpp

diff --git a/src/mc/api.cpp b/src/mc/api.cpp
index e014bedb8e..8bf2519c73 100644
--- a/src/mc/api.cpp
+++ b/src/mc/api.cpp
@@ -11,7 +11,6 @@
 #include "src/mc/Session.hpp"
 #include "src/mc/checker/Checker.hpp"
 #include "src/mc/mc_base.hpp"
-#include "src/mc/mc_comm_pattern.hpp"
 #include "src/mc/mc_exit.hpp"
 #include "src/mc/mc_pattern.hpp"
 #include "src/mc/mc_private.hpp"
@@ -34,24 +33,6 @@ using Simcall = simgrid::simix::Simcall;
 namespace simgrid {
 namespace mc {
 
-static inline const char* get_color(int id)
-{
-  static constexpr std::array<const char*, 13> colors{{"blue", "red", "green3", "goldenrod", "brown", "purple",
-                                                       "magenta", "turquoise4", "gray25", "forestgreen", "hotpink",
-                                                       "lightblue", "tan"}};
-  return colors[id % colors.size()];
-}
-
-static std::string pointer_to_string(void* pointer)
-{
-  return XBT_LOG_ISENABLED(Api, xbt_log_priority_verbose) ? xbt::string_printf("%p", pointer) : "(verbose only)";
-}
-
-static std::string buff_size_to_string(size_t buff_size)
-{
-  return XBT_LOG_ISENABLED(Api, xbt_log_priority_verbose) ? std::to_string(buff_size) : "(verbose only)";
-}
-
 /** Statically "upcast" a s_smx_actor_t into an ActorInformation
  *
  *  This gets 'actorInfo' from '&actorInfo->copy'. It upcasts in the
@@ -67,14 +48,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)
@@ -303,7 +276,7 @@ void Api::mc_check_deadlock() const
     XBT_CINFO(mc_global, "Counter-example execution trace:");
     for (auto const& s : mc_model_checker->getChecker()->get_textual_trace())
       XBT_CINFO(mc_global, "  %s", s.c_str());
-    simgrid::mc::dumpRecordPath();
+    XBT_INFO("Path = %s", mc_model_checker->getChecker()->get_record_trace().to_string().c_str());
     simgrid::mc::session_singleton->log_state();
     throw DeadlockError();
   }
@@ -359,57 +332,14 @@ 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(const Transition* t) 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;
-}
+  static constexpr std::array<const char*, 13> colors{{"blue", "red", "green3", "goldenrod", "brown", "purple",
+                                                       "magenta", "turquoise4", "gray25", "forestgreen", "hotpink",
+                                                       "lightblue", "tan"}};
+  const char* color = colors[(t->aid_ - 1) % colors.size()];
 
-std::string Api::request_get_dot_output(aid_t aid, int value) const
-{
-  const char* color = get_color(aid - 1);
-  return "label = \"" + mc_model_checker->simcall_dot_label(aid, value) + "\", color = " + color +
-         ", fontcolor = " + color;
+  return "label = \"" + t->dot_label() + "\", color = " + color + ", fontcolor = " + color;
 }
 
 #if HAVE_SMPI
@@ -441,7 +371,7 @@ bool Api::snapshot_equal(const Snapshot* s1, const Snapshot* s2) const
   return simgrid::mc::snapshot_equal(s1, s2);
 }
 
-simgrid::mc::Snapshot* Api::take_snapshot(int num_state) const
+simgrid::mc::Snapshot* Api::take_snapshot(long num_state) const
 {
   auto snapshot = new simgrid::mc::Snapshot(num_state);
   return snapshot;
@@ -454,7 +384,10 @@ void Api::s_close() const
 
 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