Respect coding style for boolean operators.

[simgrid.git] / src / mc / explo / odpor / WakeupTree.cpp

diff --git a/src/mc/explo/odpor/WakeupTree.cpp b/src/mc/explo/odpor/WakeupTree.cpp
index a07706e..22b0352 100644 (file)
--- a/src/mc/explo/odpor/WakeupTree.cpp
+++ b/src/mc/explo/odpor/WakeupTree.cpp
@@ -26,7 +26,7 @@ PartialExecution WakeupTreeNode::get_sequence() const
   // and instead track this with the iterator
   PartialExecution seq_;
   const WakeupTreeNode* cur_node = this;
-  while (cur_node != nullptr and !cur_node->is_root()) {
+  while (cur_node != nullptr && not cur_node->is_root()) {
     seq_.push_front(cur_node->action_);
     cur_node = cur_node->parent_;
   }
@@ -120,7 +120,7 @@ void WakeupTree::remove_subtree_rooted_at(WakeupTreeNode* root)
   std::list<WakeupTreeNode*> subtree_contents{root};
   std::list<WakeupTreeNode*> frontier{root};
   while (not frontier.empty()) {
-    auto node = frontier.front();
+    const auto* node = frontier.front();
     frontier.pop_front();
     for (const auto& child : node->get_ordered_children()) {
       frontier.push_back(child);
@@ -145,7 +145,7 @@ void WakeupTree::remove_min_single_process_subtree()
   }
 }
 
-bool WakeupTree::contains(WakeupTreeNode* node) const
+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();
@@ -170,7 +170,7 @@ void WakeupTree::remove_node(WakeupTreeNode* node)
   this->nodes_.erase(node);
 }
 
-void WakeupTree::insert(const Execution& E, const PartialExecution& w)
+WakeupTree::InsertionResult WakeupTree::insert(const Execution& E, const PartialExecution& w)
 {
   // See section 6.2 of Abdulla. et al.'s 2017 ODPOR paper for details
 
@@ -181,15 +181,23 @@ void WakeupTree::insert(const Execution& E, const PartialExecution& w)
         shortest_sequence.has_value()) {
       // Insert the sequence as a child of `node`, but only
       // if the node is not already a leaf
-      if (not node->is_leaf() or node == this->root_) {
-        xbt_assert(!shortest_sequence.value().empty(), "A successful insertion into an interior"
-                                                       "node of a wakeup tree should never involve "
-                                                       "an empty sequence (yet here we are, with an empty sequence)");
+      if (not node->is_leaf() || node == this->root_) {
+        // NOTE: It's entirely possible that the shortest
+        // sequence we are inserting is empty. Consider the
+        // following two cases:
+        //
+        // 1. `w` is itself empty. Evidently, insertion succeeds but nothing needs
+        // to happen
+        //
+        // 2. a leaf node in the tree already contains `w` exactly.
+        // In this case, the empty `w'` returned (viz. `shortest_seq`)
+        // such that `w [=_[E] v.w'` would be empty
         this->insert_sequence_after(node, shortest_sequence.value());
+        return node == this->root_ ? InsertionResult::root : InsertionResult::interior_node;
       }
       // Since we're following the post-order traversal of the tree,
       // the first such node we see is the smallest w.r.t "<"
-      return;
+      return InsertionResult::leaf;
     }
   }
   xbt_die("Insertion should always succeed with the root node (which contains no "
@@ -208,4 +216,4 @@ void WakeupTree::insert_sequence_after(WakeupTreeNode* node, const PartialExecut
   }
 }
 
-} // namespace simgrid::mc::odpor
\ No newline at end of file
+} // namespace simgrid::mc::odpor