X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/c1f72d83295393da38a9373e6f0b0cf41f31cb4f..50753d5f8442a47c17c4035724201a18a7ff6146:/src/mc/explo/udpor/Unfolding.hpp

diff --git a/src/mc/explo/udpor/Unfolding.hpp b/src/mc/explo/udpor/Unfolding.hpp
index 471e04330a..0107692670 100644
--- a/src/mc/explo/udpor/Unfolding.hpp
+++ b/src/mc/explo/udpor/Unfolding.hpp
@@ -6,6 +6,7 @@
 #ifndef SIMGRID_MC_UDPOR_UNFOLDING_HPP
 #define SIMGRID_MC_UDPOR_UNFOLDING_HPP
 
+#include "src/mc/explo/udpor/EventSet.hpp"
 #include "src/mc/explo/udpor/UnfoldingEvent.hpp"
 #include "src/mc/explo/udpor/udpor_forward.hpp"
 
@@ -24,18 +25,47 @@ private:
    * of the addresses that are referenced by EventSet instances and Configuration
    * instances. UDPOR guarantees that events are persisted for as long as necessary
    */
-  std::unordered_map<UnfoldingEvent*, std::unique_ptr<UnfoldingEvent>> global_events_;
+  std::unordered_map<const UnfoldingEvent*, std::unique_ptr<UnfoldingEvent>> global_events_;
+
+  /**
+   * @brief: The collection of events in the unfolding
+   *
+   * @invariant: All of the events in this set are elements of `global_events_`
+   * and is kept updated at the same time as `global_events_`
+   */
+  EventSet event_handles;
+
+  /**
+   * @brief The "irrelevant" portions of the unfolding that do not need to be kept
+   * around to ensure that UDPOR functions correctly
+   *
+   * The set `G` is another global variable maintained by the UDPOR algorithm which
+   * is used to keep track of all events which used to be important to UDPOR.
+   *
+   * @note: The current implementation does not touch the set `G`. Its use is perhaps
+   * limited to debugging and/or model-checking acyclic state spaces
+   */
+  EventSet G;
 
 public:
   Unfolding()                       = default;
   Unfolding& operator=(Unfolding&&) = default;
   Unfolding(Unfolding&&)            = default;
 
-  void remove(UnfoldingEvent* e);
+  void remove(const UnfoldingEvent* e);
+  void remove(const EventSet& events);
   void insert(std::unique_ptr<UnfoldingEvent> e);
+  bool contains_event_equivalent_to(const UnfoldingEvent* e) const;
 
+  auto begin() const { return this->event_handles.begin(); }
+  auto end() const { return this->event_handles.end(); }
+  auto cbegin() const { return this->event_handles.cbegin(); }
+  auto cend() const { return this->event_handles.cend(); }
   size_t size() const { return this->global_events_.size(); }
   bool empty() const { return this->global_events_.empty(); }
+
+  /// @brief Computes "#ⁱ_U(e)" for the given event
+  EventSet get_immediate_conflicts_of(const UnfoldingEvent*) const;
 };
 
 } // namespace simgrid::mc::udpor