Add logic for subtree node removal

ODPOR also mandates that subtrees be removed
from a wakeup tree after having finished searching
"in the direction" of the subtree. This commit
adds a method to WakeupTree which, given a handle
to a node in the tree, removes the subtree rooted at
that node.

diff --git a/src/mc/explo/odpor/WakeupTree.cpp b/src/mc/explo/odpor/WakeupTree.cpp
index e5f983f..662585e 100644 (file)
--- a/src/mc/explo/odpor/WakeupTree.cpp
+++ b/src/mc/explo/odpor/WakeupTree.cpp
@@ -67,6 +67,37 @@ WakeupTree WakeupTree::new_subtree_rooted_at(WakeupTreeNode* root)
   return subtree;
 }
 
+void WakeupTree::remove_subtree_rooted_at(WakeupTreeNode* root)
+{
+  if (not contains(root)) {
+    throw std::invalid_argument("Attempting to remove a subtree pivoted from a node "
+                                "that is not contained in this wakeup tree");
+  }
+
+  std::list<WakeupTreeNode*> subtree_contents;
+  std::list<WakeupTreeNode*> frontier{root};
+  while (not frontier.empty()) {
+    auto node = frontier.front();
+    frontier.pop_front();
+    for (const auto& child : node->get_ordered_children()) {
+      frontier.push_back(child);
+      subtree_contents.push_back(child);
+    }
+  }
+
+  // After having found each node with BFS, now we can
+  // remove them. This prevents the "joys" iteration during mutation
+  for (WakeupTreeNode* node_to_remove : subtree_contents) {
+    this->remove_node(node_to_remove);
+  }
+}
+
+bool WakeupTree::contains(WakeupTreeNode* node) const
+{
+  return std::find_if(this->nodes_.begin(), this->nodes_.end(), [=](const auto& pair) { return pair.first == node; }) !=
+         this->nodes_.end();
+}
+
 WakeupTreeNode* WakeupTree::make_node(const PartialExecution& u)
 {
   auto node                 = std::unique_ptr<WakeupTreeNode>(new WakeupTreeNode(u));
@@ -81,6 +112,11 @@ void WakeupTree::insert_node(std::unique_ptr<WakeupTreeNode> node)
   this->nodes_[node_handle] = std::move(node);
 }
 
+void WakeupTree::remove_node(WakeupTreeNode* node)
+{
+  this->nodes_.erase(node);
+}
+
 void WakeupTree::insert(const Execution& E, const PartialExecution& w)
 {
   // See section 6.2 of Abdulla. et al.'s 2017 ODPOR paper for details

diff --git a/src/mc/explo/odpor/WakeupTree.hpp b/src/mc/explo/odpor/WakeupTree.hpp
index 8ffbe61..28f549e 100644 (file)
--- a/src/mc/explo/odpor/WakeupTree.hpp
+++ b/src/mc/explo/odpor/WakeupTree.hpp
@@ -64,27 +64,40 @@ private:
    */
   std::unordered_map<WakeupTreeNode*, std::unique_ptr<WakeupTreeNode>> nodes_;
 
-  /**
-   * @brief Transfers the lifetime of node `node` to the tree
-   */
   void insert_node(std::unique_ptr<WakeupTreeNode> node);
+  void remove_node(WakeupTreeNode* node);
 
   /**
-   * @brief Creates a new, disconnected node in this tree
+   * @brief Adds a new node to the tree, disconnected from
+   * any other, which represents the partial execution
+   * "fragment" `u`
    */
   WakeupTreeNode* make_node(const PartialExecution& u);
 
+  bool contains(WakeupTreeNode* node) const;
+
   /* Allow the iterator to access the contents of the tree */
   friend WakeupTreeIterator;
 
 public:
   WakeupTree();
   explicit WakeupTree(std::unique_ptr<WakeupTreeNode> root);
-  static WakeupTree new_subtree_rooted_at(WakeupTreeNode* root);
 
   auto begin() const { return WakeupTreeIterator(*this); }
   auto end() const { return WakeupTreeIterator(); }
 
+  void remove_subtree_rooted_at(WakeupTreeNode* root);
+  static WakeupTree new_subtree_rooted_at(WakeupTreeNode* root);
+
+  /**
+   * @brief Whether or not this tree is considered empty
+   *
+   * @note Unlike other collection types, a wakeup tree is
+   * considered "empty" if it only contains the root node;
+   * that is, if it is "uninteresting". In such a case,
+   */
+  bool is_empty() const { return nodes_.size() == static_cast<size_t>(1); }
+
   /**
    * @brief Inserts an sequence `seq` of processes into the tree
    * such that that this tree is a wakeup tree relative to the