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

Fixed min/max Abstract w. repr. 

Finally.


Former-commit-id: 1ccc06d924
tempestpy_adaptions
PBerger 8 years ago
parent
a0ad4b25de
commit
d3c492124a
4 changed files with 418 additions and 130 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. 273
      resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c
  2. 11
      resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h
  3. 116
      test/functional/storage/CuddDdTest.cpp
  4. 148
      test/functional/storage/SylvanDdTest.cpp

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

@ -213,7 +213,7 @@ TASK_IMPL_2(MTBDD, mtbdd_op_less, MTBDD*, pa, MTBDD*, pb)
}
/**
* Binary operation Equals (for MTBDDs of same type)
* Binary operation Less or Equals (for MTBDDs of same type)
* Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
* For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
* then the result is mtbdd_false (i.e. not defined).
@ -261,6 +261,55 @@ TASK_IMPL_2(MTBDD, mtbdd_op_less_or_equal, MTBDD*, pa, MTBDD*, pb)
return mtbdd_invalid;
}
/**
* Binary operation Greater or Equals (for MTBDDs of same type)
* Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
* For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
* then the result is mtbdd_false (i.e. not defined).
*/
TASK_IMPL_2(MTBDD, mtbdd_op_greater_or_equal, MTBDD*, pa, MTBDD*, pb)
{
MTBDD a = *pa, b = *pb;
if (a == mtbdd_false && b == mtbdd_false) return mtbdd_true;
if (a == mtbdd_true && b == mtbdd_true) return mtbdd_true;
mtbddnode_t na = MTBDD_GETNODE(a);
mtbddnode_t nb = MTBDD_GETNODE(b);
if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) {
uint64_t val_a = mtbddnode_getvalue(na);
uint64_t val_b = mtbddnode_getvalue(nb);
if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
int64_t va = *(int64_t*)(&val_a);
int64_t vb = *(int64_t*)(&val_b);
return va >= vb ? mtbdd_true : mtbdd_false;
} else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
// both double
double vval_a = *(double*)&val_a;
double vval_b = *(double*)&val_b;
if (vval_a >= vval_b) return mtbdd_true;
return mtbdd_false;
} else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
// both fraction
uint64_t nom_a = val_a>>32;
uint64_t nom_b = val_b>>32;
uint64_t denom_a = val_a&0xffffffff;
uint64_t denom_b = val_b&0xffffffff;
nom_a *= denom_b;
nom_b *= denom_a;
return nom_a >= nom_b ? mtbdd_true : mtbdd_false;
}
#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) {
printf("ERROR mtbdd_op_greater_or_equal type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID");
assert(0);
}
#endif
}
return mtbdd_invalid;
}
/**
* Binary operation Pow (for MTBDDs of same type)
* Only for MTBDDs where either all leaves are Double.
@ -629,54 +678,81 @@ TASK_IMPL_2(MTBDD, mtbdd_op_complement, MTBDD, a, size_t, k)
}
TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR, prev_level) {
BDD zero = sylvan_false;
/* Maybe perform garbage collection */
sylvan_gc_test();
/* Cube is guaranteed to be a cube at this point. */
printf("Entered method.\n");
if (sylvan_set_isempty(variables)) {
return sylvan_true;
}
/* Cube is guaranteed to be a cube at this point. */
if (mtbdd_isleaf(a)) {
printf("is leaf\n");
if (sylvan_set_isempty(variables)) {
printf("set is empty\n");
return sylvan_true; // FIXME?
} else {
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;
}
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_not(sylvan_ite(sylvan_ithvar(bddnode_getvariable(BDD_GETNODE(variables))), sylvan_true, sylvan_not(res)));
if (res1 == sylvan_invalid) {
sylvan_deref(res);
return res1;
return sylvan_invalid;
}
sylvan_deref(res);
return res1;
}
mtbddnode_t na = MTBDD_GETNODE(a);
uint32_t va = mtbddnode_getvariable(na);
bddnode_t nv = BDD_GETNODE(variables);
BDDVAR vv = bddnode_getvariable(nv);
/* Abstract a variable that does not appear in a. */
if (va > vv) {
BDD _v = sylvan_set_next(variables);
BDD res = CALL(mtbdd_minExistsRepresentative, a, _v, va);
if (res == sylvan_invalid) {
return sylvan_invalid;
}
} 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);
// Fill in the missing variables to make representative unique.
sylvan_ref(res);
BDD res1 = sylvan_ite(sylvan_ithvar(vv), sylvan_false, res);
if (res1 == sylvan_invalid) {
sylvan_deref(res);
return sylvan_invalid;
}
sylvan_deref(res);
return res1;
}
/* TODO: Caching here. */
/*if ((res = cuddCacheLookup2(manager, Cudd_addMinAbstractRepresentative, f, cube)) != NULL) {
return(res);
}*/
MTBDD E = mtbdd_getlow(a);
MTBDD T = mtbdd_gethigh(a);
/* If the two indices are the same, so are their levels. */
if (va == vv) {
BDD _v = sylvan_set_next(variables);
BDD res1 = CALL(mtbdd_minExistsRepresentative, E, _v, va);
if (res1 == sylvan_invalid) {
return sylvan_invalid;
}
sylvan_ref(res1);
BDD res2 = CALL(mtbdd_minExistsRepresentative, T, variables, va);
BDD res2 = CALL(mtbdd_minExistsRepresentative, T, _v, va);
if (res2 == sylvan_invalid) {
sylvan_deref(res1);
return sylvan_invalid;
}
sylvan_ref(res2);
MTBDD left = mtbdd_abstract_min(E, variables);
MTBDD left = mtbdd_abstract_min(E, _v);
if (left == mtbdd_invalid) {
sylvan_deref(res1);
sylvan_deref(res2);
@ -684,7 +760,7 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR
}
mtbdd_ref(left);
MTBDD right = mtbdd_abstract_min(T, variables);
MTBDD right = mtbdd_abstract_min(T, _v);
if (right == mtbdd_invalid) {
sylvan_deref(res1);
sylvan_deref(res2);
@ -706,7 +782,7 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR
mtbdd_deref(left);
mtbdd_deref(right);
BDD res1Inf = sylvan_ite(tmp, res1, zero);
BDD res1Inf = sylvan_ite(tmp, res1, sylvan_false);
if (res1Inf == sylvan_invalid) {
sylvan_deref(res1);
sylvan_deref(res2);
@ -715,30 +791,19 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR
}
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);
BDD res2Inf = sylvan_ite(tmp, sylvan_false, res2);
if (res2Inf == sylvan_invalid) {
sylvan_deref(res2);
sylvan_deref(res1Inf);
sylvan_deref(tmp2);
sylvan_deref(tmp);
return sylvan_invalid;
}
sylvan_ref(res2Inf);
sylvan_deref(res2);
sylvan_deref(tmp2);
sylvan_deref(tmp);
BDD res = (res1Inf == res2Inf) ? sylvan_ite(sylvan_ithvar(va), zero, res1Inf) : sylvan_ite(sylvan_ithvar(va), res2Inf, res1Inf);
BDD res = (res1Inf == res2Inf) ? sylvan_ite(sylvan_ithvar(va), sylvan_false, res1Inf) : sylvan_ite(sylvan_ithvar(va), res2Inf, res1Inf);
if (res == sylvan_invalid) {
sylvan_deref(res1Inf);
@ -754,7 +819,59 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR
sylvan_deref(res);
return res;
}
else { /* if (va < vv) */
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);
BDD res = (res1 == res2) ? res1 : sylvan_ite(sylvan_ithvar(va), res2, res1);
if (res == sylvan_invalid) {
sylvan_deref(res1);
sylvan_deref(res2);
return sylvan_invalid;
}
sylvan_deref(res1);
sylvan_deref(res2);
/* TODO: Caching here. */
//cuddCacheInsert2(manager, Cudd_addMinAbstractRepresentative, f, cube, res);
return res;
}
}
TASK_IMPL_3(BDD, mtbdd_maxExistsRepresentative, MTBDD, a, MTBDD, variables, uint32_t, prev_level) {
/* Maybe perform garbage collection */
sylvan_gc_test();
if (sylvan_set_isempty(variables)) {
return sylvan_true;
}
/* Cube is guaranteed to be a cube at this point. */
if (mtbdd_isleaf(a)) {
BDD _v = sylvan_set_next(variables);
BDD res = CALL(mtbdd_maxExistsRepresentative, a, _v, prev_level);
if (res == sylvan_invalid) {
return sylvan_invalid;
}
sylvan_ref(res);
BDD res1 = sylvan_not(sylvan_ite(sylvan_ithvar(bddnode_getvariable(BDD_GETNODE(variables))), sylvan_true, sylvan_not(res)));
if (res1 == sylvan_invalid) {
sylvan_deref(res);
return sylvan_invalid;
}
sylvan_deref(res);
return res1;
}
mtbddnode_t na = MTBDD_GETNODE(a);
uint32_t va = mtbddnode_getvariable(na);
@ -763,16 +880,15 @@ 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);
BDD res = CALL(mtbdd_maxExistsRepresentative, a, _v, va);
if (res == sylvan_invalid) {
return sylvan_invalid;
}
// Fill in the missing variables to make representative unique.
sylvan_ref(res);
BDD res1 = sylvan_ite(sylvan_ithvar(vv), zero, res);
BDD res1 = sylvan_ite(sylvan_ithvar(vv), sylvan_false, res);
if (res1 == sylvan_invalid) {
sylvan_deref(res);
return sylvan_invalid;
@ -792,22 +908,21 @@ 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);
BDD res1 = CALL(mtbdd_maxExistsRepresentative, E, _v, va);
if (res1 == sylvan_invalid) {
return sylvan_invalid;
}
sylvan_ref(res1);
BDD res2 = CALL(mtbdd_minExistsRepresentative, T, _v, va);
BDD res2 = CALL(mtbdd_maxExistsRepresentative, T, _v, va);
if (res2 == sylvan_invalid) {
sylvan_deref(res1);
return sylvan_invalid;
}
sylvan_ref(res2);
MTBDD left = mtbdd_abstract_min(E, _v);
MTBDD left = mtbdd_abstract_max(E, _v);
if (left == mtbdd_invalid) {
sylvan_deref(res1);
sylvan_deref(res2);
@ -815,7 +930,7 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR
}
mtbdd_ref(left);
MTBDD right = mtbdd_abstract_min(T, _v);
MTBDD right = mtbdd_abstract_max(T, _v);
if (right == mtbdd_invalid) {
sylvan_deref(res1);
sylvan_deref(res2);
@ -824,7 +939,7 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR
}
mtbdd_ref(right);
BDD tmp = mtbdd_less_or_equal_as_bdd(left, right);
BDD tmp = mtbdd_greater_or_equal_as_bdd(left, right);
if (tmp == sylvan_invalid) {
sylvan_deref(res1);
sylvan_deref(res2);
@ -837,7 +952,7 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR
mtbdd_deref(left);
mtbdd_deref(right);
BDD res1Inf = sylvan_ite(tmp, res1, zero);
BDD res1Inf = sylvan_ite(tmp, res1, sylvan_false);
if (res1Inf == sylvan_invalid) {
sylvan_deref(res1);
sylvan_deref(res2);
@ -846,30 +961,19 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR
}
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);
BDD res2Inf = sylvan_ite(tmp, sylvan_false, res2);
if (res2Inf == sylvan_invalid) {
sylvan_deref(res2);
sylvan_deref(res1Inf);
sylvan_deref(tmp2);
sylvan_deref(tmp);
return sylvan_invalid;
}
sylvan_ref(res2Inf);
sylvan_deref(res2);
sylvan_deref(tmp2);
sylvan_deref(tmp);
BDD res = (res1Inf == res2Inf) ? sylvan_ite(sylvan_ithvar(va), zero, res1Inf) : sylvan_ite(sylvan_ithvar(va), res2Inf, res1Inf);
BDD res = (res1Inf == res2Inf) ? sylvan_ite(sylvan_ithvar(va), sylvan_false, res1Inf) : sylvan_ite(sylvan_ithvar(va), res2Inf, res1Inf);
if (res == sylvan_invalid) {
sylvan_deref(res1Inf);
@ -887,20 +991,19 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR
return res;
}
else { /* if (va < vv) */
printf("va < vv\n");
BDD res1 = CALL(mtbdd_minExistsRepresentative, E, variables, va);
BDD res1 = CALL(mtbdd_maxExistsRepresentative, E, variables, va);
if (res1 == sylvan_invalid) {
return sylvan_invalid;
}
sylvan_ref(res1);
BDD res2 = CALL(mtbdd_minExistsRepresentative, T, variables, va);
BDD res2 = CALL(mtbdd_maxExistsRepresentative, T, variables, va);
if (res2 == sylvan_invalid) {
sylvan_deref(res1);
return sylvan_invalid;
}
sylvan_ref(res2);
BDD res = (res1 == res2) ? sylvan_ite(sylvan_ithvar(va), zero, res1) : sylvan_ite(sylvan_ithvar(va), res2, res1);
BDD res = (res1 == res2) ? res1 : sylvan_ite(sylvan_ithvar(va), res2, res1);
if (res == sylvan_invalid) {
sylvan_deref(res1);
sylvan_deref(res2);
@ -911,11 +1014,5 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR
/* TODO: Caching here. */
//cuddCacheInsert2(manager, Cudd_addMinAbstractRepresentative, f, cube, res);
return res;
}
}
TASK_IMPL_3(BDD, mtbdd_maxExistsRepresentative, MTBDD, a, MTBDD, variables, uint32_t, prev_level) {
(void)variables;
(void)prev_level;
return a;
}
}

11
resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h
View File

@ -28,7 +28,7 @@ TASK_DECL_2(MTBDD, mtbdd_op_less, MTBDD*, MTBDD*)
#define mtbdd_less_as_bdd(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_less))
/**
* Binary operation Less (for MTBDDs of same type)
* Binary operation Less or Equal (for MTBDDs of same type)
* Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
* For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
* then the result is the other operand.
@ -36,6 +36,15 @@ TASK_DECL_2(MTBDD, mtbdd_op_less, MTBDD*, MTBDD*)
TASK_DECL_2(MTBDD, mtbdd_op_less_or_equal, MTBDD*, MTBDD*)
#define mtbdd_less_or_equal_as_bdd(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_less_or_equal))
/**
* Binary operation Greater or Equal (for MTBDDs of same type)
* Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
* For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
* then the result is the other operand.
*/
TASK_DECL_2(MTBDD, mtbdd_op_greater_or_equal, MTBDD*, MTBDD*)
#define mtbdd_greater_or_equal_as_bdd(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_greater_or_equal))
/**
* Binary operation Pow (for MTBDDs of same type)
* Only for MTBDDs where either all leaves are Integer, Double or a Fraction.

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

@ -203,8 +203,6 @@ TEST(CuddDd, AddMinExistAbstractRepresentative) {
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");
// Abstract from TRUE
storm::dd::Bdd<storm::dd::DdType::CUDD> representative_true_x = addOne.minAbstractRepresentative({x.first});
@ -231,8 +229,6 @@ 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");
// Abstract y
storm::dd::Bdd<storm::dd::DdType::CUDD> representative_complex_y = complexAdd.minAbstractRepresentative({y.first});
@ -246,8 +242,6 @@ 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");
// Abstract z
storm::dd::Bdd<storm::dd::DdType::CUDD> representative_complex_z = complexAdd.minAbstractRepresentative({z.first});
@ -261,9 +255,6 @@ TEST(CuddDd, AddMinExistAbstractRepresentative) {
EXPECT_EQ(1ul, representative_complex_z.getLeafCount());
EXPECT_EQ(4ul, representative_complex_z.getNodeCount());
EXPECT_TRUE(representative_complex_z == comparison_complex_z);
// 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
storm::dd::Bdd<storm::dd::DdType::CUDD> representative_complex_xyz = complexAdd.minAbstractRepresentative({x.first, y.first, z.first});
@ -272,8 +263,111 @@ TEST(CuddDd, AddMinExistAbstractRepresentative) {
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, AddMaxExistAbstractRepresentative) {
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> 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));
// Abstract from FALSE
storm::dd::Bdd<storm::dd::DdType::CUDD> representative_false_x = addZero.maxAbstractRepresentative({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);
// Abstract from TRUE
storm::dd::Bdd<storm::dd::DdType::CUDD> representative_true_x = addOne.maxAbstractRepresentative({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);
storm::dd::Bdd<storm::dd::DdType::CUDD> representative_true_xyz = addOne.maxAbstractRepresentative({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
storm::dd::Bdd<storm::dd::DdType::CUDD> representative_complex_x = complexAdd.maxAbstractRepresentative({x.first});
storm::dd::Bdd<storm::dd::DdType::CUDD> comparison_complex_x = (
((bddX1 && (bddY0 && bddZ0)))
|| ((bddX0 && (bddY0 && bddZ1)))
|| ((bddX1 && (bddY1 && bddZ0)))
|| ((bddX0 && (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);
// Abstract y
storm::dd::Bdd<storm::dd::DdType::CUDD> representative_complex_y = complexAdd.maxAbstractRepresentative({y.first});
storm::dd::Bdd<storm::dd::DdType::CUDD> comparison_complex_y = (
((bddX0 && (bddY1 && bddZ0)))
|| ((bddX0 && (bddY0 && bddZ1)))
|| ((bddX1 && (bddY1 && bddZ0)))
|| ((bddX1 && (bddY1 && 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);
// Abstract z
storm::dd::Bdd<storm::dd::DdType::CUDD> representative_complex_z = complexAdd.maxAbstractRepresentative({z.first});
storm::dd::Bdd<storm::dd::DdType::CUDD> comparison_complex_z = (
((bddX0 && (bddY0 && bddZ1)))
|| ((bddX0 && (bddY1 && bddZ1)))
|| ((bddX1 && (bddY0 && bddZ0)))
|| ((bddX1 && (bddY1 && bddZ0)))
);
EXPECT_EQ(4ul, representative_complex_z.getNonZeroCount());
EXPECT_EQ(1ul, representative_complex_z.getLeafCount());
EXPECT_EQ(3ul, representative_complex_z.getNodeCount());
EXPECT_TRUE(representative_complex_z == comparison_complex_z);
// Abstract x, y, z
storm::dd::Bdd<storm::dd::DdType::CUDD> representative_complex_xyz = complexAdd.maxAbstractRepresentative({x.first, y.first, z.first});
storm::dd::Bdd<storm::dd::DdType::CUDD> comparison_complex_xyz = (bddX0 && (bddY0 && bddZ1));
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);
}
TEST(CuddDd, AddGetMetaVariableTest) {

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

@ -170,7 +170,7 @@ TEST(SylvanDd, AddMinExistAbstractRepresentative) {
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;
@ -182,7 +182,7 @@ TEST(SylvanDd, AddMinExistAbstractRepresentative) {
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);
@ -199,26 +199,21 @@ TEST(SylvanDd, 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_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());
@ -226,7 +221,6 @@ TEST(SylvanDd, AddMinExistAbstractRepresentative) {
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)))
@ -234,15 +228,12 @@ TEST(SylvanDd, AddMinExistAbstractRepresentative) {
|| ((bddX0 && (bddY1 && bddZ0)))
|| ((bddX1 && (bddY1 && bddZ1)))
);
EXPECT_EQ(0ul, representative_complex_x.getNonZeroCount());
EXPECT_EQ(4ul, representative_complex_x.getNonZeroCount());
EXPECT_EQ(1ul, representative_complex_x.getLeafCount());
EXPECT_EQ(2ul, representative_complex_x.getNodeCount());
EXPECT_EQ(3ul, 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)))
@ -250,15 +241,12 @@ TEST(SylvanDd, AddMinExistAbstractRepresentative) {
|| ((bddX1 && (bddY0 && bddZ0)))
|| ((bddX1 && (bddY0 && bddZ1)))
);
EXPECT_EQ(0ul, representative_complex_y.getNonZeroCount());
EXPECT_EQ(4ul, representative_complex_y.getNonZeroCount());
EXPECT_EQ(1ul, representative_complex_y.getLeafCount());
EXPECT_EQ(2ul, representative_complex_y.getNodeCount());
EXPECT_EQ(5ul, 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)))
@ -266,23 +254,123 @@ TEST(SylvanDd, 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_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.getNonZeroCount());
EXPECT_EQ(1ul, representative_complex_xyz.getLeafCount());
EXPECT_EQ(4ul, representative_complex_xyz.getNodeCount());
EXPECT_TRUE(representative_complex_xyz == comparison_complex_xyz);
}
TEST(SylvanDd, AddMaxExistAbstractRepresentative) {
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));
// Abstract from FALSE
storm::dd::Bdd<storm::dd::DdType::Sylvan> representative_false_x = addZero.maxAbstractRepresentative({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);
// Abstract from TRUE
storm::dd::Bdd<storm::dd::DdType::Sylvan> representative_true_x = addOne.maxAbstractRepresentative({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);
storm::dd::Bdd<storm::dd::DdType::Sylvan> representative_true_xyz = addOne.maxAbstractRepresentative({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
storm::dd::Bdd<storm::dd::DdType::Sylvan> representative_complex_x = complexAdd.maxAbstractRepresentative({x.first});
storm::dd::Bdd<storm::dd::DdType::Sylvan> comparison_complex_x = (
((bddX1 && (bddY0 && bddZ0)))
|| ((bddX0 && (bddY0 && bddZ1)))
|| ((bddX1 && (bddY1 && bddZ0)))
|| ((bddX0 && (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);
// Abstract y
storm::dd::Bdd<storm::dd::DdType::Sylvan> representative_complex_y = complexAdd.maxAbstractRepresentative({y.first});
storm::dd::Bdd<storm::dd::DdType::Sylvan> comparison_complex_y = (
((bddX0 && (bddY1 && bddZ0)))
|| ((bddX0 && (bddY0 && bddZ1)))
|| ((bddX1 && (bddY1 && bddZ0)))
|| ((bddX1 && (bddY1 && 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);
// Abstract z
storm::dd::Bdd<storm::dd::DdType::Sylvan> representative_complex_z = complexAdd.maxAbstractRepresentative({z.first});
storm::dd::Bdd<storm::dd::DdType::Sylvan> comparison_complex_z = (
((bddX0 && (bddY0 && bddZ1)))
|| ((bddX0 && (bddY1 && bddZ1)))
|| ((bddX1 && (bddY0 && bddZ0)))
|| ((bddX1 && (bddY1 && bddZ0)))
);
EXPECT_EQ(4ul, representative_complex_z.getNonZeroCount());
EXPECT_EQ(1ul, representative_complex_z.getLeafCount());
EXPECT_EQ(3ul, representative_complex_z.getNodeCount());
EXPECT_TRUE(representative_complex_z == comparison_complex_z);
// Abstract x, y, z
storm::dd::Bdd<storm::dd::DdType::Sylvan> representative_complex_xyz = complexAdd.maxAbstractRepresentative({x.first, y.first, z.first});
storm::dd::Bdd<storm::dd::DdType::Sylvan> comparison_complex_xyz = (bddX0 && (bddY0 && bddZ1));
EXPECT_EQ(1ul, representative_complex_xyz.getNonZeroCount());
EXPECT_EQ(1ul, representative_complex_xyz.getLeafCount());
EXPECT_EQ(2ul, representative_complex_xyz.getNodeCount());
EXPECT_EQ(4ul, 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) {
Write Preview
Loading…
Cancel
Save