Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Add tree pruning/subtree methods to State
[simgrid.git] / src / mc / explo / odpor / WakeupTree.cpp
1 /* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved.          */
2
3 /* This program is free software; you can redistribute it and/or modify it
4  * under the terms of the license (GNU LGPL) which comes with this package. */
5
6 #include "src/mc/explo/odpor/WakeupTree.hpp"
7 #include "src/mc/explo/odpor/Execution.hpp"
8 #include "xbt/asserts.h"
9
10 #include <algorithm>
11 #include <exception>
12 #include <queue>
13
14 namespace simgrid::mc::odpor {
15
16 aid_t WakeupTreeNode::get_first_actor() const
17 {
18   if (seq_.empty()) {
19     throw std::invalid_argument("Attempted to extract the first actor from "
20                                 "a node in a wakeup tree representing the "
21                                 "empty execution (likely the root node)");
22   }
23   return get_sequence().front()->aid_;
24 }
25
26 WakeupTree::WakeupTree() : WakeupTree(std::unique_ptr<WakeupTreeNode>(new WakeupTreeNode({}))) {}
27 WakeupTree::WakeupTree(std::unique_ptr<WakeupTreeNode> root) : root_(root.get())
28 {
29   this->insert_node(std::move(root));
30 }
31
32 WakeupTree WakeupTree::make_subtree_rooted_at(WakeupTreeNode* root)
33 {
34   if (not root->is_single_process()) {
35     throw std::invalid_argument("Selecting subtrees is only defined for single-process nodes");
36   }
37
38   const aid_t p = (*(root->get_sequence().begin()))->aid_;
39
40   // Perform a BFS search to perform a deep copy of the portion
41   // of the tree underneath and including `root`. Note that `root`
42   // is contained within the context of a *different* wakeup tree;
43   // hence, we have to be careful to update each node's children
44   // appropriately
45   auto subtree                    = WakeupTree();
46   WakeupTreeNode* root_equivalent = subtree.make_node(root->get_sequence());
47
48   std::list<std::pair<WakeupTreeNode*, WakeupTreeNode*>> frontier{std::make_pair(root, root_equivalent)};
49   while (not frontier.empty()) {
50     auto [node_in_other_tree, subtree_equivalent] = frontier.front();
51     frontier.pop_front();
52
53     // For each child of the node corresponding to that in `subtree`,
54     // make clones of each of its children and add them to `frontier`
55     // to that their children are added, and so on. Note that the subtree
56     // **explicitly** removes the first process from each child
57     for (WakeupTreeNode* child_in_other_tree : node_in_other_tree->get_ordered_children()) {
58       auto p_w           = child_in_other_tree->get_sequence();
59       const auto p_again = p_w.front()->aid_;
60
61       // INVARIANT: A nodes of a wakeup tree form a prefix-closed set;
62       // this means that any child node `c` of a node `n` must contain
63       // `n.get_sequence()` as a prefix of `c.get_sequence()`
64       xbt_assert(p_again == p,
65                  "Invariant Violation: The wakeup tree from which a subtree with actor "
66                  "`%ld` is being taken is not prefix free! The child node starts with "
67                  "`%ld` while the parent is `%ld`! This indicates that there "
68                  "is a bug in the insertion logic for the wakeup tree",
69                  p, p_again, p);
70       p_w.pop_front();
71
72       WakeupTreeNode* child_equivalent = subtree.make_node(p_w);
73       subtree_equivalent->add_child(child_equivalent);
74       frontier.push_back(std::make_pair(child_in_other_tree, child_equivalent));
75     }
76   }
77   return subtree;
78 }
79
80 void WakeupTree::remove_subtree_rooted_at(WakeupTreeNode* root)
81 {
82   if (not contains(root)) {
83     throw std::invalid_argument("Attempting to remove a subtree pivoted from a node "
84                                 "that is not contained in this wakeup tree");
85   }
86
87   std::list<WakeupTreeNode*> subtree_contents;
88   std::list<WakeupTreeNode*> frontier{root};
89   while (not frontier.empty()) {
90     auto node = frontier.front();
91     frontier.pop_front();
92     for (const auto& child : node->get_ordered_children()) {
93       frontier.push_back(child);
94       subtree_contents.push_back(child);
95     }
96   }
97
98   // After having found each node with BFS, now we can
99   // remove them. This prevents the "joys" iteration during mutation
100   for (WakeupTreeNode* node_to_remove : subtree_contents) {
101     this->remove_node(node_to_remove);
102   }
103 }
104
105 bool WakeupTree::contains(WakeupTreeNode* node) const
106 {
107   return std::find_if(this->nodes_.begin(), this->nodes_.end(), [=](const auto& pair) { return pair.first == node; }) !=
108          this->nodes_.end();
109 }
110
111 WakeupTreeNode* WakeupTree::make_node(const PartialExecution& u)
112 {
113   auto node                 = std::unique_ptr<WakeupTreeNode>(new WakeupTreeNode(u));
114   auto* node_handle         = node.get();
115   this->nodes_[node_handle] = std::move(node);
116   return node_handle;
117 }
118
119 void WakeupTree::insert_node(std::unique_ptr<WakeupTreeNode> node)
120 {
121   auto* node_handle         = node.get();
122   this->nodes_[node_handle] = std::move(node);
123 }
124
125 void WakeupTree::remove_node(WakeupTreeNode* node)
126 {
127   this->nodes_.erase(node);
128 }
129
130 void WakeupTree::insert(const Execution& E, const PartialExecution& w)
131 {
132   // See section 6.2 of Abdulla. et al.'s 2017 ODPOR paper for details
133
134   // Find the first node `v` in the tree such that
135   // `v ~_[E] w` and `v`  is not a leaf node
136   for (WakeupTreeNode* node : *this) {
137     if (const auto shortest_sequence = E.get_shortest_odpor_sq_subset_insertion(node->get_sequence(), w);
138         shortest_sequence.has_value()) {
139       // Insert the sequence as a child of `node`, but only
140       // if the node is not already a leaf
141       if (not node->is_leaf() or node == this->root_) {
142         WakeupTreeNode* new_node = this->make_node(shortest_sequence.value());
143         node->add_child(new_node);
144       }
145       // Since we're following the post-order traversal of the tree,
146       // the first such node we see is the smallest w.r.t "<"
147       return;
148     }
149   }
150 }
151
152 } // namespace simgrid::mc::odpor