Add first steps towards an implementation of ex(C)

diff --git a/src/mc/api/ActorState.hpp b/src/mc/api/ActorState.hpp
index eda2808..946971a 100644 (file)
--- a/src/mc/api/ActorState.hpp
+++ b/src/mc/api/ActorState.hpp
@@ -131,6 +131,11 @@ public:
                aid_, times_considered);
     this->pending_transitions_[times_considered] = std::move(t);
   }
+
+  const std::vector<std::shared_ptr<Transition>>& get_enabled_transitions() const
+  {
+    return this->pending_transitions_;
+  };
 };
 
 } // namespace simgrid::mc

diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp
index ff61f17..abf8e1b 100644 (file)
--- a/src/mc/explo/UdporChecker.cpp
+++ b/src/mc/explo/UdporChecker.cpp
@@ -14,9 +14,7 @@ namespace simgrid::mc::udpor {
 
 UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args)
 {
-  /* Create initial data structures, if any ...*/
-
-  // TODO: Initialize state structures for the search
+  // Initialize the map
 }
 
 void UdporChecker::run()
@@ -47,7 +45,7 @@ void UdporChecker::explore(Configuration C, EventSet D, EventSet A, std::unique_
   // the unfolding, but the naming of the method
   // suggests it is doesn't have side effects. We should
   // reconcile this in the future
-  auto [exC, enC] = compute_extension(C, prev_exC);
+  auto [exC, enC] = compute_extension(C, *stateC, prev_exC);
 
   // If enC is a subset of D, intuitively
   // there aren't any enabled transitions
@@ -126,24 +124,44 @@ void UdporChecker::explore(Configuration C, EventSet D, EventSet A, std::unique_
   clean_up_explore(e, C, D);
 }
 
-std::tuple<EventSet, EventSet> UdporChecker::compute_extension(const Configuration& C, const EventSet& prev_exC) const
+std::tuple<EventSet, EventSet> UdporChecker::compute_extension(const Configuration& C, const State& stateC,
+                                                               const EventSet& prev_exC) const
 {
   // See eqs. 5.7 of section 5.2 of [3]
   // C = C' + {e_cur}, i.e. C' = C - {e_cur}
   //
   // Then
   //
-  // ex(C) = ex(C' + {e_cur}) = ex(C') / {e_cur} + U{<a, > : H }
+  // 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;
   exC.remove(e_cur);
 
-  // ... fancy computations
+  for (const auto& [aid, actor_state] : stateC.get_actors_list()) {
+    for (const auto& transition : actor_state.get_enabled_transitions()) {
+      // First check for a specialized function that can compute the extension
+      // set "quickly" based on its type. Otherwise, fall back to computing
+      // the set "by hand"
+      const auto specialized_extension_function = incremental_extension_functions.find(transition->type_);
+      if (specialized_extension_function != incremental_extension_functions.end()) {
+        exC.form_union((specialized_extension_function->second)(C, *transition));
+      } else {
+        exC.form_union(this->compute_extension_by_enumeration(C, *transition));
+      }
+    }
+  }
 
   EventSet enC;
+
   return std::tuple<EventSet, EventSet>(exC, enC);
 }
 
+EventSet UdporChecker::compute_extension_by_enumeration(const Configuration& C, const Transition& action) const
+{
+  // TODO: Do something more interesting here
+  return EventSet();
+}
+
 void UdporChecker::move_to_stateCe(State& state, const UnfoldingEvent& e)
 {
   const aid_t next_actor = e.get_transition()->aid_;

diff --git a/src/mc/explo/UdporChecker.hpp b/src/mc/explo/UdporChecker.hpp
index 7f56d6d..471d8a2 100644 (file)
--- a/src/mc/explo/UdporChecker.hpp
+++ b/src/mc/explo/UdporChecker.hpp
@@ -14,6 +14,7 @@
 #include "src/mc/explo/udpor/UnfoldingEvent.hpp"
 #include "src/mc/mc_record.hpp"
 
+#include <functional>
 #include <optional>
 
 namespace simgrid::mc::udpor {
@@ -75,10 +76,17 @@ private:
    */
   EventSet G;
 
+  /// @brief UDPOR's current "view" of the program it is exploring
+  Unfolding unfolding = Unfolding();
+
+  using ExtensionFunction = std::function<EventSet(const Configuration&, const Transition&)>;
+
   /**
-   * @brief UDPOR's current "view" of the program it is exploring
+   * @brief A collection of specialized functions which can incrementally
+   * compute the extension of a configuration based on the action taken
    */
-  Unfolding unfolding = Unfolding();
+  std::unordered_map<Transition::Type, ExtensionFunction> incremental_extension_functions =
+      std::unordered_map<Transition::Type, ExtensionFunction>();
 
 private:
   /**
@@ -137,11 +145,15 @@ private:
    *
    * @param C the configuration based on which the two sets `ex(C)` and `en(C)` are
    * computed
+   * @param stateC the state of the program after having executed C (viz. `state(C)`)
    * @param prev_exC the previous value of `ex(C)`, viz. that which was computed for
    * the configuration `C' := C - {e}`
    * @returns a tuple containing the pair of sets `ex(C)` and `en(C)` respectively
    */
-  std::tuple<EventSet, EventSet> compute_extension(const Configuration& C, const EventSet& prev_exC) const;
+  std::tuple<EventSet, EventSet> compute_extension(const Configuration& C, const State& stateC,
+                                                   const EventSet& prev_exC) const;
+
+  EventSet compute_extension_by_enumeration(const Configuration& C, const Transition& action) const;
 
   /**
    *

diff --git a/src/mc/explo/udpor/CompatibilityGraph.cpp b/src/mc/explo/udpor/CompatibilityGraph.cpp
index aafc551..179ca4e 100644 (file)
--- a/src/mc/explo/udpor/CompatibilityGraph.cpp
+++ b/src/mc/explo/udpor/CompatibilityGraph.cpp
@@ -28,7 +28,7 @@ void CompatibilityGraph::insert(std::unique_ptr<CompatibilityGraphNode> e)
     // This is bad: someone wrapped the raw event address twice
     // in two different unique ptrs and attempted to
     // insert it into the unfolding...
-    throw std::invalid_argument("Attempted to insert an unfolding event owned twice."
+    throw std::invalid_argument("Attempted to insert a node owned twice."
                                 "This will result in a  double free error and must be fixed.");
   }