diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c b/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c index 2c01c6404..b9f6a7db9 100644 --- a/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c +++ b/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c @@ -614,7 +614,7 @@ cuddBddExistAbstractRepresentativeRecur( // FIXME if (res1 == one) { if (F->ref != 1) { - cuddCacheInsert2(manager, Cudd_bddExistAbstractRepresentative, f, cube, one); + cuddCacheInsert2(manager, Cudd_bddExistAbstractRepresentative, f, cube, Cudd_Not(cube)); } return(Cudd_Not(cube)); } diff --git a/resources/3rdparty/sylvan/src/sylvan_bdd_storm.c b/resources/3rdparty/sylvan/src/sylvan_bdd_storm.c index c3226c947..3841049e8 100644 --- a/resources/3rdparty/sylvan/src/sylvan_bdd_storm.c +++ b/resources/3rdparty/sylvan/src/sylvan_bdd_storm.c @@ -11,30 +11,29 @@ TASK_IMPL_3(BDD, sylvan_existsRepresentative, BDD, a, BDD, variables, BDDVAR, pr if (aRegular == sylvan_false) { if (aIsNegated) { - //printf("return in preprocessing...1\n"); - return a; - } - - if (sylvan_set_isempty(variables)) { - //printf("return in preprocessing...2\n"); - return sylvan_true; + if (sylvan_set_isempty(variables)) { + //printf("return in preprocessing...2\n"); + return sylvan_true; + } else { + //printf("return in preprocessing...3\n"); + return variables; + } } else { - //printf("return in preprocessing...3\n"); - return variables; + return a; } } else if (sylvan_set_isempty(variables)) { //printf("return in preprocessing...4\n"); - return a; + return a; } - /* From now on, f and cube are non-constant. */ + /* From now on, f and cube are non-constant. */ bddnode_t na = GETNODE(a); BDDVAR level = bddnode_getvariable(na); bddnode_t nv = GETNODE(variables); BDDVAR vv = bddnode_getvariable(nv); - + //printf("a level %i and cube level %i\n", level, vv); - + /* Abstract a variable that does not appear in f. */ if (level > vv) { BDD _v = sylvan_set_next(variables); @@ -42,20 +41,20 @@ TASK_IMPL_3(BDD, sylvan_existsRepresentative, BDD, a, BDD, variables, BDDVAR, pr if (res == sylvan_invalid) { return sylvan_invalid; } - bdd_refs_push(res); - - BDD res1 = sylvan_makenode(vv, sylvan_false, res); + sylvan_ref(res); + + BDD res1 = sylvan_ite(sylvan_ithvar(vv), sylvan_false, res); if (res1 == sylvan_invalid) { - bdd_refs_pop(1); + sylvan_deref(res); return sylvan_invalid; } - bdd_refs_pop(1); + sylvan_deref(res); //printf("return after abstr. var that does not appear in f...\n"); return res1; } - + /* Compute the cofactors of a. */ BDD aLow = node_low(a, na); // ELSE BDD aHigh = node_high(a, na); // THEN @@ -68,81 +67,88 @@ TASK_IMPL_3(BDD, sylvan_existsRepresentative, BDD, a, BDD, variables, BDDVAR, pr return sylvan_invalid; } if (res1 == sylvan_true) { - return sylvan_true; + return sylvan_not(variables); } - bdd_refs_push(res1); + sylvan_ref(res1); BDD res2 = CALL(sylvan_existsRepresentative, aHigh, _v, level); if (res2 == sylvan_invalid) { - bdd_refs_pop(1); + sylvan_deref(res1); return sylvan_invalid; } - bdd_refs_push(res2); + sylvan_ref(res2); BDD left = CALL(sylvan_exists, aLow, _v, 0); if (left == sylvan_invalid) { - bdd_refs_pop(2); + sylvan_deref(res1); + sylvan_deref(res2); return sylvan_invalid; } - - bdd_refs_push(left); + sylvan_ref(left); BDD res1Inf = sylvan_ite(left, res1, sylvan_false); if (res1Inf == sylvan_invalid) { - bdd_refs_pop(3); + sylvan_deref(res1); + sylvan_deref(res2); + sylvan_deref(left); return sylvan_invalid; } - bdd_refs_push(res1Inf); - - //Cudd_IterDerefBdd(manager,res1); + sylvan_ref(res1Inf); + sylvan_deref(res1); BDD res2Inf = sylvan_ite(left, sylvan_false, res2); if (res2Inf == sylvan_invalid) { - bdd_refs_pop(4); + sylvan_deref(res2); + sylvan_deref(left); + sylvan_deref(res1Inf); return sylvan_invalid; } - bdd_refs_push(res2Inf); - - //Cudd_IterDerefBdd(manager,res2); - //Cudd_IterDerefBdd(manager,left); + sylvan_ref(res2Inf); + sylvan_deref(res2); + sylvan_deref(left); assert(res1Inf != res2Inf); - BDD res = sylvan_makenode(level, res2Inf, res1Inf); - + BDD res = sylvan_ite(sylvan_ithvar(level), res2Inf, res1Inf); if (res == sylvan_invalid) { - bdd_refs_pop(5); + sylvan_deref(res1Inf); + sylvan_deref(res2Inf); return sylvan_invalid; } // cuddCacheInsert2(manager, Cudd_bddExistAbstractRepresentative, f, cube, res); // TODO: CACHING HERE + sylvan_deref(res1Inf); + sylvan_deref(res2Inf); + //printf("return properly computed result...\n"); - bdd_refs_pop(5); return res; } else { /* if (level == vv) */ BDD res1 = CALL(sylvan_existsRepresentative, aLow, variables, level); if (res1 == sylvan_invalid){ return sylvan_invalid; } - bdd_refs_push(res1); + sylvan_ref(res1); BDD res2 = CALL(sylvan_existsRepresentative, aHigh, variables, level); if (res2 == sylvan_invalid) { - bdd_refs_pop(1); + sylvan_deref(res1); return sylvan_invalid; } - bdd_refs_push(res2); + sylvan_ref(res2); /* ITE takes care of possible complementation of res1 and of the ** case in which res1 == res2. */ - BDD res = sylvan_makenode(level, res2, res1); + BDD res = sylvan_ite(sylvan_ithvar(level), res2, res1); if (res == sylvan_invalid) { - bdd_refs_pop(2); + sylvan_deref(res1); + sylvan_deref(res2); return sylvan_invalid; } - bdd_refs_pop(2); + sylvan_deref(res1); + sylvan_deref(res2); + //printf("return of last case...\n"); return res; } diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index 743456578..763fa0a69 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -59,46 +59,80 @@ TEST(CuddDd, BddConstants) { } TEST(CuddDd, BddExistAbstractRepresentative) { - std::shared_ptr> manager(new storm::dd::DdManager()); + std::shared_ptr> manager(new storm::dd::DdManager()); std::pair x; std::pair y; std::pair z; - ASSERT_NO_THROW(x = manager->addMetaVariable("x", 0, 1)); + 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 bddX = manager->getEncoding(x.first, 1); - //bddX.template toAdd().exportToDot("/opt/masterThesis/storm/build/test_cudd_add_x.dot"); - storm::dd::Bdd bddY = manager->getEncoding(y.first, 0); - //bddY.template toAdd().exportToDot("/opt/masterThesis/storm/build/test_cudd_add_y.dot"); - storm::dd::Bdd bddZ = manager->getEncoding(z.first, 0); - //bddZ.template toAdd().exportToDot("/opt/masterThesis/storm/build/test_cudd_add_z.dot"); - - storm::dd::Bdd bddX1Y0Z0 = (bddX && bddY) && bddZ; - //bddX1Y0Z0.template toAdd().exportToDot("/opt/masterThesis/storm/build/test_cudd_bddX1Y0Z0.dot"); - - EXPECT_EQ(1ul, bddX1Y0Z0.getNonZeroCount()); - EXPECT_EQ(1ul, bddX1Y0Z0.getLeafCount()); - EXPECT_EQ(4ul, bddX1Y0Z0.getNodeCount()); - + + storm::dd::Bdd bddX1 = manager->getEncoding(x.first, 1); + storm::dd::Bdd bddY0 = manager->getEncoding(y.first, 0); + storm::dd::Bdd bddZ0 = manager->getEncoding(z.first, 0); + + storm::dd::Bdd bddX1Y0Z0 = (bddX1 && bddY0) && bddZ0; + EXPECT_EQ(1ul, bddX1Y0Z0.getNonZeroCount()); + EXPECT_EQ(1ul, bddX1Y0Z0.getLeafCount()); + EXPECT_EQ(4ul, bddX1Y0Z0.getNodeCount()); + storm::dd::Bdd 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_EQ(1ul, representative_x.getLeafCount()); + EXPECT_EQ(4ul, representative_x.getNodeCount()); EXPECT_TRUE(bddX1Y0Z0 == representative_x); - //representative_x.template toAdd().exportToDot("/opt/masterThesis/storm/build/test_representativea_x.dot"); + storm::dd::Bdd 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_EQ(1ul, representative_y.getLeafCount()); + EXPECT_EQ(4ul, representative_y.getNodeCount()); EXPECT_TRUE(bddX1Y0Z0 == representative_y); - //representative_y.template toAdd().exportToDot("/opt/masterThesis/storm/build/test_representativea_y.dot"); + storm::dd::Bdd 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_EQ(1ul, representative_z.getLeafCount()); + EXPECT_EQ(4ul, representative_z.getNodeCount()); EXPECT_TRUE(bddX1Y0Z0 == representative_z); - //representative_z.template toAdd().exportToDot("/opt/masterThesis/storm/build/test_representativea_z.dot"); + + storm::dd::Bdd 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::Bdd bddX0 = manager->getEncoding(x.first, 0); + storm::dd::Bdd bddY1 = manager->getEncoding(y.first, 1); + storm::dd::Bdd bddZ1 = manager->getEncoding(z.first, 1); + + storm::dd::Bdd bddX0Y0Z0 = (bddX0 && bddY0) && bddZ0; + storm::dd::Bdd bddX1Y1Z1 = (bddX1 && bddY1) && bddZ1; + + storm::dd::Bdd 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); } TEST(CuddDd, AddGetMetaVariableTest) { diff --git a/test/functional/storage/SylvanDdTest.cpp b/test/functional/storage/SylvanDdTest.cpp index 6695d34f7..5b0c26b47 100644 --- a/test/functional/storage/SylvanDdTest.cpp +++ b/test/functional/storage/SylvanDdTest.cpp @@ -62,34 +62,80 @@ TEST(SylvanDd, BddConstants) { } TEST(SylvanDd, BddExistAbstractRepresentative) { - std::shared_ptr> manager(new storm::dd::DdManager()); + std::shared_ptr> manager(new storm::dd::DdManager()); std::pair x; std::pair y; std::pair z; - ASSERT_NO_THROW(x = manager->addMetaVariable("x", 0, 1)); + 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 bddX = manager->getEncoding(x.first, 1); - //bddX.exportToDot("/opt/masterThesis/storm/build/tests_bdd_x.dot"); - storm::dd::Bdd bddY = manager->getEncoding(y.first, 0); - //bddY.exportToDot("/opt/masterThesis/storm/build/tests_bdd_y.dot"); - storm::dd::Bdd bddZ = manager->getEncoding(z.first, 0); - //bddZ.exportToDot("/opt/masterThesis/storm/build/tests_bdd_z.dot"); - - storm::dd::Bdd bddX1Y0Z0 = (bddX && bddY) && bddZ; - //bddX1Y0Z0.exportToDot("/opt/masterThesis/storm/build/tests_bddX1Y0Z0.dot"); - - EXPECT_EQ(1ul, bddX1Y0Z0.getNonZeroCount()); - EXPECT_EQ(1ul, bddX1Y0Z0.getLeafCount()); - EXPECT_EQ(4ul, bddX1Y0Z0.getNodeCount()); - + + storm::dd::Bdd bddX1 = manager->getEncoding(x.first, 1); + storm::dd::Bdd bddY0 = manager->getEncoding(y.first, 0); + storm::dd::Bdd bddZ0 = manager->getEncoding(z.first, 0); + + storm::dd::Bdd bddX1Y0Z0 = (bddX1 && bddY0) && bddZ0; + EXPECT_EQ(1ul, bddX1Y0Z0.getNonZeroCount()); + EXPECT_EQ(1ul, bddX1Y0Z0.getLeafCount()); + EXPECT_EQ(4ul, bddX1Y0Z0.getNodeCount()); + storm::dd::Bdd representative_x = bddX1Y0Z0.existsAbstractRepresentative({x.first}); - //representative_x.exportToDot("/opt/masterThesis/storm/build/tests_representative_x.dot"); + 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::Bdd representative_y = bddX1Y0Z0.existsAbstractRepresentative({y.first}); - //representative_y.exportToDot("/opt/masterThesis/storm/build/tests_representative_y.dot"); + 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::Bdd representative_z = bddX1Y0Z0.existsAbstractRepresentative({z.first}); - //representative_z.exportToDot("/opt/masterThesis/storm/build/tests_representative_z.dot"); + 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::Bdd 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::Bdd bddX0 = manager->getEncoding(x.first, 0); + storm::dd::Bdd bddY1 = manager->getEncoding(y.first, 1); + storm::dd::Bdd bddZ1 = manager->getEncoding(z.first, 1); + + storm::dd::Bdd bddX0Y0Z0 = (bddX0 && bddY0) && bddZ0; + storm::dd::Bdd bddX1Y1Z1 = (bddX1 && bddY1) && bddZ1; + + storm::dd::Bdd bddAllTrueOrAllFalse = bddX0Y0Z0 || bddX1Y1Z1; + //bddAllTrueOrAllFalse.template toAdd().exportToDot("test_Sylvan_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); } TEST(SylvanDd, AddGetMetaVariableTest) {