X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/573b5f83d54c3137fbedd6597bbef9ed3d4645fc..45c3a73f3553c8d365f61eaa8445f038db9bdb8f:/src/mc/explo/udpor/UnfoldingEvent.hpp diff --git a/src/mc/explo/udpor/UnfoldingEvent.hpp b/src/mc/explo/udpor/UnfoldingEvent.hpp index 5604362d21..5486709576 100644 --- a/src/mc/explo/udpor/UnfoldingEvent.hpp +++ b/src/mc/explo/udpor/UnfoldingEvent.hpp @@ -8,34 +8,72 @@ #include "src/mc/explo/udpor/EventSet.hpp" #include "src/mc/explo/udpor/udpor_forward.hpp" +#include "src/mc/transition/Transition.hpp" +#include +#include #include 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 init_list); + UnfoldingEvent(EventSet immediate_causes = EventSet(), + std::shared_ptr transition = std::make_unique()); + UnfoldingEvent(const UnfoldingEvent&) = default; UnfoldingEvent& operator=(UnfoldingEvent const&) = default; UnfoldingEvent(UnfoldingEvent&&) = default; EventSet get_history() const; - bool in_history_of(const UnfoldingEvent* otherEvent) const; + EventSet get_local_config() const; + bool in_history_of(const UnfoldingEvent* other) const; + + /** + * @brief Whether or not the given event is a decendant + * of or an ancestor of the given event + */ + 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; + + /// @brief Whether or not this event is in conflict with + /// any event in the given set + bool conflicts_with_any(const EventSet& events) const; + + /// @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; - bool conflicts_with(const UnfoldingEvent* otherEvent) const; - bool conflicts_with(const Configuration& config) const; - bool immediately_conflicts_with(const UnfoldingEvent* otherEvt) const; + unsigned get_id() const { return this->id; } + aid_t get_actor() const { return get_transition()->aid_; } + const EventSet& get_immediate_causes() const { return this->immediate_causes; } + Transition* get_transition() const { return this->associated_transition.get(); } - inline StateHandle get_state_id() const { return state_id; } - inline void set_state_id(StateHandle sid) { state_id = sid; } + void set_transition(std::shared_ptr t) { this->associated_transition = std::move(t); } + + std::string to_string() const; 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 associated_transition; /** * @brief The "immediate" causes of this event. @@ -54,7 +92,12 @@ private: * so on. */ EventSet immediate_causes; - StateHandle state_id = 0ul; + + /** + * @brief An identifier which is used to sort events + * deterministically + */ + uint64_t id = 0; }; } // namespace simgrid::mc::udpor