From 56b5b98a2c20e2fcda32fc3e7cd7c8900650cb23 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 24 Aug 2016 18:13:16 +0200 Subject: [PATCH] towards strategy generation in game solver Former-commit-id: fb582ba53149be8bcb6c80c9f93b9041a89465ec --- .../3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc | 8 ++-- .../3rdparty/cudd-3.0.0/cplusplus/cuddObj.hh | 4 +- src/solver/SymbolicGameSolver.cpp | 44 ++++++++++++++++--- src/solver/SymbolicGameSolver.h | 36 ++++++++++++--- .../SymbolicMinMaxLinearEquationSolver.h | 8 ++-- 5 files changed, 78 insertions(+), 22 deletions(-) diff --git a/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc b/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc index 222b58f25..753a40b8a 100644 --- a/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc +++ b/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc @@ -2667,22 +2667,22 @@ ADD::MaxAbstract(const ADD& cube) const return ADD(p, result); } // ADD::MaxAbstract -ADD +BDD ADD::MinAbstractRepresentative(const ADD& cube) const { DdManager *mgr = checkSameManager(cube); DdNode *result = Cudd_addMinAbstractRepresentative(mgr, node, cube.node); checkReturnValue(result); - return ADD(p, result); + return BDD(p, result); } // ADD::MinRepresentative -ADD +BDD ADD::MaxAbstractRepresentative(const ADD& cube) const { DdManager *mgr = checkSameManager(cube); DdNode *result = Cudd_addMaxAbstractRepresentative(mgr, node, cube.node); checkReturnValue(result); - return ADD(p, result); + return BDD(p, result); } // ADD::MaxRepresentative ADD diff --git a/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.hh b/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.hh index b672e2965..84018dc07 100644 --- a/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.hh +++ b/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.hh @@ -336,8 +336,8 @@ public: ADD MinAbstract(const ADD& cube) const; ADD MinAbstractExcept0(const ADD& cube) const; ADD MaxAbstract(const ADD& cube) const; - ADD MinAbstractRepresentative(const ADD& cube) const; - ADD MaxAbstractRepresentative(const ADD& cube) const; + BDD MinAbstractRepresentative(const ADD& cube) const; + BDD 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/solver/SymbolicGameSolver.cpp b/src/solver/SymbolicGameSolver.cpp index 347e317c1..b6f73e6df 100644 --- a/src/solver/SymbolicGameSolver.cpp +++ b/src/solver/SymbolicGameSolver.cpp @@ -1,21 +1,26 @@ #include "src/solver/SymbolicGameSolver.h" +#include "src/storage/dd/DdManager.h" #include "src/storage/dd/Bdd.h" #include "src/storage/dd/Add.h" #include "src/settings/SettingsManager.h" #include "src/settings/modules/NativeEquationSolverSettings.h" +#include "src/utility/constants.h" +#include "src/utility/macros.h" +#include "src/exceptions/IllegalFunctionCallException.h" + namespace storm { namespace solver { template - SymbolicGameSolver::SymbolicGameSolver(storm::dd::Add const& gameMatrix, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalPlayer1Mask, storm::dd::Bdd const& illegalPlayer2Mask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables) : gameMatrix(gameMatrix), allRows(allRows), illegalPlayer1Mask(illegalPlayer1Mask.template toAdd()), illegalPlayer2Mask(illegalPlayer2Mask.template toAdd()), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables) { + SymbolicGameSolver::SymbolicGameSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalPlayer1Mask, storm::dd::Bdd const& illegalPlayer2Mask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables) : A(A), allRows(allRows), illegalPlayer1Mask(illegalPlayer1Mask.ite(A.getDdManager().getConstant(storm::utility::infinity()), A.getDdManager().template getAddZero())), illegalPlayer2Mask(illegalPlayer2Mask.ite(A.getDdManager().getConstant(storm::utility::infinity()), A.getDdManager().template getAddZero())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables), generatePlayer1Strategy(false), generatePlayer2Strategy(false) { // Intentionally left empty. } template - SymbolicGameSolver::SymbolicGameSolver(storm::dd::Add const& gameMatrix, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalPlayer1Mask, storm::dd::Bdd const& illegalPlayer2Mask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : AbstractGameSolver(precision, maximalNumberOfIterations, relative), gameMatrix(gameMatrix), allRows(allRows), illegalPlayer1Mask(illegalPlayer1Mask.template toAdd()), illegalPlayer2Mask(illegalPlayer2Mask.template toAdd()), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables) { + SymbolicGameSolver::SymbolicGameSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalPlayer1Mask, storm::dd::Bdd const& illegalPlayer2Mask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : AbstractGameSolver(precision, maximalNumberOfIterations, relative), A(A), allRows(allRows), illegalPlayer1Mask(illegalPlayer1Mask.template toAdd()), illegalPlayer2Mask(illegalPlayer2Mask.template toAdd()), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables), generatePlayer1Strategy(false), generatePlayer2Strategy(false) { // Intentionally left empty. } @@ -25,11 +30,11 @@ namespace storm { storm::dd::Add xCopy = x; uint_fast64_t iterations = 0; bool converged = false; - + do { - // Compute tmp = A * x + b + // Compute tmp = A * x + b. storm::dd::Add xCopyAsColumn = xCopy.swapVariables(this->rowColumnMetaVariablePairs); - storm::dd::Add tmp = this->gameMatrix.multiplyMatrix(xCopyAsColumn, this->columnMetaVariables); + storm::dd::Add tmp = this->A.multiplyMatrix(xCopyAsColumn, this->columnMetaVariables); tmp += b; // Now abstract from player 2 and player 1 variables. @@ -59,6 +64,35 @@ namespace storm { return xCopy; } + template + void SymbolicGameSolver::setGeneratePlayer1Strategy(bool value) { + generatePlayer1Strategy = value; + } + + template + void SymbolicGameSolver::setGeneratePlayer2Strategy(bool value) { + generatePlayer2Strategy = value; + } + + template + void SymbolicGameSolver::setGeneratePlayerStrategies(bool value) { + setGeneratePlayer1Strategy(value); + setGeneratePlayer2Strategy(value); + } + + template + storm::dd::Bdd const& SymbolicGameSolver::getPlayer1Strategy() const { + STORM_LOG_THROW(player1Strategy, storm::exceptions::IllegalFunctionCallException, "Cannot retrieve player 1 strategy because none was generated."); + return player1Strategy.get(); + } + + template + storm::dd::Bdd const& SymbolicGameSolver::getPlayer2Strategy() const { + STORM_LOG_THROW(player2Strategy, storm::exceptions::IllegalFunctionCallException, "Cannot retrieve player 2 strategy because none was generated."); + return player2Strategy.get(); + } + + template class SymbolicGameSolver; template class SymbolicGameSolver; diff --git a/src/solver/SymbolicGameSolver.h b/src/solver/SymbolicGameSolver.h index 91802a2bf..a6ac3c007 100644 --- a/src/solver/SymbolicGameSolver.h +++ b/src/solver/SymbolicGameSolver.h @@ -68,12 +68,21 @@ namespace storm { */ virtual storm::dd::Add solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, storm::dd::Add const& x, storm::dd::Add const& b) const; + // Setters that enable the generation of the players' strategies. + void setGeneratePlayer1Strategy(bool value); + void setGeneratePlayer2Strategy(bool value); + void setGeneratePlayerStrategies(bool value); + + // Getters to retrieve the players' strategies. Only legal if they were generated. + storm::dd::Bdd const& getPlayer1Strategy() const; + storm::dd::Bdd const& getPlayer2Strategy() const; + protected: // The matrix defining the coefficients of the linear equation system. - storm::dd::Add const& gameMatrix; + storm::dd::Add A; // A BDD characterizing all rows of the equation system. - storm::dd::Bdd const& allRows; + storm::dd::Bdd allRows; // An ADD that can be used to compensate for the illegal choices of player 1. storm::dd::Add illegalPlayer1Mask; @@ -82,19 +91,32 @@ namespace storm { storm::dd::Add illegalPlayer2Mask; // The row variables. - std::set const& rowMetaVariables; + std::set rowMetaVariables; // The column variables. - std::set const& columnMetaVariables; + std::set columnMetaVariables; // The pairs of meta variables used for renaming. - std::vector> const& rowColumnMetaVariablePairs; + std::vector> rowColumnMetaVariablePairs; // The player 1 variables. - std::set const& player1Variables; + std::set player1Variables; // The player 2 variables. - std::set const& player2Variables; + std::set player2Variables; + + // A flag indicating whether a player 1 is to be generated. + bool generatePlayer1Strategy; + + // A player 1 strategy if one was generated. + boost::optional> player1Strategy; + + // A flag indicating whether a player 2 is to be generated. + bool generatePlayer2Strategy; + + // A player 1 strategy if one was generated. + boost::optional> player2Strategy; + }; } // namespace solver diff --git a/src/solver/SymbolicMinMaxLinearEquationSolver.h b/src/solver/SymbolicMinMaxLinearEquationSolver.h index 98cb94102..da98d5c8d 100644 --- a/src/solver/SymbolicMinMaxLinearEquationSolver.h +++ b/src/solver/SymbolicMinMaxLinearEquationSolver.h @@ -91,10 +91,10 @@ namespace storm { protected: // The matrix defining the coefficients of the linear equation system. - storm::dd::Add const& A; + storm::dd::Add A; // A BDD characterizing all rows of the equation system. - storm::dd::Bdd const& allRows; + storm::dd::Bdd allRows; // An ADD characterizing the illegal choices. storm::dd::Add illegalMaskAdd; @@ -106,10 +106,10 @@ namespace storm { std::set columnMetaVariables; // The choice variables - std::set const& choiceVariables; + std::set choiceVariables; // The pairs of meta variables used for renaming. - std::vector> const& rowColumnMetaVariablePairs; + std::vector> rowColumnMetaVariablePairs; // The precision to achive. double precision;