Add more docmentation for get_first_sdpor_initial()

[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 f3b44e7..d190a72 100644 (file)
--- a/src/mc/explo/odpor/Execution.cpp
+++ b/src/mc/explo/odpor/Execution.cpp
@@ -24,11 +24,6 @@ void Execution::push_transition(const Transition* t)
   contents_.push_back(Event({t, max_clock_vector}));
 }
 
-void Execution::pop_latest()
-{
-  contents_.pop_back();
-}
-
 std::unordered_set<Execution::EventHandle> Execution::get_racing_events_of(Execution::EventHandle target) const
 {
   std::unordered_set<Execution::EventHandle> racing_events;
@@ -89,6 +84,16 @@ std::optional<aid_t> Execution::get_first_sdpor_initial_from(EventHandle e,
     return std::nullopt;
   }
 
+  // To actually compute `I_[E'](v) ∩ backtrack(E')`, we must
+  // first compute `E'` and "move" in the direction of `v`.
+  // We perform a scan over `E` (this execution) and make
+  // note of any events which occur after `e` but don't
+  // "happen-after" `e` by pushing them onto `E'`. Note that
+  // correctness is still preserved in computing `v` "on-the-fly"
+  // to determine if an actor `q` is an initial for `E'` after `v`:
+  // only those events that "occur-before" `v`
+  // could happen-before `v` for any valid happens-before relation.
+
   // First, grab `E' := pre(e, E)` and determine what actor `p` is
   // TODO: Instead of copying around these big structs, it
   // would behoove us to incorporate some way to reference