diff --git a/resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h b/resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h index bba6713d2..542dd8fdf 100644 --- a/resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h +++ b/resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h @@ -769,6 +769,8 @@ extern DdNode * Cudd_addUnivAbstract (DdManager *manager, DdNode *f, DdNode *cub extern DdNode * Cudd_addOrAbstract (DdManager *manager, DdNode *f, DdNode *cube); extern DdNode * Cudd_addMinAbstract(DdManager * manager, DdNode * f, DdNode * cube); extern DdNode * Cudd_addMaxAbstract(DdManager * manager, DdNode * f, DdNode * cube); +extern DdNode * Cudd_addMinAbstractRepresentative(DdManager * manager, DdNode * f, DdNode * cube); +extern DdNode * Cudd_addMaxAbstractRepresentative(DdManager * manager, DdNode * f, DdNode * cube); extern DdNode * Cudd_addApply (DdManager *dd, DdNode * (*)(DdManager *, DdNode **, DdNode **), DdNode *f, DdNode *g); extern DdNode * Cudd_addPlus (DdManager *dd, DdNode **f, DdNode **g); extern DdNode * Cudd_addTimes (DdManager *dd, DdNode **f, DdNode **g); diff --git a/resources/3rdparty/cudd-2.5.0/src/cudd/cuddAddAbs.c b/resources/3rdparty/cudd-2.5.0/src/cudd/cuddAddAbs.c index 7d774586c..11e95d8b5 100644 --- a/resources/3rdparty/cudd-2.5.0/src/cudd/cuddAddAbs.c +++ b/resources/3rdparty/cudd-2.5.0/src/cudd/cuddAddAbs.c @@ -310,6 +310,78 @@ Cudd_addMaxAbstract( } /* end of Cudd_addMaxAbstract */ +/**Function******************************************************************** + + Synopsis [Just like Cudd_addMinAbstract, but instead of abstracting the + variables in the given cube, picks a unique representative that realizes th + minimal function value.] + + Description [Returns the resulting ADD if successful; NULL otherwise.] + + SideEffects [None] + + SeeAlso [Cudd_addMaxAbstractRepresentative] + + Note: Added by Christian Dehnert 8/5/14 + + ******************************************************************************/ +DdNode * +Cudd_addMinAbstractRepresentative( + DdManager * manager, + DdNode * f, + DdNode * cube) +{ + DdNode *res; + + if (addCheckPositiveCube(manager, cube) == 0) { + (void) fprintf(manager->err,"Error: Can only abstract cubes"); + return(NULL); + } + + do { + manager->reordered = 0; + res = cuddAddMinAbstractRepresentativeRecur(manager, f, cube); + } while (manager->reordered == 1); + return(res); + +} /* end of Cudd_addMinRepresentative */ + +/**Function******************************************************************** + + Synopsis [Just like Cudd_addMaxAbstract, but instead of abstracting the + variables in the given cube, picks a unique representative that realizes th + maximal function value.] + + Description [Returns the resulting ADD if successful; NULL otherwise.] + + SideEffects [None] + + SeeAlso [Cudd_addMinAbstractRepresentative] + + Note: Added by Christian Dehnert 8/5/14 + + ******************************************************************************/ +DdNode * +Cudd_addMaxAbstractRepresentative( + DdManager * manager, + DdNode * f, + DdNode * cube) +{ + DdNode *res; + + if (addCheckPositiveCube(manager, cube) == 0) { + (void) fprintf(manager->err,"Error: Can only abstract cubes"); + return(NULL); + } + + do { + manager->reordered = 0; + res = cuddAddMaxAbstractRepresentativeRecur(manager, f, cube); + } while (manager->reordered == 1); + return(res); + +} /* end of Cudd_addMaxRepresentative */ + /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ @@ -809,6 +881,374 @@ cuddAddMaxAbstractRecur( /* Definition of static functions */ /*---------------------------------------------------------------------------*/ +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Cudd_addMinAbstractRepresentative.] + + Description [Performs the recursive step of Cudd_addMinAbstractRepresentative. + Returns the ADD obtained by picking a representative over the variables in + the given cube for all other valuations. Returns the resulting ADD if successful; + NULL otherwise.] + + SideEffects [None] + + SeeAlso [] + + ******************************************************************************/ +DdNode * +cuddAddMinAbstractRepresentativeRecur( + DdManager * manager, + DdNode * f, + DdNode * cube) +{ + DdNode *T, *E, *res, *res1, *res2, *zero, *one, *res1Inf, *res2Inf, *left, *right, *tmp, *tmp2; + + zero = DD_ZERO(manager); + one = DD_ONE(manager); + + /* Cube is guaranteed to be a cube at this point. */ + if (cuddIsConstant(f)) { + if (cuddIsConstant(cube)) { + return(one); + } else { + return(cube); + } + } + + /* Abstract a variable that does not appear in f. */ + if (cuddI(manager,f->index) > cuddI(manager,cube->index)) { + res = cuddAddMinAbstractRepresentativeRecur(manager, f, cuddT(cube)); + if (res == NULL) { + return(NULL); + } + + // Fill in the missing variables to make representative unique. Set the "non-used-branch" to infinity, otherwise + // this may interfere with the minimum calculation. + cuddRef(res); + cuddRef(zero); + res1 = cuddUniqueInter(manager, (int) cube->index, zero, res); + if (res1 == NULL) { + Cudd_RecursiveDeref(manager,res); + Cudd_RecursiveDeref(manager,zero); + return(NULL); + } + Cudd_RecursiveDeref(manager, res); + cuddDeref(zero); + return(res1); + } + + if ((res = cuddCacheLookup2(manager, Cudd_addMinAbstractRepresentative, f, cube)) != NULL) { + return(res); + } + + + E = cuddE(f); + T = cuddT(f); + + /* If the two indices are the same, so are their levels. */ + if (f->index == cube->index) { + res1 = cuddAddMinAbstractRepresentativeRecur(manager, E, cuddT(cube)); + if (res1 == NULL) { + return(NULL); + } + cuddRef(res1); + + res2 = cuddAddMinAbstractRepresentativeRecur(manager, T, cuddT(cube)); + if (res2 == NULL) { + Cudd_RecursiveDeref(manager, res1); + return(NULL); + } + cuddRef(res2); + + left = cuddAddMinAbstractRecur(manager, E, cuddT(cube)); + if (left == NULL) { + Cudd_RecursiveDeref(manager, res1); + Cudd_RecursiveDeref(manager, res2); + return(NULL); + } + cuddRef(left); + right = cuddAddMinAbstractRecur(manager, T, cuddT(cube)); + if (right == NULL) { + Cudd_RecursiveDeref(manager, res1); + Cudd_RecursiveDeref(manager, res2); + Cudd_RecursiveDeref(manager, left); + return(NULL); + } + cuddRef(right); + + tmp = cuddAddApplyRecur(manager, Cudd_addLessThanEquals, left, right); + if (tmp == NULL) { + Cudd_RecursiveDeref(manager,res1); + Cudd_RecursiveDeref(manager,res2); + Cudd_RecursiveDeref(manager,left); + Cudd_RecursiveDeref(manager,right); + return(NULL); + } + cuddRef(tmp); + + Cudd_RecursiveDeref(manager, left); + Cudd_RecursiveDeref(manager, right); + + cuddRef(zero); + res1Inf = cuddAddIteRecur(manager, tmp, res1, zero); + if (res1Inf == NULL) { + Cudd_RecursiveDeref(manager,res1); + Cudd_RecursiveDeref(manager,res2); + Cudd_RecursiveDeref(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); + + cuddRef(zero); + res2Inf = cuddAddIteRecur(manager, tmp2, res2, zero); + if (res2Inf == NULL) { + Cudd_RecursiveDeref(manager,res2); + Cudd_RecursiveDeref(manager,res1Inf); + Cudd_RecursiveDeref(manager,tmp2); + cuddDeref(zero); + return(NULL); + } + cuddRef(res2Inf); + Cudd_RecursiveDeref(manager,res2); + Cudd_RecursiveDeref(manager,tmp2); + cuddDeref(zero); + + res = (res1Inf == res2Inf) ? res1Inf : cuddUniqueInter(manager, (int) f->index, res2Inf, res1Inf); + if (res == NULL) { + Cudd_RecursiveDeref(manager,res1Inf); + Cudd_RecursiveDeref(manager,res2Inf); + return(NULL); + } + cuddRef(res); + Cudd_RecursiveDeref(manager,res1Inf); + Cudd_RecursiveDeref(manager,res2Inf); + cuddCacheInsert2(manager, Cudd_addMinAbstractRepresentative, f, cube, res); + cuddDeref(res); + return(res); + } + else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */ + res1 = cuddAddMinAbstractRepresentativeRecur(manager, E, cube); + if (res1 == NULL) return(NULL); + cuddRef(res1); + res2 = cuddAddMinAbstractRepresentativeRecur(manager, T, cube); + if (res2 == NULL) { + Cudd_RecursiveDeref(manager,res1); + return(NULL); + } + cuddRef(res2); + res = (res1 == res2) ? res1 : cuddUniqueInter(manager, (int) f->index, res2, res1); + if (res == NULL) { + Cudd_RecursiveDeref(manager,res1); + Cudd_RecursiveDeref(manager,res2); + return(NULL); + } + cuddDeref(res1); + cuddDeref(res2); + cuddCacheInsert2(manager, Cudd_addMinAbstractRepresentative, f, cube, res); + return(res); + } + +} /* end of cuddAddMinAbstractRepresentativeRecur */ + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Cudd_addMaxAbstractRepresentative.] + + Description [Performs the recursive step of Cudd_addMaxAbstractRepresentative. + Returns the ADD obtained by picking a representative over the variables in + the given cube for all other valuations. Returns the resulting ADD if successful; + NULL otherwise.] + + SideEffects [None] + + SeeAlso [] + + ******************************************************************************/ +DdNode * +cuddAddMaxAbstractRepresentativeRecur( + DdManager * manager, + DdNode * f, + DdNode * cube) +{ + DdNode *T, *E, *res, *res1, *res2, *zero, *one, *res1Inf, *res2Inf, *left, *right, *tmp, *tmp2; + + zero = DD_ZERO(manager); + one = DD_ONE(manager); + + /* Cube is guaranteed to be a cube at this point. */ + if (cuddIsConstant(f)) { + if (cuddIsConstant(cube)) { + return(one); + } else { + return(cube); + } + } + + /* Abstract a variable that does not appear in f. */ + if (cuddI(manager,f->index) > cuddI(manager,cube->index)) { + res = cuddAddMaxAbstractRepresentativeRecur(manager, f, cuddT(cube)); + + if (res == NULL) { + return(NULL); + } + + // Fill in the missing variables to make representative unique. + cuddRef(res); + cuddRef(zero); + res1 = cuddUniqueInter(manager, (int) cube->index, zero, res); + if (res1 == NULL) { + Cudd_RecursiveDeref(manager, res); + Cudd_RecursiveDeref(manager,zero); + return(NULL); + } + Cudd_RecursiveDeref(manager,res); + Cudd_RecursiveDeref(manager,zero); + return(res1); + } + + if ((res = cuddCacheLookup2(manager, Cudd_addMaxAbstractRepresentative, f, cube)) != NULL) { + return(res); + } + + + E = cuddE(f); + T = cuddT(f); + + /* If the two indices are the same, so are their levels. */ + if (f->index == cube->index) { + res1 = cuddAddMaxAbstractRepresentativeRecur(manager, E, cuddT(cube)); + if (res1 == NULL) { + return(NULL); + } + cuddRef(res1); + + res2 = cuddAddMaxAbstractRepresentativeRecur(manager, T, cuddT(cube)); + if (res2 == NULL) { + Cudd_RecursiveDeref(manager, res1); + return(NULL); + } + cuddRef(res2); + + left = cuddAddMaxAbstractRecur(manager, E, cuddT(cube)); + if (left == NULL) { + Cudd_RecursiveDeref(manager, res1); + Cudd_RecursiveDeref(manager, res2); + return(NULL); + } + cuddRef(left); + right = cuddAddMaxAbstractRecur(manager, T, cuddT(cube)); + if (right == NULL) { + Cudd_RecursiveDeref(manager, res1); + Cudd_RecursiveDeref(manager, res2); + Cudd_RecursiveDeref(manager, left); + return(NULL); + } + cuddRef(right); + + tmp = cuddAddApplyRecur(manager, Cudd_addGreaterThanEquals, left, right); + if (tmp == NULL) { + Cudd_RecursiveDeref(manager,res1); + Cudd_RecursiveDeref(manager,res2); + Cudd_RecursiveDeref(manager,left); + Cudd_RecursiveDeref(manager,right); + return(NULL); + } + cuddRef(tmp); + + Cudd_RecursiveDeref(manager, left); + Cudd_RecursiveDeref(manager, right); + + cuddRef(zero); + res1Inf = cuddAddIteRecur(manager, tmp, res1, zero); + if (res1Inf == NULL) { + Cudd_RecursiveDeref(manager,res1); + Cudd_RecursiveDeref(manager,res2); + Cudd_RecursiveDeref(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); + + cuddRef(zero); + res2Inf = cuddAddIteRecur(manager, tmp2, res2, zero); + if (res2Inf == NULL) { + Cudd_RecursiveDeref(manager,res2); + Cudd_RecursiveDeref(manager,res1Inf); + Cudd_RecursiveDeref(manager,tmp2); + cuddDeref(zero); + return(NULL); + } + cuddRef(res2Inf); + Cudd_RecursiveDeref(manager,res2); + Cudd_RecursiveDeref(manager,tmp2); + cuddDeref(zero); + + res = (res1Inf == res2Inf) ? res1Inf : cuddUniqueInter(manager, (int) f->index, res2Inf, res1Inf); + if (res == NULL) { + Cudd_RecursiveDeref(manager,res1Inf); + Cudd_RecursiveDeref(manager,res2Inf); + return(NULL); + } + cuddRef(res); + Cudd_RecursiveDeref(manager,res1Inf); + Cudd_RecursiveDeref(manager,res2Inf); + cuddCacheInsert2(manager, Cudd_addMaxAbstractRepresentative, f, cube, res); + cuddDeref(res); + return(res); + } + else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */ + res1 = cuddAddMaxAbstractRepresentativeRecur(manager, E, cube); + if (res1 == NULL) return(NULL); + cuddRef(res1); + res2 = cuddAddMaxAbstractRepresentativeRecur(manager, T, cube); + if (res2 == NULL) { + Cudd_RecursiveDeref(manager,res1); + return(NULL); + } + cuddRef(res2); + res = (res1 == res2) ? res1 : cuddUniqueInter(manager, (int) f->index, res2, res1); + if (res == NULL) { + Cudd_RecursiveDeref(manager,res1); + Cudd_RecursiveDeref(manager,res2); + return(NULL); + } + cuddDeref(res1); + cuddDeref(res2); + cuddCacheInsert2(manager, Cudd_addMaxAbstractRepresentative, f, cube, res); + return(res); + } +} /* end of cuddAddMaxAbstractRepresentativeRecur */ + +/*---------------------------------------------------------------------------*/ +/* Definition of static functions */ +/*---------------------------------------------------------------------------*/ /**Function******************************************************************** diff --git a/resources/3rdparty/cudd-2.5.0/src/cudd/cuddInt.h b/resources/3rdparty/cudd-2.5.0/src/cudd/cuddInt.h index 313a56586..26bdce294 100644 --- a/resources/3rdparty/cudd-2.5.0/src/cudd/cuddInt.h +++ b/resources/3rdparty/cudd-2.5.0/src/cudd/cuddInt.h @@ -1002,6 +1002,8 @@ extern DdNode * cuddAddUnivAbstractRecur (DdManager *manager, DdNode *f, DdNode extern DdNode * cuddAddOrAbstractRecur (DdManager *manager, DdNode *f, DdNode *cube); extern DdNode * cuddAddMinAbstractRecur (DdManager *manager, DdNode *f, DdNode *cube); extern DdNode * cuddAddMaxAbstractRecur (DdManager *manager, DdNode *f, DdNode *cube); +extern DdNode * cuddAddMinAbstractRepresentativeRecur (DdManager *manager, DdNode *f, DdNode *cube); +extern DdNode * cuddAddMaxAbstractRepresentativeRecur (DdManager *manager, DdNode *f, DdNode *cube); extern DdNode * cuddAddApplyRecur (DdManager *dd, DdNode * (*)(DdManager *, DdNode **, DdNode **), DdNode *f, DdNode *g); extern DdNode * cuddAddMonadicApplyRecur (DdManager * dd, DdNode * (*op)(DdManager *, DdNode *), DdNode * f); extern DdNode * cuddAddScalarInverseRecur (DdManager *dd, DdNode *f, DdNode *epsilon); diff --git a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc index b8f7d3983..c9d0c03bc 100644 --- a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc +++ b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc @@ -2423,6 +2423,24 @@ ADD::MaxAbstract(const ADD& cube) const return ADD(p, result); } // ADD::MaxAbstract +ADD +ADD::MinAbstractRepresentative(const ADD& cube) const +{ + DdManager *mgr = checkSameManager(cube); + DdNode *result = Cudd_addMinAbstractRepresentative(mgr, node, cube.node); + checkReturnValue(result); + return ADD(p, result); +} // ADD::MinRepresentative + +ADD +ADD::MaxAbstractRepresentative(const ADD& cube) const +{ + DdManager *mgr = checkSameManager(cube); + DdNode *result = Cudd_addMaxAbstractRepresentative(mgr, node, cube.node); + checkReturnValue(result); + return ADD(p, result); +} // ADD::MaxRepresentative + ADD ADD::Plus( const ADD& g) const diff --git a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh index 0b5acf051..97ee1680e 100644 --- a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh +++ b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh @@ -376,6 +376,8 @@ public: ADD OrAbstract(const ADD& cube) const; ADD MinAbstract(const ADD& cube) const; ADD MaxAbstract(const ADD& cube) const; + ADD MinAbstractRepresentative(const ADD& cube) const; + ADD MaxAbstractRepresentative(const ADD& cube) const; ADD Plus(const ADD& g) const; ADD Times(const ADD& g) const; ADD Threshold(const ADD& g) const; diff --git a/src/storage/dd/CuddAdd.cpp b/src/storage/dd/CuddAdd.cpp index 58f17137b..eddc26e28 100644 --- a/src/storage/dd/CuddAdd.cpp +++ b/src/storage/dd/CuddAdd.cpp @@ -242,6 +242,38 @@ namespace storm { return Add(this->getDdManager(), this->getCuddAdd().MaxAbstract(cubeDd.toAdd().getCuddAdd()), newMetaVariables); } + Add Add::minAbstractRepresentative(std::set const& metaVariables) const { + Bdd cubeDd = this->getDdManager()->getBddOne(); + + std::set newMetaVariables = this->getContainedMetaVariables(); + for (auto const& metaVariable : metaVariables) { + // First check whether the DD contains the meta variable and erase it, if this is the case. + STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD."); + newMetaVariables.erase(metaVariable); + + DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); + cubeDd &= ddMetaVariable.getCube(); + } + + return Add(this->getDdManager(), this->getCuddAdd().MinAbstractRepresentative(cubeDd.toAdd().getCuddAdd()), newMetaVariables); + } + + Add Add::maxAbstractRepresentative(std::set const& metaVariables) const { + Bdd cubeDd = this->getDdManager()->getBddOne(); + + std::set newMetaVariables = this->getContainedMetaVariables(); + for (auto const& metaVariable : metaVariables) { + // First check whether the DD contains the meta variable and erase it, if this is the case. + STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD."); + newMetaVariables.erase(metaVariable); + + DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); + cubeDd &= ddMetaVariable.getCube(); + } + + return Add(this->getDdManager(), this->getCuddAdd().MaxAbstractRepresentative(cubeDd.toAdd().getCuddAdd()), newMetaVariables); + } + bool Add::equalModuloPrecision(Add const& other, double precision, bool relative) const { if (relative) { return this->getCuddAdd().EqualSupNormRel(other.getCuddAdd(), precision); diff --git a/src/storage/dd/CuddAdd.h b/src/storage/dd/CuddAdd.h index f80422493..312096b63 100644 --- a/src/storage/dd/CuddAdd.h +++ b/src/storage/dd/CuddAdd.h @@ -309,6 +309,28 @@ namespace storm { */ Add maxAbstract(std::set const& metaVariables) const; + /*! + * Computes a DD in which each concrete valuation of the meta variables not in the given set is associated + * with exactly one valuation of the meta variables in the given set that realizes the minimal function + * value (for the valuation of meta variables not in the given set). + * + * @param metaVariables The set of meta variables for which to pick unique representatives (that achieve the + * minimal function value). + * @return The resulting DD. + */ + Add minAbstractRepresentative(std::set const& metaVariables) const; + + /*! + * Computes a DD in which each concrete valuation of the meta variables not in the given set is associated + * with exactly one valuation of the meta variables in the given set that realizes the maximal function + * value (for the valuation of meta variables not in the given set). + * + * @param metaVariables The set of meta variables for which to pick unique representatives (that achieve the + * maximal function value). + * @return The resulting DD. + */ + Add maxAbstractRepresentative(std::set const& metaVariables) const; + /*! * Checks whether the current and the given ADD represent the same function modulo some given precision. *