#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>
// 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_minus_C = compute_k_partial_alternative(D, C, K); J_minus_C.has_value()) {
// 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
restore_program_state_to(*stateC);
// Explore(C, D + {e}, J \ C)
- explore(C, D, std::move(J), std::move(stateC), std::move(prev_exC));
+ explore(C, D, std::move(J_minus_C.value()), std::move(stateC), std::move(prev_exC));
}
// D <-- D - {e}
}
}
}
-
return incremental_exC;
}
return nullptr;
}
-EventSet UdporChecker::compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const
+std::vector<const UnfoldingEvent*> UdporChecker::pick_k_partial_alternative_events(const EventSet& D,
+ const unsigned k) const
{
- // TODO: Compute k-partial alternatives using [2]
- return EventSet();
+ const unsigned size = std::min(k, static_cast<unsigned>(D.size()));
+ std::vector<const UnfoldingEvent*> D_hat(size);
+
+ // Potentially select intelligently here (e.g. perhaps pick events
+ // with transitions that we know are totally independent)...
+ //
+ // For now, simply pick the first `k` events (any subset suffices)
+ std::copy_n(D.begin(), size, D_hat.begin());
+ return D_hat;
+}
+
+std::optional<EventSet> UdporChecker::compute_k_partial_alternative(const EventSet& D, const Configuration& C,
+ const unsigned k) const
+{
+ // 1. Select k (of |D|, whichever is smaller) arbitrary events e_1, ..., e_k from D
+ const auto D_hat = pick_k_partial_alternative_events(D, k);
+
+ // 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
+ Comb comb(k);
+
+ for (const auto* e : this->unfolding) {
+ for (unsigned i = 0; i < k; i++) {
+ const auto& e_i = D_hat[i];
+ if (const auto e_local_config = History(e);
+ e_i->conflicts_with(e) and (not D.contains(e_local_config)) and C.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
+
+ 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 History(map_events(*alternative)).get_event_diff_with(C);
}
void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
* 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;
+ std::optional<EventSet> compute_k_partial_alternative(const EventSet& D, const Configuration& C,
+ const unsigned k) const;
+ std::vector<const UnfoldingEvent*> pick_k_partial_alternative_events(const EventSet& D, const unsigned k) const;
/**
*
#include "src/mc/explo/udpor/Comb.hpp"
+#include <boost/iterator/function_input_iterator.hpp>
+#include <boost/iterator/indirect_iterator.hpp>
#include <functional>
namespace simgrid::mc::udpor {
-auto Comb::combinations_begin() const
-{
- std::vector<std::reference_wrapper<const Spike>> references;
- std::transform(spikes.begin(), spikes.end(), std::back_inserter(references),
- [](const Spike& spike) { return std::cref(spike); });
- return simgrid::xbt::variable_for_loop<const Spike>(std::move(references));
-}
+// auto Comb::combinations_begin() const {}
-auto Comb::combinations_end() const
-{
- return simgrid::xbt::variable_for_loop<const Spike>();
-}
+// auto Comb::combinations_end() const {}
} // namespace simgrid::mc::udpor
\ No newline at end of file
/* 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
+#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 {
class Comb {
public:
explicit Comb(unsigned k) : k(k) {}
- Comb(const Comb& other) = default;
- Comb(const Comb&& other) = default;
- Comb& operator=(const Comb& other) = default;
- Comb& operator=(const Comb&& other) = default;
+ Comb(const Comb& other) = default;
+ Comb(Comb&& other) = default;
+ Comb& operator=(const Comb& other) = default;
+ Comb& operator=(Comb&& other) = default;
Spike& operator[](unsigned i) { return spikes[i]; }
const Spike& operator[](unsigned i) const { return spikes[i]; }
- auto combinations_begin() const;
- auto combinations_end() const;
+ auto combinations_begin() const
+ {
+ std::vector<std::reference_wrapper<const Spike>> references;
+ std::transform(spikes.begin(), spikes.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>(); }
auto begin() const { return spikes.begin(); }
auto end() const { return spikes.end(); }
{
}
+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()) {
}
}
+bool Configuration::is_compatible_with(const History& history) const
+{
+ return false;
+}
+
std::vector<const UnfoldingEvent*> Configuration::get_topologically_sorted_events() const
{
return this->events_.get_topological_ordering();
Configuration& operator=(Configuration const&) = default;
Configuration(Configuration&&) = default;
+ explicit Configuration(const UnfoldingEvent* event);
explicit Configuration(const EventSet& events);
explicit Configuration(std::initializer_list<const UnfoldingEvent*> events);
*/
void add_event(const UnfoldingEvent* e);
+ bool is_compatible_with(const UnfoldingEvent* e) const;
+
+ /**
+ * @brief Whether or not the events in the given history
+ * could be added to this configuration while preserving
+ * the configuration property
+ */
+ bool is_compatible_with(const History& history) const;
+
/**
* @brief Orders the events of the configuration such that
* "more recent" events (i.e. those that are farther down in
*/
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;
