Add documentation for Comb data structure

[simgrid.git] / src / mc / explo / UdporChecker.cpp

diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp
index 04f874423eb28f2a5ef3010048a40a6947855435..899073de03c1134a87a5faca4f320751a52e5514 100644 (file)
--- a/src/mc/explo/UdporChecker.cpp
+++ b/src/mc/explo/UdporChecker.cpp
@@ -5,7 +5,10 @@
 
 #include "src/mc/explo/UdporChecker.hpp"
 #include "src/mc/api/State.hpp"
+#include "src/mc/explo/udpor/Comb.hpp"
+#include "src/mc/explo/udpor/History.hpp"
 #include "src/mc/explo/udpor/maximal_subsets_iterator.hpp"
+
 #include <xbt/asserts.h>
 #include <xbt/log.h>
 
@@ -59,10 +62,11 @@ void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, std::
     // are no enabled transitions that can be executed from the
     // state reached by `C` (denoted `state(C)`), i.e. by some
     // execution of the transitions in C obeying the causality
-    // relation. Here, then, we would be in a deadlock.
+    // relation. Here, then, we may be in a deadlock (the other
+    // possibility is that we've finished running everything, and
+    // we wouldn't be in deadlock then)
     if (enC.empty()) {
       get_remote_app().check_deadlock();
-      DIE_IMPOSSIBLE;
     }
 
     return;
@@ -93,10 +97,8 @@ void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, std::
   // D <-- D + {e}
   D.insert(e);
 
-  // TODO: Determine a value of K to use or don't use it at all
   constexpr unsigned K = 10;
-  if (auto J = compute_partial_alternative(D, C, K); !J.empty()) {
-    J.subtract(C.get_events());
+  if (auto J = C.compute_k_partial_alternative_to(D, this->unfolding, K); J.has_value()) {
 
     // Before searching the "right half", we need to make
     // sure the program actually reflects the fact
@@ -105,7 +107,8 @@ void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, std::
     restore_program_state_to(*stateC);
 
     // Explore(C, D + {e}, J \ C)
-    explore(C, D, std::move(J), std::move(stateC), std::move(prev_exC));
+    auto J_minus_C = J.value().get_events().subtracting(C.get_events());
+    explore(C, D, std::move(J_minus_C), std::move(stateC), std::move(prev_exC));
   }
 
   // D <-- D - {e}
@@ -158,7 +161,9 @@ EventSet UdporChecker::compute_exC_by_enumeration(const Configuration& C, const
        begin != maximal_subsets_iterator(); ++begin) {
     const EventSet& maximal_subset = *begin;
 
-    // TODO: Determine if `a` is enabled here
+    // Determining if `a` is enabled here might not be possible while looking at `a` opaquely
+    // We leave the implementation as-is to ensure that any addition would be simple
+    // if it were ever added
     const bool enabled_at_config_k = false;
 
     if (enabled_at_config_k) {
@@ -170,7 +175,6 @@ EventSet UdporChecker::compute_exC_by_enumeration(const Configuration& C, const
       }
     }
   }
-
   return incremental_exC;
 }
 
@@ -230,12 +234,6 @@ const UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet&
   return nullptr;
 }
 
-EventSet UdporChecker::compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const
-{
-  // TODO: Compute k-partial alternatives using [2]
-  return EventSet();
-}
-
 void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
 {
   const EventSet C_union_D              = C.get_events().make_union(D);