Phase 6 of UDPOR Integration: Add `K`-partial alternatives computation + clean up phase
See merge request simgrid/simgrid!139
include src/mc/explo/UdporChecker.cpp
include src/mc/explo/UdporChecker.hpp
include src/mc/explo/simgrid_mc.cpp
+include src/mc/explo/udpor/Comb.hpp
include src/mc/explo/udpor/Configuration.cpp
include src/mc/explo/udpor/Configuration.hpp
include src/mc/explo/udpor/Configuration_test.cpp
#include "src/mc/explo/UdporChecker.hpp"
#include "src/mc/api/State.hpp"
+#include "src/mc/explo/udpor/Comb.hpp"
+#include "src/mc/explo/udpor/History.hpp"
#include "src/mc/explo/udpor/maximal_subsets_iterator.hpp"
+
#include <xbt/asserts.h>
#include <xbt/log.h>
// 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.
+ // relation. Here, then, we may be in a deadlock (the other
+ // possibility is that we've finished running everything, and
+ // we wouldn't be in deadlock then)
if (enC.empty()) {
get_remote_app().check_deadlock();
}
"the search, yet no events were actually chosen\n"
"*********************************\n\n");
- // Move the application into stateCe and actually make note of that state
+ // Move the application into stateCe and make note of that state
move_to_stateCe(*stateC, *e);
auto stateCe = record_current_state();
// 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;
- if (auto J = compute_partial_alternative(D, C, K); !J.empty()) {
- J.subtract(C.get_events());
+ if (auto J = C.compute_k_partial_alternative_to(D, this->unfolding, K); J.has_value()) {
// Before searching the "right half", we need to make
// sure the program actually reflects the fact
restore_program_state_to(*stateC);
// Explore(C, D + {e}, J \ C)
- explore(C, D, std::move(J), std::move(stateC), std::move(prev_exC));
+ auto J_minus_C = J.value().get_events().subtracting(C.get_events());
+ explore(C, D, std::move(J_minus_C), std::move(stateC), std::move(prev_exC));
}
// D <-- D - {e}
begin != maximal_subsets_iterator(); ++begin) {
const EventSet& maximal_subset = *begin;
- // TODO: Determine if `a` is enabled here
+ // Determining if `a` is enabled here might not be possible while looking at `a` opaquely
+ // We leave the implementation as-is to ensure that any addition would be simple
+ // if it were ever added
const bool enabled_at_config_k = false;
if (enabled_at_config_k) {
}
}
}
-
return incremental_exC;
}
void UdporChecker::restore_program_state_to(const State& stateC)
{
- // TODO: Perform state regeneration in the same manner as is done
- // in the DFSChecker.cpp
+ get_remote_app().restore_initial_state();
+ // TODO: We need to have the stack of past states available at this
+ // point. Since the method is recursive, we'll need to keep track of
+ // this as we progress
}
std::unique_ptr<State> UdporChecker::record_current_state()
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
+ const EventSet C_union_D = C.get_events().make_union(D);
+ const EventSet es_immediate_conflicts = this->unfolding.get_immediate_conflicts_of(e);
+ const EventSet Q_CDU = C_union_D.make_union(es_immediate_conflicts.get_local_config());
+
+ // Move {e} \ Q_CDU from U to G
+ if (Q_CDU.contains(e)) {
+ this->unfolding.remove(e);
+ }
+
+ // foreach ê in #ⁱ_U(e)
+ for (const auto* e_hat : es_immediate_conflicts) {
+ // Move [ê] \ Q_CDU from U to G
+ const EventSet to_remove = e_hat->get_history().subtracting(Q_CDU);
+ this->unfolding.remove(to_remove);
+ }
}
RecordTrace UdporChecker::get_record_trace()
* 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.
+ * 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 {
inline std::unique_ptr<State> get_current_state() { return std::make_unique<State>(get_remote_app()); }
private:
- /**
- * @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();
/**
* 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
+ * what is akin to 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
/**
* @brief Computes a portion of the extension set of a configuration given
- * some action `action`
+ * some action `action` by directly enumerating all maximal subsets of C
+ * (i.e. without specializations based on the action)
*/
EventSet compute_exC_by_enumeration(const Configuration& C, const std::shared_ptr<Transition> action);
EventSet compute_enC(const Configuration& C, const EventSet& exC) const;
- /**
- *
- */
- EventSet compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const;
-
/**
*
*/
--- /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_COMB_HPP
+#define SIMGRID_MC_UDPOR_COMB_HPP
+
+#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
+#include "src/mc/explo/udpor/udpor_forward.hpp"
+#include "src/xbt/utils/iter/variable_for_loop.hpp"
+
+#include <boost/iterator/function_input_iterator.hpp>
+#include <boost/iterator/indirect_iterator.hpp>
+#include <functional>
+#include <vector>
+
+namespace simgrid::mc::udpor {
+
+/**
+ * @brief An individual element of a `Comb`, i.e. a
+ * sequence of `const UnfoldingEvent*`s
+ */
+using Spike = std::vector<const UnfoldingEvent*>;
+
+/**
+ * @brief A two-dimensional data structure that is used
+ * to compute partial alternatives in UDPOR
+ *
+ * The comb data structure is described in the paper
+ * "Quasi-Optimal DPOR" by Nguyen et al. Formally,
+ * if `A` is a set:
+ *
+ * """
+ * An **A-Comb C of size `n` (`n` a natural number)**
+ * is an *ordered* collection of spikes <s_1, s_2, ..., s_n>,
+ * where each spike is a sequence of elements over A.
+ *
+ * Furthermore, a **combination over C** is any tuple
+ * <a_1, a_2, ..., a_n> where a_i is a member of s_i
+ * """
+ *
+ * The name probably comes from what the structure looks
+ * like if you draw it out. For example, if `A = {1, 2, 3, ..., 10}`,
+ * then a possible `A-comb` of size 8 might look like
+ *
+ * 1 2 3 4 5 6
+ * 2 4 5 9 8
+ * 10 9 2 1 1
+ * 8 9 10 5
+ * 1
+ * 3 4 5
+ * 1 4 4 5 1 6
+ * 8 8 9
+ *
+ * which, if you squint a bit, looks like a comb (albeit with some
+ * broken bristles [or spikes]). A combination is any selection of
+ * one element within each spike; e.g. (where _x_ denotes element `x`
+ * is selected)
+ *
+ * 1 2 _3_ 4 5 6
+ * 2 _4_ 5 9 8
+ * 10 9 2 _1_ 1
+ * 8 _9_ 10 5
+ * _1_
+ * 3 4 _5_
+ * 1 _4_ 4 5 1 6
+ * _8_ 8 9
+ *
+ * A `Comb` as described by this C++ class is a `U-comb`, where
+ * `U` is the set of events that UDPOR has explored. That is,
+ * the comb is over a set of events
+ */
+class Comb : public std::vector<Spike> {
+public:
+ explicit Comb(unsigned k) : std::vector<Spike>(k) {}
+ Comb(const Comb& other) = default;
+ Comb(Comb&& other) = default;
+ Comb& operator=(const Comb& other) = default;
+ Comb& operator=(Comb&& other) = default;
+
+ auto combinations_begin() const
+ {
+ std::vector<std::reference_wrapper<const Spike>> references;
+ std::transform(begin(), end(), std::back_inserter(references), [](const Spike& spike) { return std::cref(spike); });
+ return simgrid::xbt::variable_for_loop<const Spike>(std::move(references));
+ }
+ auto combinations_end() const { return simgrid::xbt::variable_for_loop<const Spike>(); }
+};
+
+} // namespace simgrid::mc::udpor
+#endif
* 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/Comb.hpp"
#include "src/mc/explo/udpor/History.hpp"
+#include "src/mc/explo/udpor/Unfolding.hpp"
#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
#include "src/mc/explo/udpor/maximal_subsets_iterator.hpp"
#include "xbt/asserts.h"
{
}
+Configuration::Configuration(const UnfoldingEvent* e) : Configuration(e->get_history())
+{
+ // The local configuration should always be a valid configuration. We
+ // check the invariant regardless as a sanity check
+}
+
Configuration::Configuration(const EventSet& events) : events_(events)
{
if (!events_.is_valid_configuration()) {
}
}
+Configuration::Configuration(const History& history) : Configuration(history.get_all_events()) {}
+
void Configuration::add_event(const UnfoldingEvent* e)
{
if (e == nullptr) {
}
}
+bool Configuration::is_compatible_with(const UnfoldingEvent* e) const
+{
+ return not e->conflicts_with(*this);
+}
+
+bool Configuration::is_compatible_with(const History& history) const
+{
+ return std::none_of(history.begin(), history.end(),
+ [&](const UnfoldingEvent* e) { return e->conflicts_with(*this); });
+}
+
std::vector<const UnfoldingEvent*> Configuration::get_topologically_sorted_events() const
{
return this->events_.get_topological_ordering();
return minimally_reproducible_events;
}
+std::optional<Configuration> Configuration::compute_alternative_to(const EventSet& D, const Unfolding& U) const
+{
+ // A full alternative can be computed by checking against everything in D
+ return compute_k_partial_alternative_to(D, U, D.size());
+}
+
+std::optional<Configuration> Configuration::compute_k_partial_alternative_to(const EventSet& D, const Unfolding& U,
+ size_t k) const
+{
+ // 1. Select k (of |D|, whichever is smaller) arbitrary events e_1, ..., e_k from D
+ const auto D_hat = [&]() {
+ const size_t size = std::min(k, D.size());
+ std::vector<const UnfoldingEvent*> D_hat(size);
+ // TODO: Since any subset suffices for computing `k`-partial alternatives,
+ // potentially select intelligently here (e.g. perhaps pick events
+ // with transitions that we know are totally independent). This may be
+ // especially important if the enumeration is the slowest part of
+ // UDPOR
+ //
+ // For now, simply pick the first `k` events
+ std::copy_n(D.begin(), size, D_hat.begin());
+ return D_hat;
+ }();
+
+ // 2. Build a U-comb <s_1, ..., s_k> of size k, where spike `s_i` contains
+ // all events in conflict with `e_i`
+ //
+ // 3. EXCEPT those events e' for which [e'] + C is not a configuration or
+ // [e'] intersects D
+ //
+ // NOTE: This is an expensive operation as we must traverse the entire unfolding
+ // and compute `C.is_compatible_with(History)` for every event in the structure :/.
+ // A later performance improvement would be to incorporate the work of Nguyen et al.
+ // into SimGrid which associated additonal data structures with each unfolding event.
+ // Since that is a rather complicated addition, we defer it to a later time...
+ Comb comb(k);
+
+ for (const auto* e : U) {
+ for (unsigned i = 0; i < k; i++) {
+ const UnfoldingEvent* e_i = D_hat[i];
+ if (const auto e_local_config = History(e);
+ e_i->conflicts_with(e) and (not D.intersects(e_local_config)) and is_compatible_with(e_local_config)) {
+ comb[i].push_back(e);
+ }
+ }
+ }
+
+ // 4. Find any such combination <e_1', ..., e_k'> in comb satisfying
+ // ~(e_i' # e_j') for i != j
+ //
+ // NOTE: This is a VERY expensive operation: it enumerates all possible
+ // ways to select an element from each spike. Unfortunately there's no
+ // way around the enumeration, as computing a full alternative in general is
+ // NP-complete (although computing the k-partial alternative is polynomial in
+ // the number of events)
+ const auto map_events = [](const std::vector<Spike::const_iterator>& spikes) {
+ std::vector<const UnfoldingEvent*> events;
+ for (const auto& event_in_spike : spikes) {
+ events.push_back(*event_in_spike);
+ }
+ return EventSet(std::move(events));
+ };
+ const auto alternative =
+ std::find_if(comb.combinations_begin(), comb.combinations_end(),
+ [&map_events](const auto& vector) { return map_events(vector).is_conflict_free(); });
+
+ // No such alternative exists
+ if (alternative == comb.combinations_end()) {
+ return std::nullopt;
+ }
+
+ // 5. J := [e_1] + [e_2] + ... + [e_k] is a k-partial alternative
+ return Configuration(History(map_events(*alternative)));
+}
+
} // namespace simgrid::mc::udpor
#include "src/mc/explo/udpor/EventSet.hpp"
#include "src/mc/explo/udpor/udpor_forward.hpp"
+#include <optional>
+
namespace simgrid::mc::udpor {
class Configuration {
Configuration& operator=(Configuration const&) = default;
Configuration(Configuration&&) = default;
+ explicit Configuration(const UnfoldingEvent* event);
explicit Configuration(const EventSet& events);
+ explicit Configuration(const History& history);
explicit Configuration(std::initializer_list<const UnfoldingEvent*> events);
auto begin() const { return this->events_.begin(); }
*/
void add_event(const UnfoldingEvent* e);
+ /**
+ * @brief Whether or not the given event can be added to
+ * this configuration while keeping the set of events causally closed
+ * and conflict-free
+ */
+ bool is_compatible_with(const UnfoldingEvent* e) const;
+
+ /**
+ * @brief Whether or not the events in the given history can be added to
+ * this configuration while keeping the set of events causally closed
+ * and conflict-free
+ */
+ bool is_compatible_with(const History& history) const;
+
+ std::optional<Configuration> compute_alternative_to(const EventSet& D, const Unfolding& U) const;
+ std::optional<Configuration> compute_k_partial_alternative_to(const EventSet& D, const Unfolding& U, size_t k) const;
+
/**
* @brief Orders the events of the configuration such that
* "more recent" events (i.e. those that are farther down in
* of the events returned by this method is equal to the set of events
* in this configuration
*
- * @returns the smallest set of events whose events generates this configuration
- * (denoted `config(E)`)
+ * @returns the smallest set of events whose events generates
+ * this configuration (denoted `config(E)`)
*/
EventSet get_minimally_reproducible_events() const;
#include "src/mc/explo/udpor/Configuration.hpp"
#include "src/mc/explo/udpor/EventSet.hpp"
#include "src/mc/explo/udpor/History.hpp"
+#include "src/mc/explo/udpor/Unfolding.hpp"
#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
#include "src/mc/explo/udpor/maximal_subsets_iterator.hpp"
#include "src/mc/explo/udpor/udpor_tests_private.hpp"
// Iteration with events directly should now also be finished
REQUIRE(first_events == last);
}
+}
+
+TEST_CASE("simgrid::mc::udpor:Configuration: Computing Full Alternatives in Reader/Writer Example")
+{
+ // The following tests concern the given event structure that is given as
+ // an example in figure 1 of the original UDPOR paper.
+ // e0
+ // / / /
+ // e1 e4 e7
+ // / / // /
+ // / / e5 e8 e9
+ // e2 e3 / /
+ // e6 e10
+ //
+ // Theses tests walk through exactly the configurations and sets of `D` that
+ // UDPOR COULD encounter as it walks through the unfolding. Note that
+ // if there are multiple alternatives to any given configuration, UDPOR can
+ // continue searching any one of them. The sequence assumes UDPOR first picks `e1`,
+ // then `e4`, and then `e7`
+ Unfolding U;
+
+ auto e0 = std::make_unique<UnfoldingEvent>(EventSet(), std::make_shared<ConditionallyDependentAction>());
+ auto e0_handle = e0.get();
+
+ auto e1 = std::make_unique<UnfoldingEvent>(EventSet({e0_handle}), std::make_shared<DependentAction>());
+ auto e1_handle = e1.get();
+
+ auto e2 = std::make_unique<UnfoldingEvent>(EventSet({e1_handle}), std::make_shared<ConditionallyDependentAction>());
+ auto e2_handle = e2.get();
+
+ auto e3 = std::make_unique<UnfoldingEvent>(EventSet({e1_handle}), std::make_shared<ConditionallyDependentAction>());
+ auto e3_handle = e3.get();
+
+ auto e4 = std::make_unique<UnfoldingEvent>(EventSet({e0_handle}), std::make_shared<ConditionallyDependentAction>());
+ auto e4_handle = e4.get();
+
+ auto e5 = std::make_unique<UnfoldingEvent>(EventSet({e4_handle}), std::make_shared<DependentAction>());
+ auto e5_handle = e5.get();
+
+ auto e6 = std::make_unique<UnfoldingEvent>(EventSet({e5_handle}), std::make_shared<ConditionallyDependentAction>());
+ auto e6_handle = e6.get();
+
+ auto e7 = std::make_unique<UnfoldingEvent>(EventSet({e0_handle}), std::make_shared<ConditionallyDependentAction>());
+ auto e7_handle = e7.get();
+
+ auto e8 = std::make_unique<UnfoldingEvent>(EventSet({e4_handle, e7_handle}), std::make_shared<DependentAction>());
+ auto e8_handle = e8.get();
+
+ auto e9 = std::make_unique<UnfoldingEvent>(EventSet({e7_handle}), std::make_shared<DependentAction>());
+ auto e9_handle = e9.get();
+
+ auto e10 = std::make_unique<UnfoldingEvent>(EventSet({e9_handle}), std::make_shared<ConditionallyDependentAction>());
+ auto e10_handle = e10.get();
+
+ SECTION("Alternative computation call 1")
+ {
+ // During the first call to Alt(C, D + {e}),
+ // UDPOR believes `U` to be the following:
+ //
+ // e0
+ // / / /
+ // e1 e4 e7
+ // /
+ // / /
+ // e2 e3
+ //
+ // C := {e0, e1, e2} and `Explore(C, D, A)` picked `e3`
+ // (since en(C') where C' := {e0, e1, e2, e3} is empty
+ // [so UDPOR will simply return when C' is reached])
+ //
+ // Thus the computation is (since D is empty at first)
+ //
+ // Alt(C, D + {e}) --> Alt({e0, e1, e2}, {e3})
+ //
+ // where U is given above. There are no alternatives in
+ // this case since `e4` and `e7` conflict with `e1` (so
+ // they cannot be added to C to form a configuration)
+ const Configuration C{e0_handle, e1_handle, e2_handle};
+ const EventSet D_plus_e{e3_handle};
+
+ REQUIRE(U.empty());
+ U.insert(std::move(e0));
+ U.insert(std::move(e1));
+ U.insert(std::move(e2));
+ U.insert(std::move(e3));
+ U.insert(std::move(e4));
+ U.insert(std::move(e7));
+
+ const auto alternative = C.compute_alternative_to(D_plus_e, U);
+ REQUIRE_FALSE(alternative.has_value());
+ }
+
+ SECTION("Alternative computation call 2")
+ {
+ // During the second call to Alt(C, D + {e}),
+ // UDPOR believes `U` to be the following:
+ //
+ // e0
+ // / / /
+ // e1 e4 e7
+ // /
+ // / /
+ // e2 e3
+ //
+ // C := {e0, e1} and `Explore(C, D, A)` picked `e2`.
+ //
+ // Thus the computation is (since D is still empty)
+ //
+ // Alt(C, D + {e}) --> Alt({e0, e1}, {e2})
+ //
+ // where U is given above. There are no alternatives in
+ // this case since `e4` and `e7` conflict with `e1` (so
+ // they cannot be added to C to form a configuration) and
+ // e3 is NOT in conflict with either e0 or e1
+ const Configuration C{e0_handle, e1_handle};
+ const EventSet D_plus_e{e2_handle};
+
+ REQUIRE(U.empty());
+ U.insert(std::move(e0));
+ U.insert(std::move(e1));
+ U.insert(std::move(e2));
+ U.insert(std::move(e3));
+ U.insert(std::move(e4));
+ U.insert(std::move(e7));
+
+ const auto alternative = C.compute_alternative_to(D_plus_e, U);
+ REQUIRE_FALSE(alternative.has_value());
+ }
+
+ SECTION("Alternative computation call 3")
+ {
+ // During the thrid call to Alt(C, D + {e}),
+ // UDPOR believes `U` to be the following:
+ //
+ // e0
+ // / / /
+ // e1 e4 e7
+ // /
+ // / /
+ // e2 e3
+ //
+ // C := {e0} and `Explore(C, D, A)` picked `e1`.
+ //
+ // Thus the computation is (since D is still empty)
+ //
+ // Alt(C, D + {e}) --> Alt({e0}, {e1})
+ //
+ // where U is given above. There are two alternatives in this case:
+ // {e0, e4} and {e0, e7}. Either one would be a valid choice for
+ // UDPOR, so we must check for the precense of either
+ const Configuration C{e0_handle};
+ const EventSet D_plus_e{e1_handle};
+
+ REQUIRE(U.empty());
+ U.insert(std::move(e0));
+ U.insert(std::move(e1));
+ U.insert(std::move(e2));
+ U.insert(std::move(e3));
+ U.insert(std::move(e4));
+ U.insert(std::move(e7));
+
+ const auto alternative = C.compute_alternative_to(D_plus_e, U);
+ REQUIRE(alternative.has_value());
+
+ // The first alternative that is found is the one that is chosen. Since
+ // traversal over the elements of an unordered_set<> are not guaranteed,
+ // both {e0, e4} and {e0, e7} are valid alternatives
+ REQUIRE((alternative.value().get_events() == EventSet({e0_handle, e4_handle}) or
+ alternative.value().get_events() == EventSet({e0_handle, e7_handle})));
+ }
+
+ SECTION("Alternative computation call 4")
+ {
+ // During the fourth call to Alt(C, D + {e}),
+ // UDPOR believes `U` to be the following:
+ //
+ // e0
+ // / / /
+ // e1 e4 e7
+ // / / //
+ // / / e5 e8
+ // e2 e3 /
+ // e6
+ //
+ // C := {e0, e4, e5} and `Explore(C, D, A)` picked `e6`
+ // (since en(C') where C' := {e0, e4, e5, e6} is empty
+ // [so UDPOR will simply return when C' is reached])
+ //
+ // Thus the computation is (since D is {e1})
+ //
+ // Alt(C, D + {e}) --> Alt({e0, e4, e5}, {e1, e6})
+ //
+ // where U is given above. There are no alternatives in this
+ // case, since:
+ //
+ // 1.`e2/e3` are eliminated since their histories contain `e1`
+ // 2. `e7/e8` are eliminated because they conflict with `e5`
+ const Configuration C{e0_handle, e4_handle, e5_handle};
+ const EventSet D_plus_e{e1_handle, e6_handle};
+
+ REQUIRE(U.empty());
+ U.insert(std::move(e0));
+ U.insert(std::move(e1));
+ U.insert(std::move(e2));
+ U.insert(std::move(e3));
+ U.insert(std::move(e4));
+ U.insert(std::move(e6));
+ U.insert(std::move(e7));
+ U.insert(std::move(e8));
+
+ const auto alternative = C.compute_alternative_to(D_plus_e, U);
+ REQUIRE_FALSE(alternative.has_value());
+ }
+
+ SECTION("Alternative computation call 5")
+ {
+ // During the fifth call to Alt(C, D + {e}),
+ // UDPOR believes `U` to be the following:
+ //
+ // e0
+ // / / /
+ // e1 e4 e7
+ // / / //
+ // / / e5 e8
+ // e2 e3 /
+ // e6
+ //
+ // C := {e0, e4} and `Explore(C, D, A)` picked `e5`
+ // (since en(C') where C' := {e0, e4, e5, e6} is empty
+ // [so UDPOR will simply return when C' is reached])
+ //
+ // Thus the computation is (since D is {e1})
+ //
+ // Alt(C, D + {e}) --> Alt({e0, e4}, {e1, e5})
+ //
+ // where U is given above. There are THREE alternatives in this case,
+ // viz. {e0, e7}, {e0, e4, e7} and {e0, e4, e7, e8}.
+ //
+ // To continue the search, UDPOR computes J / C which in this
+ // case gives {e7, e8}. Since `e8` is not in en(C), UDPOR will
+ // choose `e7` next and add `e5` to `D`
+ const Configuration C{e0_handle, e4_handle};
+ const EventSet D_plus_e{e1_handle, e5_handle};
+
+ REQUIRE(U.empty());
+ U.insert(std::move(e0));
+ U.insert(std::move(e1));
+ U.insert(std::move(e2));
+ U.insert(std::move(e3));
+ U.insert(std::move(e4));
+ U.insert(std::move(e6));
+ U.insert(std::move(e7));
+ U.insert(std::move(e8));
+ REQUIRE(U.size() == 8);
+
+ const auto alternative = C.compute_alternative_to(D_plus_e, U);
+ REQUIRE(alternative.has_value());
+ REQUIRE((alternative.value().get_events() == EventSet({e0_handle, e7_handle}) or
+ alternative.value().get_events() == EventSet({e0_handle, e4_handle, e7_handle}) or
+ alternative.value().get_events() == EventSet({e0_handle, e4_handle, e7_handle, e8_handle})));
+ }
+
+ SECTION("Alternative computation call 6")
+ {
+ // During the sixth call to Alt(C, D + {e}),
+ // UDPOR believes `U` to be the following:
+ //
+ // e0
+ // / / /
+ // e1 e4 e7
+ // / / // /
+ // / / e5 e8 e9
+ // e2 e3 /
+ // e6
+ //
+ // C := {e0, e4, e7} and `Explore(C, D, A)` picked `e8`
+ // (since en(C') where C' := {e0, e4, e7, e8} is empty
+ // [so UDPOR will simply return when C' is reached])
+ //
+ // Thus the computation is (since D is {e1, e5} [see the last step])
+ //
+ // Alt(C, D + {e}) --> Alt({e0, e4, e7}, {e1, e5, e8})
+ //
+ // where U is given above. There are no alternatives in this case
+ // since all `e9` conflicts with `e4` and all other events of `U`
+ // are eliminated since their history intersects `D`
+ const Configuration C{e0_handle, e4_handle, e7_handle};
+ const EventSet D_plus_e{e1_handle, e5_handle, e8_handle};
+
+ REQUIRE(U.empty());
+ U.insert(std::move(e0));
+ U.insert(std::move(e1));
+ U.insert(std::move(e2));
+ U.insert(std::move(e3));
+ U.insert(std::move(e4));
+ U.insert(std::move(e6));
+ U.insert(std::move(e7));
+ U.insert(std::move(e8));
+ U.insert(std::move(e9));
+
+ const auto alternative = C.compute_alternative_to(D_plus_e, U);
+ REQUIRE_FALSE(alternative.has_value());
+ }
+
+ SECTION("Alternative computation call 7")
+ {
+ // During the seventh call to Alt(C, D + {e}),
+ // UDPOR believes `U` to be the following:
+ //
+ // e0
+ // / / /
+ // e1 e4 e7
+ // / / // /
+ // / / e5 e8 e9
+ // e2 e3 /
+ // e6
+ //
+ // C := {e0, e4} and `Explore(C, D, A)` picked `e7`
+ //
+ // Thus the computation is (since D is {e1, e5} [see call 5])
+ //
+ // Alt(C, D + {e}) --> Alt({e0, e4}, {e1, e5, e7})
+ //
+ // where U is given above. There are no alternatives again in this case
+ // since all `e9` conflicts with `e4` and all other events of `U`
+ // are eliminated since their history intersects `D`
+ const Configuration C{e0_handle, e4_handle};
+ const EventSet D_plus_e{e1_handle, e5_handle, e7_handle};
+
+ REQUIRE(U.empty());
+ U.insert(std::move(e0));
+ U.insert(std::move(e1));
+ U.insert(std::move(e2));
+ U.insert(std::move(e3));
+ U.insert(std::move(e4));
+ U.insert(std::move(e6));
+ U.insert(std::move(e7));
+ U.insert(std::move(e8));
+ U.insert(std::move(e9));
+
+ const auto alternative = C.compute_alternative_to(D_plus_e, U);
+ REQUIRE_FALSE(alternative.has_value());
+ }
+
+ SECTION("Alternative computation call 8")
+ {
+ // During the eigth call to Alt(C, D + {e}),
+ // UDPOR believes `U` to be the following:
+ //
+ // e0
+ // / / /
+ // e1 e4 e7
+ // / / // /
+ // / / e5 e8 e9
+ // e2 e3 /
+ // e6
+ //
+ // C := {e0} and `Explore(C, D, A)` picked `e4`. At this
+ // point, UDPOR finished its recursive search of {e0, e4}
+ // after having finished {e0, e1} prior.
+ //
+ // Thus the computation is (since D = {e1})
+ //
+ // Alt(C, D + {e}) --> Alt({e0}, {e1, e4})
+ //
+ // where U is given above. There is one alternative in this
+ // case, viz {e0, e7, e9} since
+ // 1. e9 conflicts with e4 in D
+ // 2. e7 conflicts with e1 in D
+ // 3. the set {e7, e9} is conflict-free since `e7 < e9`
+ // 4. all other events are eliminated since their histories
+ // intersect D
+ //
+ // UDPOR will continue its recursive search following `e7`
+ // and add `e4` to D
+ const Configuration C{e0_handle};
+ const EventSet D_plus_e{e1_handle, e4_handle};
+
+ REQUIRE(U.empty());
+ U.insert(std::move(e0));
+ U.insert(std::move(e1));
+ U.insert(std::move(e2));
+ U.insert(std::move(e3));
+ U.insert(std::move(e4));
+ U.insert(std::move(e6));
+ U.insert(std::move(e7));
+ U.insert(std::move(e8));
+ U.insert(std::move(e9));
+
+ const auto alternative = C.compute_alternative_to(D_plus_e, U);
+ REQUIRE(alternative.has_value());
+ REQUIRE(alternative.value().get_events() == EventSet({e0_handle, e7_handle, e9_handle}));
+ }
+
+ SECTION("Alternative computation call 9")
+ {
+ // During the ninth call to Alt(C, D + {e}),
+ // UDPOR believes `U` to be the following:
+ //
+ // e0
+ // / / /
+ // e1 e4 e7
+ // / / // /
+ // / / e5 e8 e9
+ // e2 e3 / /
+ // e6 e10
+ //
+ // C := {e0, e7, e9} and `Explore(C, D, A)` picked `e10`.
+ // (since en(C') where C' := {e0, e7, e9, e10} is empty
+ // [so UDPOR will simply return when C' is reached]).
+ //
+ // Thus the computation is (since D = {e1, e4} [see the previous step])
+ //
+ // Alt(C, D + {e}) --> Alt({e0}, {e1, e4, e10})
+ //
+ // where U is given above. There are no alternatives in this case
+ const Configuration C{e0_handle, e7_handle, e9_handle};
+ const EventSet D_plus_e{e1_handle, e4_handle, e10_handle};
+
+ REQUIRE(U.empty());
+ U.insert(std::move(e0));
+ U.insert(std::move(e1));
+ U.insert(std::move(e2));
+ U.insert(std::move(e3));
+ U.insert(std::move(e4));
+ U.insert(std::move(e6));
+ U.insert(std::move(e7));
+ U.insert(std::move(e8));
+ U.insert(std::move(e9));
+ U.insert(std::move(e10));
+
+ const auto alternative = C.compute_alternative_to(D_plus_e, U);
+ REQUIRE_FALSE(alternative.has_value());
+ }
+
+ SECTION("Alternative computation call 10")
+ {
+ // During the tenth call to Alt(C, D + {e}),
+ // UDPOR believes `U` to be the following:
+ //
+ // e0
+ // / / /
+ // e1 e4 e7
+ // / / // /
+ // / / e5 e8 e9
+ // e2 e3 / /
+ // e6 e10
+ //
+ // C := {e0, e7} and `Explore(C, D, A)` picked `e9`.
+ //
+ // Thus the computation is (since D = {e1, e4} [see call 8])
+ //
+ // Alt(C, D + {e}) --> Alt({e0}, {e1, e4, e9})
+ //
+ // where U is given above. There are no alternatives in this case
+ const Configuration C{e0_handle, e7_handle};
+ const EventSet D_plus_e{e1_handle, e4_handle, e9_handle};
+
+ REQUIRE(U.empty());
+ U.insert(std::move(e0));
+ U.insert(std::move(e1));
+ U.insert(std::move(e2));
+ U.insert(std::move(e3));
+ U.insert(std::move(e4));
+ U.insert(std::move(e6));
+ U.insert(std::move(e7));
+ U.insert(std::move(e8));
+ U.insert(std::move(e9));
+ U.insert(std::move(e10));
+
+ const auto alternative = C.compute_alternative_to(D_plus_e, U);
+ REQUIRE_FALSE(alternative.has_value());
+ }
+
+ SECTION("Alternative computation call 11 (final call)")
+ {
+ // During the eleventh and final call to Alt(C, D + {e}),
+ // UDPOR believes `U` to be the following:
+ //
+ // e0
+ // / / /
+ // e1 e4 e7
+ // / / // /
+ // / / e5 e8 e9
+ // e2 e3 / /
+ // e6 e10
+ //
+ // C := {e0} and `Explore(C, D, A)` picked `e7`.
+ //
+ // Thus the computation is (since D = {e1, e4} [see call 8])
+ //
+ // Alt(C, D + {e}) --> Alt({e0}, {e1, e4, e7})
+ //
+ // where U is given above. There are no alternatives in this case:
+ // everyone is eliminated!
+ const Configuration C{e0_handle, e7_handle};
+ const EventSet D_plus_e{e1_handle, e4_handle, e9_handle};
+
+ REQUIRE(U.empty());
+ U.insert(std::move(e0));
+ U.insert(std::move(e1));
+ U.insert(std::move(e2));
+ U.insert(std::move(e3));
+ U.insert(std::move(e4));
+ U.insert(std::move(e6));
+ U.insert(std::move(e7));
+ U.insert(std::move(e8));
+ U.insert(std::move(e9));
+ U.insert(std::move(e10));
+
+ const auto alternative = C.compute_alternative_to(D_plus_e, U);
+ REQUIRE_FALSE(alternative.has_value());
+ }
+
+ SECTION("Alternative computation next")
+ {
+ SECTION("Followed {e0, e7} first")
+ {
+ const EventSet D{e1_handle, e7_handle};
+ const Configuration C{e0_handle};
+
+ REQUIRE(U.empty());
+ U.insert(std::move(e0));
+ U.insert(std::move(e1));
+ U.insert(std::move(e2));
+ U.insert(std::move(e3));
+ U.insert(std::move(e4));
+ U.insert(std::move(e5));
+ U.insert(std::move(e7));
+ U.insert(std::move(e8));
+ U.insert(std::move(e9));
+ U.insert(std::move(e10));
+
+ const auto alternative = C.compute_alternative_to(D, U);
+ REQUIRE(alternative.has_value());
+
+ // In this case, only {e0, e4} is a valid alternative
+ REQUIRE(alternative.value().get_events() == EventSet({e0_handle, e4_handle, e5_handle}));
+ }
+
+ SECTION("Followed {e0, e4} first")
+ {
+ const EventSet D{e1_handle, e4_handle};
+ const Configuration C{e0_handle};
+
+ REQUIRE(U.empty());
+ U.insert(std::move(e0));
+ U.insert(std::move(e1));
+ U.insert(std::move(e2));
+ U.insert(std::move(e3));
+ U.insert(std::move(e4));
+ U.insert(std::move(e5));
+ U.insert(std::move(e6));
+ U.insert(std::move(e7));
+ U.insert(std::move(e8));
+ U.insert(std::move(e9));
+
+ const auto alternative = C.compute_alternative_to(D, U);
+ REQUIRE(alternative.has_value());
+
+ // In this case, only {e0, e7} is a valid alternative
+ REQUIRE(alternative.value().get_events() == EventSet({e0_handle, e7_handle, e9_handle}));
+ }
+ }
}
\ No newline at end of file
return make_union(config.get_events());
}
+EventSet EventSet::get_local_config() const
+{
+ return History(*this).get_all_events();
+}
+
size_t EventSet::size() const
{
return this->events_.size();
return std::all_of(history.begin(), history.end(), [=](const UnfoldingEvent* e) { return this->contains(e); });
}
+bool EventSet::intersects(const History& history) const
+{
+ return std::any_of(history.begin(), history.end(), [=](const UnfoldingEvent* e) { return this->contains(e); });
+}
+
bool EventSet::is_maximal() const
{
// A set of events is maximal if no event from
EventSet make_union(const UnfoldingEvent*) const;
EventSet make_union(const EventSet&) const;
EventSet make_union(const Configuration&) const;
+ EventSet get_local_config() const;
size_t size() const;
bool empty() const;
bool contains(const UnfoldingEvent*) const;
bool contains(const History&) const;
+ bool intersects(const History&) const;
bool is_subset_of(const EventSet&) const;
bool operator==(const EventSet& other) const { return this->events_ == other.events_; }
namespace simgrid::mc::udpor {
+void Unfolding::remove(const EventSet& events)
+{
+ for (const auto e : events) {
+ remove(e);
+ }
+}
+
void Unfolding::remove(const 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);
+ this->event_handles.remove(e);
}
void Unfolding::insert(std::unique_ptr<UnfoldingEvent> e)
}
// Map the handle to its owner
+ this->event_handles.insert(handle);
this->global_events_[handle] = std::move(e);
}
{
// Notice the use of `==` equality here. `e` may not be contained in the
// unfolding; but some event which is "equivalent" to it could be.
- for (const auto& [event, _] : global_events_) {
+ for (const auto event : *this) {
if (*event == *e) {
return true;
}
return false;
}
+EventSet Unfolding::get_immediate_conflicts_of(const UnfoldingEvent* e) const
+{
+ EventSet immediate_conflicts;
+ for (const auto event : *this) {
+ if (event->immediately_conflicts_with(e)) {
+ immediate_conflicts.insert(e);
+ }
+ }
+ return immediate_conflicts;
+}
+
} // namespace simgrid::mc::udpor
#ifndef SIMGRID_MC_UDPOR_UNFOLDING_HPP
#define SIMGRID_MC_UDPOR_UNFOLDING_HPP
+#include "src/mc/explo/udpor/EventSet.hpp"
#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
#include "src/mc/explo/udpor/udpor_forward.hpp"
*/
std::unordered_map<const UnfoldingEvent*, std::unique_ptr<UnfoldingEvent>> global_events_;
+ /**
+ * @brief: The collection of events in the unfolding
+ *
+ * @invariant: All of the events in this set are elements of `global_events_`
+ * and is kept updated at the same time as `global_events_`
+ */
+ EventSet event_handles;
+
+ /**
+ * @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.
+ *
+ * @note: The current implementation does not touch the set `G`. Its use is perhaps
+ * limited to debugging and/or model-checking acyclic state spaces
+ */
+ EventSet G;
+
public:
Unfolding() = default;
Unfolding& operator=(Unfolding&&) = default;
Unfolding(Unfolding&&) = default;
void remove(const UnfoldingEvent* e);
+ void remove(const EventSet& events);
void insert(std::unique_ptr<UnfoldingEvent> e);
bool contains_event_equivalent_to(const UnfoldingEvent* e) const;
+ auto begin() const { return this->event_handles.begin(); }
+ auto end() const { return this->event_handles.end(); }
+ auto cbegin() const { return this->event_handles.cbegin(); }
+ auto cend() const { return this->event_handles.cend(); }
size_t size() const { return this->global_events_.size(); }
bool empty() const { return this->global_events_.empty(); }
+
+ /// @brief Computes "#ⁱ_U(e)" for the given event
+ EventSet get_immediate_conflicts_of(const UnfoldingEvent*) const;
};
} // namespace simgrid::mc::udpor
bool UnfoldingEvent::operator==(const UnfoldingEvent& other) const
{
- // Must be run by the same actor
- if (associated_transition->aid_ != other.associated_transition->aid_)
- return false;
-
- // If run by the same actor, must be the same _step_ of that actor's
- // execution
-
- // 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
+ // Two events are equivalent iff:
+ // 1. they have the same action
+ // 2. they have the same history
+ //
+ // NOTE: 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;
+ return associated_transition->aid_ == other.associated_transition->aid_ &&
+ associated_transition->type_ == other.associated_transition->type_ &&
+ associated_transition->times_considered_ == other.associated_transition->times_considered_ &&
+ this->immediate_causes == other.immediate_causes;
}
EventSet UnfoldingEvent::get_history() const
bool in_history_of(const UnfoldingEvent* other) const;
bool related_to(const UnfoldingEvent* other) const;
+ /// @brief Whether or not this event is in conflict with
+ /// the given one (i.e. whether `this # other`)
bool conflicts_with(const UnfoldingEvent* other) const;
+
+ /// @brief Whether or not this event is in conflict with
+ /// any event in the given configuration
bool conflicts_with(const Configuration& config) const;
+
+ /// @brief Computes "this #ⁱ other"
bool immediately_conflicts_with(const UnfoldingEvent* other) const;
bool is_dependent_with(const Transition*) const;
bool is_dependent_with(const UnfoldingEvent* other) const;
#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
#include "src/mc/explo/udpor/udpor_tests_private.hpp"
+using namespace simgrid::mc;
using namespace simgrid::mc::udpor;
+TEST_CASE("simgrid::mc::udpor::UnfoldingEvent: Semantic Equivalence Tests")
+{
+ UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+ UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+ UnfoldingEvent e3(EventSet({&e1}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+ UnfoldingEvent e4(EventSet({&e1}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+
+ UnfoldingEvent e5(EventSet({&e1, &e3, &e2}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+ UnfoldingEvent e6(EventSet({&e1, &e3, &e2}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+ UnfoldingEvent e7(EventSet({&e1, &e3, &e2}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+
+ SECTION("Equivalence is an equivalence relation")
+ {
+ SECTION("Equivalence is reflexive")
+ {
+ REQUIRE(e1 == e1);
+ REQUIRE(e2 == e2);
+ REQUIRE(e3 == e3);
+ REQUIRE(e4 == e4);
+ }
+
+ SECTION("Equivalence is symmetric")
+ {
+ REQUIRE(e2 == e3);
+ REQUIRE(e3 == e2);
+ REQUIRE(e3 == e4);
+ REQUIRE(e4 == e3);
+ REQUIRE(e2 == e4);
+ REQUIRE(e4 == e2);
+ }
+
+ SECTION("Equivalence is transitive")
+ {
+ REQUIRE(e2 == e3);
+ REQUIRE(e3 == e4);
+ REQUIRE(e2 == e4);
+ REQUIRE(e5 == e6);
+ REQUIRE(e6 == e7);
+ REQUIRE(e5 == e7);
+ }
+ }
+
+ SECTION("Equivalence fails with different actors")
+ {
+ UnfoldingEvent e1_diff_actor(EventSet(), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1, 0));
+ UnfoldingEvent e2_diff_actor(EventSet({&e1}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1, 0));
+ UnfoldingEvent e5_diff_actor(EventSet({&e1, &e3, &e2}),
+ std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1, 0));
+ REQUIRE(e1 != e1_diff_actor);
+ REQUIRE(e1 != e2_diff_actor);
+ REQUIRE(e1 != e5_diff_actor);
+ }
+
+ SECTION("Equivalence fails with different transition types")
+ {
+ // NOTE: We're comparing the transition `type_` field directly. To avoid
+ // modifying the `Type` enum that exists in `Transition` just for the tests,
+ // we instead provide different values of `Transition::Type` to simulate
+ // the different types
+ UnfoldingEvent e1_diff_transition(EventSet(),
+ std::make_shared<IndependentAction>(Transition::Type::ACTOR_JOIN, 0, 0));
+ UnfoldingEvent e2_diff_transition(EventSet({&e1}),
+ std::make_shared<IndependentAction>(Transition::Type::ACTOR_JOIN, 0, 0));
+ UnfoldingEvent e5_diff_transition(EventSet({&e1, &e3, &e2}),
+ std::make_shared<IndependentAction>(Transition::Type::ACTOR_JOIN, 0, 0));
+ REQUIRE(e1 != e1_diff_transition);
+ REQUIRE(e1 != e2_diff_transition);
+ REQUIRE(e1 != e5_diff_transition);
+ }
+
+ SECTION("Equivalence fails with different `times_considered`")
+ {
+ // With a different number for `times_considered`, we know
+ UnfoldingEvent e1_diff_considered(EventSet(), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 1));
+ UnfoldingEvent e2_diff_considered(EventSet({&e1}),
+ std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 1));
+ UnfoldingEvent e5_diff_considered(EventSet({&e1, &e3, &e2}),
+ std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 1));
+ REQUIRE(e1 != e1_diff_considered);
+ REQUIRE(e1 != e2_diff_considered);
+ REQUIRE(e1 != e5_diff_considered);
+ }
+
+ SECTION("Equivalence fails with different immediate histories of events")
+ {
+ UnfoldingEvent e1_diff_hist(EventSet({&e2}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+ UnfoldingEvent e2_diff_hist(EventSet({&e3}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+ UnfoldingEvent e5_diff_hist(EventSet({&e1, &e2}),
+ std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+ REQUIRE(e1 != e1_diff_hist);
+ REQUIRE(e1 != e2_diff_hist);
+ REQUIRE(e1 != e5_diff_hist);
+ }
+}
+
TEST_CASE("simgrid::mc::udpor::UnfoldingEvent: Dependency/Conflict Tests")
{
SECTION("Properties of the relations")
#include "src/mc/explo/udpor/Unfolding.hpp"
#include "src/mc/explo/udpor/udpor_tests_private.hpp"
+using namespace simgrid::mc;
using namespace simgrid::mc::udpor;
TEST_CASE("simgrid::mc::udpor::Unfolding: Creating an unfolding")
unfolding.remove(e2_handle);
REQUIRE(unfolding.size() == 0);
REQUIRE(unfolding.empty());
-}
\ No newline at end of file
+}
+
+TEST_CASE("simgrid::mc::udpor::Unfolding: Checking for semantically equivalent events")
+{
+ Unfolding unfolding;
+ auto e1 = std::make_unique<UnfoldingEvent>(
+ EventSet(), std::make_shared<IndependentAction>(Transition::Type::BARRIER_ASYNC_LOCK, 6, 2));
+ auto e2 = std::make_unique<UnfoldingEvent>(
+ EventSet(), std::make_shared<IndependentAction>(Transition::Type::BARRIER_ASYNC_LOCK, 6, 2));
+
+ // e1 and e2 are equivalent
+ REQUIRE(*e1 == *e2);
+
+ const auto e1_handle = e1.get();
+ const auto e2_handle = e2.get();
+ unfolding.insert(std::move(e1));
+
+ REQUIRE(unfolding.contains_event_equivalent_to(e1_handle));
+ REQUIRE(unfolding.contains_event_equivalent_to(e2_handle));
+}
+
+TEST_CASE("simgrid::mc::udpor::Unfolding: Checking all immediate conflicts restricted to an unfolding") {}
\ No newline at end of file
#ifndef SIMGRID_MC_UDPOR_TEST_PRIVATE_HPP
#define SIMGRID_MC_UDPOR_TEST_PRIVATE_HPP
+#include "src/mc/transition/Transition.hpp"
+
namespace simgrid::mc::udpor {
struct IndependentAction : public Transition {
+ IndependentAction() = default;
+ IndependentAction(Type type, aid_t issuer, int times_considered) : Transition(type, issuer, times_considered) {}
+
// Independent with everyone else
bool depends(const Transition* other) const override { return false; }
};
struct DependentAction : public Transition {
+ DependentAction() = default;
+ DependentAction(Type type, aid_t issuer, int times_considered) : Transition(type, issuer, times_considered) {}
+
// Dependent with everyone else (except IndependentAction)
bool depends(const Transition* other) const override
{
};
struct ConditionallyDependentAction : public Transition {
+ ConditionallyDependentAction() = default;
+ ConditionallyDependentAction(Type type, aid_t issuer, int times_considered)
+ : Transition(type, issuer, times_considered)
+ {
+ }
+
// Dependent only with DependentAction (i.e. not itself)
bool depends(const Transition* other) const override
{
src/mc/explo/LivenessChecker.hpp
src/mc/explo/UdporChecker.cpp
src/mc/explo/UdporChecker.hpp
-
+
+ src/mc/explo/udpor/Comb.hpp
src/mc/explo/udpor/Configuration.hpp
src/mc/explo/udpor/Configuration.cpp
src/mc/explo/udpor/EventSet.cpp
