for (const auto& [aid, actor_state] : stateC.get_actors_list()) {
for (const auto& transition : actor_state.get_enabled_transitions()) {
- EventSet extension = ExtensionSetCalculator::partially_extend(C, unfolding, transition);
+ EventSet extension = ExtensionSetCalculator::partially_extend(C, &unfolding, transition);
exC.form_union(extension);
}
}
return std::any_of(history.begin(), history.end(), [=](const UnfoldingEvent* e) { return this->contains(e); });
}
+EventSet EventSet::get_largest_maximal_subset() const
+{
+ const History history(*this);
+ return history.get_all_maximal_events();
+}
+
bool EventSet::is_maximal() const
{
// A set of events is maximal if no event from
// the original set is ruled out when traversing
// the history of the events
- const History history(*this);
- return *this == history.get_all_maximal_events();
+ return *this == this->get_largest_maximal_subset();
}
bool EventSet::is_conflict_free() const
*/
bool is_conflict_free() const;
+ /**
+ * @brief Produces the largest subset of this
+ * set of events which is maximal
+ */
+ EventSet get_largest_maximal_subset() const;
+
/**
* @brief Orders the events of the set such that
* "more recent" events (i.e. those that are farther down in
* under the terms of the license (GNU LGPL) which comes with this package. */
#include "src/mc/explo/udpor/ExtensionSetCalculator.hpp"
+#include "src/mc/explo/udpor/Configuration.hpp"
+#include "src/mc/explo/udpor/History.hpp"
+#include "src/mc/explo/udpor/Unfolding.hpp"
#include <functional>
#include <unordered_map>
namespace simgrid::mc::udpor {
-EventSet ExtensionSetCalculator::partially_extend(const Configuration& C, const Unfolding& U,
+EventSet ExtensionSetCalculator::partially_extend(const Configuration& C, Unfolding* U,
const std::shared_ptr<Transition> action)
{
switch (action->type_) {
}
}
-EventSet ExtensionSetCalculator::partially_extend_CommSend(const Configuration& C, const Unfolding& U,
- const std::shared_ptr<CommSendTransition> action)
+EventSet ExtensionSetCalculator::partially_extend_CommSend(const Configuration& C, Unfolding* U,
+ const std::shared_ptr<CommSendTransition> send_action)
{
- return EventSet();
+ EventSet exC;
+
+ // TODO: if this is the first action by the actor, no such previous event exists.
+ // How do we react here? Do we say we're dependent with the root event?
+ const unsigned sender_mailbox = send_action->get_mailbox();
+ const auto pre_event_a_C = C.pre_event(send_action->aid_).value();
+
+ // 1. Create `e' := <a, config(preEvt(a, C))>` and add `e'` to `ex(C)`
+ const auto e_prime = U->discover_event(EventSet({pre_event_a_C}), send_action);
+ exC.insert(e_prime);
+
+ // 2. foreach e ∈ C s.t. λ(e) ∈ {AsyncSend(m, _), TestAny(Com)} where
+ // Com contains a matching c' = AsyncReceive(m, _) with a
+ for (const auto e : C) {
+ const bool transition_type_check = [&]() {
+ if (const auto* async_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
+ e != nullptr && async_send->get_mailbox() == sender_mailbox) {
+ return true;
+ } else if (const auto* e_test_any = dynamic_cast<const CommTestTransition*>(e->get_transition());
+ e_test_any != nullptr) {
+ // TODO: Check if there's a way to find a matching AsyncReceive -> matching when? in the history?
+ return true;
+ }
+ return false;
+ }();
+
+ if (transition_type_check) {
+ const EventSet K = EventSet({e, pre_event_a_C}).get_largest_maximal_subset();
+
+ // TODO: How do we compute D_K(a, b)? There's a specialized
+ // function for each case it appears, but I don't see where
+ // `config(K)` comes in
+ if (false) {
+ const auto e_prime = U->discover_event(std::move(K), send_action);
+ exC.insert(e_prime);
+ }
+ }
+ }
+
+ return exC;
}
-EventSet ExtensionSetCalculator::partially_extend_CommRecv(const Configuration& C, const Unfolding& U,
- const std::shared_ptr<CommRecvTransition> action)
+EventSet ExtensionSetCalculator::partially_extend_CommRecv(const Configuration& C, Unfolding* U,
+ const std::shared_ptr<CommRecvTransition> recv_action)
{
return EventSet();
}
-EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration&, const Unfolding& U,
- std::shared_ptr<CommWaitTransition>)
+EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration&, Unfolding* U,
+ std::shared_ptr<CommWaitTransition> wait_action)
{
return EventSet();
}
-EventSet ExtensionSetCalculator::partially_extend_CommTest(const Configuration&, const Unfolding& U,
- std::shared_ptr<CommTestTransition>)
+EventSet ExtensionSetCalculator::partially_extend_CommTest(const Configuration&, Unfolding* U,
+ std::shared_ptr<CommTestTransition> test_action)
{
return EventSet();
+ // EventSet exC;
+
+ // // TODO: if this is the first action by the actor, no such previous event exists.
+ // // How do we react here? Do we say we're dependent with the root event?
+ // const auto tested_mailbox = test_action->get_mailbox();
+ // const auto pre_event_a_C = C.pre_event(send_action->aid_).value();
+
+ // for (const auto e : C) {
+ // if (e == pre_event_a_C) {
+ // const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), action);
+ // exC.insert(e_prime);
+ // } else {
+ // // TODO: Check condition
+ // const bool should_process = [&]() { return false; }();
+
+ // EventSet K;
+ // if (not(e < pre_event_a_C))
+ // K.insert(e);
+ // if (not(pre_event_a_C < e))
+ // K.insert(pre_event_a_C);
+
+ // // TODO: How do we compute D_K(a, b)? There's a specialized
+ // // function for each case it appears, but I don't see where
+ // // `config(K)` comes in
+ // if (should_process) {
+ // const auto e_prime = U->discover_event(std::move(K), action);
+ // exC.insert(e_prime);
+ // }
+ // }
+ // }
}
} // namespace simgrid::mc::udpor
\ No newline at end of file
*/
struct ExtensionSetCalculator final {
private:
- static EventSet partially_extend_CommSend(const Configuration&, const Unfolding&,
- std::shared_ptr<CommSendTransition>);
- static EventSet partially_extend_CommRecv(const Configuration&, const Unfolding&,
- std::shared_ptr<CommRecvTransition>);
- static EventSet partially_extend_CommWait(const Configuration&, const Unfolding&,
- std::shared_ptr<CommWaitTransition>);
- static EventSet partially_extend_CommTest(const Configuration&, const Unfolding&,
- std::shared_ptr<CommTestTransition>);
+ static EventSet partially_extend_CommSend(const Configuration&, Unfolding*, std::shared_ptr<CommSendTransition>);
+ static EventSet partially_extend_CommRecv(const Configuration&, Unfolding*, std::shared_ptr<CommRecvTransition>);
+ static EventSet partially_extend_CommWait(const Configuration&, Unfolding*, std::shared_ptr<CommWaitTransition>);
+ static EventSet partially_extend_CommTest(const Configuration&, Unfolding*, std::shared_ptr<CommTestTransition>);
public:
- static EventSet partially_extend(const Configuration&, const Unfolding&, const std::shared_ptr<Transition>);
+ static EventSet partially_extend(const Configuration&, Unfolding*, const std::shared_ptr<Transition>);
};
} // namespace simgrid::mc::udpor
#include <boost/iterator/iterator_facade.hpp>
#include <functional>
+#include <initializer_list>
#include <optional>
namespace simgrid::mc::udpor {
History& operator=(History const&) = default;
History(History&&) = default;
- explicit History(EventSet event_set = EventSet()) : events_(std::move(event_set)) {}
explicit History(const UnfoldingEvent* e) : events_({e}) {}
+ explicit History(EventSet event_set = EventSet()) : events_(std::move(event_set)) {}
+ explicit History(std::initializer_list<const UnfoldingEvent*> list) : events_(std::move(list)) {}
auto begin() const { return Iterator(events_); }
auto end() const { return Iterator(EventSet()); }
/// in the unfolding
const UnfoldingEvent* insert(std::unique_ptr<UnfoldingEvent> e);
- /// @brief Computes "#ⁱ_U(e)" for the given event
+ /**
+ * @brief Informs the unfolding of a (potentially) new event
+ *
+ * The unfolding of a concurrent program is a well-defined
+ * structure. Given the labeled transition system (LTS) of
+ * a program, the unfolding of that program can be determined
+ * algorithmically. However, UDPOR does not a priori know the structure of the
+ * unfolding as it performs its exploration. Thus, events in the
+ * unfolding are "discovered" as they are encountered, specifically
+ * when computing the extension sets of the configurations that
+ * UDPOR decides to search.
+ *
+ * This lends itself to the following problem: the extension sets
+ * of two different configurations may overlap one another. That
+ * is, for two configurations C and C' explored by UDPOR where C != C',
+ *
+ * ex(C) - ex(C') != empty
+ *
+ * Hence, when extending both `C` and `C'`, any events contained in
+ * the intersection of ex(C) and ex(C') will be attempted to be added
+ * twice. The unfolding will notice that these events have already
+ * been added and simply return the event already added to the unfolding
+ *
+ * @tparam ...Args arguments passed to the `UnfoldingEvent` constructor
+ * @return the handle to either the newly created event OR
+ * to an equivalent event that was already noted by the unfolding
+ * at some point in the past
+ */
+ template <typename... Args> const UnfoldingEvent* discover_event(Args... args)
+ {
+ auto candidate_event = std::make_unique<UnfoldingEvent>(std::forward<Args>(args)...);
+ return insert(std::move(candidate_event));
+ }
+
+ /// @brief Computes "#ⁱ_U(e)" for the given event, where `U` is the set
+ /// of the events in this unfolding
EventSet get_immediate_conflicts_of(const UnfoldingEvent*) const;
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
+ * i.e. the unique pointer that manages the data at 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
*/
*
* @invariant: All of the events in this set are elements of `global_events_`
* and is kept updated at the same time as `global_events_`
+ *
+ * @note: This is for the convenience of iteration over the unfolding
*/
EventSet event_handles;
bool UnfoldingEvent::operator==(const UnfoldingEvent& other) const
{
+ // Intrinsic identity check
+ if (this == &other) {
+ return true;
+ }
// Two events are equivalent iff:
// 1. they have the same action
// 2. they have the same history
EventSet get_history() const;
bool in_history_of(const UnfoldingEvent* other) const;
+
+ /**
+ * @brief Whether or not the given event is a decendant
+ * of or an ancestor of the given event
+ */
bool related_to(const UnfoldingEvent* other) const;
/// @brief Whether or not this event is in conflict with
