#include "src/mc/explo/UdporChecker.hpp"
#include "src/mc/api/State.hpp"
+#include "src/mc/explo/udpor/CompatibilityGraph.hpp"
#include <xbt/asserts.h>
#include <xbt/log.h>
//
// Then
//
- // ex(C) = ex(C' + {e_cur}) = ex(C') / {e_cur} + U{<a, K> : K is maximal, a depends on all of K, a enabled at K }
+ // ex(C) = ex(C' + {e_cur}) = ex(C') / {e_cur} +
+ // U{<a, K> : K is maximal, `a` depends on all of K, `a` enabled at K }
UnfoldingEvent* e_cur = C.get_latest_event();
EventSet exC = prev_exC;
exC.remove(e_cur);
}
EventSet enC;
+ // TODO: Compute enC based on conflict relations
return std::tuple<EventSet, EventSet>(exC, enC);
}
EventSet UdporChecker::compute_extension_by_enumeration(const Configuration& C, const Transition& action) const
{
- // TODO: Do something more interesting here
- return EventSet();
+ // Here we're computing the following:
+ //
+ // U{<a, K> : K is maximal, `a` depends on all of K, `a` enabled at K }
+ //
+ // where `a` is the `action` given to us.
+ EventSet incremental_exC;
+
+ // We only consider those combinations of events for which `action` is dependent with
+ // the action associated with any given event ("`a` depends on all of K")
+ const std::unique_ptr<CompatibilityGraph> G = C.make_compatibility_graph_filtered_on([=](UnfoldingEvent* e) {
+ const auto e_transition = e->get_transition();
+ return action.depends(e_transition);
+ });
+
+ // TODO: Now that the graph has been constructed, enumerate
+ // all possible k-cliques of the complement of G
+
+ // TODO: For each enumeration, check all possible
+ // combinations of selecting a single event from
+ // each set associated with the graph nodes
+
+ return incremental_exC;
}
void UdporChecker::move_to_stateCe(State& state, const UnfoldingEvent& e)
+/* Copyright (c) 2008-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/mc/explo/udpor/CompatibilityGraphNode.hpp"
+
+namespace simgrid::mc::udpor {
+
+CompatibilityGraphNode::CompatibilityGraphNode(std::unordered_set<CompatibilityGraphNode*> conflicts, EventSet events_)
+ : conflicts(std::move(conflicts)), events_(std::move(events_))
+{
+}
+
+} // namespace simgrid::mc::udpor
* associated with the node
*/
class CompatibilityGraphNode {
+private:
+ std::unordered_set<CompatibilityGraphNode*> conflicts;
+ EventSet events_;
+
public:
CompatibilityGraphNode(const CompatibilityGraphNode&) = default;
CompatibilityGraphNode& operator=(CompatibilityGraphNode const&) = default;
CompatibilityGraphNode(CompatibilityGraphNode&&) = default;
- CompatibilityGraphNode(std::unordered_set<CompatibilityGraphNode*> conflicts);
-
- void add_event(UnfoldingEvent* e);
+ CompatibilityGraphNode(std::unordered_set<CompatibilityGraphNode*> conflicts, EventSet events_ = EventSet());
-private:
- EventSet events_;
-
- /**
- * @brief The nodes with which this node is in conflict with
- */
- std::unordered_set<CompatibilityGraphNode*> conflicts;
+ void add_event(UnfoldingEvent* e) { this->events_.insert(e); }
+ const EventSet& get_events() const { return this->events_; }
};
} // namespace simgrid::mc::udpor
#include "src/mc/explo/udpor/Configuration.hpp"
#include "src/mc/explo/udpor/History.hpp"
#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
+#include "xbt/asserts.h"
#include <algorithm>
#include <stack>
return topological_events;
}
+std::unique_ptr<CompatibilityGraph>
+Configuration::make_compatibility_graph_filtered_on(std::function<bool(UnfoldingEvent*)> pred) const
+{
+ auto G = std::make_unique<CompatibilityGraph>();
+
+ std::unordered_map<UnfoldingEvent*, std::unordered_set<CompatibilityGraphNode*>> discovered_conflicts;
+ std::unordered_map<UnfoldingEvent*, CompatibilityGraphNode*> potential_placements;
+ std::unordered_map<UnfoldingEvent*, int> direct_children_count;
+
+ for (auto* e : get_topologically_sorted_events_of_reverse_graph()) {
+
+ // 1. Figure out where to place `e` in `G`
+
+ // Determine which nodes in the graph are in conflict
+ // with this event. These nodes would have been added by child
+ // events while iterating over the topological ordering of the reverse graph
+ const auto known_conflicts = discovered_conflicts.find(e);
+ const auto potential_placement = potential_placements.find(e);
+ const auto potential_child_count = direct_children_count.find(e);
+
+ const bool no_known_conflicts = known_conflicts == discovered_conflicts.end();
+ const bool no_known_placement = potential_placement == potential_placements.end();
+ const bool no_known_child_count = potential_child_count == direct_children_count.end();
+
+ const auto e_conflicts =
+ no_known_conflicts ? std::unordered_set<CompatibilityGraphNode*>() : std::move(known_conflicts->second);
+ const auto e_child_count = no_known_child_count ? 0 : potential_child_count->second;
+
+ CompatibilityGraphNode* e_placement = nullptr;
+
+ // The justification is as follows:
+ //
+ // no_known_placement:
+ // If nobody told us about a placement, we must either be a leaf event
+ // OR be the cause of an event that itself has more than one cause.
+ //
+ // child_count >= 2:
+ // If there are two or more events that this event causes,
+ // then we certainly must be part of a different compatibility
+ // graph node since
+ const bool new_placement_required = no_known_placement || e_child_count >= 2;
+
+ if (new_placement_required) {
+ auto new_graph_node = std::make_unique<CompatibilityGraphNode>(e_conflicts, EventSet({e}));
+ e_placement = new_graph_node.get();
+ G->insert(std::move(new_graph_node));
+ } else {
+ xbt_assert(e_child_count == 1, "An event was informed by an immediate child of placement in "
+ "the same compatibility graph node, yet the child did not inform "
+ "the parent about its precense");
+ // A child event told us this node can be in the
+ // same compatibility node in the graph G. Add ourselves now
+ e_placement = potential_placement->second;
+ e_placement->add_event(e);
+ }
+
+ // 2. Update the children of `e`
+
+ const EventSet& e_immediate_causes = e->get_immediate_causes();
+ if (e_immediate_causes.size() == 1) {
+ // If there is only a single ancestor, then it MAY BE in
+ // the same "chain" of events as us. Note that the ancestor must
+ // also have only a single child (see the note on `new_placement_required`)
+ UnfoldingEvent* only_ancestor = *e_immediate_causes.begin();
+ potential_placements[only_ancestor] = e_placement;
+ }
+
+ // Our ancestors conflict with everyone `e` does else PLUS `e` itself
+ auto parent_conflicts = std::move(e_conflicts);
+ parent_conflicts.insert(e_placement);
+ for (auto* cause : e_immediate_causes) {
+ direct_children_count[cause] += 1;
+ discovered_conflicts[cause] = parent_conflicts;
+ }
+
+ // This event will only ever be seen once in the
+ // topological ordering. Hence, its resources do not
+ // need to be kept around
+ discovered_conflicts.erase(e);
+ direct_children_count.erase(e);
+ potential_placements.erase(e);
+ }
+
+ return G;
+}
+
} // namespace simgrid::mc::udpor
#ifndef SIMGRID_MC_UDPOR_CONFIGURATION_HPP
#define SIMGRID_MC_UDPOR_CONFIGURATION_HPP
+#include "src/mc/explo/udpor/CompatibilityGraph.hpp"
#include "src/mc/explo/udpor/EventSet.hpp"
#include "src/mc/explo/udpor/udpor_forward.hpp"
+#include <functional>
#include <initializer_list>
#include <vector>
*/
std::vector<UnfoldingEvent*> get_topologically_sorted_events_of_reverse_graph() const;
+ /**
+ * @brief Construct a new compatibility graph from the events of the
+ * configuration whose associated transitions are dependent with the
+ * given action
+ *
+ * @param pred whether or not to even consider the unfolding event in any
+ * compatibility nodes of the resulting graph
+ * @returns a new compatibility graph that defines possible maximal subsets
+ * of events of C that satisfy the predicate `pred`
+ */
+ std::unique_ptr<CompatibilityGraph>
+ make_compatibility_graph_filtered_on(std::function<bool(UnfoldingEvent*)> pred) const;
+
private:
/**
* @brief The most recent event added to the configuration
