From b29859b1864263db00c35861e20441e0634c3535 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Mon, 29 Jul 2024 11:23:01 +0200 Subject: [PATCH] Add 'relnext(states, relation, varcount)' and 'relprev(states, relation, varcount)' overloads While maybe not as good in practice as the interleaved ordering, it is used in quite a few academic texts (see the referenced unit tests and also the paper on Knor by Tom van Dijk) --- src/adiar/bdd.h | 50 + src/adiar/bdd/relprod.cpp | 36 + test/adiar/bdd/test_relprod.cpp | 3371 +++++++++++++++++++++---------- 3 files changed, 2341 insertions(+), 1116 deletions(-) diff --git a/src/adiar/bdd.h b/src/adiar/bdd.h index 629a66c75..e39ee88ec 100644 --- a/src/adiar/bdd.h +++ b/src/adiar/bdd.h @@ -1456,6 +1456,31 @@ namespace adiar const function(bdd::label_type)>& m, replace_type m_type); + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Forwards step with the Relational Product for *disjoint* variable orderings, + /// including relabelling. + /// + /// \param states + /// A symbolic representation of the *current* set of states. These are all encoded with the + /// variables `0`, `1`, ... `varcount - 1`. + /// + /// \param relation + /// A relation between *current* and *next* state variables. The *next* state is encoded with + /// variables `varcount`, `varcount+1`, ... `2*varcount - 1`. + ////////////////////////////////////////////////////////////////////////////////////////////////// + bdd + bdd_relnext(const bdd& states, const bdd& relation, const bdd::label_type varcount); + + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Forwards step with the Relational Product for *disjoint* variable orderings, + /// including relabelling. + ////////////////////////////////////////////////////////////////////////////////////////////////// + bdd + bdd_relnext(const exec_policy& ep, + const bdd& states, + const bdd& relation, + const bdd::label_type varcount); + ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Forwards step with the Relational Product for *interleaved* variable orderings, /// including relabelling. @@ -1538,6 +1563,31 @@ namespace adiar const function(bdd::label_type)>& m, replace_type m_type); + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Backwards step with the Relational Product for *disjoint* variable orderings, + /// including relabelling. + /// + /// \param states + /// A symbolic representation of the *current* set of states. These are all encoded with the + /// variables `0`, `1`, ... `varcount - 1`. + /// + /// \param relation + /// A relation between *current* and *next* state variables. The *next* state is encoded with + /// variables `varcount`, `varcount+1`, ... `2*varcount - 1`. + ////////////////////////////////////////////////////////////////////////////////////////////////// + bdd + bdd_relprev(const bdd& states, const bdd& relation, const bdd::label_type varcount); + + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Backwards step with the Relational Product for *disjoint* variable orderings, + /// including relabelling. + ////////////////////////////////////////////////////////////////////////////////////////////////// + bdd + bdd_relprev(const exec_policy& ep, + const bdd& states, + const bdd& relation, + const bdd::label_type varcount); + ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Backwards step with the Relational Product for *interleaved* variable orderings, /// including relabelling. diff --git a/src/adiar/bdd/relprod.cpp b/src/adiar/bdd/relprod.cpp index 5e74ac855..a93f31f86 100644 --- a/src/adiar/bdd/relprod.cpp +++ b/src/adiar/bdd/relprod.cpp @@ -349,6 +349,24 @@ namespace adiar return bdd_relnext(exec_policy(), states, relation, m); } + bdd + bdd_relnext(const exec_policy& ep, + const bdd& states, + const bdd& relation, + const bdd::label_type varcount) + { + const auto map = [=](const bdd::label_type x) -> adiar::optional { + return x < varcount ? adiar::make_optional() : adiar::make_optional(x - varcount); + }; + return bdd_relnext(ep, states, relation, map, replace_type::Shift); + } + + bdd + bdd_relnext(const bdd& states, const bdd& relation, const bdd::label_type varcount) + { + return bdd_relnext(exec_policy(), states, relation, varcount); + } + bdd bdd_relnext(const exec_policy& ep, const bdd& states, const bdd& relation) { @@ -415,6 +433,24 @@ namespace adiar return bdd_relprev(exec_policy(), states, relation, m); } + bdd + bdd_relprev(const exec_policy& ep, + const bdd& states, + const bdd& relation, + const bdd::label_type varcount) + { + const auto map = [=](const bdd::label_type x) -> adiar::optional { + return varcount <= x ? adiar::make_optional() : adiar::make_optional(x + varcount); + }; + return bdd_relprev(ep, states, relation, map, replace_type::Shift); + } + + bdd + bdd_relprev(const bdd& states, const bdd& relation, const bdd::label_type varcount) + { + return bdd_relprev(exec_policy(), states, relation, varcount); + } + bdd bdd_relprev(const exec_policy& ep, const bdd& states, const bdd& relation) { diff --git a/test/adiar/bdd/test_relprod.cpp b/test/adiar/bdd/test_relprod.cpp index 8b55d38a3..7298318dc 100644 --- a/test/adiar/bdd/test_relprod.cpp +++ b/test/adiar/bdd/test_relprod.cpp @@ -6171,27 +6171,27 @@ go_bandit([]() { }); }); - describe("bdd_relnext(const bdd&, const bdd&)", [&]() { - it("has single successor [{10} + H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relnext(huth_10, huth_fig28); + describe("bdd_relnext(const bdd&, const bdd&, const bdd::label_type)", [&]() { + it("has single successor [{01} + K&D Fig. 7(b)]", [&]() { + const bdd out = bdd_relnext(kalin_01, kalin_fig7_b, 2); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_F, terminal_T))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); AssertThat(out_nodes.can_pull(), Is().True()); AssertThat( out_nodes.pull(), - Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_F))); + Is().EqualTo(node(0, bdd::max_id, terminal_F, bdd::pointer_type(1, bdd::max_id)))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); AssertThat(out_meta.can_pull(), Is().True()); AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); @@ -6214,26 +6214,26 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has single successor [{01} + H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relnext(huth_01, huth_fig28); + it("has single successor [{01} + K&D Fig. 9]", [&]() { + const bdd out = bdd_relnext(kalin_01, kalin_fig9, 2); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); AssertThat(out_nodes.can_pull(), Is().True()); AssertThat( out_nodes.pull(), - Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_F))); + Is().EqualTo(node(0, bdd::max_id, terminal_F, bdd::pointer_type(1, bdd::max_id)))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); AssertThat(out_meta.can_pull(), Is().True()); AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); @@ -6256,21 +6256,131 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has multiple successors [{00} + H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relnext(huth_00, huth_fig28); + it("has single successor [{00} + K&D Fig. 9]", [&]() { + const bdd out = bdd_relnext(kalin_00, kalin_fig9, 2); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_F, terminal_T))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(1, bdd::max_id), terminal_F))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has no successors [{11} + K&D Fig. 9]", [&]() { + const bdd out = bdd_relnext(kalin_11, kalin_fig9, 2); + + // Check it looks all right + AssertThat(out->sorted, Is().True()); + AssertThat(out->indexable, Is().True()); + AssertThat(bdd_iscanonical(out), Is().True()); + + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has no successors of non-current states [{01} + K&D Fig. 7(a)]", [&]() { + const bdd out = bdd_relnext(kalin_01, kalin_fig7_a, 2); + + // Check it looks all right + AssertThat(out->sorted, Is().True()); + AssertThat(out->indexable, Is().True()); + AssertThat(bdd_iscanonical(out), Is().True()); + + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has multiple successors [{10} + K&D Fig. 9]", [&]() { + const bdd out = bdd_relnext(kalin_10, kalin_fig9, 2); + + // Check it looks all right + // + // NOTE: Fig. 11 in Kalin's and Dahlsen-Jensen's BSc Thesis + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_F, terminal_T))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); AssertThat(out_meta.can_pull(), Is().False()); @@ -6290,19 +6400,27 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has successors of all current states [H&R Fig. 6.26(a) + H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relnext(huth_fig26_a, huth_fig28); + it("has successors of all current states [K&D Fig. 11 + K&D Fig. 7(b)]", [&]() { + const bdd out = bdd_relnext(kalin_fig11, kalin_fig7_b, 2); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(0, bdd::max_id, terminal_T, terminal_F))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, terminal_F, bdd::pointer_type(1, bdd::max_id)))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + AssertThat(out_meta.can_pull(), Is().True()); AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); @@ -6311,52 +6429,105 @@ go_bandit([]() { AssertThat(out->width, Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u)); AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has no successors for empty set of states [H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relnext(false, huth_fig28, huth_relnext_map); + it("has successors of all current states [K&D Fig. 11 + K&D Fig. 9]", [&]() { + const bdd out = bdd_relnext(kalin_fig11, kalin_fig9, 2); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, terminal_F, bdd::pointer_type(1, bdd::max_id)))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out->width, Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has successors of all current states [{01,10} + K&D Fig. 9]", [&]() { + const bdd out = bdd_relnext(kalin_01_10, kalin_fig9, 2); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_F, terminal_T))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(1, bdd::max_id), terminal_T))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); }); it("has no successors for empty set of states []", [&]() { - const bdd out = bdd_relnext(false, true); + const bdd out = bdd_relnext(false, true, 2); // Check it looks all right node_test_stream out_nodes(out); @@ -6388,7 +6559,7 @@ go_bandit([]() { it("has no successors for empty set of states [] [~]", [&]() { const bdd T = true; - const bdd out = bdd_relnext(bdd_not(T), T); + const bdd out = bdd_relnext(bdd_not(T), T, 2); // Check it looks all right node_test_stream out_nodes(out); @@ -6418,8 +6589,8 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); }); - it("has no successors for empty set of states [H&R Fig. 28]", [&]() { - const bdd out = bdd_relnext(false, huth_fig28); + it("has no successors for empty set of states [K&D Fig. 9]", [&]() { + const bdd out = bdd_relnext(false, kalin_fig9, 2); // Check it looks all right node_test_stream out_nodes(out); @@ -6449,8 +6620,8 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); }); - it("has no successors for empty set of edges [H&R Fig. 26(b) + ]", [&]() { - const bdd out = bdd_relnext(huth_fig26_b, false); + it("has no successors for empty set of edges [K&D Fig. 11 + ]", [&]() { + const bdd out = bdd_relnext(kalin_fig11, false, 2); // Check it looks all right node_test_stream out_nodes(out); @@ -6482,7 +6653,7 @@ go_bandit([]() { it("has no successors for empty set of edges [~ + ]", [&]() { const bdd F = false; - const bdd out = bdd_relnext(bdd_not(F), F); + const bdd out = bdd_relnext(bdd_not(F), F, 2); // Check it looks all right node_test_stream out_nodes(out); @@ -6514,14 +6685,14 @@ go_bandit([]() { it("has no successors for empty set of nodes and edges []", [&]() { const bdd F = false; - const bdd out = bdd_relnext(F, F); + const bdd out = bdd_relnext(F, F, 2); AssertThat(out.file_ptr(), Is().EqualTo(F.file_ptr())); AssertThat(out.is_negated(), Is().False()); }); - it("has all successors for total graph [H&R Fig. 26(b) + ]", [&]() { - const bdd out = bdd_relnext(huth_fig26_b, true); + it("has all successors for total graph [K&D Fig. 11 + ]", [&]() { + const bdd out = bdd_relnext(kalin_fig11, true, 2); // Check it looks all right node_test_stream out_nodes(out); @@ -6553,34 +6724,34 @@ go_bandit([]() { it("has all successors for all nodes and total graph []", [&]() { const bdd T = true; - const bdd out = bdd_relnext(T, T); + const bdd out = bdd_relnext(T, T, 2); AssertThat(out.file_ptr(), Is().EqualTo(T.file_ptr())); AssertThat(out.is_negated(), Is().False()); }); }); - describe("bdd_relprev(const bdd&, const bdd&, )", [&]() { - it("has single predecessor [{01} + K&D Fig. 7(a)]", [&]() { - const bdd out = bdd_relprev(kalin_01, kalin_fig7_a, kalin_relprev_map); + describe("bdd_relnext(const bdd&, const bdd&)", [&]() { + it("has single successor [{10} + H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relnext(huth_10, huth_fig28); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_F, terminal_T))); AssertThat(out_nodes.can_pull(), Is().True()); AssertThat( out_nodes.pull(), - Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(1, bdd::max_id), terminal_F))); + Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_F))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); AssertThat(out_meta.can_pull(), Is().True()); AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); @@ -6603,26 +6774,26 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has single predecessor [{10} + K&D Fig. 7(b)]", [&]() { - const bdd out = bdd_relprev(kalin_10, kalin_fig7_b, kalin_relprev_map); + it("has single successor [{01} + H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relnext(huth_01, huth_fig28); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_F, terminal_T))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); AssertThat(out_nodes.can_pull(), Is().True()); AssertThat( out_nodes.pull(), - Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(1, bdd::max_id), terminal_F))); + Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_F))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); AssertThat(out_meta.can_pull(), Is().True()); AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); @@ -6645,56 +6816,48 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has single predecessor [{10} + K&D Fig. 9]", [&]() { - const bdd out = bdd_relprev(kalin_10, kalin_fig9, kalin_relprev_map); + it("has multiple successors [{00} + H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relnext(huth_00, huth_fig28); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_F, terminal_T))); - - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat( - out_nodes.pull(), - Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(1, bdd::max_id), terminal_F))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); - - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); AssertThat(out_meta.can_pull(), Is().False()); AssertThat(out->width, Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has single predecessor [{01} + H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relprev(huth_01, huth_fig28, huth_relprev_map); + it("has successors of all current states [H&R Fig. 6.26(a) + H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relnext(huth_fig26_a, huth_fig28); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(0, bdd::max_id, terminal_F, terminal_T))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(0, bdd::max_id, terminal_T, terminal_F))); AssertThat(out_nodes.can_pull(), Is().False()); @@ -6721,96 +6884,71 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has single predecessor [{10} + H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relprev(huth_10, huth_fig28, huth_relprev_map); + it("has no successors for empty set of states [H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relnext(false, huth_fig28, huth_relnext_map); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); - - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat( - out_nodes.pull(), - Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_F))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); - - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); - AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(1u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); }); - it("has single predecessor [{00} + B Fig. 18 (x:=0)]", [&]() { - const bdd out = bdd_relprev(bryant_00, bryant_fig18_x0, bryant_relprev_map); + it("has no successors for empty set of states []", [&]() { + const bdd out = bdd_relnext(false, true); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); - - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat( - out_nodes.pull(), - Is().EqualTo(node(1, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_F))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); - - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); - AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(1u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); }); - it("has no predecessors [{00} + K&D Fig. 9]", [&]() { - const bdd out = bdd_relprev(kalin_00, kalin_fig9, kalin_relprev_map); + it("has no successors for empty set of states [] [~]", [&]() { + const bdd T = true; + const bdd out = bdd_relnext(bdd_not(T), T); // Check it looks all right node_test_stream out_nodes(out); @@ -6840,8 +6978,8 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); }); - it("has no predecessors [{01} + B Fig. 18]", [&]() { - const bdd out = bdd_relprev(bryant_01, bryant_fig18, bryant_relprev_map); + it("has no successors for empty set of states [H&R Fig. 28]", [&]() { + const bdd out = bdd_relnext(false, huth_fig28); // Check it looks all right node_test_stream out_nodes(out); @@ -6871,8 +7009,8 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); }); - it("has no predecessors of non-current states [{10} + K&D Fig. 7(a)]", [&]() { - const bdd out = bdd_relprev(kalin_10, kalin_fig7_a, kalin_relprev_map); + it("has no successors for empty set of edges [H&R Fig. 26(b) + ]", [&]() { + const bdd out = bdd_relnext(huth_fig26_b, false); // Check it looks all right node_test_stream out_nodes(out); @@ -6902,8 +7040,9 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); }); - it("has no predecessors of non-current states [{01} + K&D Fig. 7(b)]", [&]() { - const bdd out = bdd_relprev(kalin_01, kalin_fig7_b, kalin_relprev_map); + it("has no successors for empty set of edges [~ + ]", [&]() { + const bdd F = false; + const bdd out = bdd_relnext(bdd_not(F), F); // Check it looks all right node_test_stream out_nodes(out); @@ -6933,14 +7072,22 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); }); - it("has no predecessors of non-current states [{10} + B Fig. 18 (x:=1)]", [&]() { - const bdd out = bdd_relprev(bryant_10, bryant_fig18_x1, bryant_relprev_map); + it("has no successors for empty set of nodes and edges []", [&]() { + const bdd F = false; + const bdd out = bdd_relnext(F, F); + + AssertThat(out.file_ptr(), Is().EqualTo(F.file_ptr())); + AssertThat(out.is_negated(), Is().False()); + }); + + it("has all successors for total graph [H&R Fig. 26(b) + ]", [&]() { + const bdd out = bdd_relnext(huth_fig26_b, true); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); AssertThat(out_nodes.can_pull(), Is().False()); @@ -6951,21 +7098,31 @@ go_bandit([]() { AssertThat(out->width, Is().EqualTo(0u)); AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has multiple predecessors [{01} + K&D Fig. 9]", [&]() { - const bdd out = bdd_relprev(kalin_01, kalin_fig9, kalin_relprev_map); + it("has all successors for all nodes and total graph []", [&]() { + const bdd T = true; + const bdd out = bdd_relnext(T, T); + + AssertThat(out.file_ptr(), Is().EqualTo(T.file_ptr())); + AssertThat(out.is_negated(), Is().False()); + }); + }); + + describe("bdd_relprev(const bdd&, const bdd&, )", [&]() { + it("has single predecessor [{01} + K&D Fig. 7(a)]", [&]() { + const bdd out = bdd_relprev(kalin_01, kalin_fig7_a, kalin_relprev_map); // Check it looks all right node_test_stream out_nodes(out); @@ -6973,6 +7130,11 @@ go_bandit([]() { AssertThat(out_nodes.can_pull(), Is().True()); AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(1, bdd::max_id), terminal_F))); + AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); @@ -6980,44 +7142,47 @@ go_bandit([]() { AssertThat(out_meta.can_pull(), Is().True()); AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + AssertThat(out_meta.can_pull(), Is().False()); AssertThat(out->width, Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u)); AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has multiple predecessors [{00} + H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relprev(huth_00, huth_fig28, huth_relprev_map); + it("has single predecessor [{10} + K&D Fig. 7(b)]", [&]() { + const bdd out = bdd_relprev(kalin_10, kalin_fig7_b, kalin_relprev_map); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_F, terminal_T))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_F, terminal_T))); AssertThat(out_nodes.can_pull(), Is().True()); AssertThat( out_nodes.pull(), - Is().EqualTo(node(0, bdd::max_id, terminal_T, bdd::pointer_type(2, bdd::max_id)))); + Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(1, bdd::max_id), terminal_F))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); AssertThat(out_meta.can_pull(), Is().True()); AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); @@ -7027,287 +7192,284 @@ go_bandit([]() { AssertThat(out->width, Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); + AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has multiple predecessors [{00} + B Fig. 18]", [&]() { - const bdd out = bdd_relprev(bryant_00, bryant_fig18, bryant_relprev_map); + it("has single predecessor [{10} + K&D Fig. 9]", [&]() { + const bdd out = bdd_relprev(kalin_10, kalin_fig9, kalin_relprev_map); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_F, terminal_T))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(1, bdd::max_id), terminal_F))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out->width, Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u)); AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has multiple predecessors [{10} + B Fig. 18]", [&]() { - const bdd out = bdd_relprev(bryant_10, bryant_fig18, bryant_relprev_map); + it("has single predecessor [{01} + H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relprev(huth_01, huth_fig28, huth_relprev_map); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(0, bdd::max_id, terminal_F, terminal_T))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out->width, Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has predecessors of all current states [{00,10} + K&D Fig. 9]", [&]() { - const bdd out = bdd_relprev(kalin_00_01, kalin_fig9, kalin_relprev_map); + it("has single predecessor [{10} + H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relprev(huth_10, huth_fig28, huth_relprev_map); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_F))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); AssertThat(out_meta.can_pull(), Is().False()); AssertThat(out->width, Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u)); AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u)); AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has predecessors of all current states [{01,10} + K&D Fig. 9]", [&]() { - const bdd out = bdd_relprev(kalin_01_10, kalin_fig9, kalin_relprev_map); + it("has single predecessor [{00} + B Fig. 18 (x:=0)]", [&]() { + const bdd out = bdd_relprev(bryant_00, bryant_fig18_x0, bryant_relprev_map); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); AssertThat(out_nodes.can_pull(), Is().True()); AssertThat( out_nodes.pull(), - Is().EqualTo(node(0, bdd::max_id, terminal_T, bdd::pointer_type(1, bdd::max_id)))); + Is().EqualTo(node(1, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_F))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); AssertThat(out_meta.can_pull(), Is().False()); AssertThat(out->width, Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); + AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has predecessors of all current states [K&D Fig. 11 + K&D Fig. 9]", [&]() { - const bdd out = bdd_relprev(kalin_fig11, kalin_fig9, kalin_relprev_map); + it("has no predecessors [{00} + K&D Fig. 9]", [&]() { + const bdd out = bdd_relprev(kalin_00, kalin_fig9, kalin_relprev_map); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); - AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(1u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); }); - it("has predecessors of all current states [H&R Fig.6.26(a) + H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relprev(huth_fig26_a, huth_fig28, huth_relprev_map); + it("has no predecessors [{01} + B Fig. 18]", [&]() { + const bdd out = bdd_relprev(bryant_01, bryant_fig18, bryant_relprev_map); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); - - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat( - out_nodes.pull(), - Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_T))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); - - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); - AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(1u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().LessThanOrEqualTo(3u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().LessThanOrEqualTo(3u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); }); - it("has predecessors of all current states [H&R Fig.6.26(b) + H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relprev(huth_fig26_b, huth_fig28, huth_relprev_map); + it("has no predecessors of non-current states [{10} + K&D Fig. 7(a)]", [&]() { + const bdd out = bdd_relprev(kalin_10, kalin_fig7_a, kalin_relprev_map); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); - - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat( - out_nodes.pull(), - Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_T))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); - - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); - AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(1u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().LessThanOrEqualTo(3u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().LessThanOrEqualTo(3u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); }); - it("has predecessors of all current states [{00,01} + H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relprev(huth_00_01, huth_fig28, huth_relprev_map); + it("has no predecessors of non-current states [{01} + K&D Fig. 7(b)]", [&]() { + const bdd out = bdd_relprev(kalin_01, kalin_fig7_b, kalin_relprev_map); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); AssertThat(out_nodes.can_pull(), Is().False()); @@ -7318,26 +7480,27 @@ go_bandit([]() { AssertThat(out->width, Is().EqualTo(0u)); AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); }); - it("has predecessors of all current states [{00,10} + B Fig. 18 (x:=0)]", [&]() { - const bdd out = bdd_relprev(bryant_00_10, bryant_fig18, bryant_relprev_map); + it("has no predecessors of non-current states [{10} + B Fig. 18 (x:=1)]", [&]() { + const bdd out = bdd_relprev(bryant_10, bryant_fig18_x1, bryant_relprev_map); + // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); AssertThat(out_nodes.can_pull(), Is().False()); @@ -7348,21 +7511,21 @@ go_bandit([]() { AssertThat(out->width, Is().EqualTo(0u)); AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); }); - it("excludes deadlocks [{__} + K&D Fig. 9]", [&]() { - const bdd out = bdd_relprev(true, kalin_fig9, kalin_relprev_map); + it("has multiple predecessors [{01} + K&D Fig. 9]", [&]() { + const bdd out = bdd_relprev(kalin_01, kalin_fig9, kalin_relprev_map); // Check it looks all right node_test_stream out_nodes(out); @@ -7370,17 +7533,51 @@ go_bandit([]() { AssertThat(out_nodes.can_pull(), Is().True()); AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has multiple predecessors [{00} + H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relprev(huth_00, huth_fig28, huth_relprev_map); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_F, terminal_T))); + AssertThat(out_nodes.can_pull(), Is().True()); AssertThat( out_nodes.pull(), - Is().EqualTo(node(0, bdd::max_id, terminal_T, bdd::pointer_type(1, bdd::max_id)))); + Is().EqualTo(node(0, bdd::max_id, terminal_T, bdd::pointer_type(2, bdd::max_id)))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); AssertThat(out_meta.can_pull(), Is().True()); AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); @@ -7403,8 +7600,8 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); }); - it("has no deadlocks [{__} + H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relprev(true, huth_fig28, huth_relprev_map); + it("has multiple predecessors [{00} + B Fig. 18]", [&]() { + const bdd out = bdd_relprev(bryant_00, bryant_fig18, bryant_relprev_map); // Check it looks all right node_test_stream out_nodes(out); @@ -7434,8 +7631,8 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has no deadlocks [{__} + B Fig. 18]", [&]() { - const bdd out = bdd_relprev(true, bryant_fig18, bryant_relprev_map); + it("has multiple predecessors [{10} + B Fig. 18]", [&]() { + const bdd out = bdd_relprev(bryant_10, bryant_fig18, bryant_relprev_map); // Check it looks all right node_test_stream out_nodes(out); @@ -7447,6 +7644,8 @@ go_bandit([]() { level_info_test_stream out_meta(out); + AssertThat(out_meta.can_pull(), Is().False()); + AssertThat(out->width, Is().EqualTo(0u)); AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); @@ -7463,170 +7662,212 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has no predecessors for empty set of states []", [&]() { - const bdd out = bdd_relprev(false, true, kalin_relprev_map); + it("has predecessors of all current states [{00,10} + K&D Fig. 9]", [&]() { + const bdd out = bdd_relprev(kalin_00_01, kalin_fig9, kalin_relprev_map); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out->width, Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has no predecessors for empty set of states [K&D Fig. 9]", [&]() { - const bdd out = bdd_relprev(false, kalin_fig9, kalin_relprev_map); + it("has predecessors of all current states [{01,10} + K&D Fig. 9]", [&]() { + const bdd out = bdd_relprev(kalin_01_10, kalin_fig9, kalin_relprev_map); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, terminal_T, bdd::pointer_type(1, bdd::max_id)))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out->width, Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); }); - it("has no predecessors for empty set of states [H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relprev(false, huth_fig28, huth_relprev_map); + it("has predecessors of all current states [K&D Fig. 11 + K&D Fig. 9]", [&]() { + const bdd out = bdd_relprev(kalin_fig11, kalin_fig9, kalin_relprev_map); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out->width, Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has no predecessors for empty set of states [B Fig. 6.28]", [&]() { - const bdd out = bdd_relprev(false, bryant_fig18, bryant_relprev_map); + it("has predecessors of all current states [H&R Fig.6.26(a) + H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relprev(huth_fig26_a, huth_fig28, huth_relprev_map); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_T))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out->width, Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().LessThanOrEqualTo(3u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().LessThanOrEqualTo(3u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); }); - it("has no predecessors for empty set of edges [K&D Fig. 11 + ]", [&]() { - const bdd out = bdd_relprev(kalin_fig11, false, kalin_relprev_map); + it("has predecessors of all current states [H&R Fig.6.26(b) + H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relprev(huth_fig26_b, huth_fig28, huth_relprev_map); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_T))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out->width, Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().LessThanOrEqualTo(3u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().LessThanOrEqualTo(3u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); }); - it("has no predecessors for empty set of edges [~ + ]", [&]() { - const bdd F = false; - const bdd out = bdd_relprev(bdd_not(F), F, kalin_relprev_map); + it("has predecessors of all current states [{00,01} + H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relprev(huth_00_01, huth_fig28, huth_relprev_map); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); AssertThat(out_nodes.can_pull(), Is().False()); @@ -7637,30 +7878,21 @@ go_bandit([]() { AssertThat(out->width, Is().EqualTo(0u)); AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); - }); - - it("has no predecessors for empty set of nodes and edges []", [&]() { - const bdd F = false; - const bdd out = bdd_relprev(F, F, kalin_relprev_map); - - AssertThat(out.file_ptr(), Is().EqualTo(F.file_ptr())); - AssertThat(out.is_negated(), Is().False()); + AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has all predecessors for total graph [K&D Fig. 11 + ]", [&]() { - const bdd out = bdd_relprev(kalin_fig11, true, kalin_relprev_map); - + it("has predecessors of all current states [{00,10} + B Fig. 18 (x:=0)]", [&]() { + const bdd out = bdd_relprev(bryant_00_10, bryant_fig18, bryant_relprev_map); // Check it looks all right node_test_stream out_nodes(out); @@ -7689,302 +7921,422 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has all predecessors for all nodes and total graph []", [&]() { - const bdd T = true; - const bdd out = bdd_relprev(T, T, kalin_relprev_map); - - AssertThat(out.file_ptr(), Is().EqualTo(T.file_ptr())); - AssertThat(out.is_negated(), Is().False()); - }); + it("excludes deadlocks [{__} + K&D Fig. 9]", [&]() { + const bdd out = bdd_relprev(true, kalin_fig9, kalin_relprev_map); - it("throws exception if mapping is not monotone [{01} + K&D Fig. 9]", [&]() { - const auto kalin_relprev_map__flipped = [&kalin_relprev_pred](int x) -> optional { - return kalin_relprev_pred(x) ? make_optional() : make_optional(2 + !x); - }; - AssertThrows(invalid_argument, - bdd_relprev(kalin_01, kalin_fig9, kalin_relprev_map__flipped)); - }); - }); + // Check it looks all right + node_test_stream out_nodes(out); - describe( - "bdd_relprev(const bdd&, const bdd&, , replace_type::Non_Monotone)", [&]() { - it("throws exception if mapping is not monotone [{01} + K&D Fig. 9]", [&]() { - // NOTE: We actually provide a Monotone map, but do not claim to do so! - AssertThrows( - invalid_argument, - bdd_relprev(kalin_01, kalin_fig9, kalin_relprev_map, replace_type::Non_Monotone)); - }); - }); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); - describe( - "bdd_relprev(const bdd&, const bdd&, , replace_type::Monotone)", [&]() { - it("has single predecessor [{10} + K&D Fig. 9]", [&]() { - const bdd out = - bdd_relprev(kalin_10, kalin_fig9, kalin_relprev_map, replace_type::Monotone); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, terminal_T, bdd::pointer_type(1, bdd::max_id)))); - // Check it looks all right - node_test_stream out_nodes(out); + AssertThat(out_nodes.can_pull(), Is().False()); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_F, terminal_T))); + level_info_test_stream out_meta(out); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat( - out_nodes.pull(), - Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(1, bdd::max_id), terminal_F))); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); - AssertThat(out_nodes.can_pull(), Is().False()); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); - level_info_test_stream out_meta(out); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + AssertThat(out->width, Is().EqualTo(1u)); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); - AssertThat(out_meta.can_pull(), Is().False()); - - AssertThat(out->width, Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); + }); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + it("has no deadlocks [{__} + H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relprev(true, huth_fig28, huth_relprev_map); - AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); - }); + // Check it looks all right + node_test_stream out_nodes(out); - it("has single predecessor [{01} + H&R Fig. 6.28]", [&]() { - const bdd out = - bdd_relprev(huth_01, huth_fig28, huth_relprev_map, replace_type::Monotone); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); - // Check it looks all right - node_test_stream out_nodes(out); + AssertThat(out_nodes.can_pull(), Is().False()); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(0, bdd::max_id, terminal_F, terminal_T))); + level_info_test_stream out_meta(out); - AssertThat(out_nodes.can_pull(), Is().False()); + AssertThat(out_meta.can_pull(), Is().False()); - level_info_test_stream out_meta(out); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out_meta.can_pull(), Is().False()); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->width, Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); + it("has no deadlocks [{__} + B Fig. 18]", [&]() { + const bdd out = bdd_relprev(true, bryant_fig18, bryant_relprev_map); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); + // Check it looks all right + node_test_stream out_nodes(out); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); - }); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); - it("has single predecessor [{00} + B Fig. 18 (x:=0)]", [&]() { - const bdd out = - bdd_relprev(bryant_00, bryant_fig18_x0, bryant_relprev_map, replace_type::Monotone); + AssertThat(out_nodes.can_pull(), Is().False()); - // Check it looks all right - node_test_stream out_nodes(out); + level_info_test_stream out_meta(out); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat( - out_nodes.pull(), - Is().EqualTo(node(1, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_F))); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out_nodes.can_pull(), Is().False()); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - level_info_test_stream out_meta(out); + AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); + it("has no predecessors for empty set of states []", [&]() { + const bdd out = bdd_relprev(false, true, kalin_relprev_map); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + // Check it looks all right + node_test_stream out_nodes(out); - AssertThat(out_meta.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); - AssertThat(out->width, Is().EqualTo(1u)); + AssertThat(out_nodes.can_pull(), Is().False()); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + level_info_test_stream out_meta(out); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); - }); + AssertThat(out->width, Is().EqualTo(0u)); - it("has no predecessors [{00} + K&D Fig. 9]", [&]() { - const bdd out = - bdd_relprev(kalin_00, kalin_fig9, kalin_relprev_map, replace_type::Monotone); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - // Check it looks all right - node_test_stream out_nodes(out); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); - AssertThat(out_nodes.can_pull(), Is().False()); + it("has no predecessors for empty set of states [K&D Fig. 9]", [&]() { + const bdd out = bdd_relprev(false, kalin_fig9, kalin_relprev_map); - level_info_test_stream out_meta(out); + // Check it looks all right + node_test_stream out_nodes(out); - AssertThat(out_meta.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out_nodes.can_pull(), Is().False()); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + level_info_test_stream out_meta(out); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); - }); + AssertThat(out->width, Is().EqualTo(0u)); - it("has no predecessors [{01} + B Fig. 18]", [&]() { - const bdd out = - bdd_relprev(bryant_01, bryant_fig18, bryant_relprev_map, replace_type::Monotone); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - // Check it looks all right - node_test_stream out_nodes(out); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); - AssertThat(out_nodes.can_pull(), Is().False()); + it("has no predecessors for empty set of states [H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relprev(false, huth_fig28, huth_relprev_map); - level_info_test_stream out_meta(out); + // Check it looks all right + node_test_stream out_nodes(out); - AssertThat(out_meta.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out_nodes.can_pull(), Is().False()); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + level_info_test_stream out_meta(out); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); - }); + AssertThat(out->width, Is().EqualTo(0u)); - it("has no predecessors of non-current states [{01} + K&D Fig. 7(b)]", [&]() { - const bdd out = - bdd_relprev(kalin_01, kalin_fig7_b, kalin_relprev_map, replace_type::Monotone); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - // Check it looks all right - node_test_stream out_nodes(out); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); - AssertThat(out_nodes.can_pull(), Is().False()); + it("has no predecessors for empty set of states [B Fig. 6.28]", [&]() { + const bdd out = bdd_relprev(false, bryant_fig18, bryant_relprev_map); - level_info_test_stream out_meta(out); + // Check it looks all right + node_test_stream out_nodes(out); - AssertThat(out_meta.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out_nodes.can_pull(), Is().False()); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + level_info_test_stream out_meta(out); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); - }); + AssertThat(out->width, Is().EqualTo(0u)); - it("has no predecessors of non-current states [{10} + B Fig. 18 (x:=1)]", [&]() { + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has no predecessors for empty set of edges [K&D Fig. 11 + ]", [&]() { + const bdd out = bdd_relprev(kalin_fig11, false, kalin_relprev_map); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has no predecessors for empty set of edges [~ + ]", [&]() { + const bdd F = false; + const bdd out = bdd_relprev(bdd_not(F), F, kalin_relprev_map); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has no predecessors for empty set of nodes and edges []", [&]() { + const bdd F = false; + const bdd out = bdd_relprev(F, F, kalin_relprev_map); + + AssertThat(out.file_ptr(), Is().EqualTo(F.file_ptr())); + AssertThat(out.is_negated(), Is().False()); + }); + + it("has all predecessors for total graph [K&D Fig. 11 + ]", [&]() { + const bdd out = bdd_relprev(kalin_fig11, true, kalin_relprev_map); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has all predecessors for all nodes and total graph []", [&]() { + const bdd T = true; + const bdd out = bdd_relprev(T, T, kalin_relprev_map); + + AssertThat(out.file_ptr(), Is().EqualTo(T.file_ptr())); + AssertThat(out.is_negated(), Is().False()); + }); + + it("throws exception if mapping is not monotone [{01} + K&D Fig. 9]", [&]() { + const auto kalin_relprev_map__flipped = [&kalin_relprev_pred](int x) -> optional { + return kalin_relprev_pred(x) ? make_optional() : make_optional(2 + !x); + }; + AssertThrows(invalid_argument, + bdd_relprev(kalin_01, kalin_fig9, kalin_relprev_map__flipped)); + }); + }); + + describe( + "bdd_relprev(const bdd&, const bdd&, , replace_type::Non_Monotone)", [&]() { + it("throws exception if mapping is not monotone [{01} + K&D Fig. 9]", [&]() { + // NOTE: We actually provide a Monotone map, but do not claim to do so! + AssertThrows( + invalid_argument, + bdd_relprev(kalin_01, kalin_fig9, kalin_relprev_map, replace_type::Non_Monotone)); + }); + }); + + describe( + "bdd_relprev(const bdd&, const bdd&, , replace_type::Monotone)", [&]() { + it("has single predecessor [{10} + K&D Fig. 9]", [&]() { const bdd out = - bdd_relprev(bryant_10, bryant_fig18_x1, bryant_relprev_map, replace_type::Monotone); + bdd_relprev(kalin_10, kalin_fig9, kalin_relprev_map, replace_type::Monotone); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_F, terminal_T))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(1, bdd::max_id), terminal_F))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out->width, Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has multiple predecessors [{01} + K&D Fig. 9]", [&]() { + it("has single predecessor [{01} + H&R Fig. 6.28]", [&]() { const bdd out = - bdd_relprev(kalin_01, kalin_fig9, kalin_relprev_map, replace_type::Monotone); + bdd_relprev(huth_01, huth_fig28, huth_relprev_map, replace_type::Monotone); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(0, bdd::max_id, terminal_F, terminal_T))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); AssertThat(out_meta.can_pull(), Is().False()); @@ -8004,20 +8356,20 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has multiple predecessors [{00} + H&R Fig. 6.28]", [&]() { + it("has single predecessor [{00} + B Fig. 18 (x:=0)]", [&]() { const bdd out = - bdd_relprev(huth_00, huth_fig28, huth_relprev_map, replace_type::Monotone); + bdd_relprev(bryant_00, bryant_fig18_x0, bryant_relprev_map, replace_type::Monotone); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_F, terminal_T))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); AssertThat(out_nodes.can_pull(), Is().True()); AssertThat( out_nodes.pull(), - Is().EqualTo(node(0, bdd::max_id, terminal_T, bdd::pointer_type(2, bdd::max_id)))); + Is().EqualTo(node(1, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_F))); AssertThat(out_nodes.can_pull(), Is().False()); @@ -8027,35 +8379,37 @@ go_bandit([]() { AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); AssertThat(out_meta.can_pull(), Is().False()); AssertThat(out->width, Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); + AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has multiple predecessors [{00} + B Fig. 18]", [&]() { + it("has no predecessors [{00} + K&D Fig. 9]", [&]() { const bdd out = - bdd_relprev(bryant_00, bryant_fig18, bryant_relprev_map, replace_type::Monotone); + bdd_relprev(kalin_00, kalin_fig9, kalin_relprev_map, replace_type::Monotone); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); AssertThat(out_nodes.can_pull(), Is().False()); @@ -8066,51 +8420,257 @@ go_bandit([]() { AssertThat(out->width, Is().EqualTo(0u)); AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); }); - it("has predecessors of all current states [{01,10} + K&D Fig. 9]", [&]() { + it("has no predecessors [{01} + B Fig. 18]", [&]() { const bdd out = - bdd_relprev(kalin_01_10, kalin_fig9, kalin_relprev_map, replace_type::Monotone); + bdd_relprev(bryant_01, bryant_fig18, bryant_relprev_map, replace_type::Monotone); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); - - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat( - out_nodes.pull(), - Is().EqualTo(node(0, bdd::max_id, terminal_T, bdd::pointer_type(1, bdd::max_id)))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); - - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); - AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(1u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has no predecessors of non-current states [{01} + K&D Fig. 7(b)]", [&]() { + const bdd out = + bdd_relprev(kalin_01, kalin_fig7_b, kalin_relprev_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has no predecessors of non-current states [{10} + B Fig. 18 (x:=1)]", [&]() { + const bdd out = + bdd_relprev(bryant_10, bryant_fig18_x1, bryant_relprev_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has multiple predecessors [{01} + K&D Fig. 9]", [&]() { + const bdd out = + bdd_relprev(kalin_01, kalin_fig9, kalin_relprev_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has multiple predecessors [{00} + H&R Fig. 6.28]", [&]() { + const bdd out = + bdd_relprev(huth_00, huth_fig28, huth_relprev_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_F, terminal_T))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, terminal_T, bdd::pointer_type(2, bdd::max_id)))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); + }); + + it("has multiple predecessors [{00} + B Fig. 18]", [&]() { + const bdd out = + bdd_relprev(bryant_00, bryant_fig18, bryant_relprev_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has predecessors of all current states [{01,10} + K&D Fig. 9]", [&]() { + const bdd out = + bdd_relprev(kalin_01_10, kalin_fig9, kalin_relprev_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, terminal_T, bdd::pointer_type(1, bdd::max_id)))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u)); AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); @@ -8222,331 +8782,1143 @@ go_bandit([]() { AssertThat(out_meta.can_pull(), Is().True()); AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); - AssertThat(out_meta.can_pull(), Is().False()); + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); + }); + + it("has no deadlocks [{__} + H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relprev(true, huth_fig28, huth_relprev_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has no deadlocks [{__} + B Fig. 18]", [&]() { + const bdd out = + bdd_relprev(true, bryant_fig18, bryant_relprev_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has no predecessors for empty set of states []", [&]() { + const bdd out = bdd_relprev(false, true, kalin_relprev_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has no predecessors for empty set of states [K&D Fig. 9]", [&]() { + const bdd out = bdd_relprev(false, kalin_fig9, kalin_relprev_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has no predecessors for empty set of states [H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relprev(false, huth_fig28, huth_relprev_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has no predecessors for empty set of states [B Fig. 6.28]", [&]() { + const bdd out = + bdd_relprev(false, bryant_fig18, bryant_relprev_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has no predecessors for empty set of edges [K&D Fig. 11 + ]", [&]() { + const bdd out = + bdd_relprev(kalin_fig11, false, kalin_relprev_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has no predecessors for empty set of edges [~ + ]", [&]() { + const bdd F = false; + const bdd out = bdd_relprev(bdd_not(F), F, kalin_relprev_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has no predecessors for empty set of nodes and edges []", [&]() { + const bdd F = false; + const bdd out = bdd_relprev(F, F, kalin_relprev_map, replace_type::Monotone); + + AssertThat(out.file_ptr(), Is().EqualTo(F.file_ptr())); + AssertThat(out.is_negated(), Is().False()); + }); + + it("has all predecessors for total graph [K&D Fig. 11 + ]", [&]() { + const bdd out = bdd_relprev(kalin_fig11, true, kalin_relprev_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has all predecessors for all nodes and total graph []", [&]() { + const bdd T = true; + const bdd out = bdd_relprev(T, T, kalin_relprev_map, replace_type::Monotone); + + AssertThat(out.file_ptr(), Is().EqualTo(T.file_ptr())); + AssertThat(out.is_negated(), Is().False()); + }); + }); + + describe("bdd_relprev(const bdd&, const bdd&, , replace_type::Shift)", [&]() { + it("has single predecessor [{10} + K&D Fig. 9]", [&]() { + const bdd out = bdd_relprev(kalin_10, kalin_fig9, kalin_relprev_map, replace_type::Shift); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_F, terminal_T))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(1, bdd::max_id), terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has single predecessor [{01} + H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relprev(huth_01, huth_fig28, huth_relprev_map, replace_type::Shift); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(0, bdd::max_id, terminal_F, terminal_T))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has single predecessor [{00} + B Fig. 18 (x:=0)]", [&]() { + const bdd out = + bdd_relprev(bryant_00, bryant_fig18_x0, bryant_relprev_map, replace_type::Shift); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(1, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has no predecessors [{00} + K&D Fig. 9]", [&]() { + const bdd out = bdd_relprev(kalin_00, kalin_fig9, kalin_relprev_map, replace_type::Shift); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has no predecessors [{01} + B Fig. 18]", [&]() { + const bdd out = + bdd_relprev(bryant_01, bryant_fig18, bryant_relprev_map, replace_type::Shift); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has no predecessors of non-current states [{01} + K&D Fig. 7(b)]", [&]() { + const bdd out = bdd_relprev(kalin_01, kalin_fig7_b, kalin_relprev_map, replace_type::Shift); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has no predecessors of non-current states [{10} + B Fig. 18 (x:=1)]", [&]() { + const bdd out = + bdd_relprev(bryant_10, bryant_fig18_x1, bryant_relprev_map, replace_type::Shift); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has multiple predecessors [{01} + K&D Fig. 9]", [&]() { + const bdd out = bdd_relprev(kalin_01, kalin_fig9, kalin_relprev_map, replace_type::Shift); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has multiple predecessors [{00} + H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relprev(huth_00, huth_fig28, huth_relprev_map, replace_type::Shift); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_F, terminal_T))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, terminal_T, bdd::pointer_type(2, bdd::max_id)))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); + }); + + it("has multiple predecessors [{00} + B Fig. 18]", [&]() { + const bdd out = + bdd_relprev(bryant_00, bryant_fig18, bryant_relprev_map, replace_type::Shift); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has predecessors of all current states [{01,10} + K&D Fig. 9]", [&]() { + const bdd out = + bdd_relprev(kalin_01_10, kalin_fig9, kalin_relprev_map, replace_type::Shift); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, terminal_T, bdd::pointer_type(1, bdd::max_id)))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); + }); + + it("has predecessors of all current states [H&R Fig.6.26(a) + H&R Fig. 6.28]", [&]() { + const bdd out = + bdd_relprev(huth_fig26_a, huth_fig28, huth_relprev_map, replace_type::Shift); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_T))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().LessThanOrEqualTo(3u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().LessThanOrEqualTo(3u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); + }); + + it("has predecessors of all current states [{00,10} + B Fig. 18 (x:=0)]", [&]() { + const bdd out = + bdd_relprev(bryant_00_10, bryant_fig18, bryant_relprev_map, replace_type::Shift); + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("excludes deadlocks [{__} + K&D Fig. 9]", [&]() { + const bdd out = bdd_relprev(true, kalin_fig9, kalin_relprev_map, replace_type::Shift); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, terminal_T, bdd::pointer_type(1, bdd::max_id)))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); - AssertThat(out->width, Is().EqualTo(1u)); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + AssertThat(out->width, Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(2u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); - }); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); - it("has no deadlocks [{__} + H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relprev(true, huth_fig28, huth_relprev_map, replace_type::Monotone); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); + }); - // Check it looks all right - node_test_stream out_nodes(out); + it("has no deadlocks [{__} + H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relprev(true, huth_fig28, huth_relprev_map, replace_type::Shift); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); + // Check it looks all right + node_test_stream out_nodes(out); - AssertThat(out_nodes.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); - level_info_test_stream out_meta(out); + AssertThat(out_nodes.can_pull(), Is().False()); - AssertThat(out_meta.can_pull(), Is().False()); + level_info_test_stream out_meta(out); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); - }); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - it("has no deadlocks [{__} + B Fig. 18]", [&]() { - const bdd out = - bdd_relprev(true, bryant_fig18, bryant_relprev_map, replace_type::Monotone); + AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); - // Check it looks all right - node_test_stream out_nodes(out); + it("has no deadlocks [{__} + B Fig. 18]", [&]() { + const bdd out = bdd_relprev(true, bryant_fig18, bryant_relprev_map, replace_type::Shift); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); + // Check it looks all right + node_test_stream out_nodes(out); - AssertThat(out_nodes.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); - level_info_test_stream out_meta(out); + AssertThat(out_nodes.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(0u)); + level_info_test_stream out_meta(out); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); - }); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - it("has no predecessors for empty set of states []", [&]() { - const bdd out = bdd_relprev(false, true, kalin_relprev_map, replace_type::Monotone); + AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); - // Check it looks all right - node_test_stream out_nodes(out); + it("has no predecessors for empty set of states []", [&]() { + const bdd out = bdd_relprev(false, true, kalin_relprev_map, replace_type::Shift); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + // Check it looks all right + node_test_stream out_nodes(out); - AssertThat(out_nodes.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); - level_info_test_stream out_meta(out); + AssertThat(out_nodes.can_pull(), Is().False()); - AssertThat(out_meta.can_pull(), Is().False()); + level_info_test_stream out_meta(out); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); - }); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - it("has no predecessors for empty set of states [K&D Fig. 9]", [&]() { - const bdd out = bdd_relprev(false, kalin_fig9, kalin_relprev_map, replace_type::Monotone); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); - // Check it looks all right - node_test_stream out_nodes(out); + it("has no predecessors for empty set of states [K&D Fig. 9]", [&]() { + const bdd out = bdd_relprev(false, kalin_fig9, kalin_relprev_map, replace_type::Shift); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + // Check it looks all right + node_test_stream out_nodes(out); - AssertThat(out_nodes.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); - level_info_test_stream out_meta(out); + AssertThat(out_nodes.can_pull(), Is().False()); - AssertThat(out_meta.can_pull(), Is().False()); + level_info_test_stream out_meta(out); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); - }); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - it("has no predecessors for empty set of states [H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relprev(false, huth_fig28, huth_relprev_map, replace_type::Monotone); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); - // Check it looks all right - node_test_stream out_nodes(out); + it("has no predecessors for empty set of states [H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relprev(false, huth_fig28, huth_relprev_map, replace_type::Shift); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + // Check it looks all right + node_test_stream out_nodes(out); - AssertThat(out_nodes.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); - level_info_test_stream out_meta(out); + AssertThat(out_nodes.can_pull(), Is().False()); - AssertThat(out_meta.can_pull(), Is().False()); + level_info_test_stream out_meta(out); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); - }); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - it("has no predecessors for empty set of states [B Fig. 6.28]", [&]() { - const bdd out = - bdd_relprev(false, bryant_fig18, bryant_relprev_map, replace_type::Monotone); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); - // Check it looks all right - node_test_stream out_nodes(out); + it("has no predecessors for empty set of states [B Fig. 6.28]", [&]() { + const bdd out = bdd_relprev(false, bryant_fig18, bryant_relprev_map, replace_type::Shift); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + // Check it looks all right + node_test_stream out_nodes(out); - AssertThat(out_nodes.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); - level_info_test_stream out_meta(out); + AssertThat(out_nodes.can_pull(), Is().False()); - AssertThat(out_meta.can_pull(), Is().False()); + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); - }); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); - it("has no predecessors for empty set of edges [K&D Fig. 11 + ]", [&]() { - const bdd out = - bdd_relprev(kalin_fig11, false, kalin_relprev_map, replace_type::Monotone); + it("has no predecessors for empty set of edges [K&D Fig. 11 + ]", [&]() { + const bdd out = bdd_relprev(kalin_fig11, false, kalin_relprev_map, replace_type::Shift); - // Check it looks all right - node_test_stream out_nodes(out); + // Check it looks all right + node_test_stream out_nodes(out); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); - AssertThat(out_nodes.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().False()); - level_info_test_stream out_meta(out); + level_info_test_stream out_meta(out); - AssertThat(out_meta.can_pull(), Is().False()); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); - }); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); - it("has no predecessors for empty set of edges [~ + ]", [&]() { - const bdd F = false; - const bdd out = bdd_relprev(bdd_not(F), F, kalin_relprev_map, replace_type::Monotone); + it("has no predecessors for empty set of edges [~ + ]", [&]() { + const bdd F = false; + const bdd out = bdd_relprev(bdd_not(F), F, kalin_relprev_map, replace_type::Shift); - // Check it looks all right - node_test_stream out_nodes(out); + // Check it looks all right + node_test_stream out_nodes(out); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); - AssertThat(out_nodes.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().False()); - level_info_test_stream out_meta(out); + level_info_test_stream out_meta(out); - AssertThat(out_meta.can_pull(), Is().False()); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); - }); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); - it("has no predecessors for empty set of nodes and edges []", [&]() { - const bdd F = false; - const bdd out = bdd_relprev(F, F, kalin_relprev_map, replace_type::Monotone); + it("has no predecessors for empty set of nodes and edges []", [&]() { + const bdd F = false; + const bdd out = bdd_relprev(F, F, kalin_relprev_map, replace_type::Shift); - AssertThat(out.file_ptr(), Is().EqualTo(F.file_ptr())); - AssertThat(out.is_negated(), Is().False()); - }); + AssertThat(out.file_ptr(), Is().EqualTo(F.file_ptr())); + AssertThat(out.is_negated(), Is().False()); + }); - it("has all predecessors for total graph [K&D Fig. 11 + ]", [&]() { - const bdd out = bdd_relprev(kalin_fig11, true, kalin_relprev_map, replace_type::Monotone); + it("has all predecessors for total graph [K&D Fig. 11 + ]", [&]() { + const bdd out = bdd_relprev(kalin_fig11, true, kalin_relprev_map, replace_type::Shift); - // Check it looks all right - node_test_stream out_nodes(out); + // Check it looks all right + node_test_stream out_nodes(out); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); - AssertThat(out_nodes.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().False()); - level_info_test_stream out_meta(out); + level_info_test_stream out_meta(out); - AssertThat(out_meta.can_pull(), Is().False()); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); - }); + AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); - it("has all predecessors for all nodes and total graph []", [&]() { - const bdd T = true; - const bdd out = bdd_relprev(T, T, kalin_relprev_map, replace_type::Monotone); + it("has all predecessors for all nodes and total graph []", [&]() { + const bdd T = true; + const bdd out = bdd_relprev(T, T, kalin_relprev_map, replace_type::Shift); - AssertThat(out.file_ptr(), Is().EqualTo(T.file_ptr())); - AssertThat(out.is_negated(), Is().False()); - }); + AssertThat(out.file_ptr(), Is().EqualTo(T.file_ptr())); + AssertThat(out.is_negated(), Is().False()); }); + }); - describe("bdd_relprev(const bdd&, const bdd&, , replace_type::Shift)", [&]() { - it("has single predecessor [{10} + K&D Fig. 9]", [&]() { - const bdd out = bdd_relprev(kalin_10, kalin_fig9, kalin_relprev_map, replace_type::Shift); + describe("bdd_relprev(const bdd&, const bdd&, const bdd::label_type)", [&]() { + it("has single predecessor [{01} + K&D Fig. 7(a)]", [&]() { + const bdd out = bdd_relprev(kalin_01, kalin_fig7_a, 2); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_F, terminal_T))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); AssertThat(out_nodes.can_pull(), Is().True()); AssertThat( @@ -8581,19 +9953,27 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has single predecessor [{01} + H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relprev(huth_01, huth_fig28, huth_relprev_map, replace_type::Shift); + it("has single predecessor [{10} + K&D Fig. 7(b)]", [&]() { + const bdd out = bdd_relprev(kalin_10, kalin_fig7_b, 2); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(0, bdd::max_id, terminal_F, terminal_T))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_F, terminal_T))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(1, bdd::max_id), terminal_F))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + AssertThat(out_meta.can_pull(), Is().True()); AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); @@ -8602,57 +9982,54 @@ go_bandit([]() { AssertThat(out->width, Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u)); AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has single predecessor [{00} + B Fig. 18 (x:=0)]", [&]() { - const bdd out = - bdd_relprev(bryant_00, bryant_fig18_x0, bryant_relprev_map, replace_type::Shift); + it("has single predecessor [{10} + K&D Fig. 9]", [&]() { + const bdd out = bdd_relprev(kalin_10, kalin_fig9, 2); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_F, terminal_T))); AssertThat(out_nodes.can_pull(), Is().True()); AssertThat( out_nodes.pull(), - Is().EqualTo(node(1, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_F))); + Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(1, bdd::max_id), terminal_F))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); AssertThat(out_meta.can_pull(), Is().False()); AssertThat(out->width, Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u)); AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); @@ -8660,40 +10037,8 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has no predecessors [{00} + K&D Fig. 9]", [&]() { - const bdd out = bdd_relprev(kalin_00, kalin_fig9, kalin_relprev_map, replace_type::Shift); - - // Check it looks all right - node_test_stream out_nodes(out); - - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); - - AssertThat(out_nodes.can_pull(), Is().False()); - - level_info_test_stream out_meta(out); - - AssertThat(out_meta.can_pull(), Is().False()); - - AssertThat(out->width, Is().EqualTo(0u)); - - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); - }); - - it("has no predecessors [{01} + B Fig. 18]", [&]() { - const bdd out = - bdd_relprev(bryant_01, bryant_fig18, bryant_relprev_map, replace_type::Shift); + it("has no predecessors [{00} + K&D Fig. 9]", [&]() { + const bdd out = bdd_relprev(kalin_00, kalin_fig9, 2); // Check it looks all right node_test_stream out_nodes(out); @@ -8723,8 +10068,8 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); }); - it("has no predecessors of non-current states [{01} + K&D Fig. 7(b)]", [&]() { - const bdd out = bdd_relprev(kalin_01, kalin_fig7_b, kalin_relprev_map, replace_type::Shift); + it("has no predecessors of non-current states [{10} + K&D Fig. 7(a)]", [&]() { + const bdd out = bdd_relprev(kalin_10, kalin_fig7_a, 2); // Check it looks all right node_test_stream out_nodes(out); @@ -8754,9 +10099,8 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); }); - it("has no predecessors of non-current states [{10} + B Fig. 18 (x:=1)]", [&]() { - const bdd out = - bdd_relprev(bryant_10, bryant_fig18_x1, bryant_relprev_map, replace_type::Shift); + it("has no predecessors of non-current states [{01} + K&D Fig. 7(b)]", [&]() { + const bdd out = bdd_relprev(kalin_01, kalin_fig7_b, 2); // Check it looks all right node_test_stream out_nodes(out); @@ -8787,7 +10131,7 @@ go_bandit([]() { }); it("has multiple predecessors [{01} + K&D Fig. 9]", [&]() { - const bdd out = bdd_relprev(kalin_01, kalin_fig9, kalin_relprev_map, replace_type::Shift); + const bdd out = bdd_relprev(kalin_01, kalin_fig9, 2); // Check it looks all right node_test_stream out_nodes(out); @@ -8820,29 +10164,21 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has multiple predecessors [{00} + H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relprev(huth_00, huth_fig28, huth_relprev_map, replace_type::Shift); + it("has predecessors of all current states [{00,10} + K&D Fig. 9]", [&]() { + const bdd out = bdd_relprev(kalin_00_01, kalin_fig9, 2); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_F, terminal_T))); - - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat( - out_nodes.pull(), - Is().EqualTo(node(0, bdd::max_id, terminal_T, bdd::pointer_type(2, bdd::max_id)))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); - - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); AssertThat(out_meta.can_pull(), Is().False()); @@ -8850,53 +10186,20 @@ go_bandit([]() { AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(2u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); - - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); - }); - - it("has multiple predecessors [{00} + B Fig. 18]", [&]() { - const bdd out = - bdd_relprev(bryant_00, bryant_fig18, bryant_relprev_map, replace_type::Shift); - - // Check it looks all right - node_test_stream out_nodes(out); - - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); - - AssertThat(out_nodes.can_pull(), Is().False()); - - level_info_test_stream out_meta(out); - - AssertThat(out_meta.can_pull(), Is().False()); - - AssertThat(out->width, Is().EqualTo(0u)); - - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); it("has predecessors of all current states [{01,10} + K&D Fig. 9]", [&]() { - const bdd out = - bdd_relprev(kalin_01_10, kalin_fig9, kalin_relprev_map, replace_type::Shift); + const bdd out = bdd_relprev(kalin_01_10, kalin_fig9, 2); // Check it looks all right node_test_stream out_nodes(out); @@ -8937,30 +10240,21 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); }); - it("has predecessors of all current states [H&R Fig.6.26(a) + H&R Fig. 6.28]", [&]() { - const bdd out = - bdd_relprev(huth_fig26_a, huth_fig28, huth_relprev_map, replace_type::Shift); + it("has predecessors of all current states [K&D Fig. 11 + K&D Fig. 9]", [&]() { + const bdd out = bdd_relprev(kalin_fig11, kalin_fig9, 2); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); - - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat( - out_nodes.pull(), - Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_T))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); - - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); AssertThat(out_meta.can_pull(), Is().False()); @@ -8968,53 +10262,20 @@ go_bandit([]() { AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().LessThanOrEqualTo(3u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().LessThanOrEqualTo(3u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); - - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); - }); - - it("has predecessors of all current states [{00,10} + B Fig. 18 (x:=0)]", [&]() { - const bdd out = - bdd_relprev(bryant_00_10, bryant_fig18, bryant_relprev_map, replace_type::Shift); - // Check it looks all right - node_test_stream out_nodes(out); - - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); - - AssertThat(out_nodes.can_pull(), Is().False()); - - level_info_test_stream out_meta(out); - - AssertThat(out_meta.can_pull(), Is().False()); - - AssertThat(out->width, Is().EqualTo(0u)); - - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); it("excludes deadlocks [{__} + K&D Fig. 9]", [&]() { - const bdd out = bdd_relprev(true, kalin_fig9, kalin_relprev_map, replace_type::Shift); + const bdd out = bdd_relprev(true, kalin_fig9, 2); // Check it looks all right node_test_stream out_nodes(out); @@ -9055,68 +10316,8 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); }); - it("has no deadlocks [{__} + H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relprev(true, huth_fig28, huth_relprev_map, replace_type::Shift); - - // Check it looks all right - node_test_stream out_nodes(out); - - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); - - AssertThat(out_nodes.can_pull(), Is().False()); - - level_info_test_stream out_meta(out); - - AssertThat(out_meta.can_pull(), Is().False()); - - AssertThat(out->width, Is().EqualTo(0u)); - - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - - AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); - }); - - it("has no deadlocks [{__} + B Fig. 18]", [&]() { - const bdd out = bdd_relprev(true, bryant_fig18, bryant_relprev_map, replace_type::Shift); - - // Check it looks all right - node_test_stream out_nodes(out); - - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); - - AssertThat(out_nodes.can_pull(), Is().False()); - - level_info_test_stream out_meta(out); - - AssertThat(out->width, Is().EqualTo(0u)); - - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - - AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); - }); - it("has no predecessors for empty set of states []", [&]() { - const bdd out = bdd_relprev(false, true, kalin_relprev_map, replace_type::Shift); + const bdd out = bdd_relprev(false, true, 2); // Check it looks all right node_test_stream out_nodes(out); @@ -9147,69 +10348,7 @@ go_bandit([]() { }); it("has no predecessors for empty set of states [K&D Fig. 9]", [&]() { - const bdd out = bdd_relprev(false, kalin_fig9, kalin_relprev_map, replace_type::Shift); - - // Check it looks all right - node_test_stream out_nodes(out); - - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); - - AssertThat(out_nodes.can_pull(), Is().False()); - - level_info_test_stream out_meta(out); - - AssertThat(out_meta.can_pull(), Is().False()); - - AssertThat(out->width, Is().EqualTo(0u)); - - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); - }); - - it("has no predecessors for empty set of states [H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relprev(false, huth_fig28, huth_relprev_map, replace_type::Shift); - - // Check it looks all right - node_test_stream out_nodes(out); - - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); - - AssertThat(out_nodes.can_pull(), Is().False()); - - level_info_test_stream out_meta(out); - - AssertThat(out_meta.can_pull(), Is().False()); - - AssertThat(out->width, Is().EqualTo(0u)); - - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); - }); - - it("has no predecessors for empty set of states [B Fig. 6.28]", [&]() { - const bdd out = bdd_relprev(false, bryant_fig18, bryant_relprev_map, replace_type::Shift); + const bdd out = bdd_relprev(false, kalin_fig9, 2); // Check it looks all right node_test_stream out_nodes(out); @@ -9240,7 +10379,7 @@ go_bandit([]() { }); it("has no predecessors for empty set of edges [K&D Fig. 11 + ]", [&]() { - const bdd out = bdd_relprev(kalin_fig11, false, kalin_relprev_map, replace_type::Shift); + const bdd out = bdd_relprev(kalin_fig11, false, 2); // Check it looks all right node_test_stream out_nodes(out); @@ -9272,7 +10411,7 @@ go_bandit([]() { it("has no predecessors for empty set of edges [~ + ]", [&]() { const bdd F = false; - const bdd out = bdd_relprev(bdd_not(F), F, kalin_relprev_map, replace_type::Shift); + const bdd out = bdd_relprev(bdd_not(F), F, 2); // Check it looks all right node_test_stream out_nodes(out); @@ -9304,14 +10443,14 @@ go_bandit([]() { it("has no predecessors for empty set of nodes and edges []", [&]() { const bdd F = false; - const bdd out = bdd_relprev(F, F, kalin_relprev_map, replace_type::Shift); + const bdd out = bdd_relprev(F, F, 2); AssertThat(out.file_ptr(), Is().EqualTo(F.file_ptr())); AssertThat(out.is_negated(), Is().False()); }); it("has all predecessors for total graph [K&D Fig. 11 + ]", [&]() { - const bdd out = bdd_relprev(kalin_fig11, true, kalin_relprev_map, replace_type::Shift); + const bdd out = bdd_relprev(kalin_fig11, true, 2); // Check it looks all right node_test_stream out_nodes(out); @@ -9343,7 +10482,7 @@ go_bandit([]() { it("has all predecessors for all nodes and total graph []", [&]() { const bdd T = true; - const bdd out = bdd_relprev(T, T, kalin_relprev_map, replace_type::Shift); + const bdd out = bdd_relprev(T, T, 2); AssertThat(out.file_ptr(), Is().EqualTo(T.file_ptr())); AssertThat(out.is_negated(), Is().False());