X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/16e87acf00914bbe8a17f80a352dda60a02894ad..0f0aacb167ddc9427ea1da1c8f1b66ef2d6f532e:/src/mc/api/State.hpp

diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp
index 0fee31f710..6603ff0831 100644
--- a/src/mc/api/State.hpp
+++ b/src/mc/api/State.hpp
@@ -13,10 +13,6 @@
 #include "src/mc/explo/odpor/WakeupTree.hpp"
 #include "src/mc/transition/Transition.hpp"
 
-#if SIMGRID_HAVE_STATEFUL_MC
-#include "src/mc/sosp/Snapshot.hpp"
-#endif
-
 namespace simgrid::mc {
 
 /* A node in the exploration graph (kind-of) */
@@ -32,9 +28,6 @@ class XBT_PRIVATE State : public xbt::Extendable<State> {
   /** Sequential state ID (used for debugging) */
   long num_ = 0;
 
-  /** Snapshot of system state (if needed) */
-  std::shared_ptr<Snapshot> system_state_;
-
   /** Unique parent of this state. Required both for sleep set computation
       and for guided model-checking */
   std::shared_ptr<State> parent_state_ = nullptr;
@@ -98,12 +91,9 @@ public:
   unsigned long get_actor_count() const { return strategy_->actors_to_run_.size(); }
   bool is_actor_enabled(aid_t actor) const { return strategy_->actors_to_run_.at(actor).is_enabled(); }
 
-  Snapshot* get_system_state() const { return system_state_.get(); }
-  void set_system_state(std::shared_ptr<Snapshot> state) { system_state_ = std::move(state); }
-
   /**
    * @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`
@@ -153,15 +143,25 @@ public:
    * `N` running actor `p` of this state's wakeup tree
    */
   void remove_subtree_using_current_out_transition();
+  void remove_subtree_at_aid(aid_t proc);
   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_; }