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

Added tests for minAbstractRepresentative. 

Everything still in early alpha. Expect Debug output.


Former-commit-id: 2712fce4dd
tempestpy_adaptions
PBerger 8 years ago
parent
66b0817a35
commit
da199866e6
4 changed files with 349 additions and 89 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. 125
      resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c
  2. 3
      src/storage/dd/cudd/InternalCuddAdd.cpp
  3. 188
      test/functional/storage/CuddDdTest.cpp
  4. 122
      test/functional/storage/SylvanDdTest.cpp

125
resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c
View File

@ -635,13 +635,126 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR
sylvan_gc_test();
/* Cube is guaranteed to be a cube at this point. */
printf("Entered method.\n");
if (mtbdd_isleaf(a)) {
printf("is leaf\n");
if (sylvan_set_isempty(variables)) {
printf("set is empty\n");
return sylvan_true; // FIXME?
} else {
return variables;
printf("have variables.\n");
BDD _v = sylvan_set_next(variables);
BDD res = CALL(mtbdd_minExistsRepresentative, a, _v, prev_level);
if (res == sylvan_invalid) {
return sylvan_invalid;
}
sylvan_ref(res);
BDD res1 = sylvan_ite(sylvan_ithvar(bddnode_getvariable(BDD_GETNODE(variables))), sylvan_false, res);
if (res1 == sylvan_invalid) {
sylvan_deref(res);
return sylvan_invalid;
}
sylvan_deref(res);
return res1;
}
}
} else if (sylvan_set_isempty(variables)) {
mtbddnode_t na = MTBDD_GETNODE(a);
uint32_t va = mtbddnode_getvariable(na);
MTBDD E = mtbdd_getlow(a);
MTBDD T = mtbdd_gethigh(a);
BDD res1 = CALL(mtbdd_minExistsRepresentative, E, variables, va);
if (res1 == sylvan_invalid) {
return sylvan_invalid;
}
sylvan_ref(res1);
BDD res2 = CALL(mtbdd_minExistsRepresentative, T, variables, va);
if (res2 == sylvan_invalid) {
sylvan_deref(res1);
return sylvan_invalid;
}
sylvan_ref(res2);
MTBDD left = mtbdd_abstract_min(E, variables);
if (left == mtbdd_invalid) {
sylvan_deref(res1);
sylvan_deref(res2);
return sylvan_invalid;
}
mtbdd_ref(left);
MTBDD right = mtbdd_abstract_min(T, variables);
if (right == mtbdd_invalid) {
sylvan_deref(res1);
sylvan_deref(res2);
mtbdd_deref(left);
return sylvan_invalid;
}
mtbdd_ref(right);
BDD tmp = mtbdd_less_or_equal_as_bdd(left, right);
if (tmp == sylvan_invalid) {
sylvan_deref(res1);
sylvan_deref(res2);
mtbdd_deref(left);
mtbdd_deref(right);
return sylvan_invalid;
}
sylvan_ref(tmp);
mtbdd_deref(left);
mtbdd_deref(right);
BDD res1Inf = sylvan_ite(tmp, res1, zero);
if (res1Inf == sylvan_invalid) {
sylvan_deref(res1);
sylvan_deref(res2);
sylvan_deref(tmp);
return sylvan_invalid;
}
sylvan_ref(res1Inf);
sylvan_deref(res1);
BDD tmp2 = sylvan_not(tmp);
if (tmp2 == sylvan_invalid) {
sylvan_deref(res2);
mtbdd_deref(left);
mtbdd_deref(right);
sylvan_deref(tmp);
return sylvan_invalid;
}
sylvan_ref(tmp2);
sylvan_deref(tmp);
BDD res2Inf = sylvan_ite(tmp2, res2, zero);
if (res2Inf == sylvan_invalid) {
sylvan_deref(res2);
sylvan_deref(res1Inf);
sylvan_deref(tmp2);
return sylvan_invalid;
}
sylvan_ref(res2Inf);
sylvan_deref(res2);
sylvan_deref(tmp2);
BDD res = (res1Inf == res2Inf) ? sylvan_ite(sylvan_ithvar(va), zero, res1Inf) : sylvan_ite(sylvan_ithvar(va), res2Inf, res1Inf);
if (res == sylvan_invalid) {
sylvan_deref(res1Inf);
sylvan_deref(res2Inf);
return sylvan_invalid;
}
sylvan_ref(res);
sylvan_deref(res1Inf);
sylvan_deref(res2Inf);
/* TODO: Caching here. */
//cuddCacheInsert2(manager, Cudd_addMinAbstractRepresentative, f, cube, res);
sylvan_deref(res);
return res;
}
mtbddnode_t na = MTBDD_GETNODE(a);
uint32_t va = mtbddnode_getvariable(na);
@ -650,6 +763,7 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR
/* Abstract a variable that does not appear in a. */
if (va > vv) {
printf("va > vv\n");
BDD _v = sylvan_set_next(variables);
BDD res = CALL(mtbdd_minExistsRepresentative, a, _v, va);
if (res == sylvan_invalid) {
@ -678,6 +792,7 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR
/* If the two indices are the same, so are their levels. */
if (va == vv) {
printf("va == vv\n");
BDD _v = sylvan_set_next(variables);
BDD res1 = CALL(mtbdd_minExistsRepresentative, E, _v, va);
if (res1 == sylvan_invalid) {
@ -771,7 +886,8 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR
sylvan_deref(res);
return res;
}
else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */
else { /* if (va < vv) */
printf("va < vv\n");
BDD res1 = CALL(mtbdd_minExistsRepresentative, E, variables, va);
if (res1 == sylvan_invalid) {
return sylvan_invalid;
@ -796,9 +912,6 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR
//cuddCacheInsert2(manager, Cudd_addMinAbstractRepresentative, f, cube, res);
return res;
}
// Prevent unused variable warning
(void)prev_level;
}
TASK_IMPL_3(BDD, mtbdd_maxExistsRepresentative, MTBDD, a, MTBDD, variables, uint32_t, prev_level) {

3
src/storage/dd/cudd/InternalCuddAdd.cpp
View File

@ -149,8 +149,7 @@ namespace storm {
template<typename ValueType>
InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::minAbstractRepresentative(InternalBdd<DdType::CUDD> const& cube) const {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: minAbstractRepresentative");
//return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().MinAbstractRepresentative(cube.toAdd<ValueType>().getCuddAdd()));
return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().MinAbstractRepresentative(cube.toAdd<ValueType>().getCuddAdd()));
}
template<typename ValueType>

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

@ -159,103 +159,129 @@ TEST(CuddDd, BddExistAbstractRepresentative) {
EXPECT_EQ(4ul, representative_xyz.getNodeCount());
EXPECT_TRUE(bddX0Y0Z0 == representative_xyz);
}
/*
TEST(CuddDd, AddMinExistAbstractRepresentative) {
std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
storm::dd::Bdd<storm::dd::DdType::CUDD> bddZero;
ASSERT_NO_THROW(bddZero = manager->getBddZero());
storm::dd::Bdd<storm::dd::DdType::CUDD> bddOne;
ASSERT_NO_THROW(bddOne = manager->getBddOne());
storm::dd::Add<storm::dd::DdType::CUDD, double> zero;
ASSERT_NO_THROW(zero = manager->template getAddZero<double>());
storm::dd::Add<storm::dd::DdType::CUDD, double> one;
ASSERT_NO_THROW(one = manager->template getAddOne<double>());
storm::dd::Add<storm::dd::DdType::CUDD, double> addZero;
ASSERT_NO_THROW(addZero = manager->template getAddZero<double>());
storm::dd::Add<storm::dd::DdType::CUDD, double> addOne;
ASSERT_NO_THROW(addOne = manager->template getAddOne<double>());
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(y = manager->addMetaVariable("y", 0, 1));
ASSERT_NO_THROW(z = manager->addMetaVariable("z", 0, 1));
storm::dd::Bdd<storm::dd::DdType::CUDD> bddX0 = manager->getEncoding(x.first, 0);
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> bddY1 = manager->getEncoding(y.first, 1);
storm::dd::Bdd<storm::dd::DdType::CUDD> bddZ0 = manager->getEncoding(z.first, 0);
storm::dd::Bdd<storm::dd::DdType::CUDD> bddZ1 = manager->getEncoding(z.first, 1);
storm::dd::Add<storm::dd::DdType::CUDD, double> complexAdd =
((bddX1 && (bddY1 && bddZ1)).template toAdd<double>() * manager->template getConstant<double>(0.4))
+ ((bddX1 && (bddY1 && bddZ0)).template toAdd<double>() * manager->template getConstant<double>(0.7))
+ ((bddX1 && (bddY0 && bddZ1)).template toAdd<double>() * manager->template getConstant<double>(0.3))
+ ((bddX1 && (bddY0 && bddZ0)).template toAdd<double>() * manager->template getConstant<double>(0.3))
+ ((bddX0 && (bddY1 && bddZ1)).template toAdd<double>() * manager->template getConstant<double>(0.9))
+ ((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
storm::dd::Add<storm::dd::DdType::CUDD, double> representative_false_x = zero.existsAbstractRepresentative({x.first});
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(1ul, representative_false_x.getNodeCount());
EXPECT_TRUE(representative_false_x == zero);
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");
// Abstract from TRUE
storm::dd::Add<storm::dd::DdType::CUDD, double> representative_true_x = one.existsAbstractRepresentative({x.first});
EXPECT_EQ(1ul, representative_true_x.getNonZeroCount());
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(1ul, representative_true_x.getNodeCount());
EXPECT_TRUE(representative_true_x == manager->getEncoding(x.first, 0));
EXPECT_EQ(2ul, representative_true_x.getNodeCount());
EXPECT_TRUE(representative_true_x == bddX0);
storm::dd::Add<storm::dd::DdType::CUDD, double> bddX1 = manager->getEncoding(x.first, 1);
storm::dd::Add<storm::dd::DdType::CUDD, double> bddY0 = manager->getEncoding(y.first, 0);
storm::dd::Add<storm::dd::DdType::CUDD, double> bddZ0 = manager->getEncoding(z.first, 0);
storm::dd::Add<storm::dd::DdType::CUDD, double> bddX1Y0Z0 = (bddX1 && bddY0) && bddZ0;
EXPECT_EQ(1ul, bddX1Y0Z0.getNonZeroCount());
EXPECT_EQ(1ul, bddX1Y0Z0.getLeafCount());
EXPECT_EQ(4ul, bddX1Y0Z0.getNodeCount());
storm::dd::Add<storm::dd::DdType::CUDD, double> 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);
storm::dd::Add<storm::dd::DdType::CUDD, double> 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);
storm::dd::Add<storm::dd::DdType::CUDD, double> 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);
storm::dd::Add<storm::dd::DdType::CUDD, double> 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::Add<storm::dd::DdType::CUDD, double> bddX0 = manager->getEncoding(x.first, 0);
storm::dd::Add<storm::dd::DdType::CUDD, double> bddY1 = manager->getEncoding(y.first, 1);
storm::dd::Add<storm::dd::DdType::CUDD, double> bddZ1 = manager->getEncoding(z.first, 1);
storm::dd::Add<storm::dd::DdType::CUDD, double> bddX0Y0Z0 = (bddX0 && bddY0) && bddZ0;
storm::dd::Add<storm::dd::DdType::CUDD, double> bddX1Y1Z1 = (bddX1 && bddY1) && bddZ1;
storm::dd::Add<storm::dd::DdType::CUDD, double> 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);
}*/
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());
EXPECT_EQ(4ul, representative_true_xyz.getNodeCount());
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)))
|| ((bddX1 && (bddY0 && bddZ1)))
|| ((bddX0 && (bddY1 && bddZ0)))
|| ((bddX1 && (bddY1 && bddZ1)))
);
EXPECT_EQ(4ul, representative_complex_x.getNonZeroCount());
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");
// 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)))
|| ((bddX0 && (bddY1 && bddZ1)))
|| ((bddX1 && (bddY0 && bddZ0)))
|| ((bddX1 && (bddY0 && bddZ1)))
);
EXPECT_EQ(4ul, representative_complex_y.getNonZeroCount());
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");
// 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)))
|| ((bddX0 && (bddY1 && bddZ0)))
|| ((bddX1 && (bddY0 && bddZ0)))
|| ((bddX1 && (bddY1 && bddZ1)))
);
EXPECT_EQ(0ul, representative_complex_z.getNonZeroCount());
EXPECT_EQ(1ul, representative_complex_z.getLeafCount());
EXPECT_EQ(2ul, 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");
// 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");
}
TEST(CuddDd, AddGetMetaVariableTest) {
std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());

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

@ -163,6 +163,128 @@ TEST(SylvanDd, BddExistAbstractRepresentative) {
EXPECT_TRUE(bddX0Y0Z0 == representative_xyz);
}
TEST(SylvanDd, AddMinExistAbstractRepresentative) {
std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::Sylvan>> manager(new storm::dd::DdManager<storm::dd::DdType::Sylvan>());
storm::dd::Bdd<storm::dd::DdType::Sylvan> bddZero;
ASSERT_NO_THROW(bddZero = manager->getBddZero());
storm::dd::Bdd<storm::dd::DdType::Sylvan> bddOne;
ASSERT_NO_THROW(bddOne = manager->getBddOne());
storm::dd::Add<storm::dd::DdType::Sylvan, double> addZero;
ASSERT_NO_THROW(addZero = manager->template getAddZero<double>());
storm::dd::Add<storm::dd::DdType::Sylvan, double> addOne;
ASSERT_NO_THROW(addOne = manager->template getAddOne<double>());
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(y = manager->addMetaVariable("y", 0, 1));
ASSERT_NO_THROW(z = manager->addMetaVariable("z", 0, 1));
storm::dd::Bdd<storm::dd::DdType::Sylvan> bddX0 = manager->getEncoding(x.first, 0);
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> bddY1 = manager->getEncoding(y.first, 1);
storm::dd::Bdd<storm::dd::DdType::Sylvan> bddZ0 = manager->getEncoding(z.first, 0);
storm::dd::Bdd<storm::dd::DdType::Sylvan> bddZ1 = manager->getEncoding(z.first, 1);
storm::dd::Add<storm::dd::DdType::Sylvan, double> complexAdd =
((bddX1 && (bddY1 && bddZ1)).template toAdd<double>() * manager->template getConstant<double>(0.4))
+ ((bddX1 && (bddY1 && bddZ0)).template toAdd<double>() * manager->template getConstant<double>(0.7))
+ ((bddX1 && (bddY0 && bddZ1)).template toAdd<double>() * manager->template getConstant<double>(0.3))
+ ((bddX1 && (bddY0 && bddZ0)).template toAdd<double>() * manager->template getConstant<double>(0.3))
+ ((bddX0 && (bddY1 && bddZ1)).template toAdd<double>() * manager->template getConstant<double>(0.9))
+ ((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_Sylvan_complexAdd.dot");
// Abstract from FALSE
std::cout << "Before FALSE" << std::endl;
storm::dd::Bdd<storm::dd::DdType::Sylvan> 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.template toAdd<double>().exportToDot("test_Sylvan_representative_false_x.dot");
// Abstract from TRUE
std::cout << "Before TRUE" << std::endl;
storm::dd::Bdd<storm::dd::DdType::Sylvan> 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::Sylvan> 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());
EXPECT_EQ(4ul, representative_true_xyz.getNodeCount());
EXPECT_TRUE(representative_true_xyz == ((bddX0 && bddY0) && bddZ0));
// Abstract x
std::cout << "Before x" << std::endl;
storm::dd::Bdd<storm::dd::DdType::Sylvan> representative_complex_x = complexAdd.minAbstractRepresentative({x.first});
storm::dd::Bdd<storm::dd::DdType::Sylvan> comparison_complex_x = (
((bddX0 && (bddY0 && bddZ0)))
|| ((bddX1 && (bddY0 && bddZ1)))
|| ((bddX0 && (bddY1 && bddZ0)))
|| ((bddX1 && (bddY1 && bddZ1)))
);
EXPECT_EQ(0ul, representative_complex_x.getNonZeroCount());
EXPECT_EQ(1ul, representative_complex_x.getLeafCount());
EXPECT_EQ(2ul, representative_complex_x.getNodeCount());
EXPECT_TRUE(representative_complex_x == comparison_complex_x);
representative_complex_x.template toAdd<double>().exportToDot("test_Sylvan_representative_complex_x.dot");
comparison_complex_x.template toAdd<double>().exportToDot("test_Sylvan_comparison_complex_x.dot");
// Abstract y
std::cout << "Before y" << std::endl;
storm::dd::Bdd<storm::dd::DdType::Sylvan> representative_complex_y = complexAdd.minAbstractRepresentative({y.first});
storm::dd::Bdd<storm::dd::DdType::Sylvan> comparison_complex_y = (
((bddX0 && (bddY0 && bddZ0)))
|| ((bddX0 && (bddY1 && bddZ1)))
|| ((bddX1 && (bddY0 && bddZ0)))
|| ((bddX1 && (bddY0 && bddZ1)))
);
EXPECT_EQ(0ul, representative_complex_y.getNonZeroCount());
EXPECT_EQ(1ul, representative_complex_y.getLeafCount());
EXPECT_EQ(2ul, representative_complex_y.getNodeCount());
EXPECT_TRUE(representative_complex_y == comparison_complex_y);
representative_complex_y.template toAdd<double>().exportToDot("test_Sylvan_representative_complex_y.dot");
comparison_complex_y.template toAdd<double>().exportToDot("test_Sylvan_comparison_complex_y.dot");
// Abstract z
std::cout << "Before z" << std::endl;
storm::dd::Bdd<storm::dd::DdType::Sylvan> representative_complex_z = complexAdd.minAbstractRepresentative({z.first});
storm::dd::Bdd<storm::dd::DdType::Sylvan> comparison_complex_z = (
((bddX0 && (bddY0 && bddZ0)))
|| ((bddX0 && (bddY1 && bddZ0)))
|| ((bddX1 && (bddY0 && bddZ0)))
|| ((bddX1 && (bddY1 && bddZ1)))
);
EXPECT_EQ(0ul, representative_complex_z.getNonZeroCount());
EXPECT_EQ(1ul, representative_complex_z.getLeafCount());
EXPECT_EQ(2ul, representative_complex_z.getNodeCount());
EXPECT_TRUE(representative_complex_z == comparison_complex_z);
representative_complex_z.template toAdd<double>().exportToDot("test_Sylvan_representative_complex_z.dot");
comparison_complex_z.template toAdd<double>().exportToDot("test_Sylvan_comparison_complex_z.dot");
// Abstract x, y, z
std::cout << "Before x, y, z" << std::endl;
storm::dd::Bdd<storm::dd::DdType::Sylvan> representative_complex_xyz = complexAdd.minAbstractRepresentative({x.first, y.first, z.first});
storm::dd::Bdd<storm::dd::DdType::Sylvan> comparison_complex_xyz = (bddX0 && (bddY0 && bddZ0));
EXPECT_EQ(0ul, representative_complex_xyz.getNonZeroCount());
EXPECT_EQ(1ul, representative_complex_xyz.getLeafCount());
EXPECT_EQ(2ul, representative_complex_xyz.getNodeCount());
EXPECT_TRUE(representative_complex_xyz == comparison_complex_xyz);
representative_complex_xyz.template toAdd<double>().exportToDot("test_Sylvan_representative_complex_xyz.dot");
comparison_complex_xyz.template toAdd<double>().exportToDot("test_Sylvan_representative_complex_xyz.dot");
}
TEST(SylvanDd, AddGetMetaVariableTest) {
std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::Sylvan>> manager(new storm::dd::DdManager<storm::dd::DdType::Sylvan>());
ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9));

Write Preview
Loading…
Cancel
Save