Merge branch 'odpor-implementation' into 'master'

[simgrid.git] / src / mc / explo / odpor / Execution.cpp

diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp
index b7b0cbb1bd90b5f59140e30cff40b54c106682bf..ef10e4f45f2ce393797688bfd4d383dc9f954e9f 100644 (file)
--- a/src/mc/explo/odpor/Execution.cpp
+++ b/src/mc/explo/odpor/Execution.cpp
@@ -24,6 +24,11 @@ std::vector<std::string> get_textual_trace(const PartialExecution& w)
   return trace;
 }
 
+Execution::Execution(const PartialExecution& w)
+{
+  push_partial_execution(w);
+}
+
 void Execution::push_transition(std::shared_ptr<Transition> t)
 {
   if (t == nullptr) {
@@ -39,6 +44,13 @@ void Execution::push_transition(std::shared_ptr<Transition> t)
   contents_.push_back(Event({std::move(t), max_clock_vector}));
 }
 
+void Execution::push_partial_execution(const PartialExecution& w)
+{
+  for (const auto& t : w) {
+    push_transition(t);
+  }
+}
+
 std::vector<std::string> Execution::get_textual_trace() const
 {
   std::vector<std::string> trace;
@@ -325,15 +337,17 @@ std::optional<PartialExecution> Execution::get_odpor_extension_from(EventHandle
     const Execution pre_E_e    = get_prefix_before(e);
     const auto sleeping_actors = state_at_e.get_sleeping_actors();
 
-    // Check if any enabled actor independent with this execution after `v`
-    // is contained in the sleep set
+    // Check if any enabled actor that is independent with
+    // this execution after `v` is contained in the sleep set
     for (const auto& [aid, astate] : state_at_e.get_actors_list()) {
-      // TODO: We have to be able to react appropriately here when adding new
-      // types of transitions (multiple choices can be made :( )
-      if (astate.is_enabled() and pre_E_e.is_independent_with_execution_of(v, astate.get_transition(0))) {
-        if (sleeping_actors.count(aid) > 0) {
-          return std::nullopt;
-        }
+      const bool is_in_WI_E =
+          astate.is_enabled() and pre_E_e.is_independent_with_execution_of(v, astate.get_transition());
+      const bool is_in_sleep_set = sleeping_actors.count(aid) > 0;
+
+      // `action(aid)` is in `WI_[E](v)` but also is contained in the sleep set.
+      // This implies that the intersection between the two is non-empty
+      if (is_in_WI_E && is_in_sleep_set) {
+        return std::nullopt;
       }
     }
   }
@@ -404,7 +418,7 @@ std::optional<PartialExecution> Execution::get_shortest_odpor_sq_subset_insertio
     if (E_v.is_initial_after_execution_of(w_now, p)) {
       // Remove `p` from w and continue
 
-      // TODO: If `p` occurs in `w`, it had better refer to the same
+      // INVARIANT: If `p` occurs in `w`, it had better refer to the same
       // transition referenced by `v`. Unfortunately, we have two
       // sources of truth here which can be manipulated at the same
       // time as arguments to the function. If ODPOR works correctly,
@@ -425,7 +439,7 @@ std::optional<PartialExecution> Execution::get_shortest_odpor_sq_subset_insertio
       w_now.erase(action_by_p_in_w);
     }
     // Is `E ⊢ p ◇ w`?
-    else if (E_v.is_independent_with_execution_of(w, next_E_p)) {
+    else if (E_v.is_independent_with_execution_of(w_now, next_E_p)) {
       // INVARIANT: Note that it is impossible for `p` to be
       // excluded from the set `I_[E](w)` BUT ALSO be contained in
       // `w` itself if `E ⊢ p ◇ w` (intuitively, the fact that `E ⊢ p ◇ w`