From 61c227d6f8634fcb24701b2c11ce0ca8b317e49a Mon Sep 17 00:00:00 2001 From: PBerger Date: Wed, 17 Aug 2016 02:12:28 +0200 Subject: [PATCH 1/2] Added a test for reporting a buggy bug. Former-commit-id: aace54765646e473bb44e9c9477a53c634c69190 --- test/functional/storage/CuddDdTest.cpp | 43 ++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index 695d247e2..6edd36da3 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -41,6 +41,49 @@ TEST(CuddDd, Constants) { EXPECT_EQ(2, two.getMax()); } +TEST(CuddDd, BddExistAbstractRepresentative) { + 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(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 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); + //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_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_TRUE(bddX1Y0Z0 == representative_z); + //representative_z.template toAdd().exportToDot("/opt/masterThesis/storm/build/test_representativea_z.dot"); +} + TEST(CuddDd, AddGetMetaVariableTest) { std::shared_ptr> manager(new storm::dd::DdManager()); ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9)); From 3f15644e6006757953a46583359017fe087dc7ed Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 17 Aug 2016 10:23:27 +0200 Subject: [PATCH 2/2] fixed minor bug in existsAbstractRepresentative Former-commit-id: 36a4d8d43509e67fad584accb0334fcc2c7d6a26 --- resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c b/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c index d7aa33cb3..2c01c6404 100644 --- a/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c +++ b/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c @@ -616,7 +616,7 @@ cuddBddExistAbstractRepresentativeRecur( if (F->ref != 1) { cuddCacheInsert2(manager, Cudd_bddExistAbstractRepresentative, f, cube, one); } - return(cube); + return(Cudd_Not(cube)); } cuddRef(res1);