From f95a31a473eb41bcabca9771fb2a1659f0dfbbd3 Mon Sep 17 00:00:00 2001
From: Maxwell Pirtle <maxwellpirtle@gmail.com>
Date: Mon, 15 May 2023 10:50:25 +0200
Subject: [PATCH] Add ODPOR "backtracking" logic

---
 src/mc/api/State.cpp                   |  3 ++-
 src/mc/api/State.hpp                   |  2 ++
 src/mc/explo/DFSExplorer.cpp           | 11 +++++++++++
 src/mc/explo/odpor/WakeupTree.cpp      |  4 ++++
 src/mc/transition/TransitionRandom.hpp |  8 +++++++-
 5 files changed, 26 insertions(+), 2 deletions(-)

diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp
index 2488c33c86..1c40e31d66 100644
--- a/src/mc/api/State.cpp
+++ b/src/mc/api/State.cpp
@@ -219,7 +219,8 @@ void State::seed_wakeup_tree_if_needed(const odpor::Execution& prior)
   // tree and decided upon "happens-before" at that point for different
   // executions :(
   if (wakeup_tree_.empty()) {
-    if (const aid_t next = std::get<0>(next_transition_guided()); next >= 0) {
+    strategy_->consider_best();
+    if (const aid_t next = std::get<0>(strategy_->next_transition()); next >= 0) {
       wakeup_tree_.insert(prior, odpor::PartialExecution{strategy_->actors_to_run_.at(next).get_transition()});
     }
   }
diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp
index 4b6b123ca3..d951ed93e0 100644
--- a/src/mc/api/State.hpp
+++ b/src/mc/api/State.hpp
@@ -152,6 +152,8 @@ public:
    */
   void remove_subtree_starting_with(aid_t p);
 
+  bool has_empty_tree() const { return this->wakeup_tree_.empty(); }
+
   /**
    * @brief
    */
diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index 4b2d631831..27df977e8c 100644
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -173,6 +173,11 @@ void DFSExplorer::run()
       // (rather than following the partial execution of a
       // wakeup tree). This corresponds to lines 9 to 13 of
       // the ODPOR pseudocode
+      //
+      // INVARIANT: The execution sequence should be consistent
+      // with the state when seeding the tree. If the sequence
+      // gets out of sync with the state, selection will not
+      // work as we intend
       state->seed_wakeup_tree_if_needed(execution_seq_);
     }
 
@@ -375,6 +380,12 @@ void DFSExplorer::run()
 
 std::shared_ptr<State> DFSExplorer::best_opened_state()
 {
+  if (reduction_mode_ == ReductionMode::odpor) {
+    const auto first =
+        std::find_if(stack_.rbegin(), stack_.rend(), [](const auto& state) { return !state->has_empty_tree(); });
+    return *first;
+  }
+
   int best_prio = 0; // cache the value for the best priority found so far (initialized to silence gcc)
   auto best     = end(opened_states_);   // iterator to the state to explore having the best priority
   auto valid    = begin(opened_states_); // iterator marking the limit between states still to explore, and already
diff --git a/src/mc/explo/odpor/WakeupTree.cpp b/src/mc/explo/odpor/WakeupTree.cpp
index 33a0fb6362..5e967eb582 100644
--- a/src/mc/explo/odpor/WakeupTree.cpp
+++ b/src/mc/explo/odpor/WakeupTree.cpp
@@ -162,6 +162,10 @@ void WakeupTree::insert(const Execution& E, const PartialExecution& w)
       return;
     }
   }
+  xbt_die("Insertion should always succeed with the root node (which contains no "
+          "prior execution). If we've reached this point, this implies either that "
+          "the wakeup tree traversal is broken or that computation of the shortest "
+          "sequence to insert into the tree is broken");
 }
 
 } // namespace simgrid::mc::odpor
\ No newline at end of file
diff --git a/src/mc/transition/TransitionRandom.hpp b/src/mc/transition/TransitionRandom.hpp
index ba00821584..374d69def4 100644
--- a/src/mc/transition/TransitionRandom.hpp
+++ b/src/mc/transition/TransitionRandom.hpp
@@ -17,7 +17,13 @@ class RandomTransition : public Transition {
 public:
   std::string to_string(bool verbose) const override;
   RandomTransition(aid_t issuer, int times_considered, std::stringstream& stream);
-  bool depends(const Transition* other) const override { return aid_ == other->aid_; } // Independent with any other transition
+  bool depends(const Transition* other) const override
+  {
+    if (other->type_ < type_)
+      return other->depends(this);
+
+    return aid_ == other->aid_;
+  } // Independent with any other transition
 };
 
 } // namespace simgrid::mc
-- 
2.20.1