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"
16 namespace simgrid::mc::udpor {
18 class UnfoldingEvent {
20 UnfoldingEvent(std::shared_ptr<Transition> transition = std::make_unique<Transition>(),
21 EventSet immediate_causes = EventSet(), unsigned long event_id = 0);
23 UnfoldingEvent(const UnfoldingEvent&) = default;
24 UnfoldingEvent& operator=(UnfoldingEvent const&) = default;
25 UnfoldingEvent(UnfoldingEvent&&) = default;
27 EventSet get_history() const;
28 bool in_history_of(const UnfoldingEvent* otherEvent) const;
30 bool conflicts_with(const UnfoldingEvent* otherEvent) const;
31 bool conflicts_with(const Configuration& config) const;
32 bool immediately_conflicts_with(const UnfoldingEvent* otherEvt) const;
34 const EventSet& get_immediate_causes() const { return this->immediate_causes; }
35 Transition* get_transition() const { return this->associated_transition.get(); }
37 bool operator==(const UnfoldingEvent&) const;
41 * @brief The transition that UDPOR "attaches" to this
42 * specific event for later use while computing e.g. extension
45 * The transition points to that of a particular actor
46 * in the state reached by the configuration C (recall
47 * this is denoted `state(C)`) that excludes this event.
48 * In other words, this transition was the "next" event
49 * of the actor that executes it in `state(C)`.
51 std::shared_ptr<Transition> associated_transition;
54 * @brief The "immediate" causes of this event.
56 * An event `e` is an immediate cause of an event `e'` if
59 * 2. There is no event `e''` in E such that
60 * `e < e''` and `e'' < e'`
62 * Intuitively, an immediate cause "happened right before"
63 * this event was executed. It is sufficient to store
64 * only the immediate causes of any event `e`, as any indirect
65 * causes of that event would either be an indirect cause
66 * or an immediate cause of the immediate causes of `e`, and
69 EventSet immediate_causes;
71 unsigned long event_id = 0;
74 } // namespace simgrid::mc::udpor