Begin filling in computations of ex(C) and en(C)

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

diff --git a/src/mc/explo/UdporChecker.hpp b/src/mc/explo/UdporChecker.hpp
index 7f56d6d3d5706134f8d486677e2fd6e1844c52d5..2bcdeb4065d37f4dde5537a929133e30c2aa6d16 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,14 +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
-   */
-  /* FIXME: private fields are not used
-    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
@@ -75,12 +68,17 @@ private:
    */
   EventSet G;
 
+  /// @brief UDPOR's current "view" of the program it is exploring
+  Unfolding unfolding = Unfolding();
+
   /**
-   * @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();
+  using ExtensionFunction = std::function<EventSet(const Configuration&, const std::shared_ptr<Transition>)>;
+  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"
@@ -102,7 +100,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
@@ -116,7 +114,7 @@ private:
    * by the UDPOR algorithm to select new events to search. See the original
    * paper [1] for more details
    */
-  UnfoldingEvent* select_next_unfolding_event(const EventSet& A, const EventSet& enC);
+  const UnfoldingEvent* select_next_unfolding_event(const EventSet& A, const EventSet& enC);
 
   /**
    * @brief Computes the sets `ex(C)` and `en(C)` of the given configuration
@@ -137,11 +135,20 @@ 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
+   * @returns the extension set `ex(C)` of `C`
    */
-  std::tuple<EventSet, EventSet> compute_extension(const Configuration& C, const EventSet& prev_exC) const;
+  EventSet compute_exC(const Configuration& C, const State& stateC, const EventSet& prev_exC);
+
+  /**
+   * @brief Computes a portion of the extension set of a configuration given
+   * some action `action`
+   */
+  EventSet compute_exC_by_enumeration(const Configuration& C, const std::shared_ptr<Transition> action);
+
+  EventSet compute_enC(const Configuration& C, const EventSet& exC) const;
 
   /**
    *