some work on sparse game solver

Former-commit-id: 74450365b3

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.
+        }
+    }
+}

src/solver/AbstractGameSolver.h

@@ -0,0 +1,40 @@
+#ifndef STORM_SOLVER_ABSTRACTGAMESOLVER_H_
+#define STORM_SOLVER_ABSTRACTGAMESOLVER_H_
+
+#include <cstdint>
+
+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_ */

src/solver/GameSolver.cpp

@@ -0,0 +1,17 @@
+#include "src/solver/GameSolver.h"
+
+namespace storm {
+    namespace solver {
+        GameSolver::GameSolver(storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix, storm::storage::SparseMatrix<ValueType> const& player2Matrix) : AbstractGameSolver(), player1Matrix(player1Matrix), player2Matrix(player2Matrix) {
+            // Intentionally left empty.
+        }
+
+        GameSolver::GameSolver(storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix, storm::storage::SparseMatrix<ValueType> 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<ValueType>& x, storm::dd::Add<Type> const& b) const {
+            // TODO
+        }
+    }
+}

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<typename ValueType>
+        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<storm::storage::sparse::state_type> const& player1Matrix, storm::storage::SparseMatrix<ValueType> 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<storm::storage::sparse::state_type> const& player1Matrix, storm::storage::SparseMatrix<ValueType> 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<ValueType>& x, storm::dd::Add<Type> const& b) const;
+
+        private:
+            // The matrix defining the choices of player 1.
+            storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix;
+
+            // The matrix defining the choices of player 2.
+            storm::storage::SparseMatrix<ValueType> const& player2Matrix;
+        };
+    }
+}
+
+#endif /* STORM_SOLVER_GAMESOLVER_H_ */

src/solver/SymbolicGameSolver.cpp

@@ -11,22 +11,16 @@ namespace storm {
         
         template<storm::dd::DdType Type>
         SymbolicGameSolver<Type>::SymbolicGameSolver(storm::dd::Add<Type> const& gameMatrix, storm::dd::Bdd<Type> const& allRows, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables) : gameMatrix(gameMatrix), allRows(allRows), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables) {
-            // Get the settings object to customize solving.
+            // Intentionally left empty.
-            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;
         }
         
         template<storm::dd::DdType Type>
-        SymbolicGameSolver<Type>::SymbolicGameSolver(storm::dd::Add<Type> const& gameMatrix, storm::dd::Bdd<Type> const& allRows, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> 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<Type>::SymbolicGameSolver(storm::dd::Add<Type> const& gameMatrix, storm::dd::Bdd<Type> const& allRows, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> 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::DdType Type>
-        storm::dd::Add<Type> SymbolicGameSolver<Type>::solveGame(bool player1Min, bool player2Min, storm::dd::Add<Type> const& x, storm::dd::Add<Type> const& b) const {
+        storm::dd::Add<Type> SymbolicGameSolver<Type>::solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, storm::dd::Add<Type> const& x, storm::dd::Add<Type> const& b) const {
             // Set up the environment.
             storm::dd::Add<Type> 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) {
+                switch (player2Goal) {
-                    tmp = tmp.minAbstract(this->player2Variables);
+                    case OptimizationDirection::Minimize: tmp.minAbstract(this->player2Variables); break;
-                } else {
+                    case OptimizationDirection::Maximize: tmp = tmp.maxAbstract(this->player2Variables); break;
-                    tmp = tmp.maxAbstract(this->player2Variables);
                 }
-                
+                switch (player1Goal) {
-                if (player1Min) {
+                    case OptimizationDirection::Minimize: tmp.minAbstract(this->player1Variables); break;
-                    tmp = tmp.minAbstract(this->player1Variables);
+                    case OptimizationDirection::Maximize: tmp = tmp.maxAbstract(this->player1Variables); break;
-                } else {
-                    tmp = tmp.maxAbstract(this->player1Variables);
                 }
                 
                 // Now check if the process already converged within our precision.

src/solver/SymbolicGameSolver.h

@@ -3,8 +3,11 @@
 
 #include <set>
 #include <vector>
-#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<storm::dd::DdType Type>
-        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<Type> const& gameMatrix, storm::dd::Bdd<Type> const& allRows, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> 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
+             * Solves the equation system defined by the game matrix. Note that the game matrix has to be given upon
-             * to be given upon construction time of the solver object.
+             * construction time of the solver object.
              *
-             * @param player1Min A flag indicating whether player 1 wants to minimize the result.
+             * @param player1Goal Sets whether player 1 wants to minimize or maximize.
-             * @param player2Min A flag indicating whether player 1 wants to minimize the result.
+             * @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<Type> solveGame(bool player1Min, bool player2Min, storm::dd::Add<Type> const& x, storm::dd::Add<Type> const& b) const;
+            virtual storm::dd::Add<Type> solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, storm::dd::Add<Type> const& x, storm::dd::Add<Type> const& b) const;
         
         protected:
             // The matrix defining the coefficients of the linear equation system.
@@ -69,28 +72,19 @@ namespace storm {
             storm::dd::Bdd<Type> const& allRows;
             
             // The row variables.
-            std::set<storm::expressions::Variable> rowMetaVariables;
+            std::set<storm::expressions::Variable> const& rowMetaVariables;
             
             // The column variables.
-            std::set<storm::expressions::Variable> columnMetaVariables;
+            std::set<storm::expressions::Variable> const& columnMetaVariables;
             
             // The pairs of meta variables used for renaming.
             std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs;
             
             // The player 1 variables.
-            std::set<storm::expressions::Variable> player1Variables;
+            std::set<storm::expressions::Variable> const& player1Variables;
             
             // The player 2 variables.
-            std::set<storm::expressions::Variable> player2Variables;
+            std::set<storm::expressions::Variable> const& 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;
         };
         
     } // namespace solver

test/functional/solver/FullySymbolicGameSolverTest.cpp

@@ -45,25 +45,25 @@ TEST(FullySymbolicGameSolverTest, Solve) {
     storm::dd::Add<storm::dd::DdType::CUDD> 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<storm::dd::DdType::CUDD> result = solver->solveGame(true, true, x, b);
+    storm::dd::Add<storm::dd::DdType::CUDD> 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());