From 81c627b9b74bb708bd9fbb8d80eaaa42f43ce34d Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 11 Jun 2015 20:45:52 +0200 Subject: [PATCH] First version of fully symbolic game solver. Former-commit-id: 34406f25b92de85872f9010a80a20f4f99f6ca7c --- src/models/ModelType.cpp | 1 + src/solver/FullySymbolicGameSolver.cpp | 70 +++++++++++++++++++ src/solver/FullySymbolicGameSolver.h | 67 ++++++++++++++++++ src/solver/SymbolicGameSolver.cpp | 17 +++++ src/solver/SymbolicGameSolver.h | 70 +++++++++++++++++++ src/utility/solver.cpp | 8 +++ src/utility/solver.h | 10 +++ .../solver/FullySymbolicGameSolverTest.cpp | 64 +++++++++++++++++ 8 files changed, 307 insertions(+) create mode 100644 src/solver/FullySymbolicGameSolver.cpp create mode 100644 src/solver/FullySymbolicGameSolver.h create mode 100644 src/solver/SymbolicGameSolver.cpp create mode 100644 src/solver/SymbolicGameSolver.h create mode 100644 test/functional/solver/FullySymbolicGameSolverTest.cpp diff --git a/src/models/ModelType.cpp b/src/models/ModelType.cpp index 06edc9de2..5192a8aa7 100644 --- a/src/models/ModelType.cpp +++ b/src/models/ModelType.cpp @@ -8,6 +8,7 @@ namespace storm { case ModelType::Ctmc: os << "CTMC"; break; case ModelType::Mdp: os << "MDP"; break; case ModelType::MarkovAutomaton: os << "Markov Automaton"; break; + case ModelType::S2pg: os << "S2PG"; break; } return os; } diff --git a/src/solver/FullySymbolicGameSolver.cpp b/src/solver/FullySymbolicGameSolver.cpp new file mode 100644 index 000000000..f02b50ae8 --- /dev/null +++ b/src/solver/FullySymbolicGameSolver.cpp @@ -0,0 +1,70 @@ +#include "src/solver/FullySymbolicGameSolver.h" + +#include "src/storage/dd/CuddBdd.h" +#include "src/storage/dd/CuddAdd.h" + +namespace storm { + namespace solver { + + template + FullySymbolicGameSolver::FullySymbolicGameSolver(storm::dd::Add const& gameMatrix, storm::dd::Bdd const& allRows, 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) : SymbolicGameSolver(gameMatrix, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables, player2Variables), precision(precision), maximalNumberOfIterations(maximalNumberOfIterations), relative(relative) { + // Intentionally left empty. + } + + template + FullySymbolicGameSolver::FullySymbolicGameSolver(storm::dd::Add const& gameMatrix, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables) : SymbolicGameSolver(gameMatrix, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables, player2Variables) { + // Get the settings object to customize solving. + storm::settings::modules::NativeEquationSolverSettings const& settings = storm::settings::nativeEquationSolverSettings(); + storm::settings::modules::GeneralSettings const& generalSettings = storm::settings::generalSettings(); + + // Get appropriate settings. + maximalNumberOfIterations = settings.getMaximalIterationCount(); + precision = settings.getPrecision(); + relative = settings.getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative; + } + + template + storm::dd::Add FullySymbolicGameSolver::solveGame(bool player1Min, bool player2Min, storm::dd::Add const& x, storm::dd::Add const& b) const { + // Set up the environment. + storm::dd::Add xCopy = x; + uint_fast64_t iterations = 0; + bool converged = false; + + while (!converged && iterations < maximalNumberOfIterations) { + // Compute tmp = A * x + b + storm::dd::Add xCopyAsColumn = xCopy.swapVariables(this->rowColumnMetaVariablePairs); + storm::dd::Add tmp = this->gameMatrix.multiplyMatrix(xCopyAsColumn, this->columnMetaVariables); + tmp += b; + + // Now abstract from player 2 and player 1 variables. + // TODO: can this order be reversed? + if (player2Min) { + tmp = tmp.minAbstract(this->player2Variables); + } else { + tmp = tmp.maxAbstract(this->player2Variables); + } + + if (player1Min) { + tmp = tmp.minAbstract(this->player1Variables); + } else { + tmp = tmp.maxAbstract(this->player1Variables); + } + + // Now check if the process already converged within our precision. + converged = xCopy.equalModuloPrecision(tmp, precision, relative); + + // If the method did not converge yet, we prepare the x vector for the next iteration. + if (!converged) { + xCopy = tmp; + } + + ++iterations; + } + + return xCopy; + } + + template class FullySymbolicGameSolver; + + } +} \ No newline at end of file diff --git a/src/solver/FullySymbolicGameSolver.h b/src/solver/FullySymbolicGameSolver.h new file mode 100644 index 000000000..f3f5f014d --- /dev/null +++ b/src/solver/FullySymbolicGameSolver.h @@ -0,0 +1,67 @@ +#ifndef STORM_SOLVER_FULLYSYMBOLICGAMESOLVER_H_ +#define STORM_SOLVER_FULLYSYMBOLICGAMESOLVER_H_ + +#include "src/solver/SymbolicGameSolver.h" + +namespace storm { + namespace solver { + + /*! + * A interface that represents an abstract symbolic game solver. + */ + template + class FullySymbolicGameSolver : public SymbolicGameSolver { + public: + /*! + * Constructs a symbolic game solver with the given meta variable sets and pairs. + * + * @param gameMatrix The matrix defining the coefficients of the game. + * @param allRows A BDD characterizing all rows of the equation system. + * @param rowMetaVariables The meta variables used to encode the rows of the matrix. + * @param columnMetaVariables The meta variables used to encode the columns of the matrix. + * @param rowColumnMetaVariablePairs The pairs of row meta variables and the corresponding column meta + * variables. + * @param player1Variables The meta variables used to encode the player 1 choices. + * @param player2Variables The meta variables used to encode the player 2 choices. + * @param precision The precision to achieve. + * @param maximalNumberOfIterations The maximal number of iterations to perform when solving a linear + * equation system iteratively. + * @param relative Sets whether or not to use a relativ stopping criterion rather than an absolute one. + */ + FullySymbolicGameSolver(storm::dd::Add const& gameMatrix, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables); + + /*! + * Constructs a symbolic game solver with the given meta variable sets and pairs. + * + * @param gameMatrix The matrix defining the coefficients of the game. + * @param allRows A BDD characterizing all rows of the equation system. + * @param rowMetaVariables The meta variables used to encode the rows of the matrix. + * @param columnMetaVariables The meta variables used to encode the columns of the matrix. + * @param rowColumnMetaVariablePairs The pairs of row meta variables and the corresponding column meta + * variables. + * @param player1Variables The meta variables used to encode the player 1 choices. + * @param player2Variables The meta variables used to encode the player 2 choices. + * @param precision The precision to achieve. + * @param maximalNumberOfIterations The maximal number of iterations to perform when solving a linear + * equation system iteratively. + * @param relative Sets whether or not to use a relativ stopping criterion rather than an absolute one. + */ + FullySymbolicGameSolver(storm::dd::Add const& gameMatrix, storm::dd::Bdd const& allRows, 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); + + virtual storm::dd::Add solveGame(bool player1Min, bool player2Min, storm::dd::Add const& x, storm::dd::Add const& b) const override; + + private: + // The precision to achive. + double precision; + + // The maximal number of iterations to perform. + uint_fast64_t maximalNumberOfIterations; + + // A flag indicating whether a relative or an absolute stopping criterion is to be used. + bool relative; + }; + + } // namespace solver +} // namespace storm + +#endif /* STORM_SOLVER_FULLYSYMBOLICGAMESOLVER_H_ */ diff --git a/src/solver/SymbolicGameSolver.cpp b/src/solver/SymbolicGameSolver.cpp new file mode 100644 index 000000000..8224e24c9 --- /dev/null +++ b/src/solver/SymbolicGameSolver.cpp @@ -0,0 +1,17 @@ +#include "src/solver/SymbolicGameSolver.h" + +#include "src/storage/dd/CuddBdd.h" +#include "src/storage/dd/CuddAdd.h" + +namespace storm { + namespace solver { + + template + SymbolicGameSolver::SymbolicGameSolver(storm::dd::Add const& gameMatrix, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables) : gameMatrix(gameMatrix), allRows(allRows), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables) { + // Intentionally left empty. + } + + template class SymbolicGameSolver; + + } +} \ No newline at end of file diff --git a/src/solver/SymbolicGameSolver.h b/src/solver/SymbolicGameSolver.h new file mode 100644 index 000000000..bbf5d539e --- /dev/null +++ b/src/solver/SymbolicGameSolver.h @@ -0,0 +1,70 @@ +#ifndef STORM_SOLVER_SYMBOLICGAMESOLVER_H_ +#define STORM_SOLVER_SYMBOLICGAMESOLVER_H_ + +#include "src/storage/expressions/Variable.h" + +#include "src/storage/dd/Bdd.h" +#include "src/storage/dd/Add.h" + +namespace storm { + namespace solver { + + /*! + * A interface that represents an abstract symbolic game solver. + */ + template + class SymbolicGameSolver { + public: + /*! + * Constructs a symbolic game solver with the given meta variable sets and pairs. + * + * @param gameMatrix The matrix defining the coefficients of the game. + * @param allRows A BDD characterizing all rows of the equation system. + * @param rowMetaVariables The meta variables used to encode the rows of the matrix. + * @param columnMetaVariables The meta variables used to encode the columns of the matrix. + * @param rowColumnMetaVariablePairs The pairs of row meta variables and the corresponding column meta + * variables. + * @param player1Variables The meta variables used to encode the player 1 choices. + * @param player2Variables The meta variables used to encode the player 2 choices. + */ + SymbolicGameSolver(storm::dd::Add const& gameMatrix, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables); + + /*! + * Solves the equation system x = min/max(A*x + b) given by the parameters. Note that the matrix A has + * to be given upon construction time of the solver object. + * + * @param player1Min A flag indicating whether player 1 wants to minimize the result. + * @param player2Min A flag indicating whether player 1 wants to minimize the result. + * @param x The initial guess of the solution. + * @param b The vector to add after matrix-vector multiplication. + * @return The solution vector. + */ + virtual storm::dd::Add solveGame(bool player1Min, bool player2Min, storm::dd::Add const& x, storm::dd::Add const& b) const = 0; + + protected: + // The matrix defining the coefficients of the linear equation system. + storm::dd::Add const& gameMatrix; + + // A BDD characterizing all rows of the equation system. + storm::dd::Bdd const& allRows; + + // The row variables. + std::set rowMetaVariables; + + // The column variables. + std::set columnMetaVariables; + + // The pairs of meta variables used for renaming. + std::vector> const& rowColumnMetaVariablePairs; + + // The player 1 variables. + std::set player1Variables; + + // The player 2 variables. + std::set player2Variables; + }; + + } // namespace solver +} // namespace storm + +#endif /* STORM_SOLVER_SYMBOLICGAMESOLVER_H_ */ diff --git a/src/utility/solver.cpp b/src/utility/solver.cpp index 2d2c0cdcb..9b1983151 100644 --- a/src/utility/solver.cpp +++ b/src/utility/solver.cpp @@ -2,6 +2,8 @@ #include "src/settings/SettingsManager.h" +#include "src/solver/FullySymbolicGameSolver.h" + #include "src/solver/NativeLinearEquationSolver.h" #include "src/solver/GmmxxLinearEquationSolver.h" @@ -15,6 +17,11 @@ namespace storm { namespace utility { namespace solver { + template + std::unique_ptr> SymbolicGameSolverFactory::create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables) const { + return std::unique_ptr>(new storm::solver::FullySymbolicGameSolver(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables, player2Variables)); + } + template std::unique_ptr> LinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { storm::settings::modules::GeneralSettings::EquationSolver equationSolver = storm::settings::generalSettings().getEquationSolver(); @@ -79,6 +86,7 @@ namespace storm { return factory->create(name); } + template class SymbolicGameSolverFactory; template class LinearEquationSolverFactory; template class GmmxxLinearEquationSolverFactory; template class NativeLinearEquationSolverFactory; diff --git a/src/utility/solver.h b/src/utility/solver.h index a72bbdbb1..9fe4389b6 100644 --- a/src/utility/solver.h +++ b/src/utility/solver.h @@ -1,15 +1,25 @@ #ifndef STORM_UTILITY_SOLVER_H_ #define STORM_UTILITY_SOLVER_H_ +#include "src/solver/SymbolicGameSolver.h" + #include "src/solver/LinearEquationSolver.h" #include "src/solver/MinMaxLinearEquationSolver.h" #include "src/solver/LpSolver.h" +#include "src/storage/dd/DdType.h" + #include "src/exceptions/InvalidSettingsException.h" namespace storm { namespace utility { namespace solver { + template + class SymbolicGameSolverFactory { + public: + virtual std::unique_ptr> create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables) const; + }; + template class LinearEquationSolverFactory { public: diff --git a/test/functional/solver/FullySymbolicGameSolverTest.cpp b/test/functional/solver/FullySymbolicGameSolverTest.cpp new file mode 100644 index 000000000..e41606d7f --- /dev/null +++ b/test/functional/solver/FullySymbolicGameSolverTest.cpp @@ -0,0 +1,64 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "src/storage/dd/CuddDdManager.h" + +#include "src/utility/solver.h" + +TEST(FullySymbolicGameSolverTest, Solve) { + // Create some variables. + std::shared_ptr> manager(new storm::dd::DdManager()); + std::pair state = manager->addMetaVariable("x", 1, 4); + std::pair pl1 = manager->addMetaVariable("a", 0, 1); + std::pair pl2 = manager->addMetaVariable("b", 0, 1); + + storm::dd::Bdd allRows = manager->getBddZero(); + std::set rowMetaVariables({state.first}); + std::set columnMetaVariables({state.second}); + std::vector> rowColumnMetaVariablePairs = {state}; + std::set player1Variables({pl1.first}); + std::set player2Variables({pl2.first}); + + // Construct simple game. + storm::dd::Add matrix = manager->getEncoding(state.first, 1).toAdd() * manager->getEncoding(state.second, 2).toAdd() * manager->getEncoding(pl1.first, 0).toAdd() * manager->getEncoding(pl2.first, 0).toAdd() * manager->getConstant(0.6); + matrix += manager->getEncoding(state.first, 1).toAdd() * manager->getEncoding(state.second, 1).toAdd() * manager->getEncoding(pl1.first, 0).toAdd() * manager->getEncoding(pl2.first, 0).toAdd() * manager->getConstant(0.4); + + matrix += manager->getEncoding(state.first, 1).toAdd() * manager->getEncoding(state.second, 2).toAdd() * manager->getEncoding(pl1.first, 0).toAdd() * manager->getEncoding(pl2.first, 1).toAdd() * manager->getConstant(0.2); + matrix += manager->getEncoding(state.first, 1).toAdd() * manager->getEncoding(state.second, 3).toAdd() * manager->getEncoding(pl1.first, 0).toAdd() * manager->getEncoding(pl2.first, 1).toAdd() * manager->getConstant(0.8); + + matrix += manager->getEncoding(state.first, 1).toAdd() * manager->getEncoding(state.second, 3).toAdd() * manager->getEncoding(pl1.first, 1).toAdd() * manager->getEncoding(pl2.first, 0).toAdd() * manager->getConstant(0.5); + matrix += manager->getEncoding(state.first, 1).toAdd() * manager->getEncoding(state.second, 4).toAdd() * manager->getEncoding(pl1.first, 1).toAdd() * manager->getEncoding(pl2.first, 0).toAdd() * manager->getConstant(0.5); + + matrix += manager->getEncoding(state.first, 1).toAdd() * manager->getEncoding(state.second, 1).toAdd() * manager->getEncoding(pl1.first, 1).toAdd() * manager->getEncoding(pl2.first, 1).toAdd() * manager->getConstant(1); + + std::unique_ptr> solverFactory(new storm::utility::solver::SymbolicGameSolverFactory()); + std::unique_ptr> solver = solverFactory->create(matrix, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables,player2Variables); + + // Create solution and target state vector. + storm::dd::Add x = manager->getAddZero(); + storm::dd::Add b = manager->getEncoding(state.first, 2).toAdd() + manager->getEncoding(state.first, 4).toAdd(); + + // Now solve the game with different strategies for the players. + storm::dd::Add result = solver->solveGame(true, true, x, b); + result *= manager->getEncoding(state.first, 1).toAdd(); + result = result.sumAbstract({state.first}); + EXPECT_NEAR(0, result.getValue(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + x = manager->getAddZero(); + result = solver->solveGame(true, false, x, b); + result *= manager->getEncoding(state.first, 1).toAdd(); + result = result.sumAbstract({state.first}); + EXPECT_NEAR(0.5, result.getValue(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + x = manager->getAddZero(); + result = solver->solveGame(false, true, x, b); + result *= manager->getEncoding(state.first, 1).toAdd(); + result = result.sumAbstract({state.first}); + EXPECT_NEAR(0.2, result.getValue(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + x = manager->getAddZero(); + result = solver->solveGame(false, false, x, b); + result *= manager->getEncoding(state.first, 1).toAdd(); + result = result.sumAbstract({state.first}); + EXPECT_NEAR(0.99999892625817599, result.getValue(), storm::settings::nativeEquationSolverSettings().getPrecision()); +} \ No newline at end of file