Add some debug info

[simgrid.git] / src / mc / api / State.hpp

diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp
index aa04094..f10d7bd 100644 (file)
--- 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
@@ -103,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`
@@ -117,10 +117,12 @@ 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)
+  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();
   }
 
   /**
@@ -150,16 +152,26 @@ public:
    * @brief Removes the subtree rooted at the single-process node
    * `N` running actor `p` of this state's wakeup tree
    */
-  void remove_subtree_starting_with(aid_t p);
+  void remove_subtree_using_current_out_transition();
   bool has_empty_tree() const { return this->wakeup_tree_.empty(); }
+  std::string string_of_wut() const { return this->wakeup_tree_.string_of_whole_tree(); }
 
+  
   /**
    * @brief
    */
-  void mark_path_interesting_for_odpor(const odpor::PartialExecution&, const odpor::Execution&);
+  odpor::WakeupTree::InsertionResult insert_into_wakeup_tree(const odpor::PartialExecution&, const odpor::Execution&);
 
-  /** */
-  void do_odpor_backtrack_cleanup();
+  /** @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_; }