X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/b01dcb515d442ab87577ef052c3dcaec50a0a65f..cf0a1a77c65746b1a40b858228bedf7a0eb63f7f:/src/mc/explo/udpor/Configuration.hpp

diff --git a/src/mc/explo/udpor/Configuration.hpp b/src/mc/explo/udpor/Configuration.hpp
index eb365d5bbb..619871eac2 100644
--- a/src/mc/explo/udpor/Configuration.hpp
+++ b/src/mc/explo/udpor/Configuration.hpp
@@ -9,8 +9,7 @@
 #include "src/mc/explo/udpor/EventSet.hpp"
 #include "src/mc/explo/udpor/udpor_forward.hpp"
 
-#include <initializer_list>
-#include <vector>
+#include <optional>
 
 namespace simgrid::mc::udpor {
 
@@ -21,15 +20,19 @@ public:
   Configuration& operator=(Configuration const&) = default;
   Configuration(Configuration&&)                 = default;
 
-  Configuration(EventSet events);
-  Configuration(std::initializer_list<UnfoldingEvent*> events);
+  explicit Configuration(const UnfoldingEvent* event);
+  explicit Configuration(const EventSet& events);
+  explicit Configuration(const History& history);
+  explicit Configuration(std::initializer_list<const UnfoldingEvent*> events);
 
   auto begin() const { return this->events_.begin(); }
   auto end() const { return this->events_.end(); }
+  auto cbegin() const { return this->events_.cbegin(); }
+  auto cend() const { return this->events_.cend(); }
 
-  bool contains(UnfoldingEvent* e) const { return this->events_.contains(e); }
+  bool contains(const UnfoldingEvent* e) const { return this->events_.contains(e); }
   const EventSet& get_events() const { return this->events_; }
-  UnfoldingEvent* get_latest_event() const { return this->newest_event; }
+  const UnfoldingEvent* get_latest_event() const { return this->newest_event; }
 
   /**
    * @brief Insert a new event into the configuration
@@ -58,18 +61,84 @@ public:
    * we shouldn't focus so much on this (let alone the additional benefit of the
    * assertions)
    */
-  void add_event(UnfoldingEvent* e);
+  void add_event(const UnfoldingEvent* e);
 
   /**
+   * @brief Whether or not the given event can be added to
+   * this configuration while keeping the set of events causally closed
+   * and conflict-free
+   */
+  bool is_compatible_with(const UnfoldingEvent* e) const;
+
+  /**
+   * @brief Whether or not the events in the given history can be added to
+   * this configuration while keeping the set of events causally closed
+   * and conflict-free
+   */
+  bool is_compatible_with(const History& history) const;
+
+  std::optional<Configuration> compute_alternative_to(const EventSet& D, const Unfolding& U) const;
+  std::optional<Configuration> compute_k_partial_alternative_to(const EventSet& D, const Unfolding& U, size_t k) const;
+
+  /**
+   * @brief Orders the events of the configuration such that
+   * "more recent" events (i.e. those that are farther down in
+   * the event structure's dependency chain) come after those
+   * that appeared "farther in the past"
+   *
+   * @returns a vector `V` with the following property:
+   *
+   * 1. Let i(e) := C -> I map events to their indices in `V`.
+   * For every pair of events e, e' in C, if e < e' then i(e) < i(e')
+   *
+   * Intuitively, events that are closer to the "bottom" of the event
+   * structure appear farther along in the list than those that appear
+   * closer to the "top"
+   */
+  std::vector<const UnfoldingEvent*> get_topologically_sorted_events() const;
+
+  /**
+   * @brief Orders the events of the configuration such that
+   * "more recent" events (i.e. those that are farther down in
+   * the event structure's dependency chain) come before those
+   * that appear "farther in the past"
+   *
+   * @note The events of the event structure are arranged such that
+   * e < e' implies a directed edge from e to e'. However, it is
+   * also useful to be able to traverse the *reverse* graph (for
+   * example when computing the compatibility graph of a configuration),
+   * hence the distinction between "reversed" and the method
+   * "Configuration::get_topologically_sorted_events()"
+   *
+   * @returns a vector `V` with the following property:
+   *
+   * 1. Let i(e) := C -> I map events to their indices in `V`.
+   * For every pair of events e, e' in C, if e < e' then i(e) > i(e')
+   *
+   * Intuitively, events that are closer to the "top" of the event
+   * structure appear farther along in the list than those that appear
+   * closer to the "bottom"
+   */
+  std::vector<const UnfoldingEvent*> get_topologically_sorted_events_of_reverse_graph() const;
+
+  /**
+   * @brief Computes the smallest set of events whose collective histories
+   * capture all events of this configuration
+   *
+   * @invariant The set of all events in the collective histories
+   * of the events returned by this method is equal to the set of events
+   * in this configuration
    *
+   * @returns the smallest set of events whose events generates
+   * this configuration (denoted `config(E)`)
    */
-  std::vector<UnfoldingEvent*> get_topogolically_sorted_events_of_reverse_graph() const;
+  EventSet get_minimally_reproducible_events() const;
 
 private:
   /**
    * @brief The most recent event added to the configuration
    */
-  UnfoldingEvent* newest_event = nullptr;
+  const UnfoldingEvent* newest_event = nullptr;
 
   /**
    * @brief The events which make up this configuration