1 /* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */
3 /* This program is free software; you can redistribute it and/or modify it
4 * under the terms of the license (GNU LGPL) which comes with this package. */
6 #ifndef SIMGRID_MC_UDPOR_UNFOLDING_EVENT_HPP
7 #define SIMGRID_MC_UDPOR_UNFOLDING_EVENT_HPP
9 #include "src/mc/explo/udpor/EventSet.hpp"
10 #include "src/mc/explo/udpor/udpor_forward.hpp"
11 #include "src/mc/transition/Transition.hpp"
13 #include <initializer_list>
17 namespace simgrid::mc::udpor {
19 class UnfoldingEvent {
21 explicit UnfoldingEvent(std::initializer_list<const UnfoldingEvent*> init_list);
22 UnfoldingEvent(EventSet immediate_causes = EventSet(),
23 std::shared_ptr<Transition> transition = std::make_unique<Transition>());
25 UnfoldingEvent(const UnfoldingEvent&) = default;
26 UnfoldingEvent& operator=(UnfoldingEvent const&) = default;
27 UnfoldingEvent(UnfoldingEvent&&) = default;
29 EventSet get_history() const;
30 EventSet get_local_config() const;
31 bool in_history_of(const UnfoldingEvent* other) const;
34 * @brief Whether or not the given event is a decendant
35 * of or an ancestor of the given event
37 bool related_to(const UnfoldingEvent* other) const;
39 /// @brief Whether or not this event is in conflict with
40 /// the given one (i.e. whether `this # other`)
41 bool conflicts_with(const UnfoldingEvent* other) const;
43 /// @brief Whether or not this event is in conflict with
44 /// any event in the given set
45 bool conflicts_with_any(const EventSet& events) const;
47 /// @brief Computes "this #ⁱ other"
48 bool immediately_conflicts_with(const UnfoldingEvent* other) const;
49 bool is_dependent_with(const Transition*) const;
50 bool is_dependent_with(const UnfoldingEvent* other) const;
52 unsigned get_id() const { return this->id; }
53 aid_t get_actor() const { return get_transition()->aid_; }
54 const EventSet& get_immediate_causes() const { return this->immediate_causes; }
55 Transition* get_transition() const { return this->associated_transition.get(); }
57 void set_transition(std::shared_ptr<Transition> t) { this->associated_transition = std::move(t); }
59 std::string to_string() const;
61 bool operator==(const UnfoldingEvent&) const;
62 bool operator!=(const UnfoldingEvent& other) const { return not(*this == other); }
66 * @brief The transition that UDPOR "attaches" to this
67 * specific event for later use while computing e.g. extension
70 * The transition points to that of a particular actor
71 * in the state reached by the configuration C (recall
72 * this is denoted `state(C)`) that excludes this event.
73 * In other words, this transition was the "next" event
74 * of the actor that executes it in `state(C)`.
76 std::shared_ptr<Transition> associated_transition;
79 * @brief The "immediate" causes of this event.
81 * An event `e` is an immediate cause of an event `e'` if
84 * 2. There is no event `e''` in E such that
85 * `e < e''` and `e'' < e'`
87 * Intuitively, an immediate cause "happened right before"
88 * this event was executed. It is sufficient to store
89 * only the immediate causes of any event `e`, as any indirect
90 * causes of that event would either be an indirect cause
91 * or an immediate cause of the immediate causes of `e`, and
94 EventSet immediate_causes;
97 * @brief An identifier which is used to sort events
100 unsigned long id = 0;
103 } // namespace simgrid::mc::udpor