kill some bits of mc::api::

diff --git a/src/mc/api.cpp b/src/mc/api.cpp
index 29b0608..450b95a 100644 (file)
--- a/src/mc/api.cpp
+++ b/src/mc/api.cpp
@@ -48,43 +48,6 @@ static simgrid::mc::ActorInformation* actor_info_cast(smx_actor_t actor)
   return process_info;
 }
 
-xbt::string const& Api::get_actor_host_name(smx_actor_t actor) const
-{
-  if (mc_model_checker == nullptr)
-    return actor->get_host()->get_name();
-
-  const simgrid::mc::RemoteProcess* process = &mc_model_checker->get_remote_process();
-
-  // Read the simgrid::xbt::string in the MCed process:
-  simgrid::mc::ActorInformation* info = actor_info_cast(actor);
-
-  if (not info->hostname) {
-    Remote<s4u::Host> temp_host = process->read(remote(actor->get_host()));
-    auto remote_string_address  = remote(&xbt::string::to_string_data(temp_host.get_buffer()->get_impl()->get_name()));
-    simgrid::xbt::string_data remote_string = process->read(remote_string_address);
-    std::vector<char> hostname(remote_string.len + 1);
-    // no need to read the terminating null byte, and thus hostname[remote_string.len] is guaranteed to be '\0'
-    process->read_bytes(hostname.data(), remote_string.len, remote(remote_string.data));
-    info->hostname = &mc_model_checker->get_host_name(hostname.data());
-  }
-  return *info->hostname;
-}
-
-xbt::string const& Api::get_actor_name(smx_actor_t actor) const
-{
-  if (mc_model_checker == nullptr)
-    return actor->get_name();
-
-  simgrid::mc::ActorInformation* info = actor_info_cast(actor);
-  if (info->name.empty()) {
-    const simgrid::mc::RemoteProcess* process = &mc_model_checker->get_remote_process();
-
-    simgrid::xbt::string_data string_data = simgrid::xbt::string::to_string_data(actor->name_);
-    info->name = process->read_string(remote(string_data.data), string_data.len);
-  }
-  return info->name;
-}
-
 simgrid::mc::Exploration* Api::initialize(char** argv, simgrid::mc::CheckerAlgorithm algo) const
 {
   simgrid::mc::session_singleton = std::make_unique<simgrid::mc::Session>([argv] {

diff --git a/src/mc/api.hpp b/src/mc/api.hpp
index 3889583..4c36702 100644 (file)
--- a/src/mc/api.hpp
+++ b/src/mc/api.hpp
@@ -21,18 +21,6 @@ namespace mc {
 
 XBT_DECLARE_ENUM_CLASS(CheckerAlgorithm, Safety, UDPOR, Liveness, CommDeterminism);
 
-/**
- * @brief Maintains the transition's information.
- */
-struct s_transition_detail {
-  simgrid::simix::Simcall call_ = simgrid::simix::Simcall::NONE;
-  long issuer_id                = -1;
-  RemotePtr<kernel::activity::MailboxImpl> mbox_remote_addr {}; // used to represent mailbox remote address for isend and ireceive transitions
-  RemotePtr<kernel::activity::ActivityImpl> comm_remote_addr {}; // the communication this transition concerns (to be used only for isend, ireceive, wait and test)
-};
-
-using transition_detail_t = std::unique_ptr<s_transition_detail>;
-
 /*
 ** This class aimes to implement FACADE APIs for simgrid. The FACADE layer sits between the CheckerSide
 ** (Unfolding_Checker, DPOR, ...) layer and the
@@ -69,10 +57,6 @@ public:
   std::vector<simgrid::mc::ActorInformation>& get_actors() const;
   unsigned long get_maxpid() const;
 
-  // COMMUNICATION APIs
-  xbt::string const& get_actor_name(smx_actor_t actor) const;
-  xbt::string const& get_actor_host_name(smx_actor_t actor) const;
-
   // REMOTE APIs
   std::size_t get_remote_heap_bytes() const;
 
@@ -92,9 +76,7 @@ public:
   void s_close() const;
 
 // AUTOMATION APIs
-#if SIMGRID_HAVE_MC
   void automaton_load(const char* file) const;
-#endif
   std::vector<int> automaton_propositional_symbol_evaluate() const;
   std::vector<xbt_automaton_state_t> get_automaton_state() const;
   int compare_automaton_exp_label(const xbt_automaton_exp_label* l) const;
@@ -103,10 +85,6 @@ public:
   {
     return DerefAndCompareByActorsCountAndUsedHeap();
   }
-  inline int automaton_state_compare(const_xbt_automaton_state_t const& s1, const_xbt_automaton_state_t const& s2) const
-  {
-    return xbt_automaton_state_compare(s1, s2);
-  }
   xbt_automaton_exp_label_t get_automaton_transition_label(xbt_dynar_t const& dynar, int index) const;
   xbt_automaton_state_t get_automaton_transition_dst(xbt_dynar_t const& dynar, int index) const;
 };

diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp
index a0073d2..2b67a9d 100644 (file)
--- a/src/mc/explo/LivenessChecker.cpp
+++ b/src/mc/explo/LivenessChecker.cpp
@@ -71,7 +71,7 @@ std::shared_ptr<VisitedPair> LivenessChecker::insert_acceptance_pair(simgrid::mc
   if (pair->search_cycle)
     for (auto i = res.first; i != res.second; ++i) {
       std::shared_ptr<simgrid::mc::VisitedPair> const& pair_test = *i;
-      if (api::get().automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) != 0 ||
+      if (xbt_automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) != 0 ||
           *(pair_test->atomic_propositions) != *(new_pair->atomic_propositions) ||
           not api::get().snapshot_equal(pair_test->graph_state->system_state_.get(),
                                         new_pair->graph_state->system_state_.get()))
@@ -148,7 +148,7 @@ int LivenessChecker::insert_visited_pair(std::shared_ptr<VisitedPair> visited_pa
 
   for (auto i = range.first; i != range.second; ++i) {
     const VisitedPair* pair_test = i->get();
-    if (api::get().automaton_state_compare(pair_test->automaton_state, visited_pair->automaton_state) != 0 ||
+    if (xbt_automaton_state_compare(pair_test->automaton_state, visited_pair->automaton_state) != 0 ||
         *(pair_test->atomic_propositions) != *(visited_pair->atomic_propositions) ||
         not api::get().snapshot_equal(pair_test->graph_state->system_state_.get(),
                                       visited_pair->graph_state->system_state_.get()))