From 375ea1b194888c91414ca1e5a359027739331193 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 26 Aug 2016 16:32:34 +0200 Subject: [PATCH] fixed bug in cudd minAbstractRepresentative, adapted tests, passing now Former-commit-id: 7f45376343da1f5c854bdfc498b30c09c1c69cce --- .../3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c | 12 +++---- test/functional/storage/CuddDdTest.cpp | 33 ++++++++----------- 2 files changed, 19 insertions(+), 26 deletions(-) diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c b/resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c index 4ffff8722..1f8414017 100644 --- a/resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c +++ b/resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c @@ -1106,7 +1106,7 @@ cuddAddMinAbstractRepresentativeRecur( cuddRef(res1Inf); Cudd_IterDerefBdd(manager,res1); - res2Inf = cuddBddIteRecur(manager, Cudd_Not(tmp), res2, logicalZero); + res2Inf = cuddBddIteRecur(manager, tmp, logicalZero, res2); Cudd_IterDerefBdd(manager,tmp); if (res2Inf == NULL) { Cudd_IterDerefBdd(manager,res2); @@ -1144,8 +1144,8 @@ cuddAddMinAbstractRepresentativeRecur( } cuddRef(res2); - int compl = (res1 == res2) ? 1 : Cudd_IsComplement(res2); - res = (res1 == res2) ? cuddUniqueInter(manager, (int) f->index, one, Cudd_Not(res1)) : cuddUniqueInter(manager, (int) f->index, Cudd_Regular(res2), Cudd_Not(res1)); + int compl = (res1 == res2) ? 0 : Cudd_IsComplement(res2); + res = (res1 == res2) ? res1 : cuddUniqueInter(manager, (int) f->index, Cudd_Regular(res2), compl ? Cudd_Not(res1) : res1); if (res == NULL) { Cudd_IterDerefBdd(manager,res1); Cudd_IterDerefBdd(manager,res2); @@ -1296,7 +1296,7 @@ cuddAddMaxAbstractRepresentativeRecur( Cudd_IterDerefBdd(manager,res1); cuddRef(zero); - res2Inf = cuddBddIteRecur(manager, Cudd_Not(tmp), res2, logicalZero); + res2Inf = cuddBddIteRecur(manager, tmp, logicalZero, res2); if (res2Inf == NULL) { Cudd_IterDerefBdd(manager,res2); Cudd_IterDerefBdd(manager,res1Inf); @@ -1335,8 +1335,8 @@ cuddAddMaxAbstractRepresentativeRecur( } cuddRef(res2); - int compl = (res1 == res2) ? 1 : Cudd_IsComplement(res2); - res = (res1 == res2) ? cuddUniqueInter(manager, (int) f->index, one, Cudd_Not(res1)) : cuddUniqueInter(manager, (int) f->index, Cudd_Regular(res2), compl ? Cudd_Not(res1) : res1); + int compl = (res1 == res2) ? 0 : Cudd_IsComplement(res2); + res = (res1 == res2) ? res1 : cuddUniqueInter(manager, (int) f->index, Cudd_Regular(res2), compl ? Cudd_Not(res1) : res1); if (res == NULL) { Cudd_IterDerefBdd(manager,res1); Cudd_IterDerefBdd(manager,res2); diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index 2229149b3..9bc65b20b 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -196,27 +196,23 @@ TEST(CuddDd, 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_CUDD_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.exportToDot("test_CUDD_representative_false_x.dot"); - bddX0.exportToDot("test_CUDD_bddX0.dot"); +// representative_false_x.exportToDot("test_CUDD_representative_false_x.dot"); +// bddX0.exportToDot("test_CUDD_bddX0.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()); @@ -224,7 +220,6 @@ TEST(CuddDd, 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))) @@ -236,11 +231,10 @@ 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"); +// 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))) @@ -252,11 +246,10 @@ 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"); +// 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))) @@ -264,23 +257,23 @@ TEST(CuddDd, 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_CUDD_representative_complex_z.dot"); - comparison_complex_z.template toAdd().exportToDot("test_CUDD_comparison_complex_z.dot"); +// 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 - 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"); +// 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) {