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_CONFIGURATION_HPP
7 #define SIMGRID_MC_UDPOR_CONFIGURATION_HPP
9 #include "src/mc/explo/udpor/CompatibilityGraph.hpp"
10 #include "src/mc/explo/udpor/EventSet.hpp"
11 #include "src/mc/explo/udpor/udpor_forward.hpp"
14 #include <initializer_list>
17 namespace simgrid::mc::udpor {
21 Configuration() = default;
22 Configuration(const Configuration&) = default;
23 Configuration& operator=(Configuration const&) = default;
24 Configuration(Configuration&&) = default;
26 Configuration(EventSet events);
27 Configuration(std::initializer_list<UnfoldingEvent*> events);
29 auto begin() const { return this->events_.begin(); }
30 auto end() const { return this->events_.end(); }
32 bool contains(UnfoldingEvent* e) const { return this->events_.contains(e); }
33 const EventSet& get_events() const { return this->events_; }
34 UnfoldingEvent* get_latest_event() const { return this->newest_event; }
37 * @brief Insert a new event into the configuration
39 * When the newly added event is inserted into the configuration,
40 * an assertion is made to ensure that the configuration remains
41 * valid, i.e. that the newly added event's dependencies are contained
42 * within the configuration.
44 * @param e the event to add to the configuration. If the event is
45 * already a part of the configuration, calling this method has no
48 * @throws an invalid argument exception is raised should the event
49 * be missing one of its dependencies
51 * @note: UDPOR technically enforces the invariant that all newly-added events
52 * will ensure that the configuration is valid. We perform extra checks to ensure
53 * that UDPOR is implemented as expected. There is a performance penalty that
54 * should be noted: checking for maximality requires ensuring that all events in the
55 * configuration have their dependencies containes within the configuration, which
56 * essentially means performing a BFS/DFS over the configuration using a History object.
57 * However, since the slowest part of UDPOR involves enumerating all
58 * subsets of maximal events and computing k-partial alternatives (the
59 * latter definitively an NP-hard problem when optimal), Amdahl's law suggests
60 * we shouldn't focus so much on this (let alone the additional benefit of the
63 void add_event(UnfoldingEvent* e);
66 * @brief Orders the events of the configuration such that
67 * "more recent" events (i.e. those that are farther down in
68 * the event structure's dependency chain) come after those
69 * that appeared "farther in the past"
71 * @returns a vector `V` with the following property:
73 * 1. Let i(e) := C -> I map events to their indices in `V`.
74 * For every pair of events e, e' in C, if e < e' then i(e) < i(e')
76 * Intuitively, events that are closer to the "bottom" of the event
77 * structure appear farther along in the list than those that appear
80 std::vector<UnfoldingEvent*> get_topologically_sorted_events() const;
83 * @brief Orders the events of the configuration such that
84 * "more recent" events (i.e. those that are farther down in
85 * the event structure's dependency chain) come before those
86 * that appear "farther in the past"
88 * @note The events of the event structure are arranged such that
89 * e < e' implies a directed edge from e to e'. However, it is
90 * also useful to be able to traverse the *reverse* graph (for
91 * example when computing the compatibility graph of a configuration),
92 * hence the distinction between "reversed" and the method
93 * "Configuration::get_topologically_sorted_events()"
95 * @returns a vector `V` with the following property:
97 * 1. Let i(e) := C -> I map events to their indices in `V`.
98 * For every pair of events e, e' in C, if e < e' then i(e) > i(e')
100 * Intuitively, events that are closer to the "top" of the event
101 * structure appear farther along in the list than those that appear
102 * closer to the "bottom"
104 std::vector<UnfoldingEvent*> get_topologically_sorted_events_of_reverse_graph() const;
107 * @brief Construct a new compatibility graph from the events of the
108 * configuration whose associated transitions are dependent with the
111 * @param pred whether or not to even consider the unfolding event in any
112 * compatibility nodes of the resulting graph
113 * @returns a new compatibility graph that defines possible maximal subsets
114 * of events of C that satisfy the predicate `pred`
116 std::unique_ptr<CompatibilityGraph>
117 make_compatibility_graph_filtered_on(std::function<bool(UnfoldingEvent*)> pred) const;
121 * @brief The most recent event added to the configuration
123 UnfoldingEvent* newest_event = nullptr;
126 * @brief The events which make up this configuration
128 * @invariant For each event `e` in `events_`, the set of
129 * dependencies of `e` is also contained in `events_`
134 } // namespace simgrid::mc::udpor