include src/mc/explo/odpor/Execution_test.cpp
include src/mc/explo/odpor/WakeupTree.cpp
include src/mc/explo/odpor/WakeupTree.hpp
+include src/mc/explo/odpor/WakeupTreeIterator.cpp
+include src/mc/explo/odpor/WakeupTreeIterator.hpp
include src/mc/explo/odpor/odpor_forward.hpp
include src/mc/explo/simgrid_mc.cpp
include src/mc/explo/udpor/Comb.hpp
namespace simgrid::mc::odpor {
-using ProcessSequence = std::list<aid_t>;
-using ExecutionSequence = std::list<const State*>;
-using Hypothetical = ExecutionSequence;
-
/**
* @brief The occurrence of a transition in an execution
*
Execution(const Execution&) = default;
Execution& operator=(Execution const&) = default;
Execution(Execution&&) = default;
- Execution(ExecutionSequence&& seq);
- Execution(const ExecutionSequence& seq);
size_t size() const { return this->contents_.size(); }
bool empty() const { return this->contents_.empty(); }
*/
std::optional<aid_t> get_first_sdpor_initial_from(EventHandle e, std::unordered_set<aid_t> backtrack_set) const;
+ std::optional<ProcessSequence> get_shortest_odpor_sq_subset_insert(const ProcessSequence& v,
+ const ExecutionSequence& w) const;
+
/**
* @brief Determines the event associated with
* the given handle `handle`
+/* 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/odpor/WakeupTree.hpp"
+#include "src/mc/explo/odpor/Execution.hpp"
+
+#include <algorithm>
+
+namespace simgrid::mc::odpor {
+
+WakeupTree::WakeupTree() : root(nullptr) {}
+
+void WakeupTree::insert(const Execution& E, const ExecutionSequence& w)
+{
+ // Find the first node `v` in the tree such that
+ // `v ~_[E] w`
+}
+
+} // namespace simgrid::mc::odpor
\ No newline at end of file
+/* 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_ODPOR_WAKEUP_TREE_HPP
+#define SIMGRID_MC_ODPOR_WAKEUP_TREE_HPP
+
+#include "src/mc/explo/odpor/odpor_forward.hpp"
+
+#include <memory>
+#include <unordered_map>
+
+namespace simgrid::mc::odpor {
+
+class WakeupTreeNode {
+private:
+ /** An ordered list of children of for this node in the tree */
+ std::list<const WakeupTreeNode*> children_;
+
+ /** @brief The contents of the node */
+ ProcessSequence seq_;
+
+public:
+ const auto begin() const { return this->children_.begin(); }
+ const auto end() const { return this->children_.end(); }
+ const auto rbegin() const { return this->children_.rbegin(); }
+ const auto rend() const { return this->children_.rend(); }
+
+ const ProcessSequence& get_sequence() const { return seq_; }
+ const std::list<const WakeupTreeNode*>& get_ordered_children() const { return children_; }
+
+ bool is_leaf() const { return children_.empty(); }
+};
+
+class WakeupTree {
+private:
+ /** @brief The root node of the tree */
+ const WakeupTreeNode* const root;
+
+ /**
+ * @brief All of the nodes that are currently are a part of the tree
+ *
+ * @invariant Each node event maps itself to the owner of that node,
+ * i.e. the unique pointer that manages the data at the address. The tree owns all
+ * of the addresses that are referenced by the nodes WakeupTreeNode and Configuration.
+ * ODPOR guarantees that nodes are persisted as long as needed.
+ */
+ std::unordered_map<const WakeupTreeNode*, std::unique_ptr<WakeupTreeNode>> nodes_;
+
+ /* Allow the iterator to access the contents of the tree */
+ friend WakeupTreeIterator;
+
+public:
+ WakeupTree();
+
+ /**
+ * @brief Inserts an sequence `seq` of processes into the tree
+ * such that that this tree is a wakeup tree relative to the
+ * given execution
+ */
+ void insert(const Execution&, const ExecutionSequence& seq);
+};
+
+} // namespace simgrid::mc::odpor
+#endif
--- /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/odpor/WakeupTreeIterator.hpp"
+
+namespace simgrid::mc::odpor {
+
+WakeupTreeIterator::WakeupTreeIterator(const WakeupTree& tree)
+{
+ // post_order_iteration.push(tree.root);
+ push_until_left_most_found();
+}
+
+void WakeupTreeIterator::push_until_left_most_found()
+{
+ // INVARIANT: Since we are traversing over a tree,
+ // there are no cycles. This means that at least
+ // one node in the tree won't have any children,
+ // so the loop will eventually terminate
+ auto* cur_top_node = *post_order_iteration.top();
+ while (!cur_top_node->is_leaf()) {
+ // INVARIANT: Since we push children in
+ // reverse order (right-most to left-most),
+ // we ensure that we'll always process left-most
+ // children first
+ }
+}
+
+void WakeupTreeIterator::increment()
+{
+ // If there are no nodes in the stack, we've
+ // completed the traversal: there's nothing left
+ // to do
+ if (post_order_iteration.empty()) {
+ return;
+ }
+
+ auto prev_top_handle = post_order_iteration.top();
+ post_order_iteration.pop();
+
+ // If there are now no longer any nodes left,
+ // we know that `prev_top` must be the original
+ // root; that is, we were *just* pointing at the
+ // original root, so we're done
+ if (post_order_iteration.empty()) {
+ return;
+ }
+
+ // Otherwise, look at the next top node. If
+ // `prev_top` is that node's right-most child,
+ // then we don't attempt to re-add `next_top`'s
+ // children again for we would have already seen them
+ const auto* next_top_node = *post_order_iteration.top();
+
+ // To actually determine "right-most", we check if
+ // moving over to the right one spot brings us to the
+ // end of the candidate parent's list
+ if ((++prev_top_handle) != next_top_node->get_ordered_children().end()) {
+ push_until_left_most_found();
+ }
+}
+
+} // namespace simgrid::mc::odpor
\ No newline at end of file
--- /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_ODPOR_WAKEUP_TREE_ITERATOR_HPP
+#define SIMGRID_MC_ODPOR_WAKEUP_TREE_ITERATOR_HPP
+
+#include "src/mc/explo/odpor/WakeupTree.hpp"
+
+#include <boost/iterator/iterator_facade.hpp>
+#include <list>
+#include <stack>
+
+namespace simgrid::mc::odpor {
+
+struct WakeupTreeIterator
+ : public boost::iterator_facade<WakeupTreeIterator, const WakeupTreeNode*, boost::forward_traversal_tag> {
+public:
+ WakeupTreeIterator() = default;
+ explicit WakeupTreeIterator(const WakeupTree& tree);
+
+private:
+ using node_handle = std::list<const WakeupTreeNode*>::iterator;
+
+ /**
+ * @brief The current "view" of the iteration in post-order traversal
+ */
+ std::stack<node_handle> post_order_iteration;
+
+ /**
+ *
+ */
+ void push_until_left_most_found();
+
+ // boost::iterator_facade<...> interface to implement
+ void increment();
+ bool equal(const WakeupTreeIterator& other) const { return post_order_iteration == other.post_order_iteration; }
+ const WakeupTreeNode*& dereference() const { return *post_order_iteration.top(); }
+
+ // Allows boost::iterator_facade<...> to function properly
+ friend class boost::iterator_core_access;
+};
+
+} // namespace simgrid::mc::odpor
+#endif
#define SIMGRID_MC_ODPOR_FORWARD_HPP
#include "src/mc/mc_forward.hpp"
+#include <list>
#include <simgrid/forward.h>
namespace simgrid::mc::odpor {
+using ProcessSequence = std::list<aid_t>;
+using ExecutionSequence = std::list<const Transition*>;
+
class Event;
class Execution;
-class ExecutionView;
class WakeupTree;
+class WakeupTreeIterator;
} // namespace simgrid::mc::odpor
src/mc/explo/odpor/Execution.hpp
src/mc/explo/odpor/WakeupTree.cpp
src/mc/explo/odpor/WakeupTree.hpp
+ src/mc/explo/odpor/WakeupTreeIterator.cpp
+ src/mc/explo/odpor/WakeupTreeIterator.hpp
src/mc/explo/odpor/odpor_forward.hpp
src/mc/remote/AppSide.cpp
