Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
mc::api: Inline a useless function
authorMartin Quinson <martin.quinson@ens-rennes.fr>
Tue, 12 Jul 2022 21:31:23 +0000 (23:31 +0200)
committerMartin Quinson <martin.quinson@ens-rennes.fr>
Wed, 13 Jul 2022 16:16:13 +0000 (18:16 +0200)
src/mc/VisitedState.cpp
src/mc/api.cpp
src/mc/api.hpp
src/mc/explo/DFSExplorer.cpp
src/mc/explo/LivenessChecker.cpp

index 6e46c3c..5ad4043 100644 (file)
@@ -20,7 +20,7 @@ namespace simgrid::mc {
 VisitedState::VisitedState(unsigned long state_number) : num(state_number)
 {
   this->heap_bytes_used = Api::get().get_remote_heap_bytes();
-  this->actors_count    = Api::get().get_actors().size();
+  this->actors_count    = mc_model_checker->get_remote_process().actors().size();
   this->system_state = std::make_shared<simgrid::mc::Snapshot>(state_number);
 }
 
index 638d44a..a29dbf2 100644 (file)
@@ -73,11 +73,6 @@ simgrid::mc::Exploration* Api::initialize(char** argv, const std::unordered_map<
   return explo;
 }
 
-std::vector<simgrid::mc::ActorInformation>& Api::get_actors() const
-{
-  return mc_model_checker->get_remote_process().actors();
-}
-
 unsigned long Api::get_maxpid() const
 {
   return mc_model_checker->get_remote_process().get_maxpid();
index 3edcb07..c30d999 100644 (file)
@@ -57,7 +57,6 @@ public:
                                        simgrid::mc::ExplorationAlgorithm algo);
 
   // ACTOR APIs
-  std::vector<simgrid::mc::ActorInformation>& get_actors() const;
   unsigned long get_maxpid() const;
 
   // REMOTE APIs
index b39b7fb..900c40e 100644 (file)
@@ -165,7 +165,7 @@ void DFSExplorer::run()
     /* If this is a new state (or if we don't care about state-equality reduction) */
     if (visited_state_ == nullptr) {
       /* Get an enabled process and insert it in the interleave set of the next state */
-      auto actors = Api::get().get_actors();
+      auto actors = mc_model_checker->get_remote_process().actors();
       for (auto& remoteActor : actors) {
         auto actor = remoteActor.copy.get_buffer();
         if (get_session().actor_is_enabled(actor->get_pid())) {
@@ -296,7 +296,7 @@ DFSExplorer::DFSExplorer(Session* session) : Exploration(session)
   XBT_DEBUG("**************************************************");
 
   /* Get an enabled actor and insert it in the interleave set of the initial state */
-  auto actors = Api::get().get_actors();
+  auto actors = mc_model_checker->get_remote_process().actors();
   XBT_DEBUG("Initial state. %zu actors to consider", actors.size());
   for (auto& actor : actors) {
     aid_t aid = actor.copy.get_buffer()->get_pid();
index c467eee..0d7acc6 100644 (file)
@@ -27,7 +27,7 @@ VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state,
   if (not this->graph_state->get_system_state())
     this->graph_state->set_system_state(std::make_shared<Snapshot>(pair_num));
   this->heap_bytes_used     = Api::get().get_remote_heap_bytes();
-  this->actors_count        = Api::get().get_actors().size();
+  this->actors_count        = mc_model_checker->get_remote_process().actors().size();
   this->other_num           = -1;
   this->atomic_propositions = std::move(atomic_propositions);
 }
@@ -231,7 +231,7 @@ std::shared_ptr<Pair> LivenessChecker::create_pair(const Pair* current_pair, xbt
   else
     next_pair->depth = 1;
   /* Add all enabled actors to the interleave set of the initial state */
-  for (auto& act : Api::get().get_actors()) {
+  for (auto& act : mc_model_checker->get_remote_process().actors()) {
     auto actor = act.copy.get_buffer();
     if (get_session().actor_is_enabled(actor->get_pid()))
       next_pair->graph_state->mark_todo(actor->get_pid());