X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/b5d393903a5be21cbf4ee4374dbbcd9141c70383..8f3beaedaaa72be7f2af8e3a1f72552b5e3b78f3:/src/mc/explo/udpor/Unfolding.hpp

diff --git a/src/mc/explo/udpor/Unfolding.hpp b/src/mc/explo/udpor/Unfolding.hpp
index 1c6ff6c04f..8f5848651c 100644
--- a/src/mc/explo/udpor/Unfolding.hpp
+++ b/src/mc/explo/udpor/Unfolding.hpp
@@ -36,7 +36,42 @@ public:
   /// in the unfolding
   const UnfoldingEvent* insert(std::unique_ptr<UnfoldingEvent> e);
 
-  /// @brief Computes "#ⁱ_U(e)" for the given event
+  /**
+   * @brief Informs the unfolding of a (potentially) new event
+   *
+   * The unfolding of a concurrent program is a well-defined
+   * structure. Given the labeled transition system (LTS) of
+   * a program, the unfolding of that program can be determined
+   * algorithmically. However, UDPOR does not a priori know the structure of the
+   * unfolding as it performs its exploration. Thus, events in the
+   * unfolding are "discovered" as they are encountered, specifically
+   * when computing the extension sets of the configurations that
+   * UDPOR decides to search.
+   *
+   * This lends itself to the following problem: the extension sets
+   * of two different configurations may overlap one another. That
+   * is, for two configurations C and C' explored by UDPOR where C != C',
+   *
+   * ex(C) - ex(C') != empty
+   *
+   * Hence, when extending both `C` and `C'`, any events contained in
+   * the intersection of ex(C) and ex(C') will be attempted to be added
+   * twice. The unfolding will notice that these events have already
+   * been added and simply return the event already added to the unfolding
+   *
+   * @tparam ...Args arguments passed to the `UnfoldingEvent` constructor
+   * @return the handle to either the newly created event OR
+   * to an equivalent event that was already noted by the unfolding
+   * at some point in the past
+   */
+  template <typename... Args> const UnfoldingEvent* discover_event(Args... args)
+  {
+    auto candidate_event = std::make_unique<UnfoldingEvent>(std::forward<Args>(args)...);
+    return insert(std::move(candidate_event));
+  }
+
+  /// @brief Computes "#ⁱ_U(e)" for the given event, where `U` is the set
+  /// of the events in this unfolding
   EventSet get_immediate_conflicts_of(const UnfoldingEvent*) const;
 
 private:
@@ -44,7 +79,7 @@ private:
    * @brief All of the events that are currently are a part of the unfolding
    *
    * @invariant Each unfolding event maps itself to the owner of that event,
-   * i.e. the unique pointer that owns the address. The Unfolding owns all
+   * i.e. the unique pointer that manages the data at the address. The Unfolding owns all
    * of the addresses that are referenced by EventSet instances and Configuration
    * instances. UDPOR guarantees that events are persisted for as long as necessary
    */
@@ -55,6 +90,8 @@ private:
    *
    * @invariant: All of the events in this set are elements of `global_events_`
    * and is kept updated at the same time as `global_events_`
+   *
+   * @note: This is for the convenience of iteration over the unfolding
    */
   EventSet event_handles;