Merge branch 'udpor-phase6' into 'master'

[simgrid.git] / src / mc / explo / udpor / UnfoldingEvent.hpp

diff --git a/src/mc/explo/udpor/UnfoldingEvent.hpp b/src/mc/explo/udpor/UnfoldingEvent.hpp
index 5604362..aeb4902 100644 (file)
--- a/src/mc/explo/udpor/UnfoldingEvent.hpp
+++ b/src/mc/explo/udpor/UnfoldingEvent.hpp
@@ -8,34 +8,60 @@
 
 #include "src/mc/explo/udpor/EventSet.hpp"
 #include "src/mc/explo/udpor/udpor_forward.hpp"
+#include "src/mc/transition/Transition.hpp"
 
+#include <initializer_list>
+#include <memory>
 #include <string>
 
 namespace simgrid::mc::udpor {
 
 class UnfoldingEvent {
 public:
-  UnfoldingEvent(unsigned int nb_events, std::string const& trans_tag, EventSet const& immediate_causes,
-                 StateHandle sid);
-  UnfoldingEvent(unsigned int nb_events, std::string const& trans_tag, EventSet const& immediate_causes);
+  explicit UnfoldingEvent(std::initializer_list<const UnfoldingEvent*> init_list);
+  UnfoldingEvent(EventSet immediate_causes              = EventSet(),
+                 std::shared_ptr<Transition> transition = std::make_unique<Transition>());
+
   UnfoldingEvent(const UnfoldingEvent&)            = default;
   UnfoldingEvent& operator=(UnfoldingEvent const&) = default;
   UnfoldingEvent(UnfoldingEvent&&)                 = default;
 
   EventSet get_history() const;
-  bool in_history_of(const UnfoldingEvent* otherEvent) const;
+  bool in_history_of(const UnfoldingEvent* other) const;
+  bool related_to(const UnfoldingEvent* other) const;
+
+  /// @brief Whether or not this event is in conflict with
+  /// the given one (i.e. whether `this # other`)
+  bool conflicts_with(const UnfoldingEvent* other) const;
 
-  bool conflicts_with(const UnfoldingEvent* otherEvent) const;
+  /// @brief Whether or not this event is in conflict with
+  /// any event in the given configuration
   bool conflicts_with(const Configuration& config) const;
-  bool immediately_conflicts_with(const UnfoldingEvent* otherEvt) const;
 
-  inline StateHandle get_state_id() const { return state_id; }
-  inline void set_state_id(StateHandle sid) { state_id = sid; }
+  /// @brief Computes "this #ⁱ other"
+  bool immediately_conflicts_with(const UnfoldingEvent* other) const;
+  bool is_dependent_with(const Transition*) const;
+  bool is_dependent_with(const UnfoldingEvent* other) const;
+
+  const EventSet& get_immediate_causes() const { return this->immediate_causes; }
+  Transition* get_transition() const { return this->associated_transition.get(); }
 
   bool operator==(const UnfoldingEvent&) const;
+  bool operator!=(const UnfoldingEvent& other) const { return not(*this == other); }
 
 private:
-  int id = -1;
+  /**
+   * @brief The transition that UDPOR "attaches" to this
+   * specific event for later use while computing e.g. extension
+   * sets
+   *
+   * The transition points to that of a particular actor
+   * in the state reached by the configuration C (recall
+   * this is denoted `state(C)`) that excludes this event.
+   * In other words, this transition was the "next" event
+   * of the actor that executes it in `state(C)`.
+   */
+  std::shared_ptr<Transition> associated_transition;
 
   /**
    * @brief The "immediate" causes of this event.
@@ -54,7 +80,6 @@ private:
    * so on.
    */
   EventSet immediate_causes;
-  StateHandle state_id = 0ul;
 };
 
 } // namespace simgrid::mc::udpor