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_HPP
7 #define SIMGRID_MC_UDPOR_UNFOLDING_HPP
9 #include "src/mc/explo/udpor/EventSet.hpp"
10 #include "src/mc/explo/udpor/UnfoldingEvent.hpp"
11 #include "src/mc/explo/udpor/udpor_forward.hpp"
14 #include <unordered_map>
16 namespace simgrid::mc::udpor {
21 * @brief All of the events that are currently are a part of the unfolding
23 * @invariant Each unfolding event maps itself to the owner of that event,
24 * i.e. the unique pointer that owns the address. The Unfolding owns all
25 * of the addresses that are referenced by EventSet instances and Configuration
26 * instances. UDPOR guarantees that events are persisted for as long as necessary
28 std::unordered_map<const UnfoldingEvent*, std::unique_ptr<UnfoldingEvent>> global_events_;
31 * @brief: The collection of events in the unfolding
33 * @invariant: All of the events in this set are elements of `global_events_`
34 * and is kept updated at the same time as `global_events_`
36 EventSet event_handles;
39 * @brief The "irrelevant" portions of the unfolding that do not need to be kept
40 * around to ensure that UDPOR functions correctly
42 * The set `G` is another global variable maintained by the UDPOR algorithm which
43 * is used to keep track of all events which used to be important to UDPOR.
45 * @note: The current implementation does not touch the set `G`. Its use is perhaps
46 * limited to debugging and/or model-checking acyclic state spaces
51 Unfolding() = default;
52 Unfolding& operator=(Unfolding&&) = default;
53 Unfolding(Unfolding&&) = default;
55 void remove(const UnfoldingEvent* e);
56 void remove(const EventSet& events);
57 void insert(std::unique_ptr<UnfoldingEvent> e);
58 bool contains_event_equivalent_to(const UnfoldingEvent* e) const;
60 auto begin() const { return this->event_handles.begin(); }
61 auto end() const { return this->event_handles.end(); }
62 auto cbegin() const { return this->event_handles.cbegin(); }
63 auto cend() const { return this->event_handles.cend(); }
64 size_t size() const { return this->global_events_.size(); }
65 bool empty() const { return this->global_events_.empty(); }
67 /// @brief Computes "#ⁱ_U(e)" for the given event
68 EventSet get_immediate_conflicts_of(const UnfoldingEvent*) const;
71 } // namespace simgrid::mc::udpor