Reindent -- almost no real change

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

diff --git a/src/mc/explo/UdporChecker.hpp b/src/mc/explo/UdporChecker.hpp
index e63802bb385034fe588cbe843120282260a9d75d..30407c42178afc644b3bc6046c21c0a4ca61a447 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 {
@@ -41,12 +42,6 @@ public:
   inline std::unique_ptr<State> get_current_state() { return std::make_unique<State>(get_remote_app()); }
 
 private:
-  /**
-   * The total number of events created whilst exploring the unfolding
-   */
-  uint32_t nb_events = 0;
-  uint32_t nb_traces = 0;
-
   /**
    * @brief The "relevant" portions of the unfolding that must be kept around to ensure that
    * UDPOR properly searches the state space
@@ -73,12 +68,18 @@ 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:
   /**
    * @brief Explores the unfolding of the concurrent system
    * represented by the ModelChecker instance "mcmodel_checker"
@@ -100,7 +101,7 @@ private:
    * TODO: Add the optimization where we can check if e == e_prior
    * to prevent repeated work when computing ex(C)
    */
-  void explore(Configuration C, EventSet D, EventSet A, std::unique_ptr<State> stateC, EventSet prev_exC);
+  void explore(const Configuration& C, EventSet D, EventSet A, std::unique_ptr<State> stateC, EventSet prev_exC);
 
   /**
    * @brief Identifies the next event from the unfolding of the concurrent system
@@ -135,11 +136,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;
 
   /**
    *