include src/mc/transition/TransitionRandom.hpp
include src/mc/transition/TransitionSynchro.cpp
include src/mc/transition/TransitionSynchro.hpp
-include src/mc/explo/udpor/CompatibilityGraph.hpp
-include src/mc/explo/udpor/CompatibilityGraph.cpp
-include src/mc/explo/udpor/CompatibilityGraphNode.hpp
-include src/mc/explo/udpor/CompatibilityGraphNode.cpp
include src/mc/explo/udpor/Configuration.hpp
include src/mc/explo/udpor/Configuration.cpp
include src/mc/explo/udpor/EventSet.cpp
#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>
// 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([=](const 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
+ // Compute the extension set here using the algorithm Martin described...
return incremental_exC;
}
+++ /dev/null
-/* 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/CompatibilityGraph.hpp"
-
-#include <stdexcept>
-
-namespace simgrid::mc::udpor {
-
-// TODO: Remove duplication between the CompatibilityGraph
-// and the Unfolding: they are practically identical
-
-void CompatibilityGraph::remove(CompatibilityGraphNode* e)
-{
- if (e == nullptr) {
- throw std::invalid_argument("Expected a non-null pointer to an event, but received NULL");
- }
- this->nodes.erase(e);
-}
-
-void CompatibilityGraph::insert(std::unique_ptr<CompatibilityGraphNode> e)
-{
- CompatibilityGraphNode* handle = e.get();
- auto loc = this->nodes.find(handle);
- if (loc != this->nodes.end()) {
- // This is bad: someone wrapped the raw event address twice
- // in two different unique ptrs and attempted to
- // insert it into the unfolding...
- throw std::invalid_argument("Attempted to insert a node owned twice."
- "This will result in a double free error and must be fixed.");
- }
-
- // Map the handle to its owner
- this->nodes[handle] = std::move(e);
-}
-
-} // namespace simgrid::mc::udpor
+++ /dev/null
-/* Copyright (c) 2007-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. */
-
-#ifndef SIMGRID_MC_UDPOR_COMPATIBILITY_GRAPH_HPP
-#define SIMGRID_MC_UDPOR_COMPATIBILITY_GRAPH_HPP
-
-#include "src/mc/explo/udpor/CompatibilityGraphNode.hpp"
-#include "src/mc/explo/udpor/udpor_forward.hpp"
-
-#include <memory>
-#include <unordered_map>
-
-namespace simgrid::mc::udpor {
-
-/**
- * @brief A graph which describes the causal-conflicts between groups of
- * events from an unfolding
- *
- * A compatibility graph conceptually describes how causal "strands" of an
- * event structure are related to one another. Each node in the graph
- * represents a set of events from which only a single event could be selected
- * if creating a new subset of the events of an unfolding which is *causally-free*.
- * We say a set of events is *causally free* if and only if that set of events is a
- * maximal set of events (i.e., the two conditions are equivalent). We write
- * E(_node_) to denote the set of events associated with that node.
- *
- * The edges of the graph describe which "strands" are in causal conflict with one
- * another. That is, if (u, v) is an edge of compatibility graph G, then at
- * most one event from the set S(u) ∪ S(v) could be selected in a causally-free
- * subset of events of an unfolding.
- *
- * An important property of a compatibility graph G is that the cliques of
- * its complement graph G' (recall that the complement G' of a graph G is the
- * graph which has an edge (u,v) whenever G lacks an edge (u,v))
- * determine all possible combinations of events which are maximal events;
- * i.e., a clique of size `k` in G' is such that all maximal event sets
- * with events chosen from the union of all events mapped to each node in the
- * clique can be formed. Thus, the problem of determining sets of maximal
- * events of a configuration is equivalent to finding all possible cliques
- * of the compatibility graph. While this is an NP-complete problem in
- * general, it is still a (potentially major) refinement over checking
- * all possible subsets of events of the configuration directly.
- */
-class CompatibilityGraph {
-private:
- std::unordered_map<CompatibilityGraphNode*, std::unique_ptr<CompatibilityGraphNode>> nodes;
-
-public:
- CompatibilityGraph() = default;
- CompatibilityGraph& operator=(CompatibilityGraph&&) = default;
- CompatibilityGraph(CompatibilityGraph&&) = default;
-
- auto begin() const { return this->nodes.begin(); }
- auto end() const { return this->nodes.end(); }
-
- void remove(CompatibilityGraphNode* e);
- void insert(std::unique_ptr<CompatibilityGraphNode> e);
-
- size_t size() const { return this->nodes.size(); }
- bool empty() const { return this->nodes.empty(); }
-};
-
-} // namespace simgrid::mc::udpor
-#endif
\ No newline at end of file
+++ /dev/null
-/* 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"
-
-#include <algorithm>
-#include <numeric>
-
-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
+++ /dev/null
-/* Copyright (c) 2007-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. */
-
-#ifndef SIMGRID_MC_UDPOR_COMPATIBILITY_GRAPH_NODE_HPP
-#define SIMGRID_MC_UDPOR_COMPATIBILITY_GRAPH_NODE_HPP
-
-#include "src/mc/explo/udpor/EventSet.hpp"
-#include "src/mc/explo/udpor/udpor_forward.hpp"
-
-#include <initializer_list>
-#include <memory>
-#include <unordered_set>
-
-namespace simgrid::mc::udpor {
-
-/**
- * @brief A node in a `CompatabilityGraph` which describes which
- * combinations of events are in causal-conflict with the events
- * 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, EventSet events_ = EventSet());
-
- void add_event(UnfoldingEvent* e) { this->events_.insert(e); }
- const EventSet& get_events() const { return this->events_; }
- const std::unordered_set<CompatibilityGraphNode*>& get_conflicts() const { return this->conflicts; }
-};
-
-} // namespace simgrid::mc::udpor
-#endif
\ No newline at end of file
return topological_events;
}
-std::unique_ptr<CompatibilityGraph>
-Configuration::make_compatibility_graph_filtered_on(std::function<bool(const UnfoldingEvent*)> pred) const
-{
- auto G = std::make_unique<CompatibilityGraph>();
-
- struct UnfoldingEventSearchData {
- int immediate_children_count = 0;
- CompatibilityGraphNode* potential_placement = nullptr;
- std::unordered_set<CompatibilityGraphNode*> conflicts = std::unordered_set<CompatibilityGraphNode*>();
- };
- std::unordered_map<UnfoldingEvent*, UnfoldingEventSearchData> search_data;
-
- 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 e_search_data_loc = search_data.find(e);
- const bool e_has_no_search_data = e_search_data_loc == search_data.end();
- const auto e_search_data = e_has_no_search_data ? UnfoldingEventSearchData() : std::move(e_search_data_loc->second);
-
- const auto& e_conflicts = e_search_data.conflicts;
- const auto& e_potential_placement = e_search_data.potential_placement;
- const auto e_child_count = e_search_data.immediate_children_count;
-
- const bool e_should_appear = pred(e);
- CompatibilityGraphNode* e_placement = nullptr;
-
- if (e_should_appear) {
- // The justification is as follows:
- //
- // e_has_no_search_data:
- // The event `e` is a leaf node, so there are no prior
- // nodes in `G` to join
- //
- // child_count >= 2:
- // If there are two or more events that this event causes,
- // then we certainly must be part of a compatibility
- // graph node that conflicts with each of our children
- //
- // e_potential_placement == nullptr:
- // If nobody told us about a placement and yet still have search
- // data, this means means that our child `C` had more than one child itself,
- // so it we could not have moved into `C`'s _potential_ placement.
- const bool new_placement_required =
- e_has_no_search_data || e_child_count >= 2 || e_potential_placement == nullptr;
-
- 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 presence");
- // A child event told us this node can be in the
- // same compatibility node in the graph G. Add ourselves now
- e_placement = e_potential_placement;
- e_placement->add_event(e);
- }
- }
-
- // 2. Update the children of `e`
-
- const EventSet& e_immediate_causes = e->get_immediate_causes();
-
- // 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`).
- //
- // If there is more than one child, then each child is in conflict with `e`
- // so we don't potentially place it
- if (e_immediate_causes.size() == 1) {
- UnfoldingEvent* only_ancestor = *e_immediate_causes.begin();
-
- // If `e` is included in the graph, forward its placement on to
- // the sole child. Otherwise attempt to forward `e`'s _potential_
- // (potential is stressed) placement. We can only forward `e`'s
- // potential placement iff `e` has only a single child; for if
- // `e` had more children, then our sole ancestor would conflict with
- // each one of `e`'s children and thus couldn't be in the same group
- // as any of them
- if (e_should_appear) {
- search_data[only_ancestor].potential_placement = e_placement;
- } else {
- search_data[only_ancestor].potential_placement = e_child_count == 1 ? e_potential_placement : nullptr;
- }
- }
-
- // Our ancestors conflict with everyone `e` does else PLUS `e` itself
- // ONLY IF e actually was placed
- auto parent_conflicts = std::move(e_conflicts);
- if (e_should_appear) {
- parent_conflicts.insert(e_placement);
- }
- for (auto* cause : e_immediate_causes) {
- search_data[cause].immediate_children_count += 1;
-
- for (auto parent_conflict : parent_conflicts) {
- search_data[cause].conflicts.insert(parent_conflict);
- }
- }
-
- // This event will only ever be seen once in the
- // topological ordering. Hence, its resources do not
- // need to be kept around
- search_data.erase(e);
- }
-
- return G;
-}
-
-std::unique_ptr<CompatibilityGraph> Configuration::make_compatibility_graph() const
-{
- return make_compatibility_graph_filtered_on([=](const UnfoldingEvent*) { return true; });
-}
-
} // 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"
*/
std::vector<UnfoldingEvent*> get_topologically_sorted_events_of_reverse_graph() const;
- /**
- * @brief Construct a new compatibility graph from the events of the
- * configuration that satisfy the given predicate
- *
- * @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(const UnfoldingEvent*)> pred) const;
-
- /**
- * @brief Construct a new compatibility graph from the events of the
- * configuration
- *
- * @returns a new compatibility graph that defines possible maximal subsets
- * of events of C
- */
- std::unique_ptr<CompatibilityGraph> make_compatibility_graph() const;
-
private:
/**
* @brief The most recent event added to the configuration
namespace simgrid::mc::udpor {
class EventSet;
-class CompatabilityGraph;
-class CompatabilityGraphNode;
class Configuration;
class History;
class Unfolding;
src/mc/explo/UdporChecker.cpp
src/mc/explo/UdporChecker.hpp
- src/mc/explo/udpor/CompatibilityGraph.hpp
- src/mc/explo/udpor/CompatibilityGraph.cpp
- src/mc/explo/udpor/CompatibilityGraphNode.hpp
- src/mc/explo/udpor/CompatibilityGraphNode.cpp
src/mc/explo/udpor/Configuration.hpp
src/mc/explo/udpor/Configuration.cpp
src/mc/explo/udpor/EventSet.cpp
