include src/mc/transition/TransitionRandom.hpp
include src/mc/transition/TransitionSynchro.cpp
include src/mc/transition/TransitionSynchro.hpp
-include src/mc/udpor_global.cpp
-include src/mc/udpor_global.hpp
+include src/mc/explo/udpor/Configuration.hpp
+include src/mc/explo/udpor/Configuration.cpp
+include src/mc/explo/udpor/EventSet.cpp
+include src/mc/explo/udpor/EventSet.hpp
+include src/mc/explo/udpor/History.cpp
+include src/mc/explo/udpor/History.hpp
+include src/mc/explo/udpor/UnfoldingEvent.cpp
+include src/mc/explo/udpor/UnfoldingEvent.hpp
+include src/mc/explo/udpor/Unfolding.cpp
+include src/mc/explo/udpor/Unfolding.hpp
include src/plugins/ProducerConsumer.cpp
include src/plugins/chaos_monkey.cpp
include src/plugins/file_system/s4u_FileSystem.cpp
* This means there may be a way to store the list once and apply differences
* rather than repeating elements frequently.
*/
- std::vector<std::unique_ptr<Transition>> pending_transitions_;
+ std::vector<std::shared_ptr<Transition>> pending_transitions_;
/* Possible exploration status of an actor transition in a state.
* Either the checker did not consider the transition, or it was considered and still to do, or considered and
public:
ActorState(aid_t aid, bool enabled, unsigned int max_consider) : ActorState(aid, enabled, max_consider, {}) {}
- ActorState(aid_t aid, bool enabled, unsigned int max_consider, std::vector<std::unique_ptr<Transition>> transitions)
+ ActorState(aid_t aid, bool enabled, unsigned int max_consider, std::vector<std::shared_ptr<Transition>> transitions)
: pending_transitions_(std::move(transitions)), aid_(aid), max_consider_(max_consider), enabled_(enabled)
{
}
"(currently %d), but only %d transition(s) was/were said to be encoded",
actor.max_considered, actor.n_transitions);
- std::vector<std::unique_ptr<Transition>> actor_transitions;
+ std::vector<std::shared_ptr<Transition>> actor_transitions;
for (int times_considered = 0; times_considered < actor.n_transitions; times_considered++, probes_iter++) {
std::stringstream stream((*probes_iter).buffer.data());
actor_transitions.emplace_back(deserialize_transition(actor.aid, times_considered, stream));
return boost::range::count_if(this->actors_to_run_, [](auto& pair) { return pair.second.is_todo(); });
}
+void State::mark_all_enabled_todo()
+{
+ for (auto const& [aid, _] : this->get_actors_list()) {
+ if (this->is_actor_enabled(aid)) {
+ this->mark_todo(aid);
+ }
+ }
+}
+
Transition* State::get_transition() const
{
return transition_;
long get_num() const { return num_; }
std::size_t count_todo() const;
void mark_todo(aid_t actor) { actors_to_run_.at(actor).mark_todo(); }
+ void mark_all_enabled_todo();
bool is_done(aid_t actor) const { return actors_to_run_.at(actor).is_done(); }
Transition* get_transition() const;
void set_transition(Transition* t) { transition_ = t; }
* under the terms of the license (GNU LGPL) which comes with this package. */
#include "src/mc/explo/UdporChecker.hpp"
+#include "src/mc/api/State.hpp"
+#include <xbt/asserts.h>
#include <xbt/log.h>
-XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to MC safety verification ");
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to verification using UDPOR");
-namespace simgrid::mc {
+namespace simgrid::mc::udpor {
+
+UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args)
+{
+ /* Create initial data structures, if any ...*/
+
+ // TODO: Initialize state structures for the search
+}
+
+void UdporChecker::run()
+{
+ XBT_INFO("Starting a UDPOR exploration");
+ // NOTE: `A`, `D`, and `C` are derived from the
+ // original UDPOR paper [1], while `prev_exC` arises
+ // from the incremental computation of ex(C) from [3]
+ Configuration C_root;
+
+ // TODO: Move computing the root configuration into a method on the Unfolding
+ auto initial_state = get_current_state();
+ auto root_event = std::make_unique<UnfoldingEvent>(EventSet(), std::make_shared<Transition>());
+ auto* root_event_handle = root_event.get();
+ unfolding.insert(std::move(root_event));
+ C_root.add_event(root_event_handle);
+
+ explore(std::move(C_root), EventSet(), EventSet(), std::move(initial_state), EventSet());
+
+ XBT_INFO("UDPOR exploration terminated -- model checking completed");
+}
+
+void UdporChecker::explore(Configuration C, EventSet D, EventSet A, std::unique_ptr<State> stateC, EventSet prev_exC)
+{
+ // Perform the incremental computation of exC
+ //
+ // TODO: This method will have side effects on
+ // the unfolding, but the naming of the method
+ // suggests it is doesn't have side effects. We should
+ // reconcile this in the future
+ auto [exC, enC] = compute_extension(C, prev_exC);
+
+ // If enC is a subset of D, intuitively
+ // there aren't any enabled transitions
+ // which are "worth" exploring since their
+ // exploration would lead to a so-called
+ // "sleep-set blocked" trace.
+ if (enC.is_subset_of(D)) {
+
+ if (C.get_events().size() > 0) {
+
+ // g_var::nb_traces++;
+
+ // TODO: Log here correctly
+ // XBT_DEBUG("\n Exploring executions: %d : \n", g_var::nb_traces);
+ // ...
+ // ...
+ }
+
+ // When `en(C)` is empty, intuitively this means that there
+ // are no enabled transitions that can be executed from the
+ // state reached by `C` (denoted `state(C)`), i.e. by some
+ // execution of the transitions in C obeying the causality
+ // relation. Here, then, we would be in a deadlock.
+ if (enC.empty()) {
+ get_remote_app().check_deadlock();
+ }
+
+ return;
+ }
+
+ // TODO: Add verbose logging about which event is being explored
+
+ UnfoldingEvent* e = select_next_unfolding_event(A, enC);
+ xbt_assert(e != nullptr, "\n\n****** INVARIANT VIOLATION ******\n"
+ "UDPOR guarantees that an event will be chosen at each point in\n"
+ "the search, yet no events were actually chosen\n"
+ "*********************************\n\n");
+
+ // Move the application into stateCe and actually make note of that state
+ move_to_stateCe(*stateC, *e);
+ auto stateCe = record_current_state();
+
+ // Ce := C + {e}
+ Configuration Ce = C;
+ Ce.add_event(e);
+
+ A.remove(e);
+ exC.remove(e);
+
+ // Explore(C + {e}, D, A \ {e})
+ explore(Ce, D, std::move(A), std::move(stateCe), std::move(exC));
+
+ // D <-- D + {e}
+ D.insert(e);
+
+ // TODO: Determine a value of K to use or don't use it at all
+ constexpr unsigned K = 10;
+ auto J = compute_partial_alternative(D, C, K);
+ if (!J.empty()) {
+ J.subtract(C.get_events());
+
+ // Before searching the "right half", we need to make
+ // sure the program actually reflects the fact
+ // that we are searching again from `stateC` (the recursive
+ // search moved the program into `stateCe`)
+ restore_program_state_to(*stateC);
+
+ // Explore(C, D + {e}, J \ C)
+ explore(C, D, std::move(J), std::move(stateC), std::move(prev_exC));
+ }
+
+ // D <-- D - {e}
+ D.remove(e);
-UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args) {}
+ // Remove(e, C, D)
+ clean_up_explore(e, C, D);
+}
+
+std::tuple<EventSet, EventSet> UdporChecker::compute_extension(const Configuration& C, const EventSet& prev_exC) const
+{
+ // See eqs. 5.7 of section 5.2 of [3]
+ // C = C' + {e_cur}, i.e. C' = C - {e_cur}
+ //
+ // Then
+ //
+ // ex(C) = ex(C' + {e_cur}) = ex(C') / {e_cur} + U{<a, > : H }
+ UnfoldingEvent* e_cur = C.get_latest_event();
+ EventSet exC = prev_exC;
+ exC.remove(e_cur);
+
+ // ... fancy computations
+
+ EventSet enC;
+ return std::tuple<EventSet, EventSet>(exC, enC);
+}
+
+void UdporChecker::move_to_stateCe(State& state, const UnfoldingEvent& e)
+{
+ const aid_t next_actor = e.get_transition()->aid_;
+
+ // TODO: Add the trace if possible for reporting a bug
+ xbt_assert(next_actor >= 0, "\n\n****** INVARIANT VIOLATION ******\n"
+ "In reaching this execution path, UDPOR ensures that at least one\n"
+ "one transition of the state of an visited event is enabled, yet no\n"
+ "state was actually enabled. Please report this as a bug.\n"
+ "*********************************\n\n");
+ state.execute_next(next_actor);
+}
+
+void UdporChecker::restore_program_state_to(const State& stateC)
+{
+ // TODO: Perform state regeneration in the same manner as is done
+ // in the DFSChecker.cpp
+}
+
+std::unique_ptr<State> UdporChecker::record_current_state()
+{
+ auto next_state = this->get_current_state();
-void UdporChecker::run() {}
+ // In UDPOR, we care about all enabled transitions in a given state
+ next_state->mark_all_enabled_todo();
+
+ return next_state;
+}
+
+UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
+{
+ if (!enC.empty()) {
+ return *(enC.begin());
+ }
+
+ for (const auto& event : A) {
+ if (enC.contains(event)) {
+ return event;
+ }
+ }
+ return nullptr;
+}
+
+EventSet UdporChecker::compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const
+{
+ // TODO: Compute k-partial alternatives using [2]
+ return EventSet();
+}
+
+void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
+{
+ // TODO: Perform clean up here
+}
RecordTrace UdporChecker::get_record_trace()
{
std::vector<std::string> UdporChecker::get_textual_trace()
{
+ // TODO: Topologically sort the events of the latest configuration
+ // and iterate through that topological sorting
std::vector<std::string> trace;
return trace;
}
+} // namespace simgrid::mc::udpor
+
+namespace simgrid::mc {
+
Exploration* create_udpor_checker(const std::vector<char*>& args)
{
- return new UdporChecker(args);
+ return new simgrid::mc::udpor::UdporChecker(args);
}
} // namespace simgrid::mc
#define SIMGRID_MC_UDPOR_CHECKER_HPP
#include "src/mc/explo/Exploration.hpp"
+#include "src/mc/explo/udpor/Configuration.hpp"
+#include "src/mc/explo/udpor/EventSet.hpp"
+#include "src/mc/explo/udpor/Unfolding.hpp"
+#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
#include "src/mc/mc_record.hpp"
-namespace simgrid::mc {
+#include <optional>
+namespace simgrid::mc::udpor {
+
+/**
+ * @brief Performs exploration of a concurrent system via the
+ * UDPOR algorithm
+ *
+ * The `UdporChecker` implementation is based primarily off three papers,
+ * herein referred to as [1], [2], and [3] respectively, as well as the
+ * current implementation of `tiny_simgrid`:
+ *
+ * 1. "Unfolding-based Partial Order Reduction" by Rodriguez et al.
+ * 2. Quasi-Optimal Partial Order Reduction by Nguyen et al.
+ * 3. The Anh Pham's Thesis "Exploration efficace de l'espace ..."
+ */
class XBT_PRIVATE UdporChecker : public Exploration {
public:
explicit UdporChecker(const std::vector<char*>& args);
+
void run() override;
RecordTrace get_record_trace() override;
std::vector<std::string> get_textual_trace() override;
-};
-} // namespace simgrid::mc
+ inline std::unique_ptr<State> get_current_state() { return std::make_unique<State>(get_remote_app()); }
+
+private:
+ /**
+ * The total number of events created whilst exploring the unfolding
+ */
+ uint32_t nb_events = 0;
+ uint32_t nb_traces = 0;
+
+ /**
+ * @brief The "relevant" portions of the unfolding that must be kept around to ensure that
+ * UDPOR properly searches the state space
+ *
+ * The set `U` is a global variable which is maintained by UDPOR
+ * to keep track of "just enough" information about the unfolding
+ * to compute *alternatives* (see the paper for more details).
+ *
+ * @invariant: When a new event is created by UDPOR, it is inserted into
+ * this set. All new events that are created by UDPOR have causes that
+ * also exist in U and are valid for the duration of the search.
+ *
+ * If an event is discarded instead of moved from set `U` to set `G`,
+ * the event and its contents will be discarded.
+ */
+ EventSet U;
+
+ /**
+ * @brief The "irrelevant" portions of the unfolding that do not need to be kept
+ * around to ensure that UDPOR functions correctly
+ *
+ * The set `G` is another global variable maintained by the UDPOR algorithm which
+ * is used to keep track of all events which used to be important to UDPOR
+ */
+ EventSet G;
+
+ /**
+ * @brief UDPOR's current "view" of the program it is exploring
+ */
+ Unfolding unfolding = Unfolding();
+
+private:
+ /**
+ * @brief Explores the unfolding of the concurrent system
+ * represented by the ModelChecker instance "mcmodel_checker"
+ *
+ * This function performs the actual search following the
+ * UDPOR algorithm according to [1].
+ *
+ * @param C the current configuration from which UDPOR will be used
+ * to explore expansions of the concurrent system being modeled
+ * @param D the set of events that should not be considered by UDPOR
+ * while performing its searches, in order to avoid sleep-set blocked
+ * executions. See [1] for more details
+ * @param A the set of events to "guide" UDPOR in the correct direction
+ * when it returns back to a node in the unfolding and must decide among
+ * events to select from `ex(C)`. See [1] for more details
+ * @param stateC the state of the program after having executed `C`,
+ * viz. `state(C)` using the notation of [1]
+ *
+ * TODO: Add the optimization where we can check if e == e_prior
+ * to prevent repeated work when computing ex(C)
+ */
+ void explore(Configuration C, EventSet D, EventSet A, std::unique_ptr<State> stateC, EventSet prev_exC);
+
+ /**
+ * @brief Identifies the next event from the unfolding of the concurrent system
+ * that should next be explored as an extension of a configuration with
+ * enabled events `enC`
+ *
+ * @param A The set of events `A` maintained by the UDPOR algorithm to help
+ * determine how events should be selected. See the original paper [1] for more details
+ *
+ * @param enC The set `enC` of enabled events from the extension set `exC` used
+ * by the UDPOR algorithm to select new events to search. See the original
+ * paper [1] for more details
+ */
+ UnfoldingEvent* select_next_unfolding_event(const EventSet& A, const EventSet& enC);
+
+ /**
+ * @brief Computes the sets `ex(C)` and `en(C)` of the given configuration
+ * `C` as an incremental computation from the the previous computation of `ex(C)`
+ *
+ * A central component to UDPOR is the computation of the set `ex(C)`. The
+ * extension set `ex(C)` of a configuration `C` is defined as the set of events
+ * outside of `C` whose full dependency chain is contained in `C` (see [1]
+ * for more details).
+ *
+ * In general, computing `ex(C)` is very expensive. In paper [3], The Anh Pham
+ * shows a method of incremental computation of the set `ex(C)` under the
+ * conclusions afforded under the computation model in consideration, of which
+ * SimGrid is apart, which allow for `ex(C)` to be computed much more efficiently.
+ * Intuitively, the idea is to take advantage of the fact that you can avoid a lot
+ * of repeated computation by exploiting the aforementioned properties (in [3]) in
+ * what is effectively a dynamic programming optimization. See [3] for more details
+ *
+ * @param C the configuration based on which the two sets `ex(C)` and `en(C)` are
+ * computed
+ * @param prev_exC the previous value of `ex(C)`, viz. that which was computed for
+ * the configuration `C' := C - {e}`
+ * @returns a tuple containing the pair of sets `ex(C)` and `en(C)` respectively
+ */
+ std::tuple<EventSet, EventSet> compute_extension(const Configuration& C, const EventSet& prev_exC) const;
+
+ /**
+ *
+ */
+ EventSet compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const;
+
+ /**
+ *
+ */
+ void move_to_stateCe(State& stateC, const UnfoldingEvent& e);
+
+ /**
+ * @brief Creates a new snapshot of the state of the progam undergoing
+ * model checking
+ *
+ * @returns the handle used to uniquely identify this state later in the
+ * exploration of the unfolding. You provide this handle to an event in the
+ * unfolding to regenerate past states
+ */
+ std::unique_ptr<State> record_current_state();
+
+ /**
+ *
+ */
+ void restore_program_state_to(const State& stateC);
+
+ /**
+ *
+ */
+ void clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D);
+};
+} // namespace simgrid::mc::udpor
#endif
--- /dev/null
+/* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "src/mc/explo/udpor/Configuration.hpp"
+#include "src/mc/explo/udpor/History.hpp"
+
+#include <algorithm>
+#include <stdexcept>
+
+namespace simgrid::mc::udpor {
+
+Configuration::Configuration(std::initializer_list<UnfoldingEvent*> events) : Configuration(EventSet(std::move(events)))
+{
+}
+
+Configuration::Configuration(EventSet events) : events_(events)
+{
+ if (!events_.is_valid_configuration()) {
+ throw std::invalid_argument("The events do not form a valid configuration");
+ }
+}
+
+void Configuration::add_event(UnfoldingEvent* e)
+{
+ if (e == nullptr) {
+ throw std::invalid_argument("Expected a nonnull `UnfoldingEvent*` but received NULL instead");
+ }
+
+ if (this->events_.contains(e)) {
+ return;
+ }
+
+ this->events_.insert(e);
+ this->newest_event = e;
+
+ // Preserves the property that the configuration is valid
+ History history(e);
+ if (!this->events_.contains(history)) {
+ throw std::invalid_argument("The newly added event has dependencies "
+ "which are missing from this configuration");
+ }
+}
+
+} // namespace simgrid::mc::udpor
--- /dev/null
+/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#ifndef SIMGRID_MC_UDPOR_CONFIGURATION_HPP
+#define SIMGRID_MC_UDPOR_CONFIGURATION_HPP
+
+#include "src/mc/explo/udpor/EventSet.hpp"
+#include "src/mc/explo/udpor/udpor_forward.hpp"
+
+#include <initializer_list>
+
+namespace simgrid::mc::udpor {
+
+class Configuration {
+public:
+ Configuration() = default;
+ Configuration(const Configuration&) = default;
+ Configuration& operator=(Configuration const&) = default;
+ Configuration(Configuration&&) = default;
+
+ Configuration(EventSet events);
+ Configuration(std::initializer_list<UnfoldingEvent*> events);
+
+ auto begin() const { return this->events_.begin(); }
+ auto end() const { return this->events_.end(); }
+
+ bool contains(UnfoldingEvent* e) const { return this->events_.contains(e); }
+ const EventSet& get_events() const { return this->events_; }
+ UnfoldingEvent* get_latest_event() const { return this->newest_event; }
+
+ /**
+ * @brief Insert a new event into the configuration
+ *
+ * When the newly added event is inserted into the configuration,
+ * an assertion is made to ensure that the configuration remains
+ * valid, i.e. that the newly added event's dependencies are contained
+ * within the configuration.
+ *
+ * @param e the event to add to the configuration. If the event is
+ * already a part of the configuration, calling this method has no
+ * effect.
+ *
+ * @throws an invalid argument exception is raised should the event
+ * be missing one of its dependencies
+ *
+ * @note: UDPOR technically enforces the invariant that all newly-added events
+ * will ensure that the configuration is valid. We perform extra checks to ensure
+ * that UDPOR is implemented as expected. There is a performance penalty that
+ * should be noted: checking for maximality requires ensuring that all events in the
+ * configuration have their dependencies containes within the configuration, which
+ * essentially means performing a BFS/DFS over the configuration using a History object.
+ * However, since the slowest part of UDPOR involves enumerating all
+ * subsets of maximal events and computing k-partial alternatives (the
+ * latter definitively an NP-hard problem when optimal), Amdahl's law suggests
+ * we shouldn't focus so much on this (let alone the additional benefit of the
+ * assertions)
+ */
+ void add_event(UnfoldingEvent* e);
+
+private:
+ /**
+ * @brief The most recent event added to the configuration
+ */
+ UnfoldingEvent* newest_event = nullptr;
+
+ /**
+ * @brief The events which make up this configuration
+ *
+ * @invariant For each event `e` in `events_`, the set of
+ * dependencies of `e` is also contained in `events_`
+ */
+ EventSet events_;
+};
+
+} // namespace simgrid::mc::udpor
+#endif
--- /dev/null
+/* Copyright (c) 2017-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "src/3rd-party/catch.hpp"
+#include "src/mc/explo/udpor/Configuration.hpp"
+#include "src/mc/explo/udpor/EventSet.hpp"
+#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
+
+using namespace simgrid::mc::udpor;
+
+TEST_CASE("simgrid::mc::udpor::Configuration: Constructing Configurations")
+{
+ // The following tests concern the given event structure:
+ // e1
+ // /
+ // e2
+ // /
+ // e3
+ // / /
+ // e4 e5
+ UnfoldingEvent e1;
+ UnfoldingEvent e2{&e1};
+ UnfoldingEvent e3{&e2};
+ UnfoldingEvent e4{&e3}, e5{&e3};
+
+ SECTION("Creating a configuration without events")
+ {
+ Configuration C;
+ REQUIRE(C.get_events().empty());
+ REQUIRE(C.get_latest_event() == nullptr);
+ }
+
+ SECTION("Creating a configuration with events")
+ {
+ // 5 choose 0 = 1 test
+ REQUIRE_NOTHROW(Configuration({&e1}));
+
+ // 5 choose 1 = 5 tests
+ REQUIRE_THROWS_AS(Configuration({&e2}), std::invalid_argument);
+ REQUIRE_THROWS_AS(Configuration({&e3}), std::invalid_argument);
+ REQUIRE_THROWS_AS(Configuration({&e4}), std::invalid_argument);
+ REQUIRE_THROWS_AS(Configuration({&e5}), std::invalid_argument);
+
+ // 5 choose 2 = 10 tests
+ REQUIRE_NOTHROW(Configuration({&e1, &e2}));
+ REQUIRE_THROWS_AS(Configuration({&e1, &e3}), std::invalid_argument);
+ REQUIRE_THROWS_AS(Configuration({&e1, &e4}), std::invalid_argument);
+ REQUIRE_THROWS_AS(Configuration({&e1, &e5}), std::invalid_argument);
+ REQUIRE_THROWS_AS(Configuration({&e2, &e3}), std::invalid_argument);
+ REQUIRE_THROWS_AS(Configuration({&e2, &e4}), std::invalid_argument);
+ REQUIRE_THROWS_AS(Configuration({&e2, &e5}), std::invalid_argument);
+ REQUIRE_THROWS_AS(Configuration({&e3, &e4}), std::invalid_argument);
+ REQUIRE_THROWS_AS(Configuration({&e3, &e5}), std::invalid_argument);
+ REQUIRE_THROWS_AS(Configuration({&e4, &e5}), std::invalid_argument);
+
+ // 5 choose 3 = 10 tests
+ REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3}));
+ REQUIRE_THROWS_AS(Configuration({&e1, &e2, &e4}), std::invalid_argument);
+ REQUIRE_THROWS_AS(Configuration({&e1, &e2, &e5}), std::invalid_argument);
+ REQUIRE_THROWS_AS(Configuration({&e1, &e3, &e4}), std::invalid_argument);
+ REQUIRE_THROWS_AS(Configuration({&e1, &e3, &e5}), std::invalid_argument);
+ REQUIRE_THROWS_AS(Configuration({&e1, &e4, &e5}), std::invalid_argument);
+ REQUIRE_THROWS_AS(Configuration({&e2, &e3, &e4}), std::invalid_argument);
+ REQUIRE_THROWS_AS(Configuration({&e2, &e3, &e5}), std::invalid_argument);
+ REQUIRE_THROWS_AS(Configuration({&e2, &e4, &e5}), std::invalid_argument);
+ REQUIRE_THROWS_AS(Configuration({&e3, &e4, &e5}), std::invalid_argument);
+
+ // 5 choose 4 = 5 tests
+ REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3, &e4}));
+ REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3, &e5}));
+ REQUIRE_THROWS_AS(Configuration({&e1, &e2, &e4, &e5}), std::invalid_argument);
+ REQUIRE_THROWS_AS(Configuration({&e1, &e3, &e4, &e5}), std::invalid_argument);
+ REQUIRE_THROWS_AS(Configuration({&e2, &e3, &e4, &e5}), std::invalid_argument);
+
+ // 5 choose 5 = 1 test
+ REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3, &e4, &e5}));
+ }
+}
+
+TEST_CASE("simgrid::mc::udpor::Configuration: Adding Events")
+{
+ // The following tests concern the given event structure:
+ // e1
+ // /
+ // e2
+ // /
+ // / /
+ // e3 e4
+ UnfoldingEvent e1;
+ UnfoldingEvent e2{&e1};
+ UnfoldingEvent e3{&e2};
+ UnfoldingEvent e4{&e2};
+
+ REQUIRE_THROWS_AS(Configuration().add_event(nullptr), std::invalid_argument);
+ REQUIRE_THROWS_AS(Configuration().add_event(&e2), std::invalid_argument);
+ REQUIRE_THROWS_AS(Configuration().add_event(&e3), std::invalid_argument);
+ REQUIRE_THROWS_AS(Configuration().add_event(&e4), std::invalid_argument);
+ REQUIRE_THROWS_AS(Configuration({&e1}).add_event(&e3), std::invalid_argument);
+ REQUIRE_THROWS_AS(Configuration({&e1}).add_event(&e4), std::invalid_argument);
+
+ REQUIRE_NOTHROW(Configuration().add_event(&e1));
+ REQUIRE_NOTHROW(Configuration({&e1}).add_event(&e1));
+ REQUIRE_NOTHROW(Configuration({&e1}).add_event(&e2));
+ REQUIRE_NOTHROW(Configuration({&e1, &e2}).add_event(&e1));
+ REQUIRE_NOTHROW(Configuration({&e1, &e2}).add_event(&e2));
+ REQUIRE_NOTHROW(Configuration({&e1, &e2}).add_event(&e3));
+ REQUIRE_NOTHROW(Configuration({&e1, &e2}).add_event(&e4));
+ REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3}).add_event(&e1));
+ REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3}).add_event(&e2));
+ REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3}).add_event(&e3));
+ REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3}).add_event(&e4));
+ REQUIRE_NOTHROW(Configuration({&e1, &e2, &e4}).add_event(&e1));
+ REQUIRE_NOTHROW(Configuration({&e1, &e2, &e4}).add_event(&e2));
+ REQUIRE_NOTHROW(Configuration({&e1, &e2, &e4}).add_event(&e3));
+ REQUIRE_NOTHROW(Configuration({&e1, &e2, &e4}).add_event(&e4));
+ REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3, &e4}).add_event(&e1));
+ REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3, &e4}).add_event(&e2));
+ REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3, &e4}).add_event(&e3));
+ REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3, &e4}).add_event(&e4));
+}
--- /dev/null
+/* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "src/mc/explo/udpor/EventSet.hpp"
+#include "src/mc/explo/udpor/Configuration.hpp"
+#include "src/mc/explo/udpor/History.hpp"
+
+#include <iterator>
+
+namespace simgrid::mc::udpor {
+
+EventSet::EventSet(Configuration&& config) : EventSet(std::move(config.get_events())) {}
+
+void EventSet::remove(UnfoldingEvent* e)
+{
+ this->events_.erase(e);
+}
+
+void EventSet::subtract(const EventSet& other)
+{
+ this->events_ = std::move(subtracting(other).events_);
+}
+
+void EventSet::subtract(const Configuration& config)
+{
+ subtract(config.get_events());
+}
+
+EventSet EventSet::subtracting(const EventSet& other) const
+{
+ std::unordered_set<UnfoldingEvent*> result = this->events_;
+
+ for (UnfoldingEvent* e : other.events_)
+ result.erase(e);
+
+ return EventSet(std::move(result));
+}
+
+EventSet EventSet::subtracting(const Configuration& config) const
+{
+ return subtracting(config.get_events());
+}
+
+EventSet EventSet::subtracting(UnfoldingEvent* e) const
+{
+ auto result = this->events_;
+ result.erase(e);
+ return EventSet(std::move(result));
+}
+
+void EventSet::insert(UnfoldingEvent* e)
+{
+ this->events_.insert(e);
+}
+
+void EventSet::form_union(const EventSet& other)
+{
+ this->events_ = std::move(make_union(other).events_);
+}
+
+void EventSet::form_union(const Configuration& config)
+{
+ form_union(config.get_events());
+}
+
+EventSet EventSet::make_union(UnfoldingEvent* e) const
+{
+ auto result = this->events_;
+ result.insert(e);
+ return EventSet(std::move(result));
+}
+
+EventSet EventSet::make_union(const EventSet& other) const
+{
+ std::unordered_set<UnfoldingEvent*> result = this->events_;
+
+ for (UnfoldingEvent* e : other.events_)
+ result.insert(e);
+
+ return EventSet(std::move(result));
+}
+
+EventSet EventSet::make_union(const Configuration& config) const
+{
+ return make_union(config.get_events());
+}
+
+size_t EventSet::size() const
+{
+ return this->events_.size();
+}
+
+bool EventSet::empty() const
+{
+ return this->events_.empty();
+}
+
+bool EventSet::contains(UnfoldingEvent* e) const
+{
+ return this->events_.find(e) != this->events_.end();
+}
+
+bool EventSet::is_subset_of(const EventSet& other) const
+{
+ // If there is some element not contained in `other`, then
+ // the set difference will contain that element and the
+ // result won't be empty
+ return subtracting(other).empty();
+}
+
+bool EventSet::is_valid_configuration() const
+{
+ /// @invariant: A collection of events `E` is a configuration
+ /// if and only if following while following the history of
+ /// each event `e` of `E`you remain in `E`. In other words, you
+ /// only see events from set `E`
+ ///
+ /// The proof is based on the definition of a configuration
+ /// which requires that all
+ const History history(*this);
+ return this->contains(history);
+}
+
+bool EventSet::contains(const History& history) const
+{
+ return std::all_of(history.begin(), history.end(), [=](UnfoldingEvent* e) { return this->contains(e); });
+}
+
+bool EventSet::is_maximal_event_set() const
+{
+ const History history(*this);
+ return *this == history.get_all_maximal_events();
+}
+
+} // namespace simgrid::mc::udpor
\ No newline at end of file
--- /dev/null
+/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#ifndef SIMGRID_MC_UDPOR_EVENT_SET_HPP
+#define SIMGRID_MC_UDPOR_EVENT_SET_HPP
+
+#include "src/mc/explo/udpor/udpor_forward.hpp"
+
+#include <cstddef>
+#include <initializer_list>
+#include <unordered_set>
+
+namespace simgrid::mc::udpor {
+
+class EventSet {
+private:
+ std::unordered_set<UnfoldingEvent*> events_;
+
+public:
+ EventSet() = default;
+ EventSet(const EventSet&) = default;
+ EventSet& operator=(const EventSet&) = default;
+ EventSet& operator=(EventSet&&) = default;
+ EventSet(EventSet&&) = default;
+ explicit EventSet(Configuration&& config);
+ explicit EventSet(std::unordered_set<UnfoldingEvent*>&& raw_events) : events_(raw_events) {}
+ explicit EventSet(std::initializer_list<UnfoldingEvent*> event_list) : events_(std::move(event_list)) {}
+
+ auto begin() const { return this->events_.begin(); }
+ auto end() const { return this->events_.end(); }
+ auto cbegin() const { return this->events_.cbegin(); }
+ auto cend() const { return this->events_.cend(); }
+
+ void remove(UnfoldingEvent*);
+ void subtract(const EventSet&);
+ void subtract(const Configuration&);
+ EventSet subtracting(UnfoldingEvent*) const;
+ EventSet subtracting(const EventSet&) const;
+ EventSet subtracting(const Configuration&) const;
+
+ void insert(UnfoldingEvent*);
+ void form_union(const EventSet&);
+ void form_union(const Configuration&);
+ EventSet make_union(UnfoldingEvent*) const;
+ EventSet make_union(const EventSet&) const;
+ EventSet make_union(const Configuration&) const;
+
+ size_t size() const;
+ bool empty() const;
+ bool contains(UnfoldingEvent*) const;
+ bool contains(const History&) const;
+ bool is_subset_of(const EventSet&) const;
+
+ bool operator==(const EventSet& other) const { return this->events_ == other.events_; }
+ bool operator!=(const EventSet& other) const { return this->events_ != other.events_; }
+
+public:
+ /**
+ * @brief Whether or not this set of events could
+ * represent a configuration
+ */
+ bool is_valid_configuration() const;
+
+ /**
+ * @brief Whether or not this set of events is
+ * a *maximal event set*, i.e. whether each element
+ * of the set causes none of the others
+ */
+ bool is_maximal_event_set() const;
+};
+
+} // namespace simgrid::mc::udpor
+#endif
--- /dev/null
+/* Copyright (c) 2017-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "src/3rd-party/catch.hpp"
+#include "src/mc/explo/udpor/EventSet.hpp"
+#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
+
+using namespace simgrid::mc::udpor;
+
+TEST_CASE("simgrid::mc::udpor::EventSet: Initial conditions when creating sets")
+{
+ SECTION("Initialization with no elements")
+ {
+ SECTION("Default initializer")
+ {
+ EventSet event_set;
+ REQUIRE(event_set.size() == 0);
+ REQUIRE(event_set.empty());
+ }
+
+ SECTION("Set initializer")
+ {
+ EventSet event_set({});
+ REQUIRE(event_set.size() == 0);
+ REQUIRE(event_set.empty());
+ }
+
+ SECTION("List initialization")
+ {
+ EventSet event_set{};
+ REQUIRE(event_set.size() == 0);
+ REQUIRE(event_set.empty());
+ }
+ }
+
+ SECTION("Initialization with one or more elements")
+ {
+ UnfoldingEvent e1, e2, e3;
+
+ SECTION("Set initializer")
+ {
+ EventSet event_set({&e1, &e2, &e3});
+ REQUIRE(event_set.size() == 3);
+ REQUIRE(event_set.contains(&e1));
+ REQUIRE(event_set.contains(&e2));
+ REQUIRE(event_set.contains(&e3));
+ REQUIRE_FALSE(event_set.empty());
+ }
+
+ SECTION("List initialization")
+ {
+ UnfoldingEvent e1, e2, e3;
+ EventSet event_set{&e1, &e2, &e3};
+ REQUIRE(event_set.size() == 3);
+ REQUIRE(event_set.contains(&e1));
+ REQUIRE(event_set.contains(&e2));
+ REQUIRE(event_set.contains(&e3));
+ REQUIRE_FALSE(event_set.empty());
+ }
+ }
+}
+
+TEST_CASE("simgrid::mc::udpor::EventSet: Insertions")
+{
+ EventSet event_set;
+ UnfoldingEvent e1, e2, e3;
+
+ SECTION("Inserting unique elements")
+ {
+ event_set.insert(&e1);
+ REQUIRE(event_set.size() == 1);
+ REQUIRE(event_set.contains(&e1));
+ REQUIRE_FALSE(event_set.empty());
+
+ event_set.insert(&e2);
+ REQUIRE(event_set.size() == 2);
+ REQUIRE(event_set.contains(&e2));
+ REQUIRE_FALSE(event_set.empty());
+
+ SECTION("Check contains inserted elements")
+ {
+ REQUIRE(event_set.contains(&e1));
+ REQUIRE(event_set.contains(&e2));
+ REQUIRE_FALSE(event_set.contains(&e3));
+ }
+ }
+
+ SECTION("Inserting duplicate elements")
+ {
+ event_set.insert(&e1);
+ REQUIRE(event_set.size() == 1);
+ REQUIRE(event_set.contains(&e1));
+ REQUIRE_FALSE(event_set.empty());
+
+ event_set.insert(&e1);
+ REQUIRE(event_set.size() == 1);
+ REQUIRE(event_set.contains(&e1));
+ REQUIRE_FALSE(event_set.empty());
+
+ SECTION("Check contains inserted elements")
+ {
+ REQUIRE(event_set.contains(&e1));
+ REQUIRE_FALSE(event_set.contains(&e2));
+ REQUIRE_FALSE(event_set.contains(&e3));
+ }
+ }
+}
+
+TEST_CASE("simgrid::mc::udpor::EventSet: Deletions")
+{
+ UnfoldingEvent e1, e2, e3, e4;
+ EventSet event_set({&e1, &e2, &e3});
+
+ SECTION("Remove an element already present")
+ {
+ REQUIRE(event_set.contains(&e1));
+
+ // event_set = {e2, e3}
+ event_set.remove(&e1);
+
+ // Check that
+ // 1. the size decreases by exactly 1
+ // 2. the set remains unempty
+ // 3. the other elements are still contained in the set
+ REQUIRE(event_set.size() == 2);
+ REQUIRE_FALSE(event_set.contains(&e1));
+ REQUIRE(event_set.contains(&e2));
+ REQUIRE(event_set.contains(&e3));
+ REQUIRE_FALSE(event_set.empty());
+
+ SECTION("Remove a single element more than once")
+ {
+ // event_set = {e2, e3}
+ event_set.remove(&e1);
+ REQUIRE(event_set.size() == 2);
+ REQUIRE_FALSE(event_set.contains(&e1));
+ REQUIRE(event_set.contains(&e2));
+ REQUIRE(event_set.contains(&e3));
+ REQUIRE_FALSE(event_set.empty());
+ }
+
+ SECTION("Remove more than one element")
+ {
+ // event_set = {e3}
+ event_set.remove(&e2);
+
+ REQUIRE(event_set.size() == 1);
+ REQUIRE_FALSE(event_set.contains(&e1));
+ REQUIRE_FALSE(event_set.contains(&e2));
+ REQUIRE(event_set.contains(&e3));
+ REQUIRE_FALSE(event_set.empty());
+
+ // event_set = {}
+ event_set.remove(&e3);
+
+ REQUIRE(event_set.size() == 0);
+ REQUIRE_FALSE(event_set.contains(&e1));
+ REQUIRE_FALSE(event_set.contains(&e2));
+ REQUIRE_FALSE(event_set.contains(&e3));
+ REQUIRE(event_set.empty());
+ }
+ }
+
+ SECTION("Remove an element absent from the set")
+ {
+ REQUIRE_FALSE(event_set.contains(&e4));
+
+ // event_set = {e1, e2, e3}
+ event_set.remove(&e4);
+ REQUIRE(event_set.size() == 3);
+ REQUIRE(event_set.contains(&e1));
+ REQUIRE(event_set.contains(&e2));
+ REQUIRE(event_set.contains(&e3));
+
+ // Ensure e4 isn't somehow added
+ REQUIRE_FALSE(event_set.contains(&e4));
+ REQUIRE_FALSE(event_set.empty());
+ }
+}
+
+TEST_CASE("simgrid::mc::udpor::EventSet: Set Equality")
+{
+ UnfoldingEvent e1, e2, e3, e4;
+ EventSet A{&e1, &e2, &e3}, B{&e1, &e2, &e3}, C{&e1, &e2, &e3};
+
+ SECTION("Equality implies containment")
+ {
+ REQUIRE(A == B);
+
+ for (const auto& e : A) {
+ REQUIRE(B.contains(e));
+ }
+
+ for (const auto& e : B) {
+ REQUIRE(A.contains(e));
+ }
+ }
+
+ SECTION("Containment implies equality")
+ {
+ for (const auto& e : A) {
+ REQUIRE(B.contains(e));
+ }
+
+ for (const auto& e : C) {
+ REQUIRE(C.contains(e));
+ }
+
+ REQUIRE(A == C);
+ }
+
+ SECTION("Equality is an equivalence relation")
+ {
+ // Reflexive
+ REQUIRE(A == A);
+ REQUIRE(B == B);
+ REQUIRE(C == C);
+
+ // Symmetric
+ REQUIRE(A == B);
+ REQUIRE(B == A);
+ REQUIRE(A == C);
+ REQUIRE(C == A);
+ REQUIRE(B == C);
+ REQUIRE(C == B);
+
+ // Transitive
+ REQUIRE(A == B);
+ REQUIRE(B == C);
+ REQUIRE(A == C);
+ }
+
+ SECTION("Equality after copy (assignment + constructor)")
+ {
+ EventSet A_copy = A;
+ EventSet A_copy2(A);
+
+ REQUIRE(A == A_copy);
+ REQUIRE(A == A_copy2);
+ }
+
+ SECTION("Equality after move constructor")
+ {
+ EventSet A_copy = A;
+ EventSet A_move(std::move(A));
+ REQUIRE(A_move == A_copy);
+ }
+
+ SECTION("Equality after move-assignment")
+ {
+ EventSet A_copy = A;
+ EventSet A_move = std::move(A);
+ REQUIRE(A_move == A_copy);
+ }
+}
+
+TEST_CASE("simgrid::mc::udpor::EventSet: Set Union Tests")
+{
+ UnfoldingEvent e1, e2, e3, e4;
+
+ // C = A + B
+ EventSet A{&e1, &e2, &e3}, B{&e2, &e3, &e4}, C{&e1, &e2, &e3, &e4}, D{&e1, &e3};
+
+ SECTION("Unions with no effect")
+ {
+ EventSet A_copy = A;
+
+ SECTION("Self union")
+ {
+ // A = A union A
+ EventSet A_union = A.make_union(A);
+ REQUIRE(A == A_copy);
+
+ A.form_union(A);
+ REQUIRE(A == A_copy);
+ }
+
+ SECTION("Union with empty set")
+ {
+ // A = A union empty set
+ EventSet A_union = A.make_union(EventSet());
+ REQUIRE(A == A_union);
+
+ A.form_union(EventSet());
+ REQUIRE(A == A_copy);
+ }
+
+ SECTION("Union with an equivalent set")
+ {
+ // A = A union B if B == A
+ EventSet A_equiv{&e1, &e2, &e3};
+ REQUIRE(A == A_equiv);
+
+ EventSet A_union = A.make_union(A_equiv);
+ REQUIRE(A_union == A_copy);
+
+ A.form_union(A_equiv);
+ REQUIRE(A == A_copy);
+ }
+
+ SECTION("Union with a subset")
+ {
+ // A = A union D if D is a subset of A
+ EventSet A_union = A.make_union(D);
+ REQUIRE(A == A_union);
+
+ A.form_union(D);
+ REQUIRE(A == A_copy);
+ }
+ }
+
+ SECTION("Unions with partial overlaps")
+ {
+ EventSet A_union_B = A.make_union(B);
+ REQUIRE(A_union_B == C);
+
+ A.form_union(B);
+ REQUIRE(A == C);
+
+ EventSet B_union_D = B.make_union(D);
+ REQUIRE(B_union_D == C);
+
+ B.form_union(D);
+ REQUIRE(B == C);
+ }
+
+ SECTION("Set union properties")
+ {
+ SECTION("Union operator is symmetric")
+ {
+ EventSet A_union_B = A.make_union(B);
+ EventSet B_union_A = B.make_union(A);
+ REQUIRE(A_union_B == B_union_A);
+ }
+
+ SECTION("Union operator commutes")
+ {
+ // The last SECTION tested pair-wise
+ // equivalence, so we only check
+ // one of each pai
+ EventSet AD = A.make_union(D);
+ EventSet AC = A.make_union(C);
+ EventSet CD = D.make_union(C);
+
+ EventSet ADC = AD.make_union(C);
+ EventSet ACD = AC.make_union(D);
+ EventSet CDA = CD.make_union(A);
+
+ REQUIRE(ADC == ACD);
+ REQUIRE(ACD == CDA);
+
+ // Test `form_union()` in the same way
+
+ EventSet A_copy = A;
+ EventSet C_copy = C;
+ EventSet D_copy = D;
+
+ A.form_union(C_copy);
+ A.form_union(D_copy);
+
+ D.form_union(A_copy);
+ D.form_union(C_copy);
+
+ C.form_union(A);
+ C.form_union(D);
+
+ REQUIRE(A == D);
+ REQUIRE(C == D);
+ REQUIRE(A == C);
+ }
+ }
+}
+
+TEST_CASE("simgrid::mc::udpor::EventSet: Set Difference Tests")
+{
+ UnfoldingEvent e1, e2, e3, e4;
+
+ // C = A + B
+ // A is a subset of C
+ // B is a subset of C
+ // D is a subset of A and C
+ // E is a subset of B and C
+ // F is a subset of A, C, and D
+ EventSet A{&e1, &e2, &e3}, B{&e2, &e3, &e4}, C{&e1, &e2, &e3, &e4}, D{&e1, &e3}, E{&e4}, F{&e1};
+
+ SECTION("Difference with no effect")
+ {
+ SECTION("Difference with empty set")
+ {
+ EventSet A_copy = A.subtracting(EventSet());
+ REQUIRE(A == A_copy);
+
+ A.subtract(EventSet());
+ REQUIRE(A == A_copy);
+ }
+
+ SECTION("Difference with empty intersection")
+ {
+ // A intersection E = empty set
+ EventSet A_copy = A.subtracting(E);
+ REQUIRE(A == A_copy);
+
+ A.subtract(E);
+ REQUIRE(A == A_copy);
+
+ EventSet D_copy = D.subtracting(E);
+ REQUIRE(D == D_copy);
+
+ D.subtract(E);
+ REQUIRE(D == D_copy);
+ }
+ }
+
+ SECTION("Difference with some overlap")
+ {
+ // A - B = {&e1} = F
+ EventSet A_minus_B = A.subtracting(B);
+ REQUIRE(A_minus_B == F);
+
+ // B - D = {&e2, &e4}
+ EventSet B_minus_D = B.subtracting(D);
+ REQUIRE(B_minus_D == EventSet({&e2, &e4}));
+ }
+
+ SECTION("Difference with complete overlap")
+ {
+ SECTION("Difference with same set gives empty set")
+ {
+ REQUIRE(A.subtracting(A) == EventSet());
+ REQUIRE(B.subtracting(B) == EventSet());
+ REQUIRE(C.subtracting(C) == EventSet());
+ REQUIRE(D.subtracting(D) == EventSet());
+ REQUIRE(E.subtracting(E) == EventSet());
+ REQUIRE(F.subtracting(F) == EventSet());
+ }
+
+ SECTION("Difference with superset gives empty set")
+ {
+ REQUIRE(A.subtracting(C) == EventSet());
+ REQUIRE(B.subtracting(C) == EventSet());
+ REQUIRE(D.subtracting(A) == EventSet());
+ REQUIRE(D.subtracting(C) == EventSet());
+ REQUIRE(E.subtracting(B) == EventSet());
+ REQUIRE(E.subtracting(C) == EventSet());
+ REQUIRE(F.subtracting(A) == EventSet());
+ REQUIRE(F.subtracting(C) == EventSet());
+ REQUIRE(F.subtracting(D) == EventSet());
+ }
+ }
+}
+
+TEST_CASE("simgrid::mc::udpor::EventSet: Subset Tests")
+{
+ UnfoldingEvent e1, e2, e3, e4;
+
+ // A is a subset of C only
+ // B is a subset of C only
+ // D is a subset of C and A
+ // D is NOT a subset of B
+ // B is NOT a subset of D
+ // ...
+ EventSet A{&e1, &e2, &e3}, B{&e2, &e3, &e4}, C{&e1, &e2, &e3, &e4}, D{&e1, &e3}, E{&e2, &e3}, F{&e1, &e2, &e3};
+
+ SECTION("Subset operator properties")
+ {
+ SECTION("Subset operator is not commutative")
+ {
+ REQUIRE(A.is_subset_of(C));
+ REQUIRE_FALSE(C.is_subset_of(A));
+
+ SECTION("Commutativity implies equality and vice versa")
+ {
+ REQUIRE(A.is_subset_of(F));
+ REQUIRE(F.is_subset_of(A));
+ REQUIRE(A == F);
+
+ REQUIRE(C == C);
+ REQUIRE(A.is_subset_of(F));
+ REQUIRE(F.is_subset_of(A));
+ }
+ }
+
+ SECTION("Subset operator is transitive")
+ {
+ REQUIRE(D.is_subset_of(A));
+ REQUIRE(A.is_subset_of(C));
+ REQUIRE(D.is_subset_of(C));
+ REQUIRE(E.is_subset_of(B));
+ REQUIRE(B.is_subset_of(C));
+ REQUIRE(E.is_subset_of(C));
+ }
+
+ SECTION("Subset operator is reflexive")
+ {
+ REQUIRE(A.is_subset_of(A));
+ REQUIRE(B.is_subset_of(B));
+ REQUIRE(C.is_subset_of(C));
+ REQUIRE(D.is_subset_of(D));
+ REQUIRE(E.is_subset_of(E));
+ REQUIRE(F.is_subset_of(F));
+ }
+ }
+}
+
+TEST_CASE("simgrid::mc::udpor::EventSet: Testing Configurations")
+{
+ // The following tests concern the given event structure:
+ // e1
+ // / /
+ // e2 e5
+ // / / /
+ // e3 e4 e6
+ // The tests enumerate all possible subsets of the events
+ // in the structure and test whether those subsets are
+ // maximal and/or valid configurations
+ UnfoldingEvent e1;
+ UnfoldingEvent e2{&e1}, e5{&e1};
+ UnfoldingEvent e3{&e2}, e4{&e2};
+ UnfoldingEvent e6{&e5};
+
+ SECTION("Valid Configurations")
+ {
+ SECTION("The empty set is valid")
+ {
+ REQUIRE(EventSet().is_valid_configuration());
+ }
+
+ SECTION("The set with only the root event is valid")
+ {
+ REQUIRE(EventSet({&e1}).is_valid_configuration());
+ }
+
+ SECTION("All sets of maximal events are valid configurations")
+ {
+ REQUIRE(EventSet({&e1}).is_valid_configuration());
+ REQUIRE(EventSet({&e1, &e2}).is_valid_configuration());
+ REQUIRE(EventSet({&e1, &e2, &e3}).is_valid_configuration());
+ REQUIRE(EventSet({&e1, &e2, &e4}).is_valid_configuration());
+ REQUIRE(EventSet({&e1, &e5}).is_valid_configuration());
+ REQUIRE(EventSet({&e1, &e5, &e6}).is_valid_configuration());
+ REQUIRE(EventSet({&e1, &e2, &e5}).is_valid_configuration());
+ REQUIRE(EventSet({&e1, &e2, &e5, &e6}).is_valid_configuration());
+ REQUIRE(EventSet({&e1, &e2, &e3, &e4}).is_valid_configuration());
+ REQUIRE(EventSet({&e1, &e2, &e3, &e5}).is_valid_configuration());
+ REQUIRE(EventSet({&e1, &e2, &e4, &e5}).is_valid_configuration());
+ REQUIRE(EventSet({&e1, &e2, &e4, &e5, &e6}).is_valid_configuration());
+ REQUIRE(EventSet({&e1, &e2, &e3, &e4, &e5}).is_valid_configuration());
+ REQUIRE(EventSet({&e1, &e2, &e3, &e4, &e5, &e6}).is_valid_configuration());
+ }
+ }
+
+ SECTION("Configuration checks")
+ {
+ // 6 choose 0 = 1 test
+ REQUIRE(EventSet().is_valid_configuration());
+
+ // 6 choose 1 = 6 tests
+ REQUIRE(EventSet({&e1}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e2}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e3}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e4}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e5}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e6}).is_valid_configuration());
+
+ // 6 choose 2 = 15 tests
+ REQUIRE(EventSet({&e1, &e2}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e1, &e3}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e1, &e4}).is_valid_configuration());
+ REQUIRE(EventSet({&e1, &e5}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e1, &e6}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e2, &e3}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e2, &e4}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e2, &e5}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e2, &e6}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e3, &e4}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e3, &e5}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e3, &e6}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e4, &e5}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e4, &e6}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e5, &e6}).is_valid_configuration());
+
+ // 6 choose 3 = 20 tests
+ REQUIRE(EventSet({&e1, &e2, &e3}).is_valid_configuration());
+ REQUIRE(EventSet({&e1, &e2, &e4}).is_valid_configuration());
+ REQUIRE(EventSet({&e1, &e2, &e5}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e1, &e2, &e6}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e1, &e3, &e4}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e1, &e3, &e5}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e1, &e3, &e6}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e1, &e4, &e5}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e1, &e4, &e6}).is_valid_configuration());
+ REQUIRE(EventSet({&e1, &e5, &e6}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e2, &e3, &e4}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e2, &e3, &e5}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e2, &e3, &e6}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e2, &e4, &e5}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e2, &e4, &e6}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e2, &e5, &e6}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e3, &e4, &e5}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e3, &e4, &e6}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e3, &e5, &e6}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e4, &e5, &e6}).is_valid_configuration());
+
+ // 6 choose 4 = 15 tests
+ REQUIRE(EventSet({&e1, &e2, &e3, &e4}).is_valid_configuration());
+ REQUIRE(EventSet({&e1, &e2, &e3, &e5}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e1, &e2, &e3, &e6}).is_valid_configuration());
+ REQUIRE(EventSet({&e1, &e2, &e4, &e5}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e1, &e2, &e4, &e6}).is_valid_configuration());
+ REQUIRE(EventSet({&e1, &e2, &e5, &e6}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e1, &e3, &e4, &e5}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e1, &e3, &e4, &e6}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e1, &e3, &e5, &e6}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e1, &e4, &e5, &e6}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e2, &e3, &e4, &e5}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e2, &e3, &e4, &e6}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e2, &e3, &e5, &e6}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e2, &e4, &e5, &e6}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e3, &e4, &e5, &e6}).is_valid_configuration());
+
+ // 6 choose 5 = 6 tests
+ REQUIRE(EventSet({&e1, &e2, &e3, &e4, &e5}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e1, &e2, &e3, &e4, &e6}).is_valid_configuration());
+ REQUIRE(EventSet({&e1, &e2, &e3, &e5, &e6}).is_valid_configuration());
+ REQUIRE(EventSet({&e1, &e2, &e4, &e5, &e6}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e1, &e3, &e4, &e5, &e6}).is_valid_configuration());
+ REQUIRE_FALSE(EventSet({&e2, &e3, &e4, &e5, &e6}).is_valid_configuration());
+
+ // 6 choose 6 = 1 test
+ REQUIRE(EventSet({&e1, &e2, &e3, &e4, &e5, &e6}).is_valid_configuration());
+ }
+
+ SECTION("Maximal event sets")
+ {
+ // 6 choose 0 = 1 test
+ REQUIRE(EventSet().is_maximal_event_set());
+
+ // 6 choose 1 = 6 tests
+ REQUIRE(EventSet({&e1}).is_maximal_event_set());
+ REQUIRE(EventSet({&e2}).is_maximal_event_set());
+ REQUIRE(EventSet({&e3}).is_maximal_event_set());
+ REQUIRE(EventSet({&e4}).is_maximal_event_set());
+ REQUIRE(EventSet({&e5}).is_maximal_event_set());
+ REQUIRE(EventSet({&e6}).is_maximal_event_set());
+
+ // 6 choose 2 = 15 tests
+ REQUIRE_FALSE(EventSet({&e1, &e2}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e1, &e3}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e1, &e4}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e1, &e5}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e1, &e6}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e2, &e3}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e2, &e4}).is_maximal_event_set());
+ REQUIRE(EventSet({&e2, &e5}).is_maximal_event_set());
+ REQUIRE(EventSet({&e2, &e6}).is_maximal_event_set());
+ REQUIRE(EventSet({&e3, &e4}).is_maximal_event_set());
+ REQUIRE(EventSet({&e3, &e5}).is_maximal_event_set());
+ REQUIRE(EventSet({&e3, &e6}).is_maximal_event_set());
+ REQUIRE(EventSet({&e4, &e5}).is_maximal_event_set());
+ REQUIRE(EventSet({&e4, &e6}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e5, &e6}).is_maximal_event_set());
+
+ // 6 choose 3 = 20 tests
+ REQUIRE_FALSE(EventSet({&e1, &e2, &e3}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e1, &e2, &e4}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e1, &e2, &e5}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e1, &e2, &e6}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e1, &e3, &e4}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e1, &e3, &e5}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e1, &e3, &e6}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e1, &e4, &e5}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e1, &e4, &e6}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e1, &e5, &e6}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e2, &e3, &e4}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e2, &e3, &e5}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e2, &e3, &e6}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e2, &e4, &e5}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e2, &e4, &e6}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e2, &e5, &e6}).is_maximal_event_set());
+ REQUIRE(EventSet({&e3, &e4, &e5}).is_maximal_event_set());
+ REQUIRE(EventSet({&e3, &e4, &e6}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e3, &e5, &e6}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e4, &e5, &e6}).is_maximal_event_set());
+
+ // 6 choose 4 = 15 tests
+ REQUIRE_FALSE(EventSet({&e1, &e2, &e3, &e4}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e1, &e2, &e3, &e5}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e1, &e2, &e3, &e6}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e1, &e2, &e4, &e5}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e1, &e2, &e4, &e6}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e1, &e2, &e5, &e6}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e1, &e3, &e4, &e5}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e1, &e3, &e4, &e6}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e1, &e3, &e5, &e6}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e1, &e4, &e5, &e6}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e2, &e3, &e4, &e5}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e2, &e3, &e4, &e6}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e2, &e3, &e5, &e6}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e2, &e4, &e5, &e6}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e3, &e4, &e5, &e6}).is_maximal_event_set());
+
+ // 6 choose 5 = 6 tests
+ REQUIRE_FALSE(EventSet({&e1, &e2, &e3, &e4, &e5}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e1, &e2, &e3, &e4, &e6}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e1, &e2, &e3, &e5, &e6}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e1, &e2, &e4, &e5, &e6}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e1, &e3, &e4, &e5, &e6}).is_maximal_event_set());
+ REQUIRE_FALSE(EventSet({&e2, &e3, &e4, &e5, &e6}).is_maximal_event_set());
+
+ // 6 choose 6 = 1 test
+ REQUIRE_FALSE(EventSet({&e1, &e2, &e3, &e4, &e5, &e6}).is_maximal_event_set());
+ }
+}
\ No newline at end of file
--- /dev/null
+/* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "src/mc/explo/udpor/History.hpp"
+#include "src/mc/explo/udpor/Configuration.hpp"
+#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
+
+#include <stack>
+
+namespace simgrid::mc::udpor {
+
+History::Iterator::Iterator(const EventSet& initial_events, optional_configuration config)
+ : frontier(initial_events), maximal_events(initial_events), configuration(config)
+{
+ // NOTE: Only events in the initial set of events can ever hope to have
+ // a chance at being a maximal event, since all other events in
+ // the search are generate by looking at dependencies of these events
+ // and all subsequent events that are added by the iterator
+}
+
+History::Iterator& History::Iterator::operator++()
+{
+ if (not frontier.empty()) {
+ // "Pop" the event at the "front"
+ UnfoldingEvent* e = *frontier.begin();
+ frontier.remove(e);
+
+ // If there is a configuration and if the
+ // event is in it, skip it: the event and
+ // all of its immediate causes do not need to
+ // be searched since the configuration contains
+ // them (configuration invariant)
+ if (configuration.has_value() && configuration->get().contains(e)) {
+ return *this;
+ }
+
+ // Mark this event as seen
+ current_history.insert(e);
+
+ // Perform the expansion with all viable expansions
+ EventSet candidates = e->get_immediate_causes();
+
+ maximal_events.subtract(candidates);
+
+ candidates.subtract(current_history);
+ frontier.form_union(std::move(candidates));
+ }
+ return *this;
+}
+
+EventSet History::get_all_events() const
+{
+ auto first = this->begin();
+ const auto last = this->end();
+
+ for (; first != last; ++first)
+ ;
+
+ return first.current_history;
+}
+
+EventSet History::get_all_maximal_events() const
+{
+ auto first = this->begin();
+ const auto last = this->end();
+
+ for (; first != last; ++first)
+ ;
+
+ return first.maximal_events;
+}
+
+bool History::contains(UnfoldingEvent* e) const
+{
+ return std::any_of(this->begin(), this->end(), [=](UnfoldingEvent* e_hist) { return e == e_hist; });
+}
+
+EventSet History::get_event_diff_with(const Configuration& config) const
+{
+ auto wrapped_config = std::optional<std::reference_wrapper<const Configuration>>{config};
+ auto first = Iterator(events_, std::move(wrapped_config));
+ const auto last = this->end();
+
+ for (; first != last; ++first)
+ ;
+
+ return first.current_history;
+}
+
+} // namespace simgrid::mc::udpor
--- /dev/null
+/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#ifndef SIMGRID_MC_UDPOR_HISTORY_HPP
+#define SIMGRID_MC_UDPOR_HISTORY_HPP
+
+#include "src/mc/explo/udpor/Configuration.hpp"
+#include "src/mc/explo/udpor/EventSet.hpp"
+#include "src/mc/explo/udpor/udpor_forward.hpp"
+
+#include <functional>
+#include <optional>
+
+namespace simgrid::mc::udpor {
+
+/**
+ * @brief Conceptually describes the local configuration(s) of
+ * an event or a collection of events, encoding the history of
+ * the events without needing to actually fully compute all of
+ * the events contained in the history
+ *
+ * When you create an instance of `History`, you are effectively
+ * making a "lazy" configuration whose elements are the set of
+ * causes of a given event (if the `History` constists of a single
+ * event) or the union of all causes of all events (if the
+ * `History` consists of a set of events).
+ *
+ * Using a `History` object to represent the history of a set of
+ * events is more efficient (and reads more easily) than first
+ * computing the entire history of each of the events separately
+ * and combining the results. The former can take advantage of the
+ * fact that the histories of a set of events overlap greatly, and
+ * thus only a single BFS/DFS search over the event structure needs
+ * to be performed instead of many isolated searches for each event.
+ *
+ * The same observation also allows you to compute the difference between
+ * a configuration and a history of a set of events. This is used
+ * in UDPOR, for example, when determing the difference J / C and
+ * when using K-partial alternatives (which computes J as the union
+ * of histories of events)
+ */
+class History {
+private:
+ /**
+ * @brief The events whose history this instance describes
+ */
+ EventSet events_;
+
+public:
+ History(const History&) = default;
+ History& operator=(History const&) = default;
+ History(History&&) = default;
+
+ explicit History(UnfoldingEvent* e) : events_({e}) {}
+ explicit History(EventSet event_set = EventSet()) : events_(std::move(event_set)) {}
+
+ auto begin() const { return Iterator(events_); }
+ auto end() const { return Iterator(EventSet()); }
+
+ /**
+ * @brief Whether or not the given event is contained in the history
+ *
+ * @note If you only need to determine whether a few events are contained
+ * in a history, prefer this method. If, however, you wish to repeatedly
+ * determine over time (e.g. over the course of a computation) whether
+ * some event is part of the history, it may be better to first compute
+ * all events (see `History::get_all_events()`) and reuse this set
+ *
+ * @param e the event to check
+ * @returns whether or not `e` is contained in the collection
+ */
+ bool contains(UnfoldingEvent* e) const;
+
+ /**
+ * @brief Computes all events in the history described by this instance
+ *
+ * Sometimes, it is useful to compute the entire set of events that
+ * comprise the history of some event `e` of some set of events `E`.
+ * This method performs that computation.
+ *
+ * @returns the set of all causal dependencies of all events this
+ * history represents. Equivalently, the method returns the full
+ * dependency graph for all events in this history
+ */
+ EventSet get_all_events() const;
+
+ /**
+ * @brief Computes all events in the history described by this instance
+ * which are maximal (intuitively, those events which cause no others
+ * or are the "most recent")
+ */
+ EventSet get_all_maximal_events() const;
+
+ EventSet get_event_diff_with(const Configuration& config) const;
+
+private:
+ /**
+ * @brief An iterator which traverses the history of a set of events
+ */
+ struct Iterator {
+ public:
+ Iterator& operator++();
+ auto operator->() { return frontier.begin().operator->(); }
+ auto operator*() const { return *frontier.begin(); }
+
+ // If what the iterator sees next is the same, we consider them
+ // to be the same iterator. This way, once the iterator has completed
+ // its search, it will be "equal" to an iterator searching nothing
+ bool operator==(const Iterator& other) { return this->frontier == other.frontier; }
+ bool operator!=(const Iterator& other) { return not(this->operator==(other)); }
+
+ using iterator_category = std::forward_iterator_tag;
+ using difference_type = int; // # of steps between
+ using value_type = UnfoldingEvent*;
+ using pointer = value_type*;
+ using reference = value_type&;
+ using optional_configuration = std::optional<std::reference_wrapper<const Configuration>>;
+
+ Iterator(const EventSet& initial_events, optional_configuration config = std::nullopt);
+
+ private:
+ /// @brief Points in the graph from where to continue the search
+ EventSet frontier;
+
+ /// @brief What the iterator currently believes to be the
+ /// entire history of the events in the graph it traverses
+ EventSet current_history = EventSet();
+
+ /// @brief What the iterator currently believes
+ EventSet maximal_events;
+ optional_configuration configuration;
+ friend History;
+ };
+};
+
+} // namespace simgrid::mc::udpor
+#endif
--- /dev/null
+/* Copyright (c) 2017-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "src/3rd-party/catch.hpp"
+#include "src/mc/explo/udpor/History.hpp"
+#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
+
+using namespace simgrid::mc::udpor;
+
+TEST_CASE("simgrid::mc::udpor::History: History generation")
+{
+ // The following tests concern the given event tree
+ // e1
+ // / /
+ // e2 e6
+ // | \ \ / /
+ // e3 e4 e5 e7
+ UnfoldingEvent e1;
+ UnfoldingEvent e2{&e1}, e6{&e1};
+ UnfoldingEvent e3{&e2}, e4{&e2};
+ UnfoldingEvent e5{&e2, &e6}, e7{&e6};
+
+ SECTION("History with no events")
+ {
+ History history;
+ REQUIRE(history.get_all_events() == EventSet());
+ REQUIRE_FALSE(history.contains(&e1));
+ REQUIRE_FALSE(history.contains(&e2));
+ REQUIRE_FALSE(history.contains(&e3));
+ REQUIRE_FALSE(history.contains(&e4));
+ REQUIRE_FALSE(history.contains(&e5));
+ REQUIRE_FALSE(history.contains(&e6));
+ REQUIRE_FALSE(history.contains(&e7));
+ }
+
+ SECTION("Histories with a single event")
+ {
+ SECTION("Root event's history has a single event")
+ {
+ History history(&e1);
+ REQUIRE(history.get_all_events() == EventSet({&e1}));
+ }
+
+ SECTION("Check node e2")
+ {
+ History history(&e2);
+ REQUIRE(history.get_all_events() == EventSet({&e1, &e2}));
+ REQUIRE(history.contains(&e1));
+ REQUIRE(history.contains(&e2));
+ REQUIRE_FALSE(history.contains(&e3));
+ REQUIRE_FALSE(history.contains(&e4));
+ REQUIRE_FALSE(history.contains(&e5));
+ REQUIRE_FALSE(history.contains(&e6));
+ REQUIRE_FALSE(history.contains(&e7));
+ }
+
+ SECTION("Check node e3")
+ {
+ History history(&e3);
+ REQUIRE(history.get_all_events() == EventSet({&e1, &e2, &e3}));
+ REQUIRE(history.contains(&e1));
+ REQUIRE(history.contains(&e2));
+ REQUIRE(history.contains(&e3));
+ REQUIRE_FALSE(history.contains(&e4));
+ REQUIRE_FALSE(history.contains(&e5));
+ REQUIRE_FALSE(history.contains(&e6));
+ REQUIRE_FALSE(history.contains(&e7));
+ }
+
+ SECTION("Check node e4")
+ {
+ History history(&e4);
+ REQUIRE(history.get_all_events() == EventSet({&e1, &e2, &e4}));
+ REQUIRE(history.contains(&e1));
+ REQUIRE(history.contains(&e2));
+ REQUIRE_FALSE(history.contains(&e3));
+ REQUIRE(history.contains(&e4));
+ REQUIRE_FALSE(history.contains(&e5));
+ REQUIRE_FALSE(history.contains(&e6));
+ REQUIRE_FALSE(history.contains(&e7));
+ }
+
+ SECTION("Check node e5")
+ {
+ History history(&e5);
+ REQUIRE(history.get_all_events() == EventSet({&e1, &e2, &e6, &e5}));
+ REQUIRE(history.contains(&e1));
+ REQUIRE(history.contains(&e2));
+ REQUIRE_FALSE(history.contains(&e3));
+ REQUIRE_FALSE(history.contains(&e4));
+ REQUIRE(history.contains(&e5));
+ REQUIRE(history.contains(&e6));
+ REQUIRE_FALSE(history.contains(&e7));
+ }
+
+ SECTION("Check node e6")
+ {
+ History history(&e6);
+ REQUIRE(history.get_all_events() == EventSet({&e1, &e6}));
+ REQUIRE(history.contains(&e1));
+ REQUIRE_FALSE(history.contains(&e2));
+ REQUIRE_FALSE(history.contains(&e3));
+ REQUIRE_FALSE(history.contains(&e4));
+ REQUIRE_FALSE(history.contains(&e5));
+ REQUIRE(history.contains(&e6));
+ REQUIRE_FALSE(history.contains(&e7));
+ }
+
+ SECTION("Check node e7")
+ {
+ History history(&e7);
+ REQUIRE(history.get_all_events() == EventSet({&e1, &e6, &e7}));
+ REQUIRE(history.contains(&e1));
+ REQUIRE_FALSE(history.contains(&e2));
+ REQUIRE_FALSE(history.contains(&e3));
+ REQUIRE_FALSE(history.contains(&e4));
+ REQUIRE_FALSE(history.contains(&e5));
+ REQUIRE(history.contains(&e6));
+ REQUIRE(history.contains(&e7));
+ }
+ }
+
+ SECTION("Histories with multiple nodes")
+ {
+ SECTION("Nodes contained in the same branch")
+ {
+ History history_e1e2(EventSet({&e1, &e2}));
+ REQUIRE(history_e1e2.get_all_events() == EventSet({&e1, &e2}));
+ REQUIRE(history_e1e2.contains(&e1));
+ REQUIRE(history_e1e2.contains(&e2));
+ REQUIRE_FALSE(history_e1e2.contains(&e3));
+ REQUIRE_FALSE(history_e1e2.contains(&e4));
+ REQUIRE_FALSE(history_e1e2.contains(&e5));
+ REQUIRE_FALSE(history_e1e2.contains(&e6));
+ REQUIRE_FALSE(history_e1e2.contains(&e7));
+
+ History history_e1e3(EventSet({&e1, &e3}));
+ REQUIRE(history_e1e3.get_all_events() == EventSet({&e1, &e2, &e3}));
+ REQUIRE(history_e1e3.contains(&e1));
+ REQUIRE(history_e1e3.contains(&e2));
+ REQUIRE(history_e1e3.contains(&e3));
+ REQUIRE_FALSE(history_e1e3.contains(&e4));
+ REQUIRE_FALSE(history_e1e3.contains(&e5));
+ REQUIRE_FALSE(history_e1e3.contains(&e6));
+ REQUIRE_FALSE(history_e1e3.contains(&e7));
+
+ History history_e6e7(EventSet({&e6, &e7}));
+ REQUIRE(history_e6e7.get_all_events() == EventSet({&e1, &e6, &e7}));
+ REQUIRE(history_e6e7.contains(&e1));
+ REQUIRE_FALSE(history_e6e7.contains(&e2));
+ REQUIRE_FALSE(history_e6e7.contains(&e3));
+ REQUIRE_FALSE(history_e6e7.contains(&e4));
+ REQUIRE_FALSE(history_e6e7.contains(&e5));
+ REQUIRE(history_e6e7.contains(&e6));
+ REQUIRE(history_e6e7.contains(&e7));
+ }
+
+ SECTION("Nodes with the same ancestor")
+ {
+ History history_e3e5(EventSet({&e3, &e5}));
+ REQUIRE(history_e3e5.get_all_events() == EventSet({&e1, &e2, &e3, &e5, &e6}));
+ REQUIRE(history_e3e5.contains(&e1));
+ REQUIRE(history_e3e5.contains(&e2));
+ REQUIRE(history_e3e5.contains(&e3));
+ REQUIRE_FALSE(history_e3e5.contains(&e4));
+ REQUIRE(history_e3e5.contains(&e5));
+ REQUIRE(history_e3e5.contains(&e6));
+ REQUIRE_FALSE(history_e3e5.contains(&e7));
+ }
+
+ SECTION("Nodes with different ancestors")
+ {
+ History history_e4e7(EventSet({&e4, &e7}));
+ REQUIRE(history_e4e7.get_all_events() == EventSet({&e1, &e2, &e4, &e6, &e7}));
+ REQUIRE(history_e4e7.contains(&e1));
+ REQUIRE(history_e4e7.contains(&e2));
+ REQUIRE_FALSE(history_e4e7.contains(&e3));
+ REQUIRE(history_e4e7.contains(&e4));
+ REQUIRE_FALSE(history_e4e7.contains(&e5));
+ REQUIRE(history_e4e7.contains(&e6));
+ REQUIRE(history_e4e7.contains(&e7));
+ }
+
+ SECTION("Large number of nodes")
+ {
+ History history_e2356(EventSet({&e2, &e3, &e5, &e6}));
+ REQUIRE(history_e2356.get_all_events() == EventSet({&e1, &e2, &e3, &e5, &e6}));
+ REQUIRE(history_e2356.contains(&e1));
+ REQUIRE(history_e2356.contains(&e2));
+ REQUIRE(history_e2356.contains(&e3));
+ REQUIRE_FALSE(history_e2356.contains(&e4));
+ REQUIRE(history_e2356.contains(&e5));
+ REQUIRE(history_e2356.contains(&e6));
+ REQUIRE_FALSE(history_e2356.contains(&e7));
+ }
+
+ SECTION("History of the entire graph yields the entire graph")
+ {
+ History history(EventSet({&e1, &e2, &e3, &e4, &e5, &e6, &e7}));
+ REQUIRE(history.get_all_events() == EventSet({&e1, &e2, &e3, &e4, &e5, &e6, &e7}));
+ REQUIRE(history.contains(&e1));
+ REQUIRE(history.contains(&e2));
+ REQUIRE(history.contains(&e3));
+ REQUIRE(history.contains(&e4));
+ REQUIRE(history.contains(&e5));
+ REQUIRE(history.contains(&e6));
+ REQUIRE(history.contains(&e7));
+ }
+ }
+}
--- /dev/null
+/* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "src/mc/explo/udpor/Unfolding.hpp"
+
+#include <stdexcept>
+
+namespace simgrid::mc::udpor {
+
+void Unfolding::remove(UnfoldingEvent* e)
+{
+ if (e == nullptr) {
+ throw std::invalid_argument("Expected a non-null pointer to an event, but received NULL");
+ }
+ this->global_events_.erase(e);
+}
+
+void Unfolding::insert(std::unique_ptr<UnfoldingEvent> e)
+{
+ UnfoldingEvent* handle = e.get();
+ auto loc = this->global_events_.find(handle);
+ if (loc != this->global_events_.end()) {
+ // This is bad: someone wrapped the raw event address twice
+ // in two different unique ptrs and attempted to
+ // insert it into the unfolding...
+ throw std::invalid_argument("Attempted to insert an unfolding event owned twice."
+ "This will result in a double free error and must be fixed.");
+ }
+
+ // Map the handle to its owner
+ this->global_events_[handle] = std::move(e);
+}
+
+} // namespace simgrid::mc::udpor
--- /dev/null
+/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#ifndef SIMGRID_MC_UDPOR_UNFOLDING_HPP
+#define SIMGRID_MC_UDPOR_UNFOLDING_HPP
+
+#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
+#include "src/mc/explo/udpor/udpor_forward.hpp"
+
+#include <memory>
+#include <unordered_map>
+
+namespace simgrid::mc::udpor {
+
+class Unfolding {
+private:
+ /**
+ * @brief All of the events that are currently are a part of the unfolding
+ *
+ * @invariant Each unfolding event maps itself to the owner of that event,
+ * i.e. the unique pointer that owns the address. The Unfolding owns all
+ * of the addresses that are referenced by EventSet instances and Configuration
+ * instances. UDPOR guarantees that events are persisted for as long as necessary
+ */
+ std::unordered_map<UnfoldingEvent*, std::unique_ptr<UnfoldingEvent>> global_events_;
+
+public:
+ Unfolding() = default;
+ Unfolding& operator=(Unfolding&&) = default;
+ Unfolding(Unfolding&&) = default;
+
+ void remove(UnfoldingEvent* e);
+ void insert(std::unique_ptr<UnfoldingEvent> e);
+
+ size_t size() const { return this->global_events_.size(); }
+ bool empty() const { return this->global_events_.empty(); }
+};
+
+} // namespace simgrid::mc::udpor
+#endif
--- /dev/null
+/* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
+
+namespace simgrid::mc::udpor {
+
+UnfoldingEvent::UnfoldingEvent(std::initializer_list<UnfoldingEvent*> init_list)
+ : UnfoldingEvent(EventSet(std::move(init_list)))
+{
+}
+
+UnfoldingEvent::UnfoldingEvent(EventSet immediate_causes, std::shared_ptr<Transition> transition)
+ : associated_transition(std::move(transition)), immediate_causes(std::move(immediate_causes))
+{
+}
+
+bool UnfoldingEvent::operator==(const UnfoldingEvent& other) const
+{
+ const bool same_actor = associated_transition->aid_ == other.associated_transition->aid_;
+ if (!same_actor)
+ return false;
+
+ // TODO: Add in information to determine which step in the sequence this actor was executed
+
+ // All unfolding event objects are created in reference to
+ // an Unfolding object which owns them. Hence, the references
+ // they contain to other events in the unfolding can
+ // be used as intrinsic identities (i.e. we don't need to
+ // recursively check if each of our causes has a `==` in
+ // the other event's causes)
+ return this->immediate_causes == other.immediate_causes;
+}
+
+} // namespace simgrid::mc::udpor
--- /dev/null
+/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#ifndef SIMGRID_MC_UDPOR_UNFOLDING_EVENT_HPP
+#define SIMGRID_MC_UDPOR_UNFOLDING_EVENT_HPP
+
+#include "src/mc/explo/udpor/EventSet.hpp"
+#include "src/mc/explo/udpor/udpor_forward.hpp"
+#include "src/mc/transition/Transition.hpp"
+
+#include <initializer_list>
+#include <memory>
+#include <string>
+
+namespace simgrid::mc::udpor {
+
+class UnfoldingEvent {
+public:
+ UnfoldingEvent(std::initializer_list<UnfoldingEvent*> init_list);
+ UnfoldingEvent(EventSet immediate_causes = EventSet(),
+ std::shared_ptr<Transition> transition = std::make_unique<Transition>());
+
+ UnfoldingEvent(const UnfoldingEvent&) = default;
+ UnfoldingEvent& operator=(UnfoldingEvent const&) = default;
+ UnfoldingEvent(UnfoldingEvent&&) = default;
+
+ EventSet get_history() const;
+ bool in_history_of(const UnfoldingEvent* otherEvent) const;
+
+ bool conflicts_with(const UnfoldingEvent* otherEvent) const;
+ bool conflicts_with(const Configuration& config) const;
+ bool immediately_conflicts_with(const UnfoldingEvent* otherEvt) const;
+
+ const EventSet& get_immediate_causes() const { return this->immediate_causes; }
+ Transition* get_transition() const { return this->associated_transition.get(); }
+
+ bool operator==(const UnfoldingEvent&) const;
+
+private:
+ /**
+ * @brief The transition that UDPOR "attaches" to this
+ * specific event for later use while computing e.g. extension
+ * sets
+ *
+ * The transition points to that of a particular actor
+ * in the state reached by the configuration C (recall
+ * this is denoted `state(C)`) that excludes this event.
+ * In other words, this transition was the "next" event
+ * of the actor that executes it in `state(C)`.
+ */
+ std::shared_ptr<Transition> associated_transition;
+
+ /**
+ * @brief The "immediate" causes of this event.
+ *
+ * An event `e` is an immediate cause of an event `e'` if
+ *
+ * 1. e < e'
+ * 2. There is no event `e''` in E such that
+ * `e < e''` and `e'' < e'`
+ *
+ * Intuitively, an immediate cause "happened right before"
+ * this event was executed. It is sufficient to store
+ * only the immediate causes of any event `e`, as any indirect
+ * causes of that event would either be an indirect cause
+ * or an immediate cause of the immediate causes of `e`, and
+ * so on.
+ */
+ EventSet immediate_causes;
+};
+
+} // namespace simgrid::mc::udpor
+#endif
\ No newline at end of file
--- /dev/null
+/* Copyright (c) 2017-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "src/3rd-party/catch.hpp"
+#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
+
+using namespace simgrid::mc::udpor;
--- /dev/null
+/* Copyright (c) 2017-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "src/3rd-party/catch.hpp"
+#include "src/mc/explo/udpor/Unfolding.hpp"
+
+using namespace simgrid::mc::udpor;
+
+TEST_CASE("simgrid::mc::udpor::Unfolding: Creating an unfolding")
+{
+ Unfolding unfolding;
+ REQUIRE(unfolding.size() == 0);
+ REQUIRE(unfolding.empty());
+}
+
+TEST_CASE("simgrid::mc::udpor::Unfolding: Inserting and removing events with an unfolding")
+{
+ Unfolding unfolding;
+ auto e1 = std::make_unique<UnfoldingEvent>();
+ auto e2 = std::make_unique<UnfoldingEvent>();
+ auto e1_handle = e1.get();
+ auto e2_handle = e2.get();
+
+ unfolding.insert(std::move(e1));
+ REQUIRE(unfolding.size() == 1);
+ REQUIRE_FALSE(unfolding.empty());
+
+ unfolding.insert(std::move(e2));
+ REQUIRE(unfolding.size() == 2);
+ REQUIRE_FALSE(unfolding.empty());
+
+ unfolding.remove(e1_handle);
+ REQUIRE(unfolding.size() == 1);
+ REQUIRE_FALSE(unfolding.empty());
+
+ unfolding.remove(e2_handle);
+ REQUIRE(unfolding.size() == 0);
+ REQUIRE(unfolding.empty());
+}
\ No newline at end of file
--- /dev/null
+/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+/** @file mc_forward.hpp
+ *
+ * Forward definitions for MC types specific to UDPOR
+ */
+
+#ifndef SIMGRID_MC_UDPOR_FORWARD_HPP
+#define SIMGRID_MC_UDPOR_FORWARD_HPP
+
+namespace simgrid::mc::udpor {
+
+class EventSet;
+class Configuration;
+class History;
+class Unfolding;
+class UnfoldingEvent;
+
+} // namespace simgrid::mc::udpor
+
+#endif
+++ /dev/null
-/* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved. */
-
-/* This program is free software; you can redistribute it and/or modify it
- * under the terms of the license (GNU LGPL) which comes with this package. */
-
-#include "udpor_global.hpp"
-#include "xbt/log.h"
-#include <algorithm>
-
-XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor_global, mc, "udpor_global");
-
-namespace simgrid::mc {
-
-EventSet EvtSetTools::makeUnion(const EventSet& s1, const EventSet& s2)
-{
- EventSet res = s1;
- for (auto evt : s2)
- EvtSetTools::pushBack(res, evt);
- return res;
-}
-
-void EvtSetTools::pushBack(EventSet& events, UnfoldingEvent* e)
-{
- if (not EvtSetTools::contains(events, e))
- events.push_back(e);
-}
-
-bool EvtSetTools::contains(const EventSet& events, const UnfoldingEvent* e)
-{
- return std::any_of(events.begin(), events.end(), [e](const UnfoldingEvent* evt) { return *evt == *e; });
-}
-
-} // namespace simgrid::mc
+++ /dev/null
-/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */
-
-/* This program is free software; you can redistribute it and/or modify it
- * under the terms of the license (GNU LGPL) which comes with this package. */
-
-#ifndef SIMGRID_MC_UDPOR_GLOBAL_HPP
-#define SIMGRID_MC_UDPOR_GLOBAL_HPP
-
-#include <iostream>
-#include <queue>
-#include <string_view>
-
-/* TODO: many method declared in this module are not implemented */
-
-namespace simgrid::mc {
-
-class UnfoldingEvent;
-using EventSet = std::deque<UnfoldingEvent*>;
-
-class EvtSetTools {
-public:
- static bool contains(const EventSet& events, const UnfoldingEvent* e);
- static UnfoldingEvent* find(const EventSet& events, const UnfoldingEvent* e);
- static void subtract(EventSet& events, EventSet const& otherSet);
- static bool depends(const EventSet& events, const EventSet& otherSet);
- static bool isEmptyIntersection(EventSet evtS1, EventSet evtS2);
- static EventSet makeUnion(const EventSet& s1, const EventSet& s2);
- static void pushBack(EventSet& events, UnfoldingEvent* e);
- static void remove(EventSet& events, UnfoldingEvent* e);
- static EventSet minus(EventSet events, UnfoldingEvent* e);
- static EventSet plus(EventSet events, UnfoldingEvent* e);
-};
-
-struct s_evset_in_t {
- EventSet causuality_events;
- EventSet cause;
- EventSet ancestorSet;
-};
-
-class Configuration {
-public:
- EventSet events_;
- EventSet maxEvent; // Events recently added to events_
- EventSet actorMaxEvent; // maximal events of the actors in current configuration
- UnfoldingEvent* lastEvent; // The last added event
-
- Configuration plus_config(UnfoldingEvent*) const;
- void createEvts(Configuration C, EventSet& result, const std::string& trans_tag, s_evset_in_t ev_sets, bool chk,
- UnfoldingEvent* immPreEvt);
- void updateMaxEvent(UnfoldingEvent*); // update maximal events of the configuration and actors
- UnfoldingEvent* findActorMaxEvt(int actorId); // find maximal event of a Actor whose id = actorId
-
- UnfoldingEvent* findTestedComm(const UnfoldingEvent* testEvt); // find comm tested by action testTrans
-
- Configuration() = default;
- Configuration(const Configuration&) = default;
- Configuration& operator=(Configuration const&) = default;
- Configuration(Configuration&&) = default;
-};
-
-class UnfoldingEvent {
-public:
- UnfoldingEvent(unsigned int nb_events, std::string const& trans_tag, EventSet const& causes, int sid = -1);
- UnfoldingEvent(const UnfoldingEvent&) = default;
- UnfoldingEvent& operator=(UnfoldingEvent const&) = default;
- UnfoldingEvent(UnfoldingEvent&&) = default;
-
- EventSet getHistory() const;
-
- bool isConflict(UnfoldingEvent* event, UnfoldingEvent* otherEvent) const;
- bool concernSameComm(const UnfoldingEvent* event, const UnfoldingEvent* otherEvent) const;
-
- // check otherEvent is in my history ?
- bool inHistory(UnfoldingEvent* otherEvent) const;
-
- bool isImmediateConflict1(UnfoldingEvent* evt, UnfoldingEvent* otherEvt) const;
-
- bool conflictWithConfig(UnfoldingEvent* event, Configuration const& config) const;
- bool operator==(const UnfoldingEvent&) const { return false; };
- void print() const;
-
- inline int get_state_id() const { return state_id; }
- inline void set_state_id(int sid) { state_id = sid; }
-
- inline std::string get_transition_tag() const { return transition_tag; }
- inline void set_transition_tag(std::string_view tr_tag) { transition_tag = tr_tag; }
-
-private:
- EventSet causes; // used to store directed ancestors of event e
- int id = -1;
- int state_id{-1};
- std::string transition_tag{""}; // The tag of the last transition that lead to creating the event
- bool transition_is_IReceive(const UnfoldingEvent* testedEvt, const UnfoldingEvent* SdRcEvt) const;
- bool transition_is_ISend(const UnfoldingEvent* testedEvt, const UnfoldingEvent* SdRcEvt) const;
- bool check_tr_concern_same_comm(bool& chk1, bool& chk2, UnfoldingEvent* evt1, UnfoldingEvent* evt2) const;
-};
-} // namespace simgrid::mc
-#endif
src/mc/explo/UdporChecker.cpp
src/mc/explo/UdporChecker.hpp
+ src/mc/explo/udpor/Configuration.hpp
+ src/mc/explo/udpor/Configuration.cpp
+ src/mc/explo/udpor/EventSet.cpp
+ src/mc/explo/udpor/EventSet.hpp
+ src/mc/explo/udpor/History.cpp
+ src/mc/explo/udpor/History.hpp
+ src/mc/explo/udpor/UnfoldingEvent.cpp
+ src/mc/explo/udpor/UnfoldingEvent.hpp
+ src/mc/explo/udpor/Unfolding.cpp
+ src/mc/explo/udpor/Unfolding.hpp
+
src/mc/inspect/DwarfExpression.cpp
src/mc/inspect/DwarfExpression.hpp
src/mc/inspect/Frame.cpp
src/mc/mc_forward.hpp
src/mc/mc_private.hpp
src/mc/mc_record.cpp
- src/mc/udpor_global.cpp
- src/mc/udpor_global.hpp
src/xbt/mmalloc/mm_interface.c
)
src/xbt/xbt_str_test.cpp
src/kernel/lmm/maxmin_test.cpp)
if (SIMGRID_HAVE_MC)
- set(UNIT_TESTS ${UNIT_TESTS} src/mc/sosp/Snapshot_test.cpp src/mc/sosp/PageStore_test.cpp)
+ set(UNIT_TESTS ${UNIT_TESTS} src/mc/sosp/Snapshot_test.cpp
+ src/mc/sosp/PageStore_test.cpp
+ src/mc/explo/udpor/EventSet_test.cpp
+ src/mc/explo/udpor/Unfolding_test.cpp
+ src/mc/explo/udpor/UnfoldingEvent_test.cpp
+ src/mc/explo/udpor/History_test.cpp
+ src/mc/explo/udpor/Configuration_test.cpp)
else()
set(EXTRA_DIST ${EXTRA_DIST} src/mc/sosp/Snapshot_test.cpp src/mc/sosp/PageStore_test.cpp)
endif()
