Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Keep pointers to transitions instead of slices
authorMaxwell Pirtle <maxwellpirtle@gmail.com>
Thu, 25 May 2023 09:18:31 +0000 (11:18 +0200)
committerMaxwell Pirtle <maxwellpirtle@gmail.com>
Thu, 25 May 2023 09:18:31 +0000 (11:18 +0200)
Prior to this commit, sleep sets contained slices

src/mc/api/State.cpp
src/mc/api/State.hpp
src/mc/explo/DFSExplorer.cpp

index c8059b5..4600c3e 100644 (file)
@@ -63,16 +63,15 @@ State::State(RemoteApp& remote_app, std::shared_ptr<State> parent_state)
      * And if we kept it and the actor is enabled in this state, mark the actor as already done, so that
      * it is not explored*/
     for (auto& [aid, transition] : parent_state_->get_sleep_set()) {
-      if (not incoming_transition_->depends(&transition)) {
+      if (not incoming_transition_->depends(transition.get())) {
         sleep_set_.try_emplace(aid, transition);
         if (strategy_->actors_to_run_.count(aid) != 0) {
           XBT_DEBUG("Actor %ld will not be explored, for it is in the sleep set", aid);
-
           strategy_->actors_to_run_.at(aid).mark_done();
         }
       } else
         XBT_DEBUG("Transition >>%s<< removed from the sleep set because it was dependent with incoming >>%s<<",
-                  transition.to_string().c_str(), incoming_transition_->to_string().c_str());
+                  transition->to_string().c_str(), incoming_transition_->to_string().c_str());
     }
   }
 }
index 7f0290b..0fee31f 100644 (file)
@@ -44,7 +44,7 @@ class XBT_PRIVATE State : public xbt::Extendable<State> {
   /* Sleep sets are composed of the actor and the corresponding transition that made it being added to the sleep
    * set. With this information, it is check whether it should be removed from it or not when exploring a new
    * transition */
-  std::map<aid_t, Transition> sleep_set_;
+  std::map<aid_t, std::shared_ptr<Transition>> sleep_set_;
 
   /**
    * The wakeup tree with respect to the execution represented
@@ -117,11 +117,8 @@ public:
   std::unordered_set<aid_t> get_backtrack_set() const;
   std::unordered_set<aid_t> get_sleeping_actors() const;
   std::unordered_set<aid_t> get_enabled_actors() const;
-  std::map<aid_t, Transition> const& get_sleep_set() const { return sleep_set_; }
-  void add_sleep_set(std::shared_ptr<Transition> t)
-  {
-    sleep_set_.insert_or_assign(t->aid_, Transition(t->type_, t->aid_, t->times_considered_));
-  }
+  std::map<aid_t, std::shared_ptr<Transition>> const& get_sleep_set() const { return sleep_set_; }
+  void add_sleep_set(std::shared_ptr<Transition> t) { sleep_set_.insert_or_assign(t->aid_, std::move(t)); }
   bool is_actor_sleeping(aid_t actor) const
   {
     return std::find_if(sleep_set_.begin(), sleep_set_.end(), [=](const auto& pair) { return pair.first == actor; }) !=
index af2d8ba..2aef8ce 100644 (file)
@@ -209,7 +209,7 @@ void DFSExplorer::run()
     if (_sg_mc_sleep_set && XBT_LOG_ISENABLED(mc_dfs, xbt_log_priority_verbose)) {
       XBT_VERB("Sleep set actually containing:");
       for (auto& [aid, transition] : state->get_sleep_set())
-        XBT_VERB("  <%ld,%s>", aid, transition.to_string().c_str());
+        XBT_VERB("  <%ld,%s>", aid, transition->to_string().c_str());
     }
 
     /* Actually answer the request: let's execute the selected request (MCed does one step) */