#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;
+ 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<Transition> t) { this->associated_transition = std::move(t); }
- bool operator==(const UnfoldingEvent&) const
- {
- // TODO: Implement semantic equality
- return false;
- };
+ 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<Transition> associated_transition;
/**
* @brief The "immediate" causes of this event.
* so on.
*/
EventSet immediate_causes;
- StateHandle state_id = 0ul;
+
+ /**
+ * @brief An identifier which is used to sort events
+ * deterministically
+ */
+ unsigned long id = 0;
};
} // namespace simgrid::mc::udpor
