X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/4164a74926df84d357f66508c72d0dd716de5387..a0c8da3bbcebc9266ce49ee6e48c2b1d52b4a5f8:/src/mc/api/State.hpp

diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp
index a991219bc2..0852cd27ff 100644
--- a/src/mc/api/State.hpp
+++ b/src/mc/api/State.hpp
@@ -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
@@ -52,6 +52,7 @@ class XBT_PRIVATE State : public xbt::Extendable<State> {
    * and with respect to this state's sleep set
    */
   odpor::WakeupTree wakeup_tree_;
+  bool has_initialized_wakeup_tree = false;
 
 public:
   explicit State(RemoteApp& remote_app);
@@ -102,7 +103,7 @@ public:
 
   /**
    * @brief Computes the backtrack set for this state
-   * according to its definition in Simgrid.
+   * according to its definition in SimGrid.
    *
    * The backtrack set as it appears in DPOR, SDPOR, and ODPOR
    * in SimGrid consists of those actors marked as `todo`
@@ -114,10 +115,14 @@ public:
    * backtrack set still contains processes added to the done set.
    */
   std::unordered_set<aid_t> get_backtrack_set() const;
-  std::map<aid_t, Transition> const& get_sleep_set() const { return sleep_set_; }
-  void add_sleep_set(std::shared_ptr<Transition> t)
+  std::unordered_set<aid_t> get_sleeping_actors() const;
+  std::unordered_set<aid_t> get_enabled_actors() const;
+  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
   {
-    sleep_set_.insert_or_assign(t->aid_, Transition(t->type_, t->aid_, t->times_considered_));
+    return std::find_if(sleep_set_.begin(), sleep_set_.end(), [=](const auto& pair) { return pair.first == actor; }) !=
+           sleep_set_.end();
   }
 
   /**
@@ -136,6 +141,36 @@ public:
    */
   void seed_wakeup_tree_if_needed(const odpor::Execution& prior);
 
+  /**
+   * @brief Initializes the wakeup_tree_ instance by taking the subtree rooted at the
+   * single-process node `N` running actor `p := "actor taken by parent to form this state"`
+   * of the *parent's* wakeup tree
+   */
+  void sprout_tree_from_parent_state();
+
+  /**
+   * @brief Removes the subtree rooted at the single-process node
+   * `N` running actor `p` of this state's wakeup tree
+   */
+  void remove_subtree_using_current_out_transition();
+  bool has_empty_tree() const { return this->wakeup_tree_.empty(); }
+
+  /**
+   * @brief
+   */
+  odpor::WakeupTree::InsertionResult insert_into_wakeup_tree(const odpor::PartialExecution&, const odpor::Execution&);
+
+  /** @brief Prepares the state for re-exploration following
+   * another after having followed ODPOR from this state with
+   * the current out transition
+   *
+   * After ODPOR has completed searching a maximal trace, it
+   * finds the first point in the execution with a nonempty wakeup
+   * tree. This method corresponds to lines 20 and 21 in the ODPOR
+   * pseudocode
+   */
+  void do_odpor_unwind();
+
   /* Returns the total amount of states created so far (for statistics) */
   static long get_expanded_states() { return expended_states_; }
 };