Add tests before changes to WakeupTree structure

diff --git a/src/mc/explo/odpor/Execution_test.cpp b/src/mc/explo/odpor/Execution_test.cpp
index 143c0a7..0ed54f9 100644 (file)
--- a/src/mc/explo/odpor/Execution_test.cpp
+++ b/src/mc/explo/odpor/Execution_test.cpp
@@ -277,4 +277,20 @@ TEST_CASE("simgrid::mc::odpor::Execution: Testing Racing Events and Initials")
     // The same logic above eliminates events before 6
     REQUIRE(execution.get_racing_events_of(9) == std::unordered_set<Execution::EventHandle>{6});
   }
-}
\ No newline at end of file
+}
+
+TEST_CASE("simgrid::mc::odpor::Execution: Testing Races and Conditions")
+{
+  const auto a1 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
+  const auto a2 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
+  const auto a3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
+  const auto a4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
+  const auto a5 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
+
+  Execution execution;
+  execution.push_transition(a1);
+  execution.push_transition(a2);
+  execution.push_transition(a3);
+  execution.push_transition(a4);
+  execution.push_transition(a5);
+}

diff --git a/src/mc/explo/odpor/WakeupTree.cpp b/src/mc/explo/odpor/WakeupTree.cpp
index 5e967eb..bbd21cf 100644 (file)
--- a/src/mc/explo/odpor/WakeupTree.cpp
+++ b/src/mc/explo/odpor/WakeupTree.cpp
@@ -154,6 +154,9 @@ void WakeupTree::insert(const Execution& E, const PartialExecution& w)
       // 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)");
         WakeupTreeNode* new_node = this->make_node(shortest_sequence.value());
         node->add_child(new_node);
       }

diff --git a/src/mc/explo/odpor/WakeupTree_test.cpp b/src/mc/explo/odpor/WakeupTree_test.cpp
index c77c1e6..6649448 100644 (file)
--- a/src/mc/explo/odpor/WakeupTree_test.cpp
+++ b/src/mc/explo/odpor/WakeupTree_test.cpp
@@ -4,10 +4,104 @@
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "src/3rd-party/catch.hpp"
+#include "src/mc/explo/odpor/Execution.hpp"
 #include "src/mc/explo/odpor/WakeupTree.hpp"
 #include "src/mc/explo/udpor/udpor_tests_private.hpp"
 
 using namespace simgrid::mc;
 using namespace simgrid::mc::odpor;
+using namespace simgrid::mc::udpor;
 
-TEST_CASE("simgrid::mc::odpor::WakeupTree: ") {}
\ No newline at end of file
+TEST_CASE("simgrid::mc::odpor::WakeupTree: Testing Insertion")
+{
+  // We imagine the following completed execution `E`
+  // consisting of executing actions a0-a3. Execution
+  // `E` cis the first such maximal execution explored
+  // by ODPOR, which implies that a) all sleep sets are
+  // empty and b) all wakeup trees (i.e. for each prefix) consist of the root
+  // node with a single leaf containing the action
+  // taken, save for the wakeup tree of the execution itself
+  // which is empty
+
+  // We first notice that there's a reversible race between
+  // events 0 and 3.
+
+  const auto a0 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
+  const auto a1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 4);
+  const auto a2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+  const auto a3 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
+
+  Execution execution;
+  execution.push_transition(a0);
+  execution.push_transition(a1);
+  execution.push_transition(a2);
+  execution.push_transition(a3);
+
+  REQUIRE(execution.get_racing_events_of(2) == std::unordered_set<Execution::EventHandle>{0});
+  REQUIRE(execution.get_racing_events_of(3) == std::unordered_set<Execution::EventHandle>{0});
+
+  // First, we initialize the tree to how it looked prior
+  // to the insertion of the race
+  WakeupTree tree;
+  tree.insert(Execution(), {a0});
+
+  // Then, after insertion, we ensure that the node was
+  // indeed added to the tree
+
+  tree.insert(Execution(), {a1, a3});
+
+  WakeupTreeIterator iter = tree.begin();
+  REQUIRE((*iter)->get_sequence() == PartialExecution{a0});
+
+  ++iter;
+  REQUIRE(iter != tree.end());
+  REQUIRE((*iter)->get_sequence() == PartialExecution{a1, a3});
+
+  ++iter;
+  REQUIRE(iter != tree.end());
+  REQUIRE((*iter)->get_sequence() == PartialExecution{});
+
+  ++iter;
+  REQUIRE(iter == tree.end());
+
+  SECTION("Attempting to re-insert the same sequence should have no effect")
+  {
+    tree.insert(Execution(), {a1, a3});
+    iter = tree.begin();
+
+    REQUIRE((*iter)->get_sequence() == PartialExecution{a0});
+
+    ++iter;
+    REQUIRE(iter != tree.end());
+    REQUIRE((*iter)->get_sequence() == PartialExecution{a1, a3});
+
+    ++iter;
+    REQUIRE(iter != tree.end());
+    REQUIRE((*iter)->get_sequence() == PartialExecution{});
+
+    ++iter;
+    REQUIRE(iter == tree.end());
+  }
+
+  SECTION("Inserting an extension")
+  {
+    tree.insert(Execution(), {a1, a2});
+    iter = tree.begin();
+    REQUIRE((*iter)->get_sequence() == PartialExecution{a0});
+
+    ++iter;
+    REQUIRE(iter != tree.end());
+    REQUIRE((*iter)->get_sequence() == PartialExecution{a1, a3});
+
+    ++iter;
+    REQUIRE(iter != tree.end());
+    REQUIRE((*iter)->get_sequence() == PartialExecution{a1, a2});
+
+    ++iter;
+    REQUIRE(iter != tree.end());
+    REQUIRE((*iter)->get_sequence() == PartialExecution{});
+
+    ++iter;
+    REQUIRE(iter == tree.end());
+  }
+}
\ No newline at end of file