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

Fixed Sylvan implementation of existsAbstractRepresentative. 

Added more tests.


Former-commit-id: 6a4003bb5e
main
PBerger 9 years ago
parent
e41ddfb762
commit
e45b3d2940
4 changed files with 178 additions and 92 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. 2
      resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c
  2. 96
      resources/3rdparty/sylvan/src/sylvan_bdd_storm.c
  3. 86
      test/functional/storage/CuddDdTest.cpp
  4. 86
      test/functional/storage/SylvanDdTest.cpp

2
resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c
View File

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

96
resources/3rdparty/sylvan/src/sylvan_bdd_storm.c
View File

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

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

@ -59,46 +59,80 @@ TEST(CuddDd, BddConstants) {
}
TEST(CuddDd, BddExistAbstractRepresentative) {
std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
std::pair<storm::expressions::Variable, storm::expressions::Variable> x;
std::pair<storm::expressions::Variable, storm::expressions::Variable> y;
std::pair<storm::expressions::Variable, storm::expressions::Variable> 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<storm::dd::DdType::CUDD> bddX = manager->getEncoding(x.first, 1);
//bddX.template toAdd<double>().exportToDot("/opt/masterThesis/storm/build/test_cudd_add_x.dot");
storm::dd::Bdd<storm::dd::DdType::CUDD> bddY = manager->getEncoding(y.first, 0);
//bddY.template toAdd<double>().exportToDot("/opt/masterThesis/storm/build/test_cudd_add_y.dot");
storm::dd::Bdd<storm::dd::DdType::CUDD> bddZ = manager->getEncoding(z.first, 0);
//bddZ.template toAdd<double>().exportToDot("/opt/masterThesis/storm/build/test_cudd_add_z.dot");
storm::dd::Bdd<storm::dd::DdType::CUDD> bddX1Y0Z0 = (bddX && bddY) && bddZ;
//bddX1Y0Z0.template toAdd<double>().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<storm::dd::DdType::CUDD> bddX1 = manager->getEncoding(x.first, 1);
storm::dd::Bdd<storm::dd::DdType::CUDD> bddY0 = manager->getEncoding(y.first, 0);
storm::dd::Bdd<storm::dd::DdType::CUDD> bddZ0 = manager->getEncoding(z.first, 0);
storm::dd::Bdd<storm::dd::DdType::CUDD> bddX1Y0Z0 = (bddX1 && bddY0) && bddZ0;
EXPECT_EQ(1ul, bddX1Y0Z0.getNonZeroCount());
EXPECT_EQ(1ul, bddX1Y0Z0.getLeafCount());
EXPECT_EQ(4ul, bddX1Y0Z0.getNodeCount());
storm::dd::Bdd<storm::dd::DdType::CUDD> 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<double>().exportToDot("/opt/masterThesis/storm/build/test_representativea_x.dot");
storm::dd::Bdd<storm::dd::DdType::CUDD> 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<double>().exportToDot("/opt/masterThesis/storm/build/test_representativea_y.dot");
storm::dd::Bdd<storm::dd::DdType::CUDD> 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<double>().exportToDot("/opt/masterThesis/storm/build/test_representativea_z.dot");
storm::dd::Bdd<storm::dd::DdType::CUDD> 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<storm::dd::DdType::CUDD> bddX0 = manager->getEncoding(x.first, 0);
storm::dd::Bdd<storm::dd::DdType::CUDD> bddY1 = manager->getEncoding(y.first, 1);
storm::dd::Bdd<storm::dd::DdType::CUDD> bddZ1 = manager->getEncoding(z.first, 1);
storm::dd::Bdd<storm::dd::DdType::CUDD> bddX0Y0Z0 = (bddX0 && bddY0) && bddZ0;
storm::dd::Bdd<storm::dd::DdType::CUDD> bddX1Y1Z1 = (bddX1 && bddY1) && bddZ1;
storm::dd::Bdd<storm::dd::DdType::CUDD> bddAllTrueOrAllFalse = bddX0Y0Z0 || bddX1Y1Z1;
//bddAllTrueOrAllFalse.template toAdd<double>().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) {

86
test/functional/storage/SylvanDdTest.cpp
View File

@ -62,34 +62,80 @@ TEST(SylvanDd, BddConstants) {
}
TEST(SylvanDd, BddExistAbstractRepresentative) {
std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::Sylvan>> manager(new storm::dd::DdManager<storm::dd::DdType::Sylvan>());
std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::Sylvan>> manager(new storm::dd::DdManager<storm::dd::DdType::Sylvan>());
std::pair<storm::expressions::Variable, storm::expressions::Variable> x;
std::pair<storm::expressions::Variable, storm::expressions::Variable> y;
std::pair<storm::expressions::Variable, storm::expressions::Variable> 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<storm::dd::DdType::Sylvan> bddX = manager->getEncoding(x.first, 1);
//bddX.exportToDot("/opt/masterThesis/storm/build/tests_bdd_x.dot");
storm::dd::Bdd<storm::dd::DdType::Sylvan> bddY = manager->getEncoding(y.first, 0);
//bddY.exportToDot("/opt/masterThesis/storm/build/tests_bdd_y.dot");
storm::dd::Bdd<storm::dd::DdType::Sylvan> bddZ = manager->getEncoding(z.first, 0);
//bddZ.exportToDot("/opt/masterThesis/storm/build/tests_bdd_z.dot");
storm::dd::Bdd<storm::dd::DdType::Sylvan> 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<storm::dd::DdType::Sylvan> bddX1 = manager->getEncoding(x.first, 1);
storm::dd::Bdd<storm::dd::DdType::Sylvan> bddY0 = manager->getEncoding(y.first, 0);
storm::dd::Bdd<storm::dd::DdType::Sylvan> bddZ0 = manager->getEncoding(z.first, 0);
storm::dd::Bdd<storm::dd::DdType::Sylvan> bddX1Y0Z0 = (bddX1 && bddY0) && bddZ0;
EXPECT_EQ(1ul, bddX1Y0Z0.getNonZeroCount());
EXPECT_EQ(1ul, bddX1Y0Z0.getLeafCount());
EXPECT_EQ(4ul, bddX1Y0Z0.getNodeCount());
storm::dd::Bdd<storm::dd::DdType::Sylvan> 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<storm::dd::DdType::Sylvan> 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<storm::dd::DdType::Sylvan> 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<storm::dd::DdType::Sylvan> 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<storm::dd::DdType::Sylvan> bddX0 = manager->getEncoding(x.first, 0);
storm::dd::Bdd<storm::dd::DdType::Sylvan> bddY1 = manager->getEncoding(y.first, 1);
storm::dd::Bdd<storm::dd::DdType::Sylvan> bddZ1 = manager->getEncoding(z.first, 1);
storm::dd::Bdd<storm::dd::DdType::Sylvan> bddX0Y0Z0 = (bddX0 && bddY0) && bddZ0;
storm::dd::Bdd<storm::dd::DdType::Sylvan> bddX1Y1Z1 = (bddX1 && bddY1) && bddZ1;
storm::dd::Bdd<storm::dd::DdType::Sylvan> bddAllTrueOrAllFalse = bddX0Y0Z0 || bddX1Y1Z1;
//bddAllTrueOrAllFalse.template toAdd<double>().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) {

Write Preview
Loading…
Cancel
Save