Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Merge branch 'master' of https://framagit.org/simgrid/simgrid
[simgrid.git] / src / mc / explo / udpor / Configuration.hpp
1 /* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved.          */
2
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. */
5
6 #ifndef SIMGRID_MC_UDPOR_CONFIGURATION_HPP
7 #define SIMGRID_MC_UDPOR_CONFIGURATION_HPP
8
9 #include "src/mc/explo/udpor/EventSet.hpp"
10 #include "src/mc/explo/udpor/udpor_forward.hpp"
11
12 #include <optional>
13
14 namespace simgrid::mc::udpor {
15
16 class Configuration {
17 public:
18   Configuration()                                = default;
19   Configuration(const Configuration&)            = default;
20   Configuration& operator=(Configuration const&) = default;
21   Configuration(Configuration&&)                 = default;
22
23   explicit Configuration(const UnfoldingEvent* event);
24   explicit Configuration(const EventSet& events);
25   explicit Configuration(const History& history);
26   explicit Configuration(std::initializer_list<const UnfoldingEvent*> events);
27
28   auto begin() const { return this->events_.begin(); }
29   auto end() const { return this->events_.end(); }
30   auto cbegin() const { return this->events_.cbegin(); }
31   auto cend() const { return this->events_.cend(); }
32
33   bool contains(const UnfoldingEvent* e) const { return this->events_.contains(e); }
34   const EventSet& get_events() const { return this->events_; }
35   const UnfoldingEvent* get_latest_event() const { return this->newest_event; }
36
37   /**
38    * @brief Insert a new event into the configuration
39    *
40    * When the newly added event is inserted into the configuration,
41    * an assertion is made to ensure that the configuration remains
42    * valid, i.e. that the newly added event's dependencies are contained
43    * within the configuration.
44    *
45    * @param e the event to add to the configuration. If the event is
46    * already a part of the configuration, calling this method has no
47    * effect.
48    *
49    * @throws an invalid argument exception is raised should the event
50    * be missing one of its dependencies
51    *
52    * @note: UDPOR technically enforces the invariant that all newly-added events
53    * will ensure that the configuration is valid. We perform extra checks to ensure
54    * that UDPOR is implemented as expected. There is a performance penalty that
55    * should be noted: checking for maximality requires ensuring that all events in the
56    * configuration have their dependencies containes within the configuration, which
57    * essentially means performing a BFS/DFS over the configuration using a History object.
58    * However, since the slowest part of UDPOR involves enumerating all
59    * subsets of maximal events and computing k-partial alternatives (the
60    * latter definitively an NP-hard problem when optimal), Amdahl's law suggests
61    * we shouldn't focus so much on this (let alone the additional benefit of the
62    * assertions)
63    */
64   void add_event(const UnfoldingEvent* e);
65
66   /**
67    * @brief Whether or not the given event can be added to
68    * this configuration while keeping the set of events causally closed
69    * and conflict-free
70    */
71   bool is_compatible_with(const UnfoldingEvent* e) const;
72
73   /**
74    * @brief Whether or not the events in the given history can be added to
75    * this configuration while keeping the set of events causally closed
76    * and conflict-free
77    */
78   bool is_compatible_with(const History& history) const;
79
80   std::optional<Configuration> compute_alternative_to(const EventSet& D, const Unfolding& U) const;
81   std::optional<Configuration> compute_k_partial_alternative_to(const EventSet& D, const Unfolding& U, size_t k) const;
82
83   /**
84    * @brief Orders the events of the configuration such that
85    * "more recent" events (i.e. those that are farther down in
86    * the event structure's dependency chain) come after those
87    * that appeared "farther in the past"
88    *
89    * @returns a vector `V` with the following property:
90    *
91    * 1. Let i(e) := C -> I map events to their indices in `V`.
92    * For every pair of events e, e' in C, if e < e' then i(e) < i(e')
93    *
94    * Intuitively, events that are closer to the "bottom" of the event
95    * structure appear farther along in the list than those that appear
96    * closer to the "top"
97    */
98   std::vector<const UnfoldingEvent*> get_topologically_sorted_events() const;
99
100   /**
101    * @brief Orders the events of the configuration such that
102    * "more recent" events (i.e. those that are farther down in
103    * the event structure's dependency chain) come before those
104    * that appear "farther in the past"
105    *
106    * @note The events of the event structure are arranged such that
107    * e < e' implies a directed edge from e to e'. However, it is
108    * also useful to be able to traverse the *reverse* graph (for
109    * example when computing the compatibility graph of a configuration),
110    * hence the distinction between "reversed" and the method
111    * "Configuration::get_topologically_sorted_events()"
112    *
113    * @returns a vector `V` with the following property:
114    *
115    * 1. Let i(e) := C -> I map events to their indices in `V`.
116    * For every pair of events e, e' in C, if e < e' then i(e) > i(e')
117    *
118    * Intuitively, events that are closer to the "top" of the event
119    * structure appear farther along in the list than those that appear
120    * closer to the "bottom"
121    */
122   std::vector<const UnfoldingEvent*> get_topologically_sorted_events_of_reverse_graph() const;
123
124   /**
125    * @brief Computes the smallest set of events whose collective histories
126    * capture all events of this configuration
127    *
128    * @invariant The set of all events in the collective histories
129    * of the events returned by this method is equal to the set of events
130    * in this configuration
131    *
132    * @returns the smallest set of events whose events generates
133    * this configuration (denoted `config(E)`)
134    */
135   EventSet get_minimally_reproducible_events() const;
136
137 private:
138   /**
139    * @brief The most recent event added to the configuration
140    */
141   const UnfoldingEvent* newest_event = nullptr;
142
143   /**
144    * @brief The events which make up this configuration
145    *
146    * @invariant For each event `e` in `events_`, the set of
147    * dependencies of `e` is also contained in `events_`
148    */
149   EventSet events_;
150 };
151
152 } // namespace simgrid::mc::udpor
153 #endif