Introduce ODPOR integration with multiple actions

Prior commits had missing integration with transitions
which could be executed multiple times in the form of
variants. This commit resolves those issues by making
two important modifications:

1. Determining the "current thing that actor X is
running" from a given state `s` has been modified
to reflect what we would expect if we asked the
question even after having exhausted all combinations;
the the case where all combinations have been executed,
the last variant is that which we would expect to be
considered the transition which were enabled at `s`.
This allows us to "fix" the spot in ODPOR where we
need to determine those actions enabled at a given
state `s`. We need to treat it as if only one variant
actually exists; for if there are differences in the
dependency structure for each variant, we wouldn't
want to erroneously deduce that an actor `X` were
a weak initial for some prefix `E'` of `E` and
for some extension `v` of `E'` based on what it
HAD run in the past.

2. In ODPOR, we now only insert members into the
sleep set when all variants of a transition have
been executed. This ensures that we are effectively
treating each variant in isolation from one another;
it is only when we reach the last variant that we
can finally go ahead and say "OK actor X you can
go into the sleep set now". Note that it's perfectly
possible for the actor to later end up in sleep sets
of states that occur *later on*; but for the sleep
set that is at *this* state, we'd want to be sure
only to add it after having explored the state space
with each variant. The reasoning is the same as in
point 1: we wouldn't want the sleep set to be based
on an action that the actor HAD run in the past as
the proxy representing what that actor is doing IN
THE PRESENT. If the dependencies were different among
the different variants, we'd have an issue if we
had previously added the other variants

diff --git a/src/mc/api/ActorState.hpp b/src/mc/api/ActorState.hpp
index 8b5e03f..2e8e136 100644 (file)
--- a/src/mc/api/ActorState.hpp
+++ b/src/mc/api/ActorState.hpp
@@ -9,6 +9,7 @@
 #include "src/kernel/activity/CommImpl.hpp"
 #include "src/mc/remote/RemotePtr.hpp"
 
+#include <algorithm>
 #include <exception>
 #include <vector>
 
@@ -100,6 +101,7 @@ public:
   unsigned int get_max_considered() const { return max_consider_; }
   unsigned int get_times_considered() const { return times_considered_; }
   unsigned int get_times_not_considered() const { return max_consider_ - times_considered_; }
+  bool has_more_to_consider() const { return get_times_not_considered() > 0; }
   aid_t get_aid() const { return aid_; }
 
   /* returns whether the actor is marked as enabled in the application side */
@@ -116,7 +118,31 @@ public:
   }
   void mark_done() { this->state_ = InterleavingType::done; }
 
-  std::shared_ptr<Transition> get_transition() const { return get_transition(get_times_considered()); }
+  /**
+   * @brief Retrieves the transition that we should consider for execution by
+   * this actor from the State instance with respect to which this ActorState object
+   * is considered
+   */
+  std::shared_ptr<Transition> get_transition() const
+  {
+    // The rationale for this selection is as follows:
+    //
+    // 1. For transitions with only one possibility of execution,
+    // we always wish to select action `0` even if we've
+    // marked the transition already as considered (which
+    // we'll do if we explore a trace following that transition).
+    //
+    // 2. For transitions that can be considered multiple
+    // times, we want to be sure to select the most up-to-date
+    // action. In general, this means selecting that which is
+    // now being considered at this state. If, however, we've
+    // executed the
+    //
+    // The formula satisfies both of the above conditions:
+    //
+    // > std::clamp(times_considered_, 0u, max_consider_ - 1)
+    return get_transition(std::clamp(times_considered_, 0u, max_consider_ - 1));
+  }
 
   std::shared_ptr<Transition> get_transition(unsigned times_considered) const
   {

diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp
index 1f8786d..b05bf39 100644 (file)
--- a/src/mc/api/State.cpp
+++ b/src/mc/api/State.cpp
@@ -213,9 +213,7 @@ void State::seed_wakeup_tree_if_needed(const odpor::Execution& prior)
       if (actor.is_enabled()) {
         // For each variant of the transition, we want
         // to insert the action into the tree. This ensures
-        // that all variants are searched?
-        //
-        // TODO: How do we modify sleep sets then?
+        // that all variants are searched
         for (unsigned times = 0; times < actor.get_max_considered(); ++times) {
           wakeup_tree_.insert(prior, odpor::PartialExecution{actor.get_transition(times)});
         }
@@ -273,7 +271,15 @@ void State::do_odpor_unwind()
 {
   if (auto out_transition = get_transition_out(); out_transition != nullptr) {
     remove_subtree_using_current_out_transition();
-    add_sleep_set(std::move(out_transition));
+
+    // Only when we've exhausted all variants of the transition which
+    // can be chosen from this state do we finally add the actor to the
+    // sleep set. This ensures that the current logic handling sleep sets
+    // works with ODPOR in the way we intend it to work. There is not a
+    // good way to perform transition equality in SimGrid; instead, we
+    // effectively simply check for the presence of an actor in the sleep set.
+    if (!get_actors_list().at(out_transition->aid_).has_more_to_consider())
+      add_sleep_set(std::move(out_transition));
   }
 }
 

diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp
index 1c01e2b..ef10e4f 100644 (file)
--- a/src/mc/explo/odpor/Execution.cpp
+++ b/src/mc/explo/odpor/Execution.cpp
@@ -337,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;
       }
     }
   }