+ this->insert_node(std::move(root));
+}
+
+std::vector<std::string> WakeupTree::get_single_process_texts() const
+{
+ std::vector<std::string> trace;
+ for (const auto* child : root_->children_) {
+ const auto t = child->get_action();
+ auto message = xbt::string_printf("Actor %ld: %s", t->aid_, t->to_string(true).c_str());
+ trace.emplace_back(std::move(message));
+ }
+ return trace;
+}
+
+std::optional<aid_t> WakeupTree::get_min_single_process_actor() const
+{
+ if (const auto node = get_min_single_process_node(); node.has_value()) {
+ return node.value()->get_actor();
+ }
+ return std::nullopt;
+}
+
+std::optional<WakeupTreeNode*> WakeupTree::get_min_single_process_node() const
+{
+ if (empty()) {
+ return std::nullopt;
+ }
+ // INVARIANT: The induced post-order relation always places children
+ // in order before the parent. The list of children maintained by
+ // each node represents that ordering, and the first child of
+ // the root is by definition the smallest of the single-process nodes
+ xbt_assert(not this->root_->children_.empty(), "What the");
+ return this->root_->children_.front();
+}
+
+std::string WakeupTree::string_of_whole_tree() const
+{
+ return root_->string_of_whole_tree(0);
+}
+
+WakeupTree WakeupTree::make_subtree_rooted_at(WakeupTreeNode* root)
+{
+ // Perform a BFS search to perform a deep copy of the portion
+ // of the tree underneath and including `root`. Note that `root`
+ // is contained within the context of a *different* wakeup tree;
+ // hence, we have to be careful to update each node's children
+ // appropriately
+ auto subtree = WakeupTree();
+
+ std::list<std::pair<WakeupTreeNode*, WakeupTreeNode*>> frontier{std::make_pair(root, subtree.root_)};
+ while (not frontier.empty()) {
+ auto [node_in_other_tree, subtree_equivalent] = frontier.front();
+ frontier.pop_front();
+
+ // For each child of the node corresponding to that in `subtree`,
+ // make clones of each of its children and add them to `frontier`
+ // to that their children are added, and so on.
+ for (WakeupTreeNode* child_in_other_tree : node_in_other_tree->get_ordered_children()) {
+ WakeupTreeNode* child_equivalent = subtree.make_node(child_in_other_tree->get_action());
+ subtree_equivalent->add_child(child_equivalent);
+ frontier.push_back(std::make_pair(child_in_other_tree, child_equivalent));
+ }
+ }
+ 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{root};
+ std::list<WakeupTreeNode*> frontier{root};
+ while (not frontier.empty()) {
+ const 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" of iteration during mutation.
+ // We also remove the `root` from being referenced by its own parent (since
+ // it will soon be destroyed)
+ root->detatch_from_parent();
+ for (WakeupTreeNode* node_to_remove : subtree_contents) {
+ this->remove_node(node_to_remove);
+ }
+}
+
+void WakeupTree::remove_subtree_at_aid(aid_t proc)
+{
+ for (const auto& child : root_->get_ordered_children())
+ if (child->get_actor() == proc) {
+ this->remove_subtree_rooted_at(child);
+ break;
+ }
+}
+
+void WakeupTree::remove_min_single_process_subtree()
+{
+ if (const auto node = get_min_single_process_node(); node.has_value()) {
+ remove_subtree_rooted_at(node.value());
+ }
+}
+
+bool WakeupTree::contains(const 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(std::shared_ptr<Transition> u)
+{
+ auto node = std::make_unique<WakeupTreeNode>(std::move(u));
+ auto* node_handle = node.get();
+ this->nodes_[node_handle] = std::move(node);