diff --git a/src/solver/AbstractGameSolver.cpp b/src/solver/AbstractGameSolver.cpp new file mode 100644 index 000000000..76ea87bd1 --- /dev/null +++ b/src/solver/AbstractGameSolver.cpp @@ -0,0 +1,22 @@ +#include "src/solver/AbstractGameSolver.h" + +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" + +namespace storm { + namespace solver { + AbstractGameSolver::AbstractGameSolver() { + // Get the settings object to customize solving. + storm::settings::modules::NativeEquationSolverSettings const& settings = storm::settings::nativeEquationSolverSettings(); + + // Get appropriate settings. + maximalNumberOfIterations = settings.getMaximalIterationCount(); + precision = settings.getPrecision(); + relative = settings.getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative; + } + + AbstractGameSolver::AbstractGameSolver(double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : precision(precision), maximalNumberOfIterations(maximalNumberOfIterations), relative(relative) { + // Intentionally left empty. + } + } +} \ No newline at end of file diff --git a/src/solver/AbstractGameSolver.h b/src/solver/AbstractGameSolver.h new file mode 100644 index 000000000..693b4defa --- /dev/null +++ b/src/solver/AbstractGameSolver.h @@ -0,0 +1,40 @@ +#ifndef STORM_SOLVER_ABSTRACTGAMESOLVER_H_ +#define STORM_SOLVER_ABSTRACTGAMESOLVER_H_ + +#include + +namespace storm { + namespace solver { + /*! + * The abstract base class for the game solvers. + */ + class AbstractGameSolver { + public: + /*! + * Creates a game solver with the default parameters. + */ + AbstractGameSolver(); + + /*! + * Creates a game solver with the given parameters. + * + * @param precision The precision to achieve. + * @param maximalNumberOfIterations The maximal number of iterations to perform. + * @param relative A flag indicating whether a relative or an absolute stopping criterion is to be used. + */ + AbstractGameSolver(double precision, uint_fast64_t maximalNumberOfIterations, bool relative); + + protected: + // The precision to achieve. + 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; + }; + } +} + +#endif /* STORM_SOLVER_ABSTRACTGAMESOLVER_H_ */ diff --git a/src/solver/GameSolver.cpp b/src/solver/GameSolver.cpp new file mode 100644 index 000000000..27ccf27a5 --- /dev/null +++ b/src/solver/GameSolver.cpp @@ -0,0 +1,17 @@ +#include "src/solver/GameSolver.h" + +namespace storm { + namespace solver { + GameSolver::GameSolver(storm::storage::SparseMatrix const& player1Matrix, storm::storage::SparseMatrix const& player2Matrix) : AbstractGameSolver(), player1Matrix(player1Matrix), player2Matrix(player2Matrix) { + // Intentionally left empty. + } + + GameSolver::GameSolver(storm::storage::SparseMatrix const& player1Matrix, storm::storage::SparseMatrix const& player2Matrix, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : AbstractGameSolver(precision, maximalNumberOfIterations, relative), player1Matrix(player1Matrix), player2Matrix(player2Matrix) { + // Intentionally left empty. + } + + void GameSolver::solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, std::vector& x, storm::dd::Add const& b) const { + // TODO + } + } +} \ No newline at end of file diff --git a/src/solver/GameSolver.h b/src/solver/GameSolver.h new file mode 100644 index 000000000..35ce8204a --- /dev/null +++ b/src/solver/GameSolver.h @@ -0,0 +1,52 @@ +#ifndef STORM_SOLVER_GAMESOLVER_H_ +#define STORM_SOLVER_GAMESOLVER_H_ + +#include "src/solver/AbstractGameSolver.h" + +namespace storm { + namespace solver { + template + class GameSolver : public AbstractGameSolver { + public: + /* + * Constructs a game solver with the given player 1 and player 2 matrices. + * + * @param player1Matrix The matrix defining the choices of player 1. + * @param player2Matrix The matrix defining the choices of player 2. + */ + GameSolver(storm::storage::SparseMatrix const& player1Matrix, storm::storage::SparseMatrix const& player2Matrix); + + /* + * Constructs a game solver with the given player 1 and player 2 matrices and options. + * + * @param player1Matrix The matrix defining the choices of player 1. + * @param player2Matrix The matrix defining the choices of player 2. + * @param precision The precision that is used to detect convergence. + * @param maximalNumberOfIterations The maximal number of iterations. + * @param relative Sets whether or not to detect convergence with a relative or absolute criterion. + */ + GameSolver(storm::storage::SparseMatrix const& player1Matrix, storm::storage::SparseMatrix const& player2Matrix, double precision, uint_fast64_t maximalNumberOfIterations, bool relative); + + /*! + * Solves the equation system defined by the game matrix. Note that the game matrix has to be given upon + * construction time of the solver object. + * + * @param player1Goal Sets whether player 1 wants to minimize or maximize. + * @param player2Goal Sets whether player 2 wants to minimize or maximize. + * @param x The initial guess of the solution. + * @param b The vector to add after matrix-vector multiplication. + * @return The solution vector in the for of the vector x. + */ + virtual void solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, std::vector& x, storm::dd::Add const& b) const; + + private: + // The matrix defining the choices of player 1. + storm::storage::SparseMatrix const& player1Matrix; + + // The matrix defining the choices of player 2. + storm::storage::SparseMatrix const& player2Matrix; + }; + } +} + +#endif /* STORM_SOLVER_GAMESOLVER_H_ */ diff --git a/src/solver/SymbolicGameSolver.cpp b/src/solver/SymbolicGameSolver.cpp index 8faab2914..4c03732a8 100644 --- a/src/solver/SymbolicGameSolver.cpp +++ b/src/solver/SymbolicGameSolver.cpp @@ -11,22 +11,16 @@ namespace storm { 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) { - // Get the settings object to customize solving. - storm::settings::modules::NativeEquationSolverSettings const& settings = storm::settings::nativeEquationSolverSettings(); - - // Get appropriate settings. - maximalNumberOfIterations = settings.getMaximalIterationCount(); - precision = settings.getPrecision(); - relative = settings.getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative; + // Intentionally left empty. } 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, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : gameMatrix(gameMatrix), allRows(allRows), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables), precision(precision), maximalNumberOfIterations(maximalNumberOfIterations), relative(relative) { + 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, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : AbstractGameSolver(precision, maximalNumberOfIterations, relative), gameMatrix(gameMatrix), allRows(allRows), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables) { // Intentionally left empty. } template - storm::dd::Add SymbolicGameSolver::solveGame(bool player1Min, bool player2Min, storm::dd::Add const& x, storm::dd::Add const& b) const { + storm::dd::Add SymbolicGameSolver::solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, 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; @@ -39,16 +33,14 @@ namespace storm { tmp += b; // Now abstract from player 2 and player 1 variables. - if (player2Min) { - tmp = tmp.minAbstract(this->player2Variables); - } else { - tmp = tmp.maxAbstract(this->player2Variables); + switch (player2Goal) { + case OptimizationDirection::Minimize: tmp.minAbstract(this->player2Variables); break; + case OptimizationDirection::Maximize: tmp = tmp.maxAbstract(this->player2Variables); break; } - - if (player1Min) { - tmp = tmp.minAbstract(this->player1Variables); - } else { - tmp = tmp.maxAbstract(this->player1Variables); + + switch (player1Goal) { + case OptimizationDirection::Minimize: tmp.minAbstract(this->player1Variables); break; + case OptimizationDirection::Maximize: tmp = tmp.maxAbstract(this->player1Variables); break; } // Now check if the process already converged within our precision. diff --git a/src/solver/SymbolicGameSolver.h b/src/solver/SymbolicGameSolver.h index 6abebee54..ec4c47d68 100644 --- a/src/solver/SymbolicGameSolver.h +++ b/src/solver/SymbolicGameSolver.h @@ -3,8 +3,11 @@ #include #include -#include "src/storage/expressions/Variable.h" +#include "src/solver/AbstractGameSolver.h" +#include "src/solver/OptimizationDirection.h" + +#include "src/storage/expressions/Variable.h" #include "src/storage/dd/Bdd.h" #include "src/storage/dd/Add.h" @@ -15,7 +18,7 @@ namespace storm { * An interface that represents an abstract symbolic game solver. */ template - class SymbolicGameSolver { + class SymbolicGameSolver : public AbstractGameSolver { public: /*! * Constructs a symbolic game solver with the given meta variable sets and pairs. @@ -50,16 +53,16 @@ namespace storm { 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, double precision, uint_fast64_t maximalNumberOfIterations, bool relative); /*! - * 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. + * Solves the equation system defined by the game matrix. Note that the game matrix 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 player1Goal Sets whether player 1 wants to minimize or maximize. + * @param player2Goal Sets whether player 2 wants to minimize or maximize. * @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; + virtual storm::dd::Add solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, storm::dd::Add const& x, storm::dd::Add const& b) const; protected: // The matrix defining the coefficients of the linear equation system. @@ -69,28 +72,19 @@ namespace storm { storm::dd::Bdd const& allRows; // The row variables. - std::set rowMetaVariables; + std::set const& rowMetaVariables; // The column variables. - std::set columnMetaVariables; + std::set const& columnMetaVariables; // The pairs of meta variables used for renaming. std::vector> const& rowColumnMetaVariablePairs; // The player 1 variables. - std::set player1Variables; + std::set const& player1Variables; // The player 2 variables. - std::set player2Variables; - - // 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; + std::set const& player2Variables; }; } // namespace solver diff --git a/test/functional/solver/FullySymbolicGameSolverTest.cpp b/test/functional/solver/FullySymbolicGameSolverTest.cpp index ce9e21798..dd48ad678 100644 --- a/test/functional/solver/FullySymbolicGameSolverTest.cpp +++ b/test/functional/solver/FullySymbolicGameSolverTest.cpp @@ -45,25 +45,25 @@ TEST(FullySymbolicGameSolverTest, Solve) { 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); + storm::dd::Add result = solver->solveGame(storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, 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 = solver->solveGame(storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, 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 = solver->solveGame(storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, 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 = solver->solveGame(storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, x, b); result *= manager->getEncoding(state.first, 1).toAdd(); result = result.sumAbstract({state.first}); EXPECT_NEAR(0.99999892625817599, result.getValue(), storm::settings::nativeEquationSolverSettings().getPrecision());