X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/52367db30501439c2091f5dd858c8efe107e3340..6bc04475b4308e91e18d869a5fb665bc35b48508:/src/mc/explo/udpor/Configuration.hpp

diff --git a/src/mc/explo/udpor/Configuration.hpp b/src/mc/explo/udpor/Configuration.hpp
index 67d29b88ff..b1f6f933d2 100644
--- a/src/mc/explo/udpor/Configuration.hpp
+++ b/src/mc/explo/udpor/Configuration.hpp
@@ -9,6 +9,10 @@
 #include "src/mc/explo/udpor/EventSet.hpp"
 #include "src/mc/explo/udpor/udpor_forward.hpp"
 
+#include <optional>
+#include <string>
+#include <unordered_map>
+
 namespace simgrid::mc::udpor {
 
 class Configuration {
@@ -20,6 +24,7 @@ public:
 
   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(); }
@@ -28,8 +33,10 @@ public:
   auto cend() const { return this->events_.cend(); }
 
   bool contains(const UnfoldingEvent* e) const { return this->events_.contains(e); }
+  bool contains(const EventSet& events) const { return events.is_subset_of(this->events_); }
   const EventSet& get_events() const { return this->events_; }
   const UnfoldingEvent* get_latest_event() const { return this->newest_event; }
+  std::string to_string() const { return this->events_.to_string(); }
 
   /**
    * @brief Insert a new event into the configuration
@@ -60,15 +67,39 @@ public:
    */
   void add_event(const UnfoldingEvent* e);
 
+  /**
+   * @brief Whether or not the given event can be added to
+   * this configuration while preserving that the configuration
+   * is causally closed and conflict-free
+   *
+   * A configuration `C` is compatible with an event iff
+   * the event can be added to `C` while preserving that
+   * the configuration is causally closed and conflict-free.
+   *
+   * The method effectively answers the following question:
+   *
+   * "Is `C + {e}` a valid configuration?"
+   */
   bool is_compatible_with(const UnfoldingEvent* e) const;
 
   /**
-   * @brief Whether or not the events in the given history
-   * could be added to this configuration while preserving
-   * the configuration property
+   * @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
+   *
+   * A configuration `C` is compatible with a history iff all
+   * events of the history can be added to `C` while preserving
+   * that the configuration is causally closed and conflict-free.
+   *
+   * The method effectively answers the following question:
+   *
+   * "Is `C + (U_i [e_i])` a valid configuration?"
    */
   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
@@ -118,11 +149,45 @@ public:
    * 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)`)
+   * @returns the smallest set of events whose events generates
+   * this configuration (denoted `config(E)`)
    */
   EventSet get_minimally_reproducible_events() const;
 
+  /**
+   * @brief Determines the event in the configuration whose associated
+   * transition is the latest of the given actor
+   *
+   * @invariant: At most one event in the configuration will correspond
+   * to `preEvt(C, a)` for any action `a`. This can be argued by contradiction.
+   *
+   * If there were more than one event (`e` and `e'`) in any configuration whose
+   * associated transitions `a` were run by the same actor at the same step, then they
+   * could not be causally related (`<`) since `a` could not be enabled in
+   * both subconfigurations C' and C'' containing the hypothetical events
+   * `e` and `e` + `e'`. Since they would not be contained in each other's histories,
+   * they would be in conflict, which cannot happen between any pair of events
+   * in a configuration. Thus `e` and `e'` cannot exist simultaneously
+   */
+  std::optional<const UnfoldingEvent*> get_latest_event_of(aid_t) const;
+  /**
+   * @brief Determines the most recent transition of the given actor
+   * in this configuration, or `pre(a)` as denoted in the thesis of
+   * The Anh Pham
+   *
+   * Conceptually, the execution of an interleaving of the transitions
+   * (i.e. a topological ordering) of a configuration yields a unique
+   * state `state(C)`. Since actions taken by the same actor are always
+   * dependent with one another, any such interleaving always yields a
+   * unique
+   *
+   * @returns the most recent transition of the given actor
+   * in this configuration, or `std::nullopt` if there are no transitions
+   * in this configuration run by the given actor
+   */
+  std::optional<const Transition*> get_latest_action_of(aid_t aid) const;
+  std::optional<const UnfoldingEvent*> pre_event(aid_t aid) const { return get_latest_event_of(aid); }
+
 private:
   /**
    * @brief The most recent event added to the configuration
@@ -134,8 +199,20 @@ private:
    *
    * @invariant For each event `e` in `events_`, the set of
    * dependencies of `e` is also contained in `events_`
+   *
+   * @invariant For each pair of events `e` and `e'` in
+   * `events_`, `e` and `e'` are not in conflict
    */
   EventSet events_;
+
+  /**
+   * @brief Maps actors to the latest events which
+   * are executed by the actor
+   *
+   * @invariant: The events that are contained in the map
+   * are also contained in the set `events_`
+   */
+  std::unordered_map<aid_t, const UnfoldingEvent*> latest_event_mapping;
 };
 
 } // namespace simgrid::mc::udpor