From d3c492124aa8fc0fc62b4ae38b1a22a4260354f1 Mon Sep 17 00:00:00 2001 From: PBerger Date: Sat, 27 Aug 2016 19:18:16 +0200 Subject: [PATCH] Fixed min/max Abstract w. repr. Finally. Former-commit-id: 1ccc06d924451a8eb4832f4909d3993e3c3dbb79 --- .../3rdparty/sylvan/src/sylvan_mtbdd_storm.c | 273 ++++++++++++------ .../3rdparty/sylvan/src/sylvan_mtbdd_storm.h | 11 +- test/functional/storage/CuddDdTest.cpp | 116 +++++++- test/functional/storage/SylvanDdTest.cpp | 148 ++++++++-- 4 files changed, 418 insertions(+), 130 deletions(-) diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c index c1aede70c..2a45a913d 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c @@ -213,7 +213,7 @@ TASK_IMPL_2(MTBDD, mtbdd_op_less, MTBDD*, pa, MTBDD*, pb) } /** - * Binary operation Equals (for MTBDDs of same type) + * Binary operation Less or Equals (for MTBDDs of same type) * Only for MTBDDs where either all leaves are Boolean, or Integer, or Double. * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined), * then the result is mtbdd_false (i.e. not defined). @@ -261,6 +261,55 @@ TASK_IMPL_2(MTBDD, mtbdd_op_less_or_equal, MTBDD*, pa, MTBDD*, pb) return mtbdd_invalid; } +/** + * Binary operation Greater or Equals (for MTBDDs of same type) + * Only for MTBDDs where either all leaves are Boolean, or Integer, or Double. + * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined), + * then the result is mtbdd_false (i.e. not defined). + */ +TASK_IMPL_2(MTBDD, mtbdd_op_greater_or_equal, MTBDD*, pa, MTBDD*, pb) +{ + MTBDD a = *pa, b = *pb; + if (a == mtbdd_false && b == mtbdd_false) return mtbdd_true; + if (a == mtbdd_true && b == mtbdd_true) return mtbdd_true; + + mtbddnode_t na = MTBDD_GETNODE(a); + mtbddnode_t nb = MTBDD_GETNODE(b); + + if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) { + uint64_t val_a = mtbddnode_getvalue(na); + uint64_t val_b = mtbddnode_getvalue(nb); + if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) { + int64_t va = *(int64_t*)(&val_a); + int64_t vb = *(int64_t*)(&val_b); + return va >= vb ? mtbdd_true : mtbdd_false; + } else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) { + // both double + double vval_a = *(double*)&val_a; + double vval_b = *(double*)&val_b; + if (vval_a >= vval_b) return mtbdd_true; + return mtbdd_false; + } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) { + // both fraction + uint64_t nom_a = val_a>>32; + uint64_t nom_b = val_b>>32; + uint64_t denom_a = val_a&0xffffffff; + uint64_t denom_b = val_b&0xffffffff; + nom_a *= denom_b; + nom_b *= denom_a; + return nom_a >= nom_b ? mtbdd_true : mtbdd_false; + } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR mtbdd_op_greater_or_equal type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID"); + assert(0); + } +#endif + } + + return mtbdd_invalid; +} + /** * Binary operation Pow (for MTBDDs of same type) * Only for MTBDDs where either all leaves are Double. @@ -629,54 +678,81 @@ TASK_IMPL_2(MTBDD, mtbdd_op_complement, MTBDD, a, size_t, k) } TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR, prev_level) { - BDD zero = sylvan_false; - /* Maybe perform garbage collection */ sylvan_gc_test(); - - /* Cube is guaranteed to be a cube at this point. */ - printf("Entered method.\n"); + + if (sylvan_set_isempty(variables)) { + return sylvan_true; + } + + /* Cube is guaranteed to be a cube at this point. */ if (mtbdd_isleaf(a)) { - printf("is leaf\n"); - if (sylvan_set_isempty(variables)) { - printf("set is empty\n"); - return sylvan_true; // FIXME? - } else { - 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; - } + 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_not(sylvan_ite(sylvan_ithvar(bddnode_getvariable(BDD_GETNODE(variables))), sylvan_true, sylvan_not(res))); + if (res1 == sylvan_invalid) { sylvan_deref(res); - return res1; + return sylvan_invalid; + } + sylvan_deref(res); + return res1; + } + + mtbddnode_t na = MTBDD_GETNODE(a); + uint32_t va = mtbddnode_getvariable(na); + bddnode_t nv = BDD_GETNODE(variables); + BDDVAR vv = bddnode_getvariable(nv); + + /* Abstract a variable that does not appear in a. */ + if (va > vv) { + BDD _v = sylvan_set_next(variables); + BDD res = CALL(mtbdd_minExistsRepresentative, a, _v, va); + if (res == sylvan_invalid) { + return sylvan_invalid; } - } 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); + + // Fill in the missing variables to make representative unique. + sylvan_ref(res); + BDD res1 = sylvan_ite(sylvan_ithvar(vv), sylvan_false, res); + if (res1 == sylvan_invalid) { + sylvan_deref(res); + return sylvan_invalid; + } + sylvan_deref(res); + return res1; + } + + /* TODO: Caching here. */ + /*if ((res = cuddCacheLookup2(manager, Cudd_addMinAbstractRepresentative, f, cube)) != NULL) { + return(res); + }*/ + + + MTBDD E = mtbdd_getlow(a); + MTBDD T = mtbdd_gethigh(a); + + /* If the two indices are the same, so are their levels. */ + if (va == vv) { + BDD _v = sylvan_set_next(variables); + BDD res1 = CALL(mtbdd_minExistsRepresentative, E, _v, va); if (res1 == sylvan_invalid) { return sylvan_invalid; } sylvan_ref(res1); - BDD res2 = CALL(mtbdd_minExistsRepresentative, T, variables, va); + BDD res2 = CALL(mtbdd_minExistsRepresentative, T, _v, va); if (res2 == sylvan_invalid) { sylvan_deref(res1); return sylvan_invalid; } sylvan_ref(res2); - MTBDD left = mtbdd_abstract_min(E, variables); + MTBDD left = mtbdd_abstract_min(E, _v); if (left == mtbdd_invalid) { sylvan_deref(res1); sylvan_deref(res2); @@ -684,7 +760,7 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR } mtbdd_ref(left); - MTBDD right = mtbdd_abstract_min(T, variables); + MTBDD right = mtbdd_abstract_min(T, _v); if (right == mtbdd_invalid) { sylvan_deref(res1); sylvan_deref(res2); @@ -706,7 +782,7 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR mtbdd_deref(left); mtbdd_deref(right); - BDD res1Inf = sylvan_ite(tmp, res1, zero); + BDD res1Inf = sylvan_ite(tmp, res1, sylvan_false); if (res1Inf == sylvan_invalid) { sylvan_deref(res1); sylvan_deref(res2); @@ -715,30 +791,19 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR } 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); + + BDD res2Inf = sylvan_ite(tmp, sylvan_false, res2); if (res2Inf == sylvan_invalid) { sylvan_deref(res2); sylvan_deref(res1Inf); - sylvan_deref(tmp2); + sylvan_deref(tmp); return sylvan_invalid; } sylvan_ref(res2Inf); sylvan_deref(res2); - sylvan_deref(tmp2); + sylvan_deref(tmp); - BDD res = (res1Inf == res2Inf) ? sylvan_ite(sylvan_ithvar(va), zero, res1Inf) : sylvan_ite(sylvan_ithvar(va), res2Inf, res1Inf); + BDD res = (res1Inf == res2Inf) ? sylvan_ite(sylvan_ithvar(va), sylvan_false, res1Inf) : sylvan_ite(sylvan_ithvar(va), res2Inf, res1Inf); if (res == sylvan_invalid) { sylvan_deref(res1Inf); @@ -754,7 +819,59 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR sylvan_deref(res); return res; + } + else { /* if (va < vv) */ + 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); + + BDD res = (res1 == res2) ? res1 : sylvan_ite(sylvan_ithvar(va), res2, res1); + if (res == sylvan_invalid) { + sylvan_deref(res1); + sylvan_deref(res2); + return sylvan_invalid; + } + sylvan_deref(res1); + sylvan_deref(res2); + /* TODO: Caching here. */ + //cuddCacheInsert2(manager, Cudd_addMinAbstractRepresentative, f, cube, res); + return res; + } +} + +TASK_IMPL_3(BDD, mtbdd_maxExistsRepresentative, MTBDD, a, MTBDD, variables, uint32_t, prev_level) { + /* Maybe perform garbage collection */ + sylvan_gc_test(); + + if (sylvan_set_isempty(variables)) { + return sylvan_true; } + + /* Cube is guaranteed to be a cube at this point. */ + if (mtbdd_isleaf(a)) { + BDD _v = sylvan_set_next(variables); + BDD res = CALL(mtbdd_maxExistsRepresentative, a, _v, prev_level); + if (res == sylvan_invalid) { + return sylvan_invalid; + } + sylvan_ref(res); + + BDD res1 = sylvan_not(sylvan_ite(sylvan_ithvar(bddnode_getvariable(BDD_GETNODE(variables))), sylvan_true, sylvan_not(res))); + if (res1 == sylvan_invalid) { + sylvan_deref(res); + return sylvan_invalid; + } + sylvan_deref(res); + return res1; + } mtbddnode_t na = MTBDD_GETNODE(a); uint32_t va = mtbddnode_getvariable(na); @@ -763,16 +880,15 @@ 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); + BDD res = CALL(mtbdd_maxExistsRepresentative, a, _v, va); if (res == sylvan_invalid) { return sylvan_invalid; } // Fill in the missing variables to make representative unique. sylvan_ref(res); - BDD res1 = sylvan_ite(sylvan_ithvar(vv), zero, res); + BDD res1 = sylvan_ite(sylvan_ithvar(vv), sylvan_false, res); if (res1 == sylvan_invalid) { sylvan_deref(res); return sylvan_invalid; @@ -792,22 +908,21 @@ 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); + BDD res1 = CALL(mtbdd_maxExistsRepresentative, E, _v, va); if (res1 == sylvan_invalid) { return sylvan_invalid; } sylvan_ref(res1); - BDD res2 = CALL(mtbdd_minExistsRepresentative, T, _v, va); + BDD res2 = CALL(mtbdd_maxExistsRepresentative, T, _v, va); if (res2 == sylvan_invalid) { sylvan_deref(res1); return sylvan_invalid; } sylvan_ref(res2); - MTBDD left = mtbdd_abstract_min(E, _v); + MTBDD left = mtbdd_abstract_max(E, _v); if (left == mtbdd_invalid) { sylvan_deref(res1); sylvan_deref(res2); @@ -815,7 +930,7 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR } mtbdd_ref(left); - MTBDD right = mtbdd_abstract_min(T, _v); + MTBDD right = mtbdd_abstract_max(T, _v); if (right == mtbdd_invalid) { sylvan_deref(res1); sylvan_deref(res2); @@ -824,7 +939,7 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR } mtbdd_ref(right); - BDD tmp = mtbdd_less_or_equal_as_bdd(left, right); + BDD tmp = mtbdd_greater_or_equal_as_bdd(left, right); if (tmp == sylvan_invalid) { sylvan_deref(res1); sylvan_deref(res2); @@ -837,7 +952,7 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR mtbdd_deref(left); mtbdd_deref(right); - BDD res1Inf = sylvan_ite(tmp, res1, zero); + BDD res1Inf = sylvan_ite(tmp, res1, sylvan_false); if (res1Inf == sylvan_invalid) { sylvan_deref(res1); sylvan_deref(res2); @@ -846,30 +961,19 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR } 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); + + BDD res2Inf = sylvan_ite(tmp, sylvan_false, res2); if (res2Inf == sylvan_invalid) { sylvan_deref(res2); sylvan_deref(res1Inf); - sylvan_deref(tmp2); + sylvan_deref(tmp); return sylvan_invalid; } sylvan_ref(res2Inf); sylvan_deref(res2); - sylvan_deref(tmp2); + sylvan_deref(tmp); - BDD res = (res1Inf == res2Inf) ? sylvan_ite(sylvan_ithvar(va), zero, res1Inf) : sylvan_ite(sylvan_ithvar(va), res2Inf, res1Inf); + BDD res = (res1Inf == res2Inf) ? sylvan_ite(sylvan_ithvar(va), sylvan_false, res1Inf) : sylvan_ite(sylvan_ithvar(va), res2Inf, res1Inf); if (res == sylvan_invalid) { sylvan_deref(res1Inf); @@ -887,20 +991,19 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR return res; } else { /* if (va < vv) */ - printf("va < vv\n"); - BDD res1 = CALL(mtbdd_minExistsRepresentative, E, variables, va); + BDD res1 = CALL(mtbdd_maxExistsRepresentative, E, variables, va); if (res1 == sylvan_invalid) { return sylvan_invalid; } sylvan_ref(res1); - BDD res2 = CALL(mtbdd_minExistsRepresentative, T, variables, va); + BDD res2 = CALL(mtbdd_maxExistsRepresentative, T, variables, va); if (res2 == sylvan_invalid) { sylvan_deref(res1); return sylvan_invalid; } sylvan_ref(res2); - BDD res = (res1 == res2) ? sylvan_ite(sylvan_ithvar(va), zero, res1) : sylvan_ite(sylvan_ithvar(va), res2, res1); + BDD res = (res1 == res2) ? res1 : sylvan_ite(sylvan_ithvar(va), res2, res1); if (res == sylvan_invalid) { sylvan_deref(res1); sylvan_deref(res2); @@ -911,11 +1014,5 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR /* TODO: Caching here. */ //cuddCacheInsert2(manager, Cudd_addMinAbstractRepresentative, f, cube, res); return res; - } -} - -TASK_IMPL_3(BDD, mtbdd_maxExistsRepresentative, MTBDD, a, MTBDD, variables, uint32_t, prev_level) { - (void)variables; - (void)prev_level; - return a; + } } diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h index 0115225e6..8be736c26 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h @@ -28,7 +28,7 @@ TASK_DECL_2(MTBDD, mtbdd_op_less, MTBDD*, MTBDD*) #define mtbdd_less_as_bdd(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_less)) /** - * Binary operation Less (for MTBDDs of same type) + * Binary operation Less or Equal (for MTBDDs of same type) * Only for MTBDDs where either all leaves are Boolean, or Integer, or Double. * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined), * then the result is the other operand. @@ -36,6 +36,15 @@ TASK_DECL_2(MTBDD, mtbdd_op_less, MTBDD*, MTBDD*) TASK_DECL_2(MTBDD, mtbdd_op_less_or_equal, MTBDD*, MTBDD*) #define mtbdd_less_or_equal_as_bdd(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_less_or_equal)) +/** + * Binary operation Greater or Equal (for MTBDDs of same type) + * Only for MTBDDs where either all leaves are Boolean, or Integer, or Double. + * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined), + * then the result is the other operand. + */ +TASK_DECL_2(MTBDD, mtbdd_op_greater_or_equal, MTBDD*, MTBDD*) +#define mtbdd_greater_or_equal_as_bdd(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_greater_or_equal)) + /** * Binary operation Pow (for MTBDDs of same type) * Only for MTBDDs where either all leaves are Integer, Double or a Fraction. diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index 9bc65b20b..0686ac829 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -203,8 +203,6 @@ TEST(CuddDd, AddMinExistAbstractRepresentative) { EXPECT_EQ(1ul, representative_false_x.getLeafCount()); 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::Bdd representative_true_x = addOne.minAbstractRepresentative({x.first}); @@ -231,8 +229,6 @@ TEST(CuddDd, AddMinExistAbstractRepresentative) { 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 storm::dd::Bdd representative_complex_y = complexAdd.minAbstractRepresentative({y.first}); @@ -246,8 +242,6 @@ TEST(CuddDd, AddMinExistAbstractRepresentative) { 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 storm::dd::Bdd representative_complex_z = complexAdd.minAbstractRepresentative({z.first}); @@ -261,9 +255,6 @@ TEST(CuddDd, AddMinExistAbstractRepresentative) { EXPECT_EQ(1ul, representative_complex_z.getLeafCount()); EXPECT_EQ(4ul, representative_complex_z.getNodeCount()); EXPECT_TRUE(representative_complex_z == comparison_complex_z); -// representative_complex_z.exportToDot("test_CUDD_representative_complex_z_bdd.dot"); -// 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 storm::dd::Bdd representative_complex_xyz = complexAdd.minAbstractRepresentative({x.first, y.first, z.first}); @@ -272,8 +263,111 @@ TEST(CuddDd, AddMinExistAbstractRepresentative) { 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, AddMaxExistAbstractRepresentative) { + 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)); + + // Abstract from FALSE + storm::dd::Bdd representative_false_x = addZero.maxAbstractRepresentative({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); + + // Abstract from TRUE + storm::dd::Bdd representative_true_x = addOne.maxAbstractRepresentative({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); + + storm::dd::Bdd representative_true_xyz = addOne.maxAbstractRepresentative({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 + storm::dd::Bdd representative_complex_x = complexAdd.maxAbstractRepresentative({x.first}); + storm::dd::Bdd comparison_complex_x = ( + ((bddX1 && (bddY0 && bddZ0))) + || ((bddX0 && (bddY0 && bddZ1))) + || ((bddX1 && (bddY1 && bddZ0))) + || ((bddX0 && (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); + + // Abstract y + storm::dd::Bdd representative_complex_y = complexAdd.maxAbstractRepresentative({y.first}); + storm::dd::Bdd comparison_complex_y = ( + ((bddX0 && (bddY1 && bddZ0))) + || ((bddX0 && (bddY0 && bddZ1))) + || ((bddX1 && (bddY1 && bddZ0))) + || ((bddX1 && (bddY1 && 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); + + // Abstract z + storm::dd::Bdd representative_complex_z = complexAdd.maxAbstractRepresentative({z.first}); + storm::dd::Bdd comparison_complex_z = ( + ((bddX0 && (bddY0 && bddZ1))) + || ((bddX0 && (bddY1 && bddZ1))) + || ((bddX1 && (bddY0 && bddZ0))) + || ((bddX1 && (bddY1 && bddZ0))) + ); + EXPECT_EQ(4ul, representative_complex_z.getNonZeroCount()); + EXPECT_EQ(1ul, representative_complex_z.getLeafCount()); + EXPECT_EQ(3ul, representative_complex_z.getNodeCount()); + EXPECT_TRUE(representative_complex_z == comparison_complex_z); + + // Abstract x, y, z + storm::dd::Bdd representative_complex_xyz = complexAdd.maxAbstractRepresentative({x.first, y.first, z.first}); + storm::dd::Bdd comparison_complex_xyz = (bddX0 && (bddY0 && bddZ1)); + 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); } TEST(CuddDd, AddGetMetaVariableTest) { diff --git a/test/functional/storage/SylvanDdTest.cpp b/test/functional/storage/SylvanDdTest.cpp index e71542ad2..46be6c67a 100644 --- a/test/functional/storage/SylvanDdTest.cpp +++ b/test/functional/storage/SylvanDdTest.cpp @@ -170,7 +170,7 @@ TEST(SylvanDd, AddMinExistAbstractRepresentative) { 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; @@ -182,7 +182,7 @@ TEST(SylvanDd, AddMinExistAbstractRepresentative) { 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); @@ -199,26 +199,21 @@ TEST(SylvanDd, AddMinExistAbstractRepresentative) { + ((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()); @@ -226,7 +221,6 @@ TEST(SylvanDd, AddMinExistAbstractRepresentative) { 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))) @@ -234,15 +228,12 @@ TEST(SylvanDd, AddMinExistAbstractRepresentative) { || ((bddX0 && (bddY1 && bddZ0))) || ((bddX1 && (bddY1 && bddZ1))) ); - EXPECT_EQ(0ul, representative_complex_x.getNonZeroCount()); + EXPECT_EQ(4ul, representative_complex_x.getNonZeroCount()); EXPECT_EQ(1ul, representative_complex_x.getLeafCount()); - EXPECT_EQ(2ul, representative_complex_x.getNodeCount()); + EXPECT_EQ(3ul, 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))) @@ -250,15 +241,12 @@ TEST(SylvanDd, AddMinExistAbstractRepresentative) { || ((bddX1 && (bddY0 && bddZ0))) || ((bddX1 && (bddY0 && bddZ1))) ); - EXPECT_EQ(0ul, representative_complex_y.getNonZeroCount()); + EXPECT_EQ(4ul, representative_complex_y.getNonZeroCount()); EXPECT_EQ(1ul, representative_complex_y.getLeafCount()); - EXPECT_EQ(2ul, representative_complex_y.getNodeCount()); + EXPECT_EQ(5ul, 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))) @@ -266,23 +254,123 @@ TEST(SylvanDd, AddMinExistAbstractRepresentative) { || ((bddX1 && (bddY0 && bddZ0))) || ((bddX1 && (bddY1 && bddZ1))) ); - EXPECT_EQ(0ul, representative_complex_z.getNonZeroCount()); + EXPECT_EQ(4ul, representative_complex_z.getNonZeroCount()); EXPECT_EQ(1ul, representative_complex_z.getLeafCount()); - EXPECT_EQ(2ul, representative_complex_z.getNodeCount()); + EXPECT_EQ(4ul, 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.getNonZeroCount()); + EXPECT_EQ(1ul, representative_complex_xyz.getLeafCount()); + EXPECT_EQ(4ul, representative_complex_xyz.getNodeCount()); + EXPECT_TRUE(representative_complex_xyz == comparison_complex_xyz); +} + +TEST(SylvanDd, AddMaxExistAbstractRepresentative) { + 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)); + + // Abstract from FALSE + storm::dd::Bdd representative_false_x = addZero.maxAbstractRepresentative({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); + + // Abstract from TRUE + storm::dd::Bdd representative_true_x = addOne.maxAbstractRepresentative({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); + + storm::dd::Bdd representative_true_xyz = addOne.maxAbstractRepresentative({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 + storm::dd::Bdd representative_complex_x = complexAdd.maxAbstractRepresentative({x.first}); + storm::dd::Bdd comparison_complex_x = ( + ((bddX1 && (bddY0 && bddZ0))) + || ((bddX0 && (bddY0 && bddZ1))) + || ((bddX1 && (bddY1 && bddZ0))) + || ((bddX0 && (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); + + // Abstract y + storm::dd::Bdd representative_complex_y = complexAdd.maxAbstractRepresentative({y.first}); + storm::dd::Bdd comparison_complex_y = ( + ((bddX0 && (bddY1 && bddZ0))) + || ((bddX0 && (bddY0 && bddZ1))) + || ((bddX1 && (bddY1 && bddZ0))) + || ((bddX1 && (bddY1 && 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); + + // Abstract z + storm::dd::Bdd representative_complex_z = complexAdd.maxAbstractRepresentative({z.first}); + storm::dd::Bdd comparison_complex_z = ( + ((bddX0 && (bddY0 && bddZ1))) + || ((bddX0 && (bddY1 && bddZ1))) + || ((bddX1 && (bddY0 && bddZ0))) + || ((bddX1 && (bddY1 && bddZ0))) + ); + EXPECT_EQ(4ul, representative_complex_z.getNonZeroCount()); + EXPECT_EQ(1ul, representative_complex_z.getLeafCount()); + EXPECT_EQ(3ul, representative_complex_z.getNodeCount()); + EXPECT_TRUE(representative_complex_z == comparison_complex_z); + + // Abstract x, y, z + storm::dd::Bdd representative_complex_xyz = complexAdd.maxAbstractRepresentative({x.first, y.first, z.first}); + storm::dd::Bdd comparison_complex_xyz = (bddX0 && (bddY0 && bddZ1)); + EXPECT_EQ(1ul, representative_complex_xyz.getNonZeroCount()); EXPECT_EQ(1ul, representative_complex_xyz.getLeafCount()); - EXPECT_EQ(2ul, representative_complex_xyz.getNodeCount()); + EXPECT_EQ(4ul, 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) {