Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Merge branch 'udpor-phase3' into 'master'
[simgrid.git] / src / mc / explo / udpor / History.cpp
1 /* Copyright (c) 2008-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 #include "src/mc/explo/udpor/History.hpp"
7 #include "src/mc/explo/udpor/Configuration.hpp"
8 #include "src/mc/explo/udpor/UnfoldingEvent.hpp"
9
10 #include <stack>
11
12 namespace simgrid::mc::udpor {
13
14 History::Iterator::Iterator(const EventSet& initial_events, optional_configuration config)
15     : frontier(initial_events), maximal_events(initial_events), configuration(config)
16 {
17   // NOTE: Only events in the initial set of events can ever hope to have
18   // a chance at being a maximal event, since all other events in
19   // the search are generate by looking at dependencies of these events
20   // and all subsequent events that are added by the iterator
21 }
22
23 History::Iterator& History::Iterator::operator++()
24 {
25   if (not frontier.empty()) {
26     // "Pop" the event at the "front"
27     UnfoldingEvent* e = *frontier.begin();
28     frontier.remove(e);
29
30     // If there is a configuration and if the
31     // event is in it, skip it: the event and
32     // all of its immediate causes do not need to
33     // be searched since the configuration contains
34     // them (configuration invariant)
35     if (configuration.has_value() && configuration->get().contains(e)) {
36       return *this;
37     }
38
39     // Mark this event as seen
40     current_history.insert(e);
41
42     // Perform the expansion with all viable expansions
43     EventSet candidates = e->get_immediate_causes();
44
45     maximal_events.subtract(candidates);
46
47     candidates.subtract(current_history);
48     frontier.form_union(candidates);
49   }
50   return *this;
51 }
52
53 EventSet History::get_all_events() const
54 {
55   auto first      = this->begin();
56   const auto last = this->end();
57
58   for (; first != last; ++first)
59     ;
60
61   return first.current_history;
62 }
63
64 EventSet History::get_all_maximal_events() const
65 {
66   auto first      = this->begin();
67   const auto last = this->end();
68
69   for (; first != last; ++first)
70     ;
71
72   return first.maximal_events;
73 }
74
75 bool History::contains(const UnfoldingEvent* e) const
76 {
77   return std::any_of(this->begin(), this->end(), [=](const UnfoldingEvent* e_hist) { return e == e_hist; });
78 }
79
80 EventSet History::get_event_diff_with(const Configuration& config) const
81 {
82   auto wrapped_config = std::optional<std::reference_wrapper<const Configuration>>{config};
83   auto first          = Iterator(events_, wrapped_config);
84   const auto last     = this->end();
85
86   for (; first != last; ++first)
87     ;
88
89   return first.current_history;
90 }
91
92 } // namespace simgrid::mc::udpor