diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c index 7d05d86a1..c1aede70c 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c @@ -635,13 +635,126 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR sylvan_gc_test(); /* Cube is guaranteed to be a cube at this point. */ + printf("Entered method.\n"); if (mtbdd_isleaf(a)) { + printf("is leaf\n"); if (sylvan_set_isempty(variables)) { + printf("set is empty\n"); return sylvan_true; // FIXME? } else { - return variables; + printf("have variables.\n"); + BDD _v = sylvan_set_next(variables); + BDD res = CALL(mtbdd_minExistsRepresentative, a, _v, prev_level); + if (res == sylvan_invalid) { + return sylvan_invalid; + } + sylvan_ref(res); + + BDD res1 = sylvan_ite(sylvan_ithvar(bddnode_getvariable(BDD_GETNODE(variables))), sylvan_false, res); + if (res1 == sylvan_invalid) { + sylvan_deref(res); + return sylvan_invalid; + } + sylvan_deref(res); + return res1; } - } + } else if (sylvan_set_isempty(variables)) { + mtbddnode_t na = MTBDD_GETNODE(a); + uint32_t va = mtbddnode_getvariable(na); + MTBDD E = mtbdd_getlow(a); + MTBDD T = mtbdd_gethigh(a); + BDD res1 = CALL(mtbdd_minExistsRepresentative, E, variables, va); + if (res1 == sylvan_invalid) { + return sylvan_invalid; + } + sylvan_ref(res1); + + BDD res2 = CALL(mtbdd_minExistsRepresentative, T, variables, va); + if (res2 == sylvan_invalid) { + sylvan_deref(res1); + return sylvan_invalid; + } + sylvan_ref(res2); + + MTBDD left = mtbdd_abstract_min(E, variables); + if (left == mtbdd_invalid) { + sylvan_deref(res1); + sylvan_deref(res2); + return sylvan_invalid; + } + mtbdd_ref(left); + + MTBDD right = mtbdd_abstract_min(T, variables); + if (right == mtbdd_invalid) { + sylvan_deref(res1); + sylvan_deref(res2); + mtbdd_deref(left); + return sylvan_invalid; + } + mtbdd_ref(right); + + BDD tmp = mtbdd_less_or_equal_as_bdd(left, right); + if (tmp == sylvan_invalid) { + sylvan_deref(res1); + sylvan_deref(res2); + mtbdd_deref(left); + mtbdd_deref(right); + return sylvan_invalid; + } + sylvan_ref(tmp); + + mtbdd_deref(left); + mtbdd_deref(right); + + BDD res1Inf = sylvan_ite(tmp, res1, zero); + if (res1Inf == sylvan_invalid) { + sylvan_deref(res1); + sylvan_deref(res2); + sylvan_deref(tmp); + return sylvan_invalid; + } + sylvan_ref(res1Inf); + sylvan_deref(res1); + + BDD tmp2 = sylvan_not(tmp); + if (tmp2 == sylvan_invalid) { + sylvan_deref(res2); + mtbdd_deref(left); + mtbdd_deref(right); + sylvan_deref(tmp); + return sylvan_invalid; + } + sylvan_ref(tmp2); + sylvan_deref(tmp); + + BDD res2Inf = sylvan_ite(tmp2, res2, zero); + if (res2Inf == sylvan_invalid) { + sylvan_deref(res2); + sylvan_deref(res1Inf); + sylvan_deref(tmp2); + return sylvan_invalid; + } + sylvan_ref(res2Inf); + sylvan_deref(res2); + sylvan_deref(tmp2); + + BDD res = (res1Inf == res2Inf) ? sylvan_ite(sylvan_ithvar(va), zero, res1Inf) : sylvan_ite(sylvan_ithvar(va), res2Inf, res1Inf); + + if (res == sylvan_invalid) { + sylvan_deref(res1Inf); + sylvan_deref(res2Inf); + return sylvan_invalid; + } + sylvan_ref(res); + sylvan_deref(res1Inf); + sylvan_deref(res2Inf); + + /* TODO: Caching here. */ + //cuddCacheInsert2(manager, Cudd_addMinAbstractRepresentative, f, cube, res); + + sylvan_deref(res); + return res; + } mtbddnode_t na = MTBDD_GETNODE(a); uint32_t va = mtbddnode_getvariable(na); @@ -650,6 +763,7 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR /* Abstract a variable that does not appear in a. */ if (va > vv) { + printf("va > vv\n"); BDD _v = sylvan_set_next(variables); BDD res = CALL(mtbdd_minExistsRepresentative, a, _v, va); if (res == sylvan_invalid) { @@ -678,6 +792,7 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR /* If the two indices are the same, so are their levels. */ if (va == vv) { + printf("va == vv\n"); BDD _v = sylvan_set_next(variables); BDD res1 = CALL(mtbdd_minExistsRepresentative, E, _v, va); if (res1 == sylvan_invalid) { @@ -771,7 +886,8 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR sylvan_deref(res); return res; } - else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */ + else { /* if (va < vv) */ + printf("va < vv\n"); BDD res1 = CALL(mtbdd_minExistsRepresentative, E, variables, va); if (res1 == sylvan_invalid) { return sylvan_invalid; @@ -796,9 +912,6 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR //cuddCacheInsert2(manager, Cudd_addMinAbstractRepresentative, f, cube, res); return res; } - - // Prevent unused variable warning - (void)prev_level; } TASK_IMPL_3(BDD, mtbdd_maxExistsRepresentative, MTBDD, a, MTBDD, variables, uint32_t, prev_level) { diff --git a/src/storage/dd/cudd/InternalCuddAdd.cpp b/src/storage/dd/cudd/InternalCuddAdd.cpp index 6162ef7c5..225685a5c 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storage/dd/cudd/InternalCuddAdd.cpp @@ -149,8 +149,7 @@ namespace storm { template InternalBdd InternalAdd::minAbstractRepresentative(InternalBdd const& cube) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: minAbstractRepresentative"); - //return InternalAdd(ddManager, this->getCuddAdd().MinAbstractRepresentative(cube.toAdd().getCuddAdd())); + return InternalBdd(ddManager, this->getCuddAdd().MinAbstractRepresentative(cube.toAdd().getCuddAdd())); } template diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index 33a58ab4c..2229149b3 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -159,103 +159,129 @@ TEST(CuddDd, BddExistAbstractRepresentative) { EXPECT_EQ(4ul, representative_xyz.getNodeCount()); EXPECT_TRUE(bddX0Y0Z0 == representative_xyz); } -/* + TEST(CuddDd, AddMinExistAbstractRepresentative) { std::shared_ptr> manager(new storm::dd::DdManager()); + + storm::dd::Bdd bddZero; + ASSERT_NO_THROW(bddZero = manager->getBddZero()); + storm::dd::Bdd bddOne; + ASSERT_NO_THROW(bddOne = manager->getBddOne()); - storm::dd::Add zero; - ASSERT_NO_THROW(zero = manager->template getAddZero()); - storm::dd::Add one; - ASSERT_NO_THROW(one = manager->template getAddOne()); - + storm::dd::Add addZero; + ASSERT_NO_THROW(addZero = manager->template getAddZero()); + storm::dd::Add addOne; + ASSERT_NO_THROW(addOne = manager->template getAddOne()); + std::pair x; std::pair y; std::pair z; ASSERT_NO_THROW(x = manager->addMetaVariable("x", 0, 1)); ASSERT_NO_THROW(y = manager->addMetaVariable("y", 0, 1)); ASSERT_NO_THROW(z = manager->addMetaVariable("z", 0, 1)); + + storm::dd::Bdd bddX0 = manager->getEncoding(x.first, 0); + storm::dd::Bdd bddX1 = manager->getEncoding(x.first, 1); + storm::dd::Bdd bddY0 = manager->getEncoding(y.first, 0); + storm::dd::Bdd bddY1 = manager->getEncoding(y.first, 1); + storm::dd::Bdd bddZ0 = manager->getEncoding(z.first, 0); + storm::dd::Bdd bddZ1 = manager->getEncoding(z.first, 1); + storm::dd::Add complexAdd = + ((bddX1 && (bddY1 && bddZ1)).template toAdd() * manager->template getConstant(0.4)) + + ((bddX1 && (bddY1 && bddZ0)).template toAdd() * manager->template getConstant(0.7)) + + ((bddX1 && (bddY0 && bddZ1)).template toAdd() * manager->template getConstant(0.3)) + + ((bddX1 && (bddY0 && bddZ0)).template toAdd() * manager->template getConstant(0.3)) + + ((bddX0 && (bddY1 && bddZ1)).template toAdd() * manager->template getConstant(0.9)) + + ((bddX0 && (bddY1 && bddZ0)).template toAdd() * manager->template getConstant(0.5)) + + ((bddX0 && (bddY0 && bddZ1)).template toAdd() * manager->template getConstant(1.0)) + + ((bddX0 && (bddY0 && bddZ0)).template toAdd() * manager->template getConstant(0.0)); + complexAdd.exportToDot("test_CUDD_complexAdd.dot"); + // Abstract from FALSE - storm::dd::Add representative_false_x = zero.existsAbstractRepresentative({x.first}); + std::cout << "Before FALSE" << std::endl; + storm::dd::Bdd representative_false_x = addZero.minAbstractRepresentative({x.first}); EXPECT_EQ(0ul, representative_false_x.getNonZeroCount()); EXPECT_EQ(1ul, representative_false_x.getLeafCount()); - EXPECT_EQ(1ul, representative_false_x.getNodeCount()); - EXPECT_TRUE(representative_false_x == zero); - + EXPECT_EQ(2ul, representative_false_x.getNodeCount()); + EXPECT_TRUE(representative_false_x == bddX0); + representative_false_x.exportToDot("test_CUDD_representative_false_x.dot"); + bddX0.exportToDot("test_CUDD_bddX0.dot"); + // Abstract from TRUE - storm::dd::Add representative_true_x = one.existsAbstractRepresentative({x.first}); - EXPECT_EQ(1ul, representative_true_x.getNonZeroCount()); + std::cout << "Before TRUE" << std::endl; + storm::dd::Bdd representative_true_x = addOne.minAbstractRepresentative({x.first}); + EXPECT_EQ(0ul, representative_true_x.getNonZeroCount()); EXPECT_EQ(1ul, representative_true_x.getLeafCount()); - EXPECT_EQ(1ul, representative_true_x.getNodeCount()); - EXPECT_TRUE(representative_true_x == manager->getEncoding(x.first, 0)); + EXPECT_EQ(2ul, representative_true_x.getNodeCount()); + EXPECT_TRUE(representative_true_x == bddX0); - storm::dd::Add bddX1 = manager->getEncoding(x.first, 1); - storm::dd::Add bddY0 = manager->getEncoding(y.first, 0); - storm::dd::Add bddZ0 = manager->getEncoding(z.first, 0); - - storm::dd::Add bddX1Y0Z0 = (bddX1 && bddY0) && bddZ0; - EXPECT_EQ(1ul, bddX1Y0Z0.getNonZeroCount()); - EXPECT_EQ(1ul, bddX1Y0Z0.getLeafCount()); - EXPECT_EQ(4ul, bddX1Y0Z0.getNodeCount()); - - storm::dd::Add representative_x = bddX1Y0Z0.existsAbstractRepresentative({x.first}); - EXPECT_EQ(1ul, representative_x.getNonZeroCount()); - EXPECT_EQ(1ul, representative_x.getLeafCount()); - EXPECT_EQ(4ul, representative_x.getNodeCount()); - EXPECT_TRUE(bddX1Y0Z0 == representative_x); - - storm::dd::Add representative_y = bddX1Y0Z0.existsAbstractRepresentative({y.first}); - EXPECT_EQ(1ul, representative_y.getNonZeroCount()); - EXPECT_EQ(1ul, representative_y.getLeafCount()); - EXPECT_EQ(4ul, representative_y.getNodeCount()); - EXPECT_TRUE(bddX1Y0Z0 == representative_y); - - storm::dd::Add representative_z = bddX1Y0Z0.existsAbstractRepresentative({z.first}); - EXPECT_EQ(1ul, representative_z.getNonZeroCount()); - EXPECT_EQ(1ul, representative_z.getLeafCount()); - EXPECT_EQ(4ul, representative_z.getNodeCount()); - EXPECT_TRUE(bddX1Y0Z0 == representative_z); - - storm::dd::Add representative_xyz = bddX1Y0Z0.existsAbstractRepresentative({x.first, y.first, z.first}); - EXPECT_EQ(1ul, representative_xyz.getNonZeroCount()); - EXPECT_EQ(1ul, representative_xyz.getLeafCount()); - EXPECT_EQ(4ul, representative_xyz.getNodeCount()); - EXPECT_TRUE(bddX1Y0Z0 == representative_xyz); - - storm::dd::Add bddX0 = manager->getEncoding(x.first, 0); - storm::dd::Add bddY1 = manager->getEncoding(y.first, 1); - storm::dd::Add bddZ1 = manager->getEncoding(z.first, 1); - - storm::dd::Add bddX0Y0Z0 = (bddX0 && bddY0) && bddZ0; - storm::dd::Add bddX1Y1Z1 = (bddX1 && bddY1) && bddZ1; - - storm::dd::Add bddAllTrueOrAllFalse = bddX0Y0Z0 || bddX1Y1Z1; - //bddAllTrueOrAllFalse.template toAdd().exportToDot("test_cudd_addAllTrueOrAllFalse.dot"); - - representative_x = bddAllTrueOrAllFalse.existsAbstractRepresentative({x.first}); - EXPECT_EQ(2ul, representative_x.getNonZeroCount()); - EXPECT_EQ(1ul, representative_x.getLeafCount()); - EXPECT_EQ(5ul, representative_x.getNodeCount()); - EXPECT_TRUE(bddAllTrueOrAllFalse == representative_x); - - representative_y = bddAllTrueOrAllFalse.existsAbstractRepresentative({y.first}); - EXPECT_EQ(2ul, representative_y.getNonZeroCount()); - EXPECT_EQ(1ul, representative_y.getLeafCount()); - EXPECT_EQ(5ul, representative_y.getNodeCount()); - EXPECT_TRUE(bddAllTrueOrAllFalse == representative_y); - - representative_z = bddAllTrueOrAllFalse.existsAbstractRepresentative({z.first}); - EXPECT_EQ(2ul, representative_z.getNonZeroCount()); - EXPECT_EQ(1ul, representative_z.getLeafCount()); - EXPECT_EQ(5ul, representative_z.getNodeCount()); - EXPECT_TRUE(bddAllTrueOrAllFalse == representative_z); - - representative_xyz = bddAllTrueOrAllFalse.existsAbstractRepresentative({x.first, y.first, z.first}); - EXPECT_EQ(1ul, representative_xyz.getNonZeroCount()); - EXPECT_EQ(1ul, representative_xyz.getLeafCount()); - EXPECT_EQ(4ul, representative_xyz.getNodeCount()); - EXPECT_TRUE(bddX0Y0Z0 == representative_xyz); -}*/ + std::cout << "Before TRUE xyz" << std::endl; + storm::dd::Bdd representative_true_xyz = addOne.minAbstractRepresentative({x.first, y.first, z.first}); + EXPECT_EQ(0ul, representative_true_xyz.getNonZeroCount()); + EXPECT_EQ(1ul, representative_true_xyz.getLeafCount()); + EXPECT_EQ(4ul, representative_true_xyz.getNodeCount()); + EXPECT_TRUE(representative_true_xyz == ((bddX0 && bddY0) && bddZ0)); + + // Abstract x + std::cout << "Before x" << std::endl; + storm::dd::Bdd representative_complex_x = complexAdd.minAbstractRepresentative({x.first}); + storm::dd::Bdd comparison_complex_x = ( + ((bddX0 && (bddY0 && bddZ0))) + || ((bddX1 && (bddY0 && bddZ1))) + || ((bddX0 && (bddY1 && bddZ0))) + || ((bddX1 && (bddY1 && bddZ1))) + ); + EXPECT_EQ(4ul, representative_complex_x.getNonZeroCount()); + EXPECT_EQ(1ul, representative_complex_x.getLeafCount()); + EXPECT_EQ(3ul, representative_complex_x.getNodeCount()); + EXPECT_TRUE(representative_complex_x == comparison_complex_x); + representative_complex_x.template toAdd().exportToDot("test_CUDD_representative_complex_x.dot"); + comparison_complex_x.template toAdd().exportToDot("test_CUDD_comparison_complex_x.dot"); + + // Abstract y + std::cout << "Before y" << std::endl; + storm::dd::Bdd representative_complex_y = complexAdd.minAbstractRepresentative({y.first}); + storm::dd::Bdd comparison_complex_y = ( + ((bddX0 && (bddY0 && bddZ0))) + || ((bddX0 && (bddY1 && bddZ1))) + || ((bddX1 && (bddY0 && bddZ0))) + || ((bddX1 && (bddY0 && bddZ1))) + ); + EXPECT_EQ(4ul, representative_complex_y.getNonZeroCount()); + EXPECT_EQ(1ul, representative_complex_y.getLeafCount()); + EXPECT_EQ(5ul, representative_complex_y.getNodeCount()); + EXPECT_TRUE(representative_complex_y == comparison_complex_y); + representative_complex_y.template toAdd().exportToDot("test_CUDD_representative_complex_y.dot"); + comparison_complex_y.template toAdd().exportToDot("test_CUDD_comparison_complex_y.dot"); + + // Abstract z + std::cout << "Before z" << std::endl; + storm::dd::Bdd representative_complex_z = complexAdd.minAbstractRepresentative({z.first}); + storm::dd::Bdd comparison_complex_z = ( + ((bddX0 && (bddY0 && bddZ0))) + || ((bddX0 && (bddY1 && bddZ0))) + || ((bddX1 && (bddY0 && bddZ0))) + || ((bddX1 && (bddY1 && bddZ1))) + ); + EXPECT_EQ(0ul, representative_complex_z.getNonZeroCount()); + EXPECT_EQ(1ul, representative_complex_z.getLeafCount()); + EXPECT_EQ(2ul, representative_complex_z.getNodeCount()); + EXPECT_TRUE(representative_complex_z == comparison_complex_z); + representative_complex_z.template toAdd().exportToDot("test_CUDD_representative_complex_z.dot"); + comparison_complex_z.template toAdd().exportToDot("test_CUDD_comparison_complex_z.dot"); + + // Abstract x, y, z + std::cout << "Before x, y, z" << std::endl; + storm::dd::Bdd representative_complex_xyz = complexAdd.minAbstractRepresentative({x.first, y.first, z.first}); + storm::dd::Bdd comparison_complex_xyz = (bddX0 && (bddY0 && bddZ0)); + EXPECT_EQ(1ul, representative_complex_xyz.getNonZeroCount()); + EXPECT_EQ(1ul, representative_complex_xyz.getLeafCount()); + EXPECT_EQ(4ul, representative_complex_xyz.getNodeCount()); + EXPECT_TRUE(representative_complex_xyz == comparison_complex_xyz); + representative_complex_xyz.template toAdd().exportToDot("test_CUDD_representative_complex_xyz.dot"); + comparison_complex_xyz.template toAdd().exportToDot("test_CUDD_representative_complex_xyz.dot"); +} TEST(CuddDd, AddGetMetaVariableTest) { std::shared_ptr> manager(new storm::dd::DdManager()); diff --git a/test/functional/storage/SylvanDdTest.cpp b/test/functional/storage/SylvanDdTest.cpp index 8b5c38859..e71542ad2 100644 --- a/test/functional/storage/SylvanDdTest.cpp +++ b/test/functional/storage/SylvanDdTest.cpp @@ -163,6 +163,128 @@ TEST(SylvanDd, BddExistAbstractRepresentative) { EXPECT_TRUE(bddX0Y0Z0 == representative_xyz); } +TEST(SylvanDd, AddMinExistAbstractRepresentative) { + std::shared_ptr> manager(new storm::dd::DdManager()); + + storm::dd::Bdd bddZero; + ASSERT_NO_THROW(bddZero = manager->getBddZero()); + storm::dd::Bdd bddOne; + ASSERT_NO_THROW(bddOne = manager->getBddOne()); + + storm::dd::Add addZero; + ASSERT_NO_THROW(addZero = manager->template getAddZero()); + storm::dd::Add addOne; + ASSERT_NO_THROW(addOne = manager->template getAddOne()); + + std::pair x; + std::pair y; + std::pair z; + ASSERT_NO_THROW(x = manager->addMetaVariable("x", 0, 1)); + ASSERT_NO_THROW(y = manager->addMetaVariable("y", 0, 1)); + ASSERT_NO_THROW(z = manager->addMetaVariable("z", 0, 1)); + + storm::dd::Bdd bddX0 = manager->getEncoding(x.first, 0); + storm::dd::Bdd bddX1 = manager->getEncoding(x.first, 1); + storm::dd::Bdd bddY0 = manager->getEncoding(y.first, 0); + storm::dd::Bdd bddY1 = manager->getEncoding(y.first, 1); + storm::dd::Bdd bddZ0 = manager->getEncoding(z.first, 0); + storm::dd::Bdd bddZ1 = manager->getEncoding(z.first, 1); + + storm::dd::Add complexAdd = + ((bddX1 && (bddY1 && bddZ1)).template toAdd() * manager->template getConstant(0.4)) + + ((bddX1 && (bddY1 && bddZ0)).template toAdd() * manager->template getConstant(0.7)) + + ((bddX1 && (bddY0 && bddZ1)).template toAdd() * manager->template getConstant(0.3)) + + ((bddX1 && (bddY0 && bddZ0)).template toAdd() * manager->template getConstant(0.3)) + + ((bddX0 && (bddY1 && bddZ1)).template toAdd() * manager->template getConstant(0.9)) + + ((bddX0 && (bddY1 && bddZ0)).template toAdd() * manager->template getConstant(0.5)) + + ((bddX0 && (bddY0 && bddZ1)).template toAdd() * manager->template getConstant(1.0)) + + ((bddX0 && (bddY0 && bddZ0)).template toAdd() * manager->template getConstant(0.0)); + complexAdd.exportToDot("test_Sylvan_complexAdd.dot"); + + // Abstract from FALSE + std::cout << "Before FALSE" << std::endl; + storm::dd::Bdd representative_false_x = addZero.minAbstractRepresentative({x.first}); + EXPECT_EQ(0ul, representative_false_x.getNonZeroCount()); + EXPECT_EQ(1ul, representative_false_x.getLeafCount()); + EXPECT_EQ(2ul, representative_false_x.getNodeCount()); + EXPECT_TRUE(representative_false_x == bddX0); + representative_false_x.template toAdd().exportToDot("test_Sylvan_representative_false_x.dot"); + + // Abstract from TRUE + std::cout << "Before TRUE" << std::endl; + storm::dd::Bdd representative_true_x = addOne.minAbstractRepresentative({x.first}); + EXPECT_EQ(0ul, representative_true_x.getNonZeroCount()); + EXPECT_EQ(1ul, representative_true_x.getLeafCount()); + EXPECT_EQ(2ul, representative_true_x.getNodeCount()); + EXPECT_TRUE(representative_true_x == bddX0); + + std::cout << "Before TRUE xyz" << std::endl; + storm::dd::Bdd representative_true_xyz = addOne.minAbstractRepresentative({x.first, y.first, z.first}); + EXPECT_EQ(0ul, representative_true_xyz.getNonZeroCount()); + EXPECT_EQ(1ul, representative_true_xyz.getLeafCount()); + EXPECT_EQ(4ul, representative_true_xyz.getNodeCount()); + EXPECT_TRUE(representative_true_xyz == ((bddX0 && bddY0) && bddZ0)); + + // Abstract x + std::cout << "Before x" << std::endl; + storm::dd::Bdd representative_complex_x = complexAdd.minAbstractRepresentative({x.first}); + storm::dd::Bdd comparison_complex_x = ( + ((bddX0 && (bddY0 && bddZ0))) + || ((bddX1 && (bddY0 && bddZ1))) + || ((bddX0 && (bddY1 && bddZ0))) + || ((bddX1 && (bddY1 && bddZ1))) + ); + EXPECT_EQ(0ul, representative_complex_x.getNonZeroCount()); + EXPECT_EQ(1ul, representative_complex_x.getLeafCount()); + EXPECT_EQ(2ul, representative_complex_x.getNodeCount()); + EXPECT_TRUE(representative_complex_x == comparison_complex_x); + representative_complex_x.template toAdd().exportToDot("test_Sylvan_representative_complex_x.dot"); + comparison_complex_x.template toAdd().exportToDot("test_Sylvan_comparison_complex_x.dot"); + + // Abstract y + std::cout << "Before y" << std::endl; + storm::dd::Bdd representative_complex_y = complexAdd.minAbstractRepresentative({y.first}); + storm::dd::Bdd comparison_complex_y = ( + ((bddX0 && (bddY0 && bddZ0))) + || ((bddX0 && (bddY1 && bddZ1))) + || ((bddX1 && (bddY0 && bddZ0))) + || ((bddX1 && (bddY0 && bddZ1))) + ); + EXPECT_EQ(0ul, representative_complex_y.getNonZeroCount()); + EXPECT_EQ(1ul, representative_complex_y.getLeafCount()); + EXPECT_EQ(2ul, representative_complex_y.getNodeCount()); + EXPECT_TRUE(representative_complex_y == comparison_complex_y); + representative_complex_y.template toAdd().exportToDot("test_Sylvan_representative_complex_y.dot"); + comparison_complex_y.template toAdd().exportToDot("test_Sylvan_comparison_complex_y.dot"); + + // Abstract z + std::cout << "Before z" << std::endl; + storm::dd::Bdd representative_complex_z = complexAdd.minAbstractRepresentative({z.first}); + storm::dd::Bdd comparison_complex_z = ( + ((bddX0 && (bddY0 && bddZ0))) + || ((bddX0 && (bddY1 && bddZ0))) + || ((bddX1 && (bddY0 && bddZ0))) + || ((bddX1 && (bddY1 && bddZ1))) + ); + EXPECT_EQ(0ul, representative_complex_z.getNonZeroCount()); + EXPECT_EQ(1ul, representative_complex_z.getLeafCount()); + EXPECT_EQ(2ul, representative_complex_z.getNodeCount()); + EXPECT_TRUE(representative_complex_z == comparison_complex_z); + representative_complex_z.template toAdd().exportToDot("test_Sylvan_representative_complex_z.dot"); + comparison_complex_z.template toAdd().exportToDot("test_Sylvan_comparison_complex_z.dot"); + + // Abstract x, y, z + std::cout << "Before x, y, z" << std::endl; + storm::dd::Bdd representative_complex_xyz = complexAdd.minAbstractRepresentative({x.first, y.first, z.first}); + storm::dd::Bdd comparison_complex_xyz = (bddX0 && (bddY0 && bddZ0)); + EXPECT_EQ(0ul, representative_complex_xyz.getNonZeroCount()); + EXPECT_EQ(1ul, representative_complex_xyz.getLeafCount()); + EXPECT_EQ(2ul, representative_complex_xyz.getNodeCount()); + EXPECT_TRUE(representative_complex_xyz == comparison_complex_xyz); + representative_complex_xyz.template toAdd().exportToDot("test_Sylvan_representative_complex_xyz.dot"); + comparison_complex_xyz.template toAdd().exportToDot("test_Sylvan_representative_complex_xyz.dot"); +} + TEST(SylvanDd, AddGetMetaVariableTest) { std::shared_ptr> manager(new storm::dd::DdManager()); ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9));