Add skeleton for expansion phase of ODPOR

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

diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp
index fbacda3..a991219 100644 (file)
--- a/src/mc/api/State.hpp
+++ b/src/mc/api/State.hpp
@@ -10,6 +10,7 @@
 #include "src/mc/api/ClockVector.hpp"
 #include "src/mc/api/RemoteApp.hpp"
 #include "src/mc/api/strategy/Strategy.hpp"
+#include "src/mc/explo/odpor/WakeupTree.hpp"
 #include "src/mc/transition/Transition.hpp"
 
 #if SIMGRID_HAVE_STATEFUL_MC
@@ -45,16 +46,29 @@ class XBT_PRIVATE State : public xbt::Extendable<State> {
    * transition */
   std::map<aid_t, Transition> sleep_set_;
 
+  /**
+   * The wakeup tree with respect to the execution represented
+   * by the totality of all states before and including this one
+   * and with respect to this state's sleep set
+   */
+  odpor::WakeupTree wakeup_tree_;
+
 public:
   explicit State(RemoteApp& remote_app);
   explicit State(RemoteApp& remote_app, std::shared_ptr<State> parent_state);
   /* Returns a positive number if there is another transition to pick, or -1 if not */
   aid_t next_transition() const; // this function should disapear as it is redundant with the next one
 
-  /* Same as next_transition, but choice is now guided, and an integer corresponding to the
+  /* Same as next_transition(), but choice is now guided, and an integer corresponding to the
    internal cost of the transition is returned */
   std::pair<aid_t, int> next_transition_guided() const;
 
+  /**
+   * Same as next_transition(), but the choice is not based off the ODPOR
+   * wakeup tree associated with this state
+   */
+  aid_t next_odpor_transition() const;
+
   /**
    * @brief Explore a new path on the remote app; the parameter 'next' must be the result of a previous call to
    * next_transition()
@@ -67,8 +81,8 @@ public:
 
   /* Marking as TODO some actor in this state:
    *  + consider_one mark aid actor (and assert it is possible)
-   *  + consider_best ensure one actor is marked by eventually marking the best regarding its guiding methode
-   *  + conside_all mark all enabled actor that are not done yet */
+   *  + consider_best ensure one actor is marked by eventually marking the best regarding its guiding method
+   *  + consider_all mark all enabled actor that are not done yet */
   void consider_one(aid_t aid) const { strategy_->consider_one(aid); }
   void consider_best() const { strategy_->consider_best(); }
   unsigned long consider_all() const { return strategy_->consider_all(); }
@@ -94,7 +108,7 @@ public:
    * in SimGrid consists of those actors marked as `todo`
    * (i.e. those that have yet to be explored) as well as those
    * marked `done` (i.e. those that have already been explored)
-   * since the pseudcode in none of the above algorithms explicitly
+   * since the pseudocode in none of the above algorithms explicitly
    * removes elements from the backtrack set. DPOR makes use
    * explicitly of the `done` set, but we again note that the
    * backtrack set still contains processes added to the done set.
@@ -106,6 +120,22 @@ public:
     sleep_set_.insert_or_assign(t->aid_, Transition(t->type_, t->aid_, t->times_considered_));
   }
 
+  /**
+   * @brief Inserts an arbitrary enabled actor into the wakeup tree
+   * associated with this state, if such an actor exists and if
+   * the wakeup tree is already not empty
+   *
+   * @param prior The sequence of steps leading up to this state
+   * with respec to which the tree associated with this state should be
+   * a wakeup tree (wakeup trees are defined relative to an execution)
+   *
+   * @invariant: You should not manipulate a wakeup tree with respect
+   * to more than one execution; doing so will almost certainly lead to
+   * unexpected results as wakeup trees are defined relative to a single
+   * execution
+   */
+  void seed_wakeup_tree_if_needed(const odpor::Execution& prior);
+
   /* Returns the total amount of states created so far (for statistics) */
   static long get_expanded_states() { return expended_states_; }
 };