From 8c95e5e228e356e37e1e0364ea790f03f1a501d6 Mon Sep 17 00:00:00 2001 From: Maxwell Pirtle Date: Thu, 1 Jun 2023 11:10:18 +0200 Subject: [PATCH] Add small test for insertions --- src/mc/explo/odpor/Execution.cpp | 2 +- src/mc/explo/odpor/WakeupTree_test.cpp | 67 +++++++++++++++++++++++--- 2 files changed, 62 insertions(+), 7 deletions(-) diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp index dbbf57a30b..1c01e2b48a 100644 --- a/src/mc/explo/odpor/Execution.cpp +++ b/src/mc/explo/odpor/Execution.cpp @@ -416,7 +416,7 @@ std::optional Execution::get_shortest_odpor_sq_subset_insertio if (E_v.is_initial_after_execution_of(w_now, p)) { // Remove `p` from w and continue - // TODO: If `p` occurs in `w`, it had better refer to the same + // INVARIANT: If `p` occurs in `w`, it had better refer to the same // transition referenced by `v`. Unfortunately, we have two // sources of truth here which can be manipulated at the same // time as arguments to the function. If ODPOR works correctly, diff --git a/src/mc/explo/odpor/WakeupTree_test.cpp b/src/mc/explo/odpor/WakeupTree_test.cpp index 4db64edba3..e0ef032bb9 100644 --- a/src/mc/explo/odpor/WakeupTree_test.cpp +++ b/src/mc/explo/odpor/WakeupTree_test.cpp @@ -392,7 +392,7 @@ TEST_CASE("simgrid::mc::odpor::WakeupTree: Testing Insertion for Empty Execution } } - SECTION("Insertion with non-obvious equivalent leaf") + SECTION("Insertion with more subtle equivalents") { const auto cd_1 = std::make_shared(Transition::Type::UNKNOWN, 1); const auto i_2 = std::make_shared(Transition::Type::UNKNOWN, 2); @@ -401,14 +401,69 @@ TEST_CASE("simgrid::mc::odpor::WakeupTree: Testing Insertion for Empty Execution const auto d_2 = std::make_shared(Transition::Type::UNKNOWN, 2); WakeupTree complex_tree; // After the insertions below, the tree looks like the following: - // {} - // / / - // a0 a2 - // / | / - // a0 a3 a5 + // {} + // / / + // cd_1 i_2 + // / / + // i_2 d_2 + // / / + // d_1 cd_1 + // / / / + // i_3 d_1 i_3 + // / / / + // d_2 i_3 d_2 + // / / / + // d_2 d_2 d_1 + // + // d_1.i_3.d_2 is equivalent to i_3.d_2.d_1 complex_tree.insert(Execution(), {cd_1, i_2, d_1, i_3, d_2, d_2}); complex_tree.insert(Execution(), {i_2, d_2, cd_1, d_1, i_3, d_2}); complex_tree.insert(Execution(), {i_2, d_2, cd_1, i_3, d_2, d_1}); REQUIRE(complex_tree.get_num_nodes() == 16); + test_tree_iterator(complex_tree, std::vector{{cd_1, i_2, d_1, i_3, d_2, d_2}, + {cd_1, i_2, d_1, i_3, d_2}, + {cd_1, i_2, d_1, i_3}, + {cd_1, i_2, d_1}, + {cd_1, i_2}, + {cd_1}, + {i_2, d_2, cd_1, d_1, i_3, d_2}, + {i_2, d_2, cd_1, d_1, i_3}, + {i_2, d_2, cd_1, d_1}, + {i_2, d_2, cd_1, i_3, d_2, d_1}, + {i_2, d_2, cd_1, i_3, d_2}, + {i_2, d_2, cd_1, i_3}, + {i_2, d_2, cd_1}, + {i_2, d_2}, + {i_2}, + {}}); + // Here we note that the sequence that we are attempting to insert, viz. + // + // i_3.i_2.d_2.cd_1.d_2.d_1 + // + // is already equivalent to + // + // i_2.d_2.cd_1.i_3.d_2.d_1 + complex_tree.insert(Execution(), {i_3, i_2, d_2, cd_1, d_2, d_1}); + REQUIRE(complex_tree.get_num_nodes() == 16); + + // Here we note that the sequence that we are attempting to insert, viz. + // + // i_2.d_2.cd_1.d_1.i_3 + // + // is already equivalent to + // + // i_2.d_2.cd_1.i_3.d_2.d_1 + complex_tree.insert(Execution(), {i_2, d_2, cd_1, d_1, i_3}); + REQUIRE(complex_tree.get_num_nodes() == 16); + + // Here we note that the sequence that we are attempting to insert, viz. + // + // i_2.d_2.cd_1 + // + // is accounted for by an interior node of the tree. Since there is no + // "extra" portions that are different from what is already + // contained in the tree, nothing is added and the tree stays the same + complex_tree.insert(Execution(), {i_2, d_2, cd_1}); + REQUIRE(complex_tree.get_num_nodes() == 16); } } \ No newline at end of file -- 2.20.1