Add conflict-free invariant check to Configuration

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

diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp
index c5d596d1f15b0e775979f11325981534bb83b52d..02452aadb32becf3d677da01b5692c93b7b1b4ab 100644 (file)
--- a/src/mc/explo/UdporChecker.cpp
+++ b/src/mc/explo/UdporChecker.cpp
@@ -5,7 +5,6 @@
 
 #include "src/mc/explo/UdporChecker.hpp"
 #include "src/mc/api/State.hpp"
-#include "src/mc/explo/udpor/CompatibilityGraph.hpp"
 #include <xbt/asserts.h>
 #include <xbt/log.h>
 
@@ -57,8 +56,7 @@ void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, std::
   if (enC.is_subset_of(D)) {
 
     if (not C.get_events().empty()) {
-
-      // g_var::nb_traces++;
+      // Report information...
     }
 
     // When `en(C)` is empty, intuitively this means that there
@@ -75,7 +73,7 @@ void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, std::
 
   // TODO: Add verbose logging about which event is being explored
 
-  UnfoldingEvent* e = select_next_unfolding_event(A, enC);
+  const UnfoldingEvent* e = select_next_unfolding_event(A, enC);
   xbt_assert(e != nullptr, "\n\n****** INVARIANT VIOLATION ******\n"
                            "UDPOR guarantees that an event will be chosen at each point in\n"
                            "the search, yet no events were actually chosen\n"
@@ -130,8 +128,8 @@ std::tuple<EventSet, EventSet> UdporChecker::compute_extension(const Configurati
   //
   // ex(C) = ex(C' + {e_cur}) = ex(C') / {e_cur} +
   //    U{<a, K> : K is maximal, `a` depends on all of K, `a` enabled at K }
-  UnfoldingEvent* e_cur = C.get_latest_event();
-  EventSet exC          = prev_exC;
+  const UnfoldingEvent* e_cur = C.get_latest_event();
+  EventSet exC                = prev_exC;
   exC.remove(e_cur);
 
   for (const auto& [aid, actor_state] : stateC.get_actors_list()) {
@@ -163,19 +161,7 @@ EventSet UdporChecker::compute_extension_by_enumeration(const Configuration& C,
   // where `a` is the `action` given to us.
   EventSet incremental_exC;
 
-  // We only consider those combinations of events for which `action` is dependent with
-  // the action associated with any given event ("`a` depends on all of K")
-  const std::unique_ptr<CompatibilityGraph> G = C.make_compatibility_graph_filtered_on([=](const UnfoldingEvent* e) {
-    const auto e_transition = e->get_transition();
-    return action.depends(e_transition);
-  });
-
-  // TODO: Now that the graph has been constructed, enumerate
-  // all possible k-cliques of the complement of G
-
-  // TODO: For each enumeration, check all possible
-  // combinations of selecting a single event from
-  // each set associated with the graph nodes
+  // Compute the extension set here using the algorithm Martin described...
 
   return incremental_exC;
 }
@@ -209,7 +195,7 @@ std::unique_ptr<State> UdporChecker::record_current_state()
   return next_state;
 }
 
-UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
+const UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
 {
   if (!enC.empty()) {
     return *(enC.begin());