include src/mc/explo/udpor/EventSet.cpp
include src/mc/explo/udpor/EventSet.hpp
include src/mc/explo/udpor/EventSet_test.cpp
+include src/mc/explo/udpor/ExtensionSet_test.cpp
include src/mc/explo/udpor/ExtensionSetCalculator.cpp
include src/mc/explo/udpor/ExtensionSetCalculator.hpp
include src/mc/explo/udpor/History.cpp
return this->events_.find(e) != this->events_.end();
}
+bool EventSet::contains_equivalent_to(const UnfoldingEvent* e) const
+{
+ return std::find_if(begin(), end(), [=](const UnfoldingEvent* e_in_set) { return *e == *e_in_set; }) != end();
+}
+
bool EventSet::is_subset_of(const EventSet& other) const
{
// If there is some element not contained in `other`, then
EventSet& operator=(EventSet&&) = default;
EventSet(EventSet&&) = default;
explicit EventSet(Configuration&& config);
- explicit EventSet(std::vector<const UnfoldingEvent*>&& raw_events) : events_(raw_events.begin(), raw_events.end())
- {
- xbt_assert(std::none_of(events_.begin(), events_.end(), [](const auto* e) { return e == nullptr; }), "Oh no");
- }
- explicit EventSet(std::unordered_set<const UnfoldingEvent*>&& raw_events) : events_(raw_events)
- {
- xbt_assert(std::none_of(events_.begin(), events_.end(), [](const auto* e) { return e == nullptr; }), "Oh no");
- }
- explicit EventSet(std::initializer_list<const UnfoldingEvent*> event_list) : events_(std::move(event_list))
- {
- xbt_assert(std::none_of(events_.begin(), events_.end(), [](const auto* e) { return e == nullptr; }), "Oh no");
- }
+ explicit EventSet(std::vector<const UnfoldingEvent*>&& raw_events) : events_(raw_events.begin(), raw_events.end()) {}
+ explicit EventSet(std::unordered_set<const UnfoldingEvent*>&& raw_events) : events_(raw_events) {}
+ explicit EventSet(std::initializer_list<const UnfoldingEvent*> event_list) : events_(std::move(event_list)) {}
auto begin() const { return this->events_.begin(); }
auto end() const { return this->events_.end(); }
size_t size() const;
bool empty() const;
+
bool contains(const UnfoldingEvent*) const;
bool contains(const History&) const;
+ bool contains_equivalent_to(const UnfoldingEvent*) const;
bool intersects(const EventSet&) const;
bool intersects(const History&) const;
bool is_subset_of(const EventSet&) const;
--- /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/ExtensionSetCalculator.hpp"
+#include "src/mc/explo/udpor/History.hpp"
+#include "src/mc/explo/udpor/Unfolding.hpp"
+
+using namespace simgrid::mc;
+using namespace simgrid::mc::udpor;
+
+TEST_CASE("simgrid::mc::udpor: Testing Computation with AsyncSend/AsyncReceive Only")
+{
+ // This test checks that the unfolding constructed for the very
+ // simple program described below is extended correctly. Each
+ // step of UDPOR is observed to ensure that computations are carried
+ // out correctly. The program described is simply:
+ //
+ // 1 2
+ // AsyncSend(m) AsyncRecv(m)
+ //
+ const int times_considered = 0;
+ const int tag = 0;
+ const unsigned mbox = 0;
+ const uintptr_t comm = 0;
+
+ Unfolding U;
+
+ SECTION("Computing ex({⊥}) with 1: AsyncSend")
+ {
+ // Consider the extension with `1: AsyncSend(m)`
+ Configuration C;
+ aid_t issuer = 1;
+ const uintptr_t sbuff = 0;
+ const size_t size = 100;
+
+ const auto async_send =
+ std::make_shared<CommSendTransition>(issuer, times_considered, comm, mbox, sbuff, size, tag);
+ const auto incremental_exC = ExtensionSetCalculator::partially_extend(C, &U, async_send);
+
+ // Check that the events have been added to `U`
+ REQUIRE(U.size() == 1);
+
+ // Make assertions about the contents of ex(C)
+ UnfoldingEvent e(EventSet(), async_send);
+ REQUIRE(incremental_exC.contains_equivalent_to(&e));
+ }
+
+ SECTION("Computing ex({⊥}) with 2: AsyncRecv")
+ {
+ // Consider the extension with `2: AsyncRecv(m)`
+ Configuration C;
+ aid_t issuer = 2;
+ const uintptr_t rbuff = 0;
+
+ const auto async_recv = std::make_shared<CommRecvTransition>(issuer, times_considered, comm, mbox, rbuff, tag);
+ const auto incremental_exC = ExtensionSetCalculator::partially_extend(C, &U, async_recv);
+
+ // Check that the events have been added to `U`
+ REQUIRE(U.size() == 1);
+
+ // Make assertions about the contents of ex(C)
+ UnfoldingEvent e(EventSet(), async_recv);
+ REQUIRE(incremental_exC.contains_equivalent_to(&e));
+ }
+}
\ No newline at end of file
return false; // Comm transitions are INDEP with non-comm transitions
}
+CommRecvTransition::CommRecvTransition(aid_t issuer, int times_considered, uintptr_t comm_, unsigned mbox_,
+ uintptr_t rbuff_, int tag_)
+ : Transition(Type::COMM_ASYNC_RECV, issuer, times_considered)
+ , comm_(comm_)
+ , mbox_(mbox_)
+ , rbuff_(rbuff_)
+ , tag_(tag_)
+{
+}
CommRecvTransition::CommRecvTransition(aid_t issuer, int times_considered, std::stringstream& stream)
: Transition(Type::COMM_ASYNC_RECV, issuer, times_considered)
{
return false; // Comm transitions are INDEP with non-comm transitions
}
+CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, uintptr_t comm_, unsigned mbox_,
+ uintptr_t sbuff_, size_t size_, int tag_)
+ : Transition(Type::COMM_ASYNC_SEND, issuer, times_considered)
+ , comm_(comm_)
+ , mbox_(mbox_)
+ , sbuff_(sbuff_)
+ , size_(size_)
+ , tag_(tag_)
+{
+}
CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, std::stringstream& stream)
: Transition(Type::COMM_ASYNC_SEND, issuer, times_considered)
{
int tag_;
public:
+ CommRecvTransition(aid_t issuer, int times_considered, uintptr_t comm_, unsigned mbox_, uintptr_t rbuff_, int tag_);
CommRecvTransition(aid_t issuer, int times_considered, std::stringstream& stream);
std::string to_string(bool verbose) const override;
bool depends(const Transition* other) const override;
int tag_;
public:
+ CommSendTransition(aid_t issuer, int times_considered, uintptr_t comm_, unsigned mbox_, uintptr_t sbuff_,
+ size_t size_, int tag_);
CommSendTransition(aid_t issuer, int times_considered, std::stringstream& stream);
std::string to_string(bool verbose) const override;
bool depends(const Transition* other) const override;
src/mc/sosp/PageStore_test.cpp
src/mc/explo/udpor/Unfolding_test.cpp
src/mc/explo/udpor/UnfoldingEvent_test.cpp
-
src/mc/explo/udpor/EventSet_test.cpp
+ src/mc/explo/udpor/ExtensionSet_test.cpp
src/mc/explo/udpor/History_test.cpp
src/mc/explo/udpor/Configuration_test.cpp)
