First version of fully symbolic game solver.

Former-commit-id: 34406f25b9

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;
         }

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<storm::dd::DdType Type>
+        FullySymbolicGameSolver<Type>::FullySymbolicGameSolver(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) : SymbolicGameSolver<Type>(gameMatrix, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables, player2Variables), precision(precision), maximalNumberOfIterations(maximalNumberOfIterations), relative(relative) {
+            // Intentionally left empty.
+        }
+        
+        template<storm::dd::DdType Type>
+        FullySymbolicGameSolver<Type>::FullySymbolicGameSolver(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) : SymbolicGameSolver<Type>(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::DdType Type>
+        storm::dd::Add<Type> FullySymbolicGameSolver<Type>::solveGame(bool player1Min, bool player2Min, 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;
+            bool converged = false;
+
+            while (!converged && iterations < maximalNumberOfIterations) {
+                // Compute tmp = A * x + b
+                storm::dd::Add<Type> xCopyAsColumn = xCopy.swapVariables(this->rowColumnMetaVariablePairs);
+                storm::dd::Add<Type> 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<storm::dd::DdType::CUDD>;
+        
+    }
+}

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<storm::dd::DdType Type>
+        class FullySymbolicGameSolver : public SymbolicGameSolver<Type> {
+        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<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);
+            
+            /*!
+             * 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<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);
+            
+            virtual storm::dd::Add<Type> solveGame(bool player1Min, bool player2Min, storm::dd::Add<Type> const& x, storm::dd::Add<Type> 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_ */

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<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) {
+            // Intentionally left empty.
+        }
+     
+        template class SymbolicGameSolver<storm::dd::DdType::CUDD>;
+        
+    }
+}

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<storm::dd::DdType Type>
+        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<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);
+            
+            /*!
+             * 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<Type> solveGame(bool player1Min, bool player2Min, storm::dd::Add<Type> const& x, storm::dd::Add<Type> const& b) const = 0;
+        
+        protected:
+            // The matrix defining the coefficients of the linear equation system.
+            storm::dd::Add<Type> const& gameMatrix;
+            
+            // A BDD characterizing all rows of the equation system.
+            storm::dd::Bdd<Type> const& allRows;
+            
+            // The row variables.
+            std::set<storm::expressions::Variable> rowMetaVariables;
+            
+            // The column variables.
+            std::set<storm::expressions::Variable> 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;
+            
+            // The player 2 variables.
+            std::set<storm::expressions::Variable> player2Variables;
+        };
+        
+    } // namespace solver
+} // namespace storm
+
+#endif /* STORM_SOLVER_SYMBOLICGAMESOLVER_H_ */

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<storm::dd::DdType Type>
+            std::unique_ptr<storm::solver::SymbolicGameSolver<Type>> SymbolicGameSolverFactory<Type>::create(storm::dd::Add<Type> const& A, 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) const {
+                return std::unique_ptr<storm::solver::SymbolicGameSolver<Type>>(new storm::solver::FullySymbolicGameSolver<Type>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables, player2Variables));
+            }
+            
             template<typename ValueType>
             std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> LinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> 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<storm::dd::DdType::CUDD>;
             template class LinearEquationSolverFactory<double>;
             template class GmmxxLinearEquationSolverFactory<double>;
             template class NativeLinearEquationSolverFactory<double>;

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<storm::dd::DdType Type>
+            class SymbolicGameSolverFactory {
+            public:
+                virtual std::unique_ptr<storm::solver::SymbolicGameSolver<Type>> create(storm::dd::Add<Type> const& A, 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) const;
+            };
+            
             template<typename ValueType>
             class LinearEquationSolverFactory {
             public:

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<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
+    std::pair<storm::expressions::Variable, storm::expressions::Variable> state = manager->addMetaVariable("x", 1, 4);
+    std::pair<storm::expressions::Variable, storm::expressions::Variable> pl1 = manager->addMetaVariable("a", 0, 1);
+    std::pair<storm::expressions::Variable, storm::expressions::Variable> pl2 = manager->addMetaVariable("b", 0, 1);
+
+    storm::dd::Bdd<storm::dd::DdType::CUDD> allRows = manager->getBddZero();
+    std::set<storm::expressions::Variable> rowMetaVariables({state.first});
+    std::set<storm::expressions::Variable> columnMetaVariables({state.second});
+    std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> rowColumnMetaVariablePairs = {state};
+    std::set<storm::expressions::Variable> player1Variables({pl1.first});
+    std::set<storm::expressions::Variable> player2Variables({pl2.first});
+
+    // Construct simple game.
+    storm::dd::Add<storm::dd::DdType::CUDD> 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<storm::utility::solver::SymbolicGameSolverFactory<storm::dd::DdType::CUDD>> solverFactory(new storm::utility::solver::SymbolicGameSolverFactory<storm::dd::DdType::CUDD>());
+    std::unique_ptr<storm::solver::SymbolicGameSolver<storm::dd::DdType::CUDD>> solver = solverFactory->create(matrix, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables,player2Variables);
+    
+    // Create solution and target state vector.
+    storm::dd::Add<storm::dd::DdType::CUDD> x = manager->getAddZero();
+    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);
+    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());
+}