#include "src/mc/explo/udpor/Configuration.hpp"
#include "src/mc/explo/udpor/History.hpp"
#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
+#include "src/xbt/utils/iter/variable_for_loop.hpp"
-#include <iterator>
#include <stack>
+#include <vector>
namespace simgrid::mc::udpor {
return make_union(config.get_events());
}
+EventSet EventSet::make_intersection(const EventSet& other) const
+{
+ std::unordered_set<const UnfoldingEvent*> result;
+
+ for (const UnfoldingEvent* e : other.events_) {
+ if (contains(e)) {
+ result.insert(e);
+ }
+ }
+
+ return EventSet(std::move(result));
+}
+
+EventSet EventSet::get_local_config() const
+{
+ return History(*this).get_all_events();
+}
+
size_t EventSet::size() const
{
return this->events_.size();
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
/// which requires that all events have their history contained
/// in the set
const History history(*this);
- return this->contains(history);
+ return contains(history) && is_conflict_free();
}
bool EventSet::contains(const History& history) const
return std::all_of(history.begin(), history.end(), [=](const UnfoldingEvent* e) { return this->contains(e); });
}
-bool EventSet::is_maximal() const
+bool EventSet::intersects(const History& history) const
+{
+ return std::any_of(history.begin(), history.end(), [=](const UnfoldingEvent* e) { return this->contains(e); });
+}
+
+bool EventSet::intersects(const EventSet& other) const
+{
+ return std::any_of(other.begin(), other.end(), [=](const UnfoldingEvent* e) { return this->contains(e); });
+}
+
+EventSet EventSet::get_largest_maximal_subset() const
{
const History history(*this);
- return *this == history.get_all_maximal_events();
+ 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
+ return *this == this->get_largest_maximal_subset();
}
bool EventSet::is_conflict_free() const
{
- return false;
+ const auto begin = simgrid::xbt::variable_for_loop<const EventSet>{{*this}, {*this}};
+ const auto end = simgrid::xbt::variable_for_loop<const EventSet>();
+ return std::none_of(begin, end, [=](const auto event_pair) {
+ const UnfoldingEvent* e1 = *event_pair[0];
+ const UnfoldingEvent* e2 = *event_pair[1];
+ return e1->conflicts_with(e2);
+ });
}
std::vector<const UnfoldingEvent*> EventSet::get_topological_ordering() const
return topological_events;
}
+std::string EventSet::to_string() const
+{
+ std::string contents;
+
+ for (const auto* event : *this) {
+ contents += event->to_string();
+ contents += " + ";
+ }
+
+ return contents;
+}
+
+std::vector<const UnfoldingEvent*> EventSet::move_into_vector() const&&
+{
+ std::vector<const UnfoldingEvent*> contents;
+ contents.reserve(size());
+
+ for (auto&& event : *this) {
+ contents.push_back(event);
+ }
+
+ return contents;
+}
+
} // namespace simgrid::mc::udpor
\ No newline at end of file