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

fixed some bugs in custom cudd functions 

Former-commit-id: b73b894674
tempestpy_adaptions
dehnert 9 years ago
parent
5fcc2e9e7e
commit
8b29ab079c
7 changed files with 148 additions and 137 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/cplusplus/cuddObj.cc
  2. 239
      resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c
  3. 6
      resources/3rdparty/cudd-3.0.0/cudd/cuddAddApply.c
  4. 24
      resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c
  5. 10
      resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c
  6. 3
      src/builder/DdPrismModelBuilder.cpp
  7. 1
      src/storage/dd/Add.cpp

2
resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc
View File

@ -3208,7 +3208,7 @@ BDD
ADD::GreaterThanOrEqualBdd(const ADD& g) const
{
DdManager *mgr = checkSameManager(g);
DdNode *result = Cudd_addApply(mgr, Cudd_addToBddGreaterThanEquals, node, g.node);
DdNode *result = Cudd_addToBddApply(mgr, Cudd_addToBddGreaterThanEquals, node, g.node);
checkReturnValue(result);
return BDD(p, result);

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

@ -866,17 +866,33 @@ cuddAddMinAbstractRepresentativeRecur(
DdNode * f,
DdNode * cube)
{
DdNode *T, *E, *res, *res1, *res2, *zero, *one, *res1Inf, *res2Inf, *left, *right, *tmp, *tmp2;
DdNode *T, *E, *res, *res1, *res2, *zero, *one, *logicalZero, *res1Inf, *res2Inf, *left, *right, *tmp, *tmp2;
zero = DD_ZERO(manager);
one = DD_ONE(manager);
logicalZero = Cudd_Not(one);
/* Cube is guaranteed to be a cube at this point. */
if (cuddIsConstant(f)) {
if (cuddIsConstant(cube)) {
return(one);
return one;
} else {
return(cube);
res = cuddBddExistAbstractRepresentativeRecur(manager, f, cuddT(cube));
if (res == NULL) {
return(NULL);
}
cuddRef(res);
// We build in the negation ourselves.
res1 = cuddUniqueInter(manager, (int) cube->index, one, Cudd_Not(res));
if (res1 == NULL) {
Cudd_IterDerefBdd(manager,res);
return(NULL);
}
res1 = Cudd_Not(res1);
cuddDeref(res);
return(res1);
}
}
@ -889,15 +905,14 @@ cuddAddMinAbstractRepresentativeRecur(
// Fill in the missing variables to make representative unique.
cuddRef(res);
cuddRef(zero);
res1 = cuddUniqueInter(manager, (int) cube->index, zero, res);
// We build in the negation ourselves.
res1 = cuddUniqueInter(manager, (int) cube->index, one, Cudd_Not(res));
if (res1 == NULL) {
Cudd_RecursiveDeref(manager,res);
Cudd_RecursiveDeref(manager,zero);
Cudd_IterDerefBdd(manager,res);
return(NULL);
}
Cudd_RecursiveDeref(manager, res);
cuddDeref(zero);
res1 = Cudd_Not(res1);
cuddDeref(res);
return(res1);
}
@ -919,31 +934,31 @@ cuddAddMinAbstractRepresentativeRecur(
res2 = cuddAddMinAbstractRepresentativeRecur(manager, T, cuddT(cube));
if (res2 == NULL) {
Cudd_RecursiveDeref(manager, res1);
Cudd_IterDerefBdd(manager, res1);
return(NULL);
}
cuddRef(res2);
left = cuddAddMinAbstractRecur(manager, E, cuddT(cube));
if (left == NULL) {
Cudd_RecursiveDeref(manager, res1);
Cudd_RecursiveDeref(manager, res2);
Cudd_IterDerefBdd(manager, res1);
Cudd_IterDerefBdd(manager, res2);
return(NULL);
}
cuddRef(left);
right = cuddAddMinAbstractRecur(manager, T, cuddT(cube));
if (right == NULL) {
Cudd_RecursiveDeref(manager, res1);
Cudd_RecursiveDeref(manager, res2);
Cudd_IterDerefBdd(manager, res1);
Cudd_IterDerefBdd(manager, res2);
Cudd_RecursiveDeref(manager, left);
return(NULL);
}
cuddRef(right);
tmp = cuddAddApplyRecur(manager, Cudd_addLessThanEquals, left, right);
tmp = cuddAddToBddApplyRecur(manager, Cudd_addToBddLessThanEquals, left, right);
if (tmp == NULL) {
Cudd_RecursiveDeref(manager,res1);
Cudd_RecursiveDeref(manager,res2);
Cudd_IterDerefBdd(manager,res1);
Cudd_IterDerefBdd(manager,res2);
Cudd_RecursiveDeref(manager,left);
Cudd_RecursiveDeref(manager,right);
return(NULL);
@ -953,58 +968,39 @@ cuddAddMinAbstractRepresentativeRecur(
Cudd_RecursiveDeref(manager, left);
Cudd_RecursiveDeref(manager, right);
cuddRef(zero);
res1Inf = cuddAddIteRecur(manager, tmp, res1, zero);
res1Inf = cuddBddIteRecur(manager, tmp, res1, logicalZero);
if (res1Inf == NULL) {
Cudd_RecursiveDeref(manager,res1);
Cudd_RecursiveDeref(manager,res2);
Cudd_RecursiveDeref(manager,tmp);
cuddDeref(zero);
Cudd_IterDerefBdd(manager,res1);
Cudd_IterDerefBdd(manager,res2);
Cudd_IterDerefBdd(manager,tmp);
return(NULL);
}
cuddRef(res1Inf);
Cudd_RecursiveDeref(manager,res1);
cuddDeref(zero);
Cudd_IterDerefBdd(manager,res1);
tmp2 = cuddAddCmplRecur(manager,tmp);
if (tmp2 == NULL) {
Cudd_RecursiveDeref(manager,res2);
Cudd_RecursiveDeref(manager,left);
Cudd_RecursiveDeref(manager,right);
Cudd_RecursiveDeref(manager,tmp);
return(NULL);
}
cuddRef(tmp2);
Cudd_RecursiveDeref(manager,tmp);
cuddRef(zero);
res2Inf = cuddAddIteRecur(manager, tmp2, res2, zero);
res2Inf = cuddBddIteRecur(manager, Cudd_Not(tmp), res2, logicalZero);
Cudd_IterDerefBdd(manager,tmp);
if (res2Inf == NULL) {
Cudd_RecursiveDeref(manager,res2);
Cudd_RecursiveDeref(manager,res1Inf);
Cudd_RecursiveDeref(manager,tmp2);
cuddDeref(zero);
Cudd_IterDerefBdd(manager,res2);
Cudd_IterDerefBdd(manager,res1Inf);
return(NULL);
}
cuddRef(res2Inf);
Cudd_RecursiveDeref(manager,res2);
Cudd_RecursiveDeref(manager,tmp2);
cuddDeref(zero);
Cudd_IterDerefBdd(manager,res2);
// Originally:
// res = (res1Inf == res2Inf) ? res1Inf : cuddUniqueInter(manager, (int) f->index, res2Inf, res1Inf);
cuddRef(zero);
res = (res1Inf == res2Inf) ? cuddUniqueInter(manager, (int) f->index, zero, res1Inf) : cuddUniqueInter(manager, (int) f->index, res2Inf, res1Inf);
cuddDeref(zero);
int compl = (res1Inf == res2Inf) ? 1 : Cudd_IsComplement(res2Inf);
res = (res1Inf == res2Inf) ? cuddUniqueInter(manager, (int) f->index, one, Cudd_Not(res1Inf)) : cuddUniqueInter(manager, (int) f->index, Cudd_Regular(res2Inf), compl ? Cudd_Not(res1Inf) : res1Inf);
if (res == NULL) {
Cudd_RecursiveDeref(manager,res1Inf);
Cudd_RecursiveDeref(manager,res2Inf);
Cudd_IterDerefBdd(manager,res1Inf);
Cudd_IterDerefBdd(manager,res2Inf);
return(NULL);
}
if (compl) {
res = Cudd_Not(res);
}
cuddRef(res);
Cudd_RecursiveDeref(manager,res1Inf);
Cudd_RecursiveDeref(manager,res2Inf);
cuddDeref(res1Inf);
cuddDeref(res2Inf);
cuddCacheInsert2(manager, Cudd_addMinAbstractRepresentative, f, cube, res);
cuddDeref(res);
return(res);
@ -1015,19 +1011,21 @@ cuddAddMinAbstractRepresentativeRecur(
cuddRef(res1);
res2 = cuddAddMinAbstractRepresentativeRecur(manager, T, cube);
if (res2 == NULL) {
Cudd_RecursiveDeref(manager,res1);
Cudd_IterDerefBdd(manager,res1);
return(NULL);
}
cuddRef(res2);
cuddRef(zero);
res = (res1 == res2) ? cuddUniqueInter(manager, (int) f->index, zero, res1) : cuddUniqueInter(manager, (int) f->index, res2, res1);
cuddDeref(zero);
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));
if (res == NULL) {
Cudd_RecursiveDeref(manager,res1);
Cudd_RecursiveDeref(manager,res2);
Cudd_IterDerefBdd(manager,res1);
Cudd_IterDerefBdd(manager,res2);
return(NULL);
}
if (compl) {
res = Cudd_Not(res);
}
cuddDeref(res1);
cuddDeref(res2);
cuddCacheInsert2(manager, Cudd_addMinAbstractRepresentative, f, cube, res);
@ -1056,17 +1054,33 @@ cuddAddMaxAbstractRepresentativeRecur(
DdNode * f,
DdNode * cube)
{
DdNode *T, *E, *res, *res1, *res2, *zero, *one, *res1Inf, *res2Inf, *left, *right, *tmp, *tmp2;
DdNode *T, *E, *res, *res1, *res2, *zero, *one, *logicalZero, *res1Inf, *res2Inf, *left, *right, *tmp, *tmp2;
zero = DD_ZERO(manager);
one = DD_ONE(manager);
logicalZero = Cudd_Not(one);
/* Cube is guaranteed to be a cube at this point. */
if (cuddIsConstant(f)) {
if (cuddIsConstant(cube)) {
return(one);
return one;
} else {
return(cube);
res = cuddBddExistAbstractRepresentativeRecur(manager, f, cuddT(cube));
if (res == NULL) {
return(NULL);
}
cuddRef(res);
// We build in the negation ourselves.
res1 = cuddUniqueInter(manager, (int) cube->index, one, Cudd_Not(res));
if (res1 == NULL) {
Cudd_IterDerefBdd(manager,res);
return(NULL);
}
res1 = Cudd_Not(res1);
cuddDeref(res);
return(res1);
}
}
@ -1080,15 +1094,13 @@ cuddAddMaxAbstractRepresentativeRecur(
// Fill in the missing variables to make representative unique.
cuddRef(res);
cuddRef(zero);
res1 = cuddUniqueInter(manager, (int) cube->index, zero, res);
res1 = cuddUniqueInter(manager, (int) cube->index, one, Cudd_Not(res));
if (res1 == NULL) {
Cudd_RecursiveDeref(manager, res);
Cudd_RecursiveDeref(manager,zero);
Cudd_IterDerefBdd(manager, res);
return(NULL);
}
Cudd_RecursiveDeref(manager,res);
Cudd_RecursiveDeref(manager,zero);
res1 = Cudd_Not(res1);
Cudd_IterDerefBdd(manager,res);
return(res1);
}
@ -1110,31 +1122,31 @@ cuddAddMaxAbstractRepresentativeRecur(
res2 = cuddAddMaxAbstractRepresentativeRecur(manager, T, cuddT(cube));
if (res2 == NULL) {
Cudd_RecursiveDeref(manager, res1);
Cudd_IterDerefBdd(manager, res1);
return(NULL);
}
cuddRef(res2);
left = cuddAddMaxAbstractRecur(manager, E, cuddT(cube));
if (left == NULL) {
Cudd_RecursiveDeref(manager, res1);
Cudd_RecursiveDeref(manager, res2);
Cudd_IterDerefBdd(manager, res1);
Cudd_IterDerefBdd(manager, res2);
return(NULL);
}
cuddRef(left);
right = cuddAddMaxAbstractRecur(manager, T, cuddT(cube));
if (right == NULL) {
Cudd_RecursiveDeref(manager, res1);
Cudd_RecursiveDeref(manager, res2);
Cudd_IterDerefBdd(manager, res1);
Cudd_IterDerefBdd(manager, res2);
Cudd_RecursiveDeref(manager, left);
return(NULL);
}
cuddRef(right);
tmp = cuddAddApplyRecur(manager, Cudd_addGreaterThanEquals, left, right);
tmp = cuddAddToBddApplyRecur(manager, Cudd_addToBddGreaterThanEquals, left, right);
if (tmp == NULL) {
Cudd_RecursiveDeref(manager,res1);
Cudd_RecursiveDeref(manager,res2);
Cudd_IterDerefBdd(manager,res1);
Cudd_IterDerefBdd(manager,res2);
Cudd_RecursiveDeref(manager,left);
Cudd_RecursiveDeref(manager,right);
return(NULL);
@ -1145,58 +1157,42 @@ cuddAddMaxAbstractRepresentativeRecur(
Cudd_RecursiveDeref(manager, right);
cuddRef(zero);
res1Inf = cuddAddIteRecur(manager, tmp, res1, zero);
res1Inf = cuddBddIteRecur(manager, tmp, res1, logicalZero);
if (res1Inf == NULL) {
Cudd_RecursiveDeref(manager,res1);
Cudd_RecursiveDeref(manager,res2);
Cudd_RecursiveDeref(manager,tmp);
Cudd_IterDerefBdd(manager,res1);
Cudd_IterDerefBdd(manager,res2);
Cudd_IterDerefBdd(manager,tmp);
cuddDeref(zero);
return(NULL);
}
cuddRef(res1Inf);
Cudd_RecursiveDeref(manager,res1);
cuddDeref(zero);
tmp2 = cuddAddCmplRecur(manager,tmp);
if (tmp2 == NULL) {
Cudd_RecursiveDeref(manager,res2);
Cudd_RecursiveDeref(manager,left);
Cudd_RecursiveDeref(manager,right);
Cudd_RecursiveDeref(manager,tmp);
return(NULL);
}
cuddRef(tmp2);
Cudd_RecursiveDeref(manager,tmp);
Cudd_IterDerefBdd(manager,res1);
cuddRef(zero);
res2Inf = cuddAddIteRecur(manager, tmp2, res2, zero);
res2Inf = cuddBddIteRecur(manager, Cudd_Not(tmp), res2, logicalZero);
if (res2Inf == NULL) {
Cudd_RecursiveDeref(manager,res2);
Cudd_RecursiveDeref(manager,res1Inf);
Cudd_RecursiveDeref(manager,tmp2);
cuddDeref(zero);
Cudd_IterDerefBdd(manager,res2);
Cudd_IterDerefBdd(manager,res1Inf);
Cudd_IterDerefBdd(manager,tmp);
return(NULL);
}
cuddRef(res2Inf);
Cudd_RecursiveDeref(manager,res2);
Cudd_RecursiveDeref(manager,tmp2);
cuddDeref(zero);
// Orignally
// res = (res1Inf == res2Inf) ? res1Inf : cuddUniqueInter(manager, (int) f->index, res2Inf, res1Inf);
Cudd_IterDerefBdd(manager,res2);
Cudd_IterDerefBdd(manager,tmp);
cuddRef(zero);
res = (res1Inf == res2Inf) ? cuddUniqueInter(manager, (int) f->index, zero, res1Inf) : cuddUniqueInter(manager, (int) f->index, res2Inf, res1Inf);
cuddDeref(zero);
int compl = (res1Inf == res2Inf) ? 1 : Cudd_IsComplement(res2Inf);
res = (res1Inf == res2Inf) ? cuddUniqueInter(manager, (int) f->index, one, Cudd_Not(res1Inf)) : cuddUniqueInter(manager, (int) f->index, Cudd_Regular(res2Inf), compl ? Cudd_Not(res1Inf) : res1Inf);
if (res == NULL) {
Cudd_RecursiveDeref(manager,res1Inf);
Cudd_RecursiveDeref(manager,res2Inf);
Cudd_IterDerefBdd(manager,res1Inf);
Cudd_IterDerefBdd(manager,res2Inf);
return(NULL);
}
if (compl) {
res = Cudd_Not(res);
}
cuddRef(res);
Cudd_RecursiveDeref(manager,res1Inf);
Cudd_RecursiveDeref(manager,res2Inf);
Cudd_IterDerefBdd(manager,res1Inf);
Cudd_IterDerefBdd(manager,res2Inf);
cuddCacheInsert2(manager, Cudd_addMaxAbstractRepresentative, f, cube, res);
cuddDeref(res);
return(res);
@ -1207,18 +1203,21 @@ cuddAddMaxAbstractRepresentativeRecur(
cuddRef(res1);
res2 = cuddAddMaxAbstractRepresentativeRecur(manager, T, cube);
if (res2 == NULL) {
Cudd_RecursiveDeref(manager,res1);
Cudd_IterDerefBdd(manager,res1);
return(NULL);
}
cuddRef(res2);
cuddRef(zero);
res = (res1 == res2) ? cuddUniqueInter(manager, (int) f->index, zero, res1) : cuddUniqueInter(manager, (int) f->index, res2, res1);
cuddDeref(zero);
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);
if (res == NULL) {
Cudd_RecursiveDeref(manager,res1);
Cudd_RecursiveDeref(manager,res2);
Cudd_IterDerefBdd(manager,res1);
Cudd_IterDerefBdd(manager,res2);
return(NULL);
}
if (compl) {
res = Cudd_Not(res);
}
cuddDeref(res1);
cuddDeref(res2);
cuddCacheInsert2(manager, Cudd_addMaxAbstractRepresentative, f, cube, res);

6
resources/3rdparty/cudd-3.0.0/cudd/cuddAddApply.c
View File

@ -1454,11 +1454,11 @@ cuddAddToBddApplyRecur(
gv = gvn = g;
}
T = cuddAddApplyRecur(dd,op,fv,gv);
T = cuddAddToBddApplyRecur(dd,op,fv,gv);
if (T == NULL) return(NULL);
cuddRef(T);
E = cuddAddApplyRecur(dd,op,fvn,gvn);
E = cuddAddToBddApplyRecur(dd,op,fvn,gvn);
if (E == NULL) {
Cudd_IterDerefBdd(dd,T);
return(NULL);
@ -1480,12 +1480,14 @@ cuddAddToBddApplyRecur(
Cudd_IterDerefBdd(dd, E);
return(NULL);
}
cuddRef(res);
cuddDeref(T);
cuddDeref(E);
/* Store result. */
cuddCacheInsert2(dd,cacheOp,f,g,res);
cuddDeref(res);
return(res);
} /* end of cuddAddToBddApplyRecur */

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

@ -546,11 +546,15 @@ cuddBddExistAbstractRepresentativeRecur(
}
cuddRef(res);
res1 = cuddUniqueInter(manager, (int) cube->index, zero, res);
// res1 = cuddUniqueInter(manager, (int) cube->index, zero, res);
// We now build in the necessary negation ourselves.
res1 = cuddUniqueInter(manager, (int) cube->index, one, Cudd_Not(res));
if (res1 == NULL) {
Cudd_IterDerefBdd(manager,res);
return(NULL);
}
res1 = Cudd_Not(res1);
cuddDeref(res);
return(res1);
}
@ -568,12 +572,15 @@ cuddBddExistAbstractRepresentativeRecur(
}
cuddRef(res);
res1 = cuddUniqueInter(manager, (int) cube->index, zero, res);
// res1 = cuddUniqueInter(manager, (int) cube->index, zero, res);
// We now build in the necessary negation ourselves.
res1 = cuddUniqueInter(manager, (int) cube->index, one, Cudd_Not(res));
if (res1 == NULL) {
Cudd_IterDerefBdd(manager,res);
return(NULL);
}
res1 = Cudd_Not(res1);
cuddDeref(res);
return(res1);
@ -644,13 +651,16 @@ cuddBddExistAbstractRepresentativeRecur(
Cudd_IterDerefBdd(manager,left);
assert(res1Inf != res2Inf);
res = cuddUniqueInter(manager, (int) F->index, res2Inf, res1Inf);
int compl = Cudd_IsComplement(res2Inf);
res = cuddUniqueInter(manager, (int) F->index, Cudd_Regular(res2Inf), compl ? Cudd_Not(res1Inf) : res1Inf);
if (res == NULL) {
Cudd_IterDerefBdd(manager,res1Inf);
Cudd_IterDerefBdd(manager,res2Inf);
return(NULL);
}
if (compl) {
res = Cudd_Not(res);
}
cuddRef(res);
cuddDeref(res1Inf);
@ -675,12 +685,16 @@ cuddBddExistAbstractRepresentativeRecur(
/* ITE takes care of possible complementation of res1 and of the
** case in which res1 == res2. */
res = cuddUniqueInter(manager, (int)F->index, res2, res1);
int compl = Cudd_IsComplement(res2);
res = cuddUniqueInter(manager, (int)F->index, Cudd_Regular(res2), compl ? Cudd_Not(res1) : res1);
if (res == NULL) {
Cudd_IterDerefBdd(manager, res1);
Cudd_IterDerefBdd(manager, res2);
return(NULL);
}
if (compl) {
res = Cudd_Not(res);
}
cuddDeref(res1);
cuddDeref(res2);
if (F->ref != 1) {

10
resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c
View File

@ -31,11 +31,11 @@ int depth = 0;
* helper function for hash
*/
#ifndef rotl64
static inline uint64_t
rotl64(uint64_t x, int8_t r)
{
return ((x<<r) | (x>>(64-r)));
}
//static inline uint64_t
//rotl64(uint64_t x, int8_t r)
//{
// return ((x<<r) | (x>>(64-r)));
//}
#endif
static uint64_t

3
src/builder/DdPrismModelBuilder.cpp
View File

@ -178,9 +178,6 @@ namespace storm {
variableToColumnMetaVariableMap->emplace(booleanVariable.getExpressionVariable(), variablePair.second);
storm::dd::Bdd<Type> variableIdentity = manager->template getIdentity<ValueType>(variablePair.first).equals(manager->template getIdentity<ValueType>(variablePair.second)) && manager->getRange(variablePair.first) && manager->getRange(variablePair.second);
std::cout << "got here " << variableIdentity.isOne() << variableIdentity.isZero() << std::endl;
variableIdentity.exportToDot("id_bdd.dot");
variableIdentity.template toAdd<ValueType>().exportToDot("id_add.dot");
variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity.template toAdd<ValueType>());
moduleIdentity &= variableIdentity;
moduleRange &= manager->getRange(variablePair.first);

1
src/storage/dd/Add.cpp
View File

@ -123,7 +123,6 @@ namespace storm {
template<DdType LibraryType, typename ValueType>
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::mod(Add<LibraryType, ValueType> const& other) const {
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.mod(other), Dd<LibraryType>::joinMetaVariables(*this, other));
}
template<DdType LibraryType, typename ValueType>

Write Preview
Loading…
Cancel
Save