From 6c804732e1de7f3cf84864cd4b637b17346843b5 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 21 Sep 2015 16:32:31 +0200 Subject: [PATCH] introduced (probably buggy) versions of existsAbstractRepresentative on BDDs and prob0 for games Former-commit-id: 5e7225fe29d1a58b5c22812f3f3d6459ffbb8db7 --- resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h | 1 + .../3rdparty/cudd-2.5.0/src/cudd/cuddAddAbs.c | 27 ++- .../3rdparty/cudd-2.5.0/src/cudd/cuddBddAbs.c | 224 ++++++++++++++++++ .../3rdparty/cudd-2.5.0/src/cudd/cuddInt.h | 1 + .../3rdparty/cudd-2.5.0/src/obj/cuddObj.cc | 11 + .../3rdparty/cudd-2.5.0/src/obj/cuddObj.hh | 1 + src/models/symbolic/NondeterministicModel.cpp | 9 +- src/models/symbolic/NondeterministicModel.h | 12 +- .../symbolic/StochasticTwoPlayerGame.cpp | 23 +- src/models/symbolic/StochasticTwoPlayerGame.h | 18 ++ src/storage/dd/CuddBdd.cpp | 16 ++ src/storage/dd/CuddBdd.h | 9 + src/utility/graph.cpp | 62 ++++- src/utility/graph.h | 22 +- 14 files changed, 419 insertions(+), 17 deletions(-) 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 542dd8fdf..3169c25e9 100644 --- a/resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h +++ b/resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h @@ -848,6 +848,7 @@ extern DdNode * Cudd_RemapOverApprox (DdManager *dd, DdNode *f, int numVars, int extern DdNode * Cudd_BiasedUnderApprox (DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0); extern DdNode * Cudd_BiasedOverApprox (DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0); extern DdNode * Cudd_bddExistAbstract (DdManager *manager, DdNode *f, DdNode *cube); +extern DdNode * Cudd_bddExistAbstractRepresentative (DdManager *manager, DdNode *f, DdNode *cube); extern DdNode * Cudd_bddExistAbstractLimit(DdManager * manager, DdNode * f, DdNode * cube, unsigned int limit); extern DdNode * Cudd_bddXorExistAbstract (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube); extern DdNode * Cudd_bddUnivAbstract (DdManager *manager, DdNode *f, DdNode *cube); 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 11e95d8b5..2711d3ecd 100644 --- a/resources/3rdparty/cudd-2.5.0/src/cudd/cuddAddAbs.c +++ b/resources/3rdparty/cudd-2.5.0/src/cudd/cuddAddAbs.c @@ -922,8 +922,7 @@ cuddAddMinAbstractRepresentativeRecur( 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. + // Fill in the missing variables to make representative unique. cuddRef(res); cuddRef(zero); res1 = cuddUniqueInter(manager, (int) cube->index, zero, res); @@ -1026,8 +1025,13 @@ cuddAddMinAbstractRepresentativeRecur( Cudd_RecursiveDeref(manager,res2); Cudd_RecursiveDeref(manager,tmp2); cuddDeref(zero); + +// 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); - res = (res1Inf == res2Inf) ? res1Inf : cuddUniqueInter(manager, (int) f->index, res2Inf, res1Inf); if (res == NULL) { Cudd_RecursiveDeref(manager,res1Inf); Cudd_RecursiveDeref(manager,res2Inf); @@ -1050,7 +1054,10 @@ cuddAddMinAbstractRepresentativeRecur( return(NULL); } cuddRef(res2); - res = (res1 == res2) ? res1 : cuddUniqueInter(manager, (int) f->index, res2, res1); + + cuddRef(zero); + res = (res1 == res2) ? cuddUniqueInter(manager, (int) f->index, zero, res1) : cuddUniqueInter(manager, (int) f->index, res2, res1); + cuddDeref(zero); if (res == NULL) { Cudd_RecursiveDeref(manager,res1); Cudd_RecursiveDeref(manager,res2); @@ -1209,8 +1216,14 @@ cuddAddMaxAbstractRepresentativeRecur( Cudd_RecursiveDeref(manager,res2); Cudd_RecursiveDeref(manager,tmp2); cuddDeref(zero); + +// Orignally +// res = (res1Inf == res2Inf) ? res1Inf : cuddUniqueInter(manager, (int) f->index, res2Inf, res1Inf); - 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); + if (res == NULL) { Cudd_RecursiveDeref(manager,res1Inf); Cudd_RecursiveDeref(manager,res2Inf); @@ -1233,7 +1246,9 @@ cuddAddMaxAbstractRepresentativeRecur( return(NULL); } cuddRef(res2); - res = (res1 == res2) ? res1 : cuddUniqueInter(manager, (int) f->index, res2, res1); + cuddRef(zero); + res = (res1 == res2) ? cuddUniqueInter(manager, (int) f->index, zero, res1) : cuddUniqueInter(manager, (int) f->index, res2, res1); + cuddDeref(zero); if (res == NULL) { Cudd_RecursiveDeref(manager,res1); Cudd_RecursiveDeref(manager,res2); diff --git a/resources/3rdparty/cudd-2.5.0/src/cudd/cuddBddAbs.c b/resources/3rdparty/cudd-2.5.0/src/cudd/cuddBddAbs.c index a806078c5..6aa60fee2 100644 --- a/resources/3rdparty/cudd-2.5.0/src/cudd/cuddBddAbs.c +++ b/resources/3rdparty/cudd-2.5.0/src/cudd/cuddBddAbs.c @@ -147,6 +147,42 @@ Cudd_bddExistAbstract( } /* end of Cudd_bddExistAbstract */ +/**Function******************************************************************** + + Synopsis [Just like Cudd_bddExistAbstract, but instead of abstracting the + variables in the given cube, picks a unique representative that realizes the + existential truth value.] + + Description [Returns the resulting BDD if successful; NULL otherwise.] + + SideEffects [None] + + SeeAlso [] + + Note: Added by Christian Dehnert 9/21/15 + + ******************************************************************************/ +DdNode * +Cudd_bddExistAbstractRepresentative( + DdManager * manager, + DdNode * f, + DdNode * cube) +{ + DdNode *res; + + if (bddCheckPositiveCube(manager, cube) == 0) { + (void) fprintf(manager->err,"Error: Can only abstract positive cubes\n"); + manager->errorCode = CUDD_INVALID_ARG; + return(NULL); + } + + do { + manager->reordered = 0; + res = cuddBddExistAbstractRepresentativeRecur(manager, f, cube); + } while (manager->reordered == 1); + return(res); + +} /* end of Cudd_bddExistAbstractRepresentative */ /**Function******************************************************************** @@ -484,6 +520,194 @@ cuddBddExistAbstractRecur( } /* end of cuddBddExistAbstractRecur */ +/**Function******************************************************************** + + Synopsis [Performs the recursive steps of Cudd_bddExistAbstractRepresentative.] + + Description [Performs the recursive steps of Cudd_bddExistAbstractRepresentative. + Returns the BDD obtained by picking a representative over the variables in + the given cube for all other valuations. Returns the resulting BDD if successful; + NULL otherwise.] + + SideEffects [None] + + SeeAlso [] + + ******************************************************************************/ +DdNode * +cuddBddExistAbstractRepresentativeRecur( + DdManager * manager, + DdNode * f, + DdNode * cube) +{ + DdNode *F, *T, *E, *res, *res1, *res2, *one, *zero, *left, *right, *tmp, *res1Inf, *res2Inf; + + statLine(manager); + one = DD_ONE(manager); + zero = DD_ZERO(manager); + F = Cudd_Regular(f); + + // Store whether f is negated. + int fIsNegated = f != F; + + /* Cube is guaranteed to be a cube at this point. */ + if (F == one) { + if (fIsNegated) { + return f; + } + + if (cube == one) { + return one; + } else { + return cube; + } + } + /* From now on, f and cube are non-constant. */ + + /* Abstract a variable that does not appear in f. */ + if (manager->perm[F->index] > manager->perm[cube->index]) { + res = cuddBddExistAbstractRepresentativeRecur(manager, f, cuddT(cube)); + if (res == NULL) { + return(NULL); + } + + 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_IterDerefBdd(manager, res); + cuddDeref(zero); + return(res1); + } + + /* Check the cache. */ + if (F->ref != 1 && (res = cuddCacheLookup2(manager, Cudd_bddExistAbstractRepresentative, f, cube)) != NULL) { + return(res); + } + + /* Compute the cofactors of f. */ + T = cuddT(F); E = cuddE(F); + if (f != F) { + T = Cudd_Not(T); E = Cudd_Not(E); + } + + /* If the two indices are the same, so are their levels. */ + if (F->index == cube->index) { +// if (E == one) { +// cuddRef(zero); +// cuddRef(cuddT(cube)); +// res1 = cuddUniqueInter(manager, (int) F->index, zero, cuddT(cube)); +// cuddDeref(zero); +// cuddDeref(cuddT(cube)); +// return res1; +// } else if (T == one) { +// cuddRef(zero); +// cuddRef(cuddT(cube)); +// res1 = cuddUniqueInter(manager, (int) F->index, cuddT(cube), zero); +// cuddDeref(zero); +// cuddDeref(cuddT(cube)); +// return res1; +// } + + res1 = cuddBddExistAbstractRepresentativeRecur(manager, E, cuddT(cube)); + if (res1 == NULL) { + return(NULL); + } + if (res1 == one) { + if (F->ref != 1) + cuddCacheInsert2(manager, Cudd_bddExistAbstractRepresentative, f, cube, one); + return(one); + } + cuddRef(res1); + + res2 = cuddBddExistAbstractRepresentativeRecur(manager, T, cuddT(cube)); + if (res2 == NULL) { + Cudd_IterDerefBdd(manager,res1); + return(NULL); + } + cuddRef(res2); + + left = cuddBddExistAbstractRecur(manager, E, cuddT(cube)); + if (left == NULL) { + Cudd_IterDerefBdd(manager, res1); + Cudd_IterDerefBdd(manager, res2); + return(NULL); + } + cuddRef(left); + + cuddRef(zero); + res1Inf = cuddBddIteRecur(manager, left, res1, zero); + if (res1Inf == NULL) { + Cudd_IterDerefBdd(manager,res1); + Cudd_IterDerefBdd(manager,res2); + Cudd_IterDerefBdd(manager,left); + return(NULL); + } + cuddRef(res1Inf); + cuddDeref(zero); + + Cudd_IterDerefBdd(manager,res1); + + cuddRef(zero); + res2Inf = cuddBddIteRecur(manager, left, zero, res2); + if (res2Inf == NULL) { + Cudd_IterDerefBdd(manager,res1); + Cudd_IterDerefBdd(manager,res2); + Cudd_IterDerefBdd(manager,left); + Cudd_IterDerefBdd(manager,res1Inf); + return(NULL); + } + cuddRef(res2Inf); + cuddDeref(zero); + + Cudd_IterDerefBdd(manager,res2); + Cudd_IterDerefBdd(manager,left); + + cuddRef(zero); + res = (res1Inf == res2Inf) ? cuddUniqueInter(manager, (int) f->index, zero, res1Inf) : cuddUniqueInter(manager, (int) f->index, res2Inf, res1Inf); + cuddRef(res); + cuddDeref(zero); + + Cudd_IterDerefBdd(manager,res1Inf); + Cudd_IterDerefBdd(manager,res2Inf); + + if (res == NULL) { + Cudd_IterDerefBdd(manager,res); + return(NULL); + } + cuddCacheInsert2(manager, Cudd_bddExistAbstractRepresentative, f, cube, res); + cuddDeref(res); + return(res); + } else { /* if (cuddI(manager,F->index) < cuddI(manager,cube->index)) */ + res1 = cuddBddExistAbstractRepresentativeRecur(manager, E, cube); + if (res1 == NULL) return(NULL); + cuddRef(res1); + res2 = cuddBddExistAbstractRepresentativeRecur(manager, T, cube); + if (res2 == NULL) { + Cudd_IterDerefBdd(manager, res1); + return(NULL); + } + cuddRef(res2); + /* ITE takes care of possible complementation of res1 and of the + ** case in which res1 == res2. */ + res = cuddBddIteRecur(manager, manager->vars[F->index], res2, res1); + if (res == NULL) { + Cudd_IterDerefBdd(manager, res1); + Cudd_IterDerefBdd(manager, res2); + return(NULL); + } + cuddDeref(res1); + cuddDeref(res2); + if (F->ref != 1) + cuddCacheInsert2(manager, Cudd_bddExistAbstractRepresentative, f, cube, res); + return(res); + } + +} /* end of cuddBddExistAbstractRepresentativeRecur */ /**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 26bdce294..6d3a8da10 100644 --- a/resources/3rdparty/cudd-2.5.0/src/cudd/cuddInt.h +++ b/resources/3rdparty/cudd-2.5.0/src/cudd/cuddInt.h @@ -1017,6 +1017,7 @@ extern DdNode * cuddBiasedUnderApprox (DdManager *dd, DdNode *f, DdNode *b, int extern DdNode * cuddBddAndAbstractRecur (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube); extern int cuddAnnealing (DdManager *table, int lower, int upper); extern DdNode * cuddBddExistAbstractRecur (DdManager *manager, DdNode *f, DdNode *cube); +extern DdNode * cuddBddExistAbstractRepresentativeRecur (DdManager *manager, DdNode *f, DdNode *cube); extern DdNode * cuddBddXorExistAbstractRecur (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube); extern DdNode * cuddBddBooleanDiffRecur (DdManager *manager, DdNode *f, DdNode *var); extern DdNode * cuddBddIteRecur (DdManager *dd, DdNode *f, DdNode *g, DdNode *h); 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 c9d0c03bc..4da1b911b 100644 --- a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc +++ b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc @@ -3214,6 +3214,17 @@ BDD::ExistAbstract( } // BDD::ExistAbstract +BDD +BDD::ExistAbstractRepresentative( + const BDD& cube) const +{ + DdManager *mgr = checkSameManager(cube); + DdNode *result; + result = Cudd_bddExistAbstractRepresentative(mgr, node, cube.node); + checkReturnValue(result); + return BDD(p, result); + +} // BDD::ExistAbstractRepresentative BDD BDD::XorExistAbstract( 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 97ee1680e..509f6178c 100644 --- a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh +++ b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh @@ -255,6 +255,7 @@ public: BDD BiasedOverApprox(const BDD& bias, int numVars, int threshold = 0, double quality1 = 1.0, double quality0 = 1.0) const; BDD ExistAbstract(const BDD& cube, unsigned int limit = 0) const; + BDD ExistAbstractRepresentative(const BDD& cube) const; BDD XorExistAbstract(const BDD& g, const BDD& cube) const; BDD UnivAbstract(const BDD& cube) const; BDD BooleanDiff(int x) const; diff --git a/src/models/symbolic/NondeterministicModel.cpp b/src/models/symbolic/NondeterministicModel.cpp index f5decd7d5..140811ddd 100644 --- a/src/models/symbolic/NondeterministicModel.cpp +++ b/src/models/symbolic/NondeterministicModel.cpp @@ -27,8 +27,7 @@ namespace storm { : Model(modelType, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels), nondeterminismVariables(nondeterminismVariables) { // Prepare the mask of illegal nondeterministic choices. - illegalMask = transitionMatrix.notZero().existsAbstract(this->getColumnVariables()); - illegalMask = !illegalMask && reachableStates; + illegalMask = !(transitionMatrix.notZero().existsAbstract(this->getColumnVariables())) && reachableStates; } template @@ -50,6 +49,12 @@ namespace storm { return illegalMask; } + template + storm::dd::Bdd NondeterministicModel::getIllegalSuccessorMask() const { + storm::dd::Bdd transitionMatrixBdd = this->getTransitionMatrix().notZero(); + return !transitionMatrixBdd && transitionMatrixBdd.existsAbstract(this->getColumnVariables()); + } + template void NondeterministicModel::printModelInformationToStream(std::ostream& out) const { this->printModelInformationHeaderToStream(out); diff --git a/src/models/symbolic/NondeterministicModel.h b/src/models/symbolic/NondeterministicModel.h index dc5194320..d5c7175a4 100644 --- a/src/models/symbolic/NondeterministicModel.h +++ b/src/models/symbolic/NondeterministicModel.h @@ -78,19 +78,27 @@ namespace storm { */ storm::dd::Bdd const& getIllegalMask() const; + /*! + * Retrieves a BDD characterizing the illegal successors for each choice. + * + * @return A BDD characterizing the illegal successors for each choice. + */ + storm::dd::Bdd getIllegalSuccessorMask() const; + virtual void printModelInformationToStream(std::ostream& out) const override; protected: virtual void printDdVariableInformationToStream(std::ostream& out) const override; + + // A mask that characterizes all illegal nondeterministic choices. + storm::dd::Bdd illegalMask; private: // The meta variables encoding the nondeterminism in the model. std::set nondeterminismVariables; - // A mask that characterizes all legal nondeterministic choices. - storm::dd::Bdd illegalMask; }; } // namespace symbolic diff --git a/src/models/symbolic/StochasticTwoPlayerGame.cpp b/src/models/symbolic/StochasticTwoPlayerGame.cpp index 370df9ffb..d8f1df1f6 100644 --- a/src/models/symbolic/StochasticTwoPlayerGame.cpp +++ b/src/models/symbolic/StochasticTwoPlayerGame.cpp @@ -25,8 +25,27 @@ namespace storm { std::set const& nondeterminismVariables, std::map labelToExpressionMap, std::unordered_map const& rewardModels) - : NondeterministicModel(storm::models::ModelType::S2pg, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, nondeterminismVariables, labelToExpressionMap, rewardModels), player1Variables(player1Variables), player2Variables(player2Variables) { - // Intentionally left empty. + : NondeterministicModel(storm::models::ModelType::S2pg, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, nondeterminismVariables, labelToExpressionMap, rewardModels), player1Variables(player1Variables), player2Variables(player2Variables) { + + // Compute legal player 1 mask. + illegalPlayer1Mask = transitionMatrix.notZero().existsAbstract(this->getColumnVariables()).existsAbstract(this->getPlayer2Variables()); + + // Correct the mask for player 2. This is necessary, because it is not yet restricted to the legal choices of player 1. + this->illegalMask &= illegalPlayer1Mask; + + // Then set the illegal mask for player 1 correctly. + illegalPlayer1Mask = !illegalPlayer1Mask && reachableStates; + } + + template + storm::dd::Bdd StochasticTwoPlayerGame::getIllegalPlayer1Mask() const { + return illegalPlayer1Mask; + } + + template + storm::dd::Bdd StochasticTwoPlayerGame::getIllegalPlayer2Mask() const { + // For player 2, we can simply return the mask of the superclass. + return this->getIllegalMask(); } template diff --git a/src/models/symbolic/StochasticTwoPlayerGame.h b/src/models/symbolic/StochasticTwoPlayerGame.h index ae295ba6c..aba4ee561 100644 --- a/src/models/symbolic/StochasticTwoPlayerGame.h +++ b/src/models/symbolic/StochasticTwoPlayerGame.h @@ -73,7 +73,25 @@ namespace storm { */ std::set const& getPlayer2Variables() const; + /*! + * Retrieves a BDD characterizing all illegal player 1 choice encodings in the model. + * + * @return A BDD characterizing all illegal player 1 choice encodings in the model. + */ + storm::dd::Bdd getIllegalPlayer1Mask() const; + + /*! + * Retrieves a BDD characterizing all illegal player 2 choice encodings in the model. + * + * @return A BDD characterizing all illegal player 2 choice encodings in the model. + */ + storm::dd::Bdd getIllegalPlayer2Mask() const; + private: + // A mask that characterizes all illegal player 1 choices. The mask for player 2 is given by the mask + // of the superclass (nondeterminstic model). + storm::dd::Bdd illegalPlayer1Mask; + // The meta variables used to encode the nondeterministic choices of player 1. std::set player1Variables; diff --git a/src/storage/dd/CuddBdd.cpp b/src/storage/dd/CuddBdd.cpp index 09e59f390..bdcccd515 100644 --- a/src/storage/dd/CuddBdd.cpp +++ b/src/storage/dd/CuddBdd.cpp @@ -134,6 +134,22 @@ namespace storm { return Bdd(this->getDdManager(), this->getCuddBdd().ExistAbstract(cubeBdd.getCuddBdd()), newMetaVariables); } + Bdd Bdd::existsAbstractRepresentative(std::set const& metaVariables) const { + Bdd cubeBdd = this->getDdManager()->getBddOne(); + + std::set newMetaVariables = this->getContainedMetaVariables(); + for (auto const& metaVariable : metaVariables) { + // First check whether the BDD 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); + cubeBdd &= ddMetaVariable.getCube(); + } + + return Bdd(this->getDdManager(), this->getCuddBdd().ExistAbstractRepresentative(cubeBdd.getCuddBdd()), newMetaVariables); + } + Bdd Bdd::universalAbstract(std::set const& metaVariables) const { Bdd cubeBdd = this->getDdManager()->getBddOne(); diff --git a/src/storage/dd/CuddBdd.h b/src/storage/dd/CuddBdd.h index a21402c86..b7015b3a3 100644 --- a/src/storage/dd/CuddBdd.h +++ b/src/storage/dd/CuddBdd.h @@ -166,6 +166,15 @@ namespace storm { * @param metaVariables The meta variables from which to abstract. */ Bdd existsAbstract(std::set const& metaVariables) const; + + /*! + * Similar to existsAbstract, but does not abstract from the variables but rather picks a + * valuation of each of the meta variables "to abstract from" such that for this valuation, there exists a + * valuation (of the other variables) that that make the function evaluate to true. + * + * @param metaVariables The meta variables from which to abstract. + */ + Bdd existsAbstractRepresentative(std::set const& metaVariables) const; /*! * Universally abstracts from the given meta variables. diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp index 3e12abcd2..e377c4f09 100644 --- a/src/utility/graph.cpp +++ b/src/utility/graph.cpp @@ -8,6 +8,7 @@ #include "src/models/symbolic/DeterministicModel.h" #include "src/models/symbolic/NondeterministicModel.h" #include "src/models/symbolic/StandardRewardModel.h" +#include "src/models/symbolic/StochasticTwoPlayerGame.h" #include "src/models/sparse/DeterministicModel.h" #include "src/models/sparse/NondeterministicModel.h" #include "src/models/sparse/StandardRewardModel.h" @@ -688,6 +689,64 @@ namespace storm { return result; } + template + void performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy) { + + // The solution set. + storm::dd::Bdd solution = psiStates; + + bool done = false; + uint_fast64_t iterations = 0; + while (!done) { + storm::dd::Bdd tmp = (transitionMatrix && solution.swapVariables(model.getRowColumnMetaVariablePairs())).existsAbstract(model.getColumnVariables()) && phiStates; + + if (player2Strategy == OptimizationDirection::Minimize) { + tmp = (tmp || model.getIllegalPlayer2Mask()).universalAbstract(model.getPlayer2Variables()); + } else { + tmp = tmp.existsAbstract(model.getPlayer2Variables()); + } + + if (player1Strategy == OptimizationDirection::Minimize) { + tmp = (tmp || model.getIllegalPlayer1Mask()).universalAbstract(model.getPlayer1Variables()); + } else { + tmp = tmp.existsAbstract(model.getPlayer1Variables()); + } + + tmp |= solution; + + if (tmp == solution) { + done = true; + } + + solution = tmp; + ++iterations; + } + + // Since we have determined the inverse of the desired set, we need to complement it now. + solution = !solution && model.getReachableStates(); + + // Determine all transitions between prob0 states. + storm::dd::Bdd transitionsBetweenProb0States = solution && (transitionMatrix && solution.swapVariables(model.getRowColumnMetaVariablePairs())); + + // Determine the distributions that have only successors that are prob0 states. + storm::dd::Bdd onlyProb0Successors = (transitionsBetweenProb0States || model.getIllegalSuccessorMask()).universalAbstract(model.getColumnVariables()); + + boost::optional> player2StrategyBdd; + if (player2Strategy == OptimizationDirection::Minimize) { + // Pick a distribution that has only prob0 successors. + player2StrategyBdd = onlyProb0Successors.existsAbstractRepresentative(model.getPlayer2Variables()); + } + + boost::optional> player1StrategyBdd; + if (player1Strategy == OptimizationDirection::Minimize) { + // Move from player 2 choices with only prob0 successors to player 1 choices with only prob 0 successors. + onlyProb0Successors = onlyProb0Successors.existsAbstract(model.getPlayer2Variables()); + + // Pick a prob0 player 2 state. + onlyProb0Successors.existsAbstractRepresentative(model.getPlayer1Variables()); + } + } + template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) { if (matrix.getRowCount() != matrix.getColumnCount()) { @@ -997,7 +1056,7 @@ namespace storm { template std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); - + template storm::dd::Bdd performProbGreater0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); @@ -1020,6 +1079,7 @@ namespace storm { template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; + template void performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy); } // namespace graph } // namespace utility diff --git a/src/utility/graph.h b/src/utility/graph.h index 3ae26d34f..5118ef726 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -11,6 +11,8 @@ #include "src/models/sparse/DeterministicModel.h" #include "src/storage/dd/DdType.h" +#include "src/solver/OptimizationDirection.h" + namespace storm { namespace storage { class BitVector; @@ -23,6 +25,7 @@ namespace storm { template class Model; template class DeterministicModel; template class NondeterministicModel; + template class StochasticTwoPlayerGame; } } @@ -393,7 +396,7 @@ namespace storm { * @return A BDD representing all such states. */ template - storm::dd::Bdd performProb0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; + storm::dd::Bdd performProb0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); /*! * Computes the set of states for which all schedulers achieve probability one of satisfying phi until psi. @@ -425,10 +428,21 @@ namespace storm { storm::dd::Bdd performProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0E) ; template - std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; + std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + + template + std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + /*! + * Computes the set of states that have probability 0 given the strategies of the two players. + * + * @param model The (symbolic) model for which to compute the set of states. + * @param transitionMatrix The transition matrix of the model as a BDD. + * @param phiStates The BDD containing all phi states of the model. + * @param psiStates The BDD containing all psi states of the model. + */ template - std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; + void performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy); /*! * Performs a topological sort of the states of the system according to the given transitions. @@ -437,7 +451,7 @@ namespace storm { * @return A vector of indices that is a topological sort of the states. */ template - std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) ; + std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix); /*! * A class needed to compare the distances for two states in the Dijkstra search.