sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

fixed bug in cudd minAbstractRepresentative, adapted tests, passing now 

Former-commit-id: 7f45376343
tempestpy_adaptions
dehnert 8 years ago
parent
39de9561cd
commit
375ea1b194
2 changed files with 19 additions and 26 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 12
      resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c
  2. 33
      test/functional/storage/CuddDdTest.cpp

12
resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c
View File

@ -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);

33
test/functional/storage/CuddDdTest.cpp
View File

@ -196,27 +196,23 @@ TEST(CuddDd, AddMinExistAbstractRepresentative) {
+ ((bddX0 && (bddY1 && bddZ0)).template toAdd<double>() * manager->template getConstant<double>(0.5))
+ ((bddX0 && (bddY0 && bddZ1)).template toAdd<double>() * manager->template getConstant<double>(1.0))
+ ((bddX0 && (bddY0 && bddZ0)).template toAdd<double>() * manager->template getConstant<double>(0.0));
complexAdd.exportToDot("test_CUDD_complexAdd.dot");
// Abstract from FALSE
std::cout << "Before FALSE" << std::endl;
storm::dd::Bdd<storm::dd::DdType::CUDD> 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<storm::dd::DdType::CUDD> 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<storm::dd::DdType::CUDD> 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<storm::dd::DdType::CUDD> representative_complex_x = complexAdd.minAbstractRepresentative({x.first});
storm::dd::Bdd<storm::dd::DdType::CUDD> 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<double>().exportToDot("test_CUDD_representative_complex_x.dot");
comparison_complex_x.template toAdd<double>().exportToDot("test_CUDD_comparison_complex_x.dot");
// representative_complex_x.template toAdd<double>().exportToDot("test_CUDD_representative_complex_x.dot");
// comparison_complex_x.template toAdd<double>().exportToDot("test_CUDD_comparison_complex_x.dot");
// Abstract y
std::cout << "Before y" << std::endl;
storm::dd::Bdd<storm::dd::DdType::CUDD> representative_complex_y = complexAdd.minAbstractRepresentative({y.first});
storm::dd::Bdd<storm::dd::DdType::CUDD> 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<double>().exportToDot("test_CUDD_representative_complex_y.dot");
comparison_complex_y.template toAdd<double>().exportToDot("test_CUDD_comparison_complex_y.dot");
// representative_complex_y.template toAdd<double>().exportToDot("test_CUDD_representative_complex_y.dot");
// comparison_complex_y.template toAdd<double>().exportToDot("test_CUDD_comparison_complex_y.dot");
// Abstract z
std::cout << "Before z" << std::endl;
storm::dd::Bdd<storm::dd::DdType::CUDD> representative_complex_z = complexAdd.minAbstractRepresentative({z.first});
storm::dd::Bdd<storm::dd::DdType::CUDD> 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<double>().exportToDot("test_CUDD_representative_complex_z.dot");
comparison_complex_z.template toAdd<double>().exportToDot("test_CUDD_comparison_complex_z.dot");
// representative_complex_z.exportToDot("test_CUDD_representative_complex_z_bdd.dot");
// representative_complex_z.template toAdd<double>().exportToDot("test_CUDD_representative_complex_z.dot");
// comparison_complex_z.template toAdd<double>().exportToDot("test_CUDD_comparison_complex_z.dot");
// Abstract x, y, z
std::cout << "Before x, y, z" << std::endl;
storm::dd::Bdd<storm::dd::DdType::CUDD> representative_complex_xyz = complexAdd.minAbstractRepresentative({x.first, y.first, z.first});
storm::dd::Bdd<storm::dd::DdType::CUDD> 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<double>().exportToDot("test_CUDD_representative_complex_xyz.dot");
comparison_complex_xyz.template toAdd<double>().exportToDot("test_CUDD_representative_complex_xyz.dot");
// representative_complex_xyz.template toAdd<double>().exportToDot("test_CUDD_representative_complex_xyz.dot");
// comparison_complex_xyz.template toAdd<double>().exportToDot("test_CUDD_representative_complex_xyz.dot");
}
TEST(CuddDd, AddGetMetaVariableTest) {

Write Preview
Loading…
Cancel
Save