Merge branch 'future' of https://sselab.de/lab9/private/git/storm into future

Former-commit-id: ed2036c1ae

src/parser/NondeterministicSparseTransitionParser.cpp

@@ -117,15 +117,21 @@ namespace storm {
                     // If we have switched the source state, we possibly need to insert the rows of the last
                     // source state.
                     if (source != lastSource) {
-                        curRow += ((modelInformation.getRowGroupIndices())[lastSource + 1] - (modelInformation.getRowGroupIndices())[lastSource]) -(lastChoice + 1);
+                        curRow += ((modelInformation.getRowGroupIndices())[lastSource + 1] - (modelInformation.getRowGroupIndices())[lastSource]) - (lastChoice + 1);
                     }
 
                     // If we skipped some states, we need to reserve empty rows for all their nondeterministic
-                    // choices.
+                    // choices and create the row groups.
                     for (uint_fast64_t i = lastSource + 1; i < source; ++i) {
+                        matrixBuilder.newRowGroup(modelInformation.getRowGroupIndices()[i]);
                         curRow += ((modelInformation.getRowGroupIndices())[i + 1] - (modelInformation.getRowGroupIndices())[i]);
                     }
 
+                    // If we moved to the next source, we need to open the next row group.
+                    if (source != lastSource) {
+                        matrixBuilder.newRowGroup(modelInformation.getRowGroupIndices()[source]);
+                    }
+
                     // If we advanced to the next state, but skipped some choices, we have to reserve rows
                     // for them
                     if (source != lastSource) {
@@ -155,7 +161,7 @@ namespace storm {
                         }
                     }
                     if (source != lastSource) {
-                        // Add create a new rowGroup for the source, if this is the first choice we encounter for this state.
+                        // Create a new rowGroup for the source, if this is the first choice we encounter for this state.
                         matrixBuilder.newRowGroup(curRow);
                     }
                 }
@@ -178,13 +184,8 @@ namespace storm {
 
             // Since we assume the transition rewards are for the transitions of the model, we copy the rowGroupIndices.
             if (isRewardFile) {
-                // We already have rowGroup 0.
-                for (uint_fast64_t index = 1; index < modelInformation.getRowGroupIndices().size() - 1; index++) {
-                    matrixBuilder.newRowGroup(modelInformation.getRowGroupIndices()[index]);
-                }
-            } else {
-                for (uint_fast64_t node = lastSource + 1; node <= firstPass.highestStateIndex; node++) {
-                    matrixBuilder.newRowGroup(curRow + 1);
+                for (uint_fast64_t node = lastSource + 1; node < modelInformation.getRowGroupCount(); node++) {
+                    matrixBuilder.newRowGroup(modelInformation.getRowGroupIndices()[node]);
                 }
             }
 

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,76 @@
+#include "src/solver/GameSolver.h"
+
+#include "src/storage/SparseMatrix.h"
+
+#include "src/utility/vector.h"
+
+namespace storm {
+    namespace solver {
+        template <typename ValueType>
+        GameSolver<ValueType>::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.
+        }
+
+        template <typename ValueType>
+        GameSolver<ValueType>::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.
+        }
+
+        template <typename ValueType>
+        void GameSolver<ValueType>::solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
+            // Set up the environment for value iteration.
+            uint_fast64_t numberOfPlayer1States = x.size();
+
+            bool converged = false;
+            std::vector<ValueType> tmpResult(numberOfPlayer1States);
+            std::vector<ValueType> nondetResult(player2Matrix.getRowCount());
+            std::vector<ValueType> player2Result(player2Matrix.getRowGroupCount());
+
+            // Now perform the actual value iteration.
+            uint_fast64_t iterations = 0;
+            do {
+                player2Matrix.multiplyWithVector(x, nondetResult);
+                storm::utility::vector::addVectors(b, nondetResult, nondetResult);
+
+                if (player2Goal == OptimizationDirection::Minimize) {
+                    storm::utility::vector::reduceVectorMin(nondetResult, player2Result, player2Matrix.getRowGroupIndices());
+                } else {
+                    storm::utility::vector::reduceVectorMax(nondetResult, player2Result, player2Matrix.getRowGroupIndices());
+                }
+
+                for (uint_fast64_t pl1State = 0; pl1State < numberOfPlayer1States; ++pl1State) {
+                    storm::storage::SparseMatrix<storm::storage::sparse::state_type>::const_rows relevantRows = player1Matrix.getRowGroup(pl1State);
+                    if (relevantRows.getNumberOfEntries() > 0) {
+                        storm::storage::SparseMatrix<storm::storage::sparse::state_type>::const_iterator it = relevantRows.begin();
+                        storm::storage::SparseMatrix<storm::storage::sparse::state_type>::const_iterator ite = relevantRows.end();
+
+                        // Set the first value.
+                        tmpResult[pl1State] = player2Result[it->getColumn()];
+                        ++it;
+
+                        // Now iterate through the different values and pick the extremal one.
+                        if (player1Goal == OptimizationDirection::Minimize) {
+                            for (; it != ite; ++it) {
+                                tmpResult[pl1State] = std::min(tmpResult[pl1State], player2Result[it->getColumn()]);
+                            }
+                        } else {
+                            for (; it != ite; ++it) {
+                                tmpResult[pl1State] = std::max(tmpResult[pl1State], player2Result[it->getColumn()]);
+                            }
+                        }
+                    } else {
+                        tmpResult[pl1State] = storm::utility::zero<ValueType>();
+                    }
+                }
+
+                // Check if the process converged and set up the new iteration in case we are not done.
+                converged = storm::utility::vector::equalModuloPrecision(x, tmpResult, precision, relative);
+                std::swap(x, tmpResult);
+
+                ++iterations;
+            } while (!converged && iterations < maximalNumberOfIterations);
+        }
+
+        template class GameSolver<double>;
+    }
+}

src/solver/GameSolver.h

@@ -0,0 +1,62 @@
+#ifndef STORM_SOLVER_GAMESOLVER_H_
+#define STORM_SOLVER_GAMESOLVER_H_
+
+#include <vector>
+
+#include "src/solver/AbstractGameSolver.h"
+#include "src/solver/OptimizationDirection.h"
+
+#include "src/storage/sparse/StateType.h"
+
+namespace storm {
+    namespace storage {
+        template<typename ValueType>
+        class SparseMatrix;
+    }
+
+    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, std::vector<ValueType> 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,44 +11,36 @@ 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.
-            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<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;
             bool converged = false;
             
-            while (!converged && iterations < maximalNumberOfIterations) {
+            do {
                 // 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.
-                if (player2Min) {
-                    tmp = tmp.minAbstract(this->player2Variables);
-                } else {
-                    tmp = tmp.maxAbstract(this->player2Variables);
+                switch (player2Goal) {
+                    case OptimizationDirection::Minimize: tmp = 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 = tmp.minAbstract(this->player1Variables); break;
+                    case OptimizationDirection::Maximize: tmp = tmp.maxAbstract(this->player1Variables); break;
                 }
                 
                 // Now check if the process already converged within our precision.
@@ -60,7 +52,7 @@ namespace storm {
                 }
                 
                 ++iterations;
-            }
+            } while (!converged && iterations < maximalNumberOfIterations);
             
             return xCopy;
         }

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
-             * 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<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;
-            
-            // 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<storm::expressions::Variable> const& player2Variables;
         };
         
     } // namespace solver

src/storage/SparseMatrix.cpp

@@ -1,4 +1,5 @@
 #include <boost/functional/hash.hpp>
+#include <src/storage/sparse/StateType.h>
 
 // To detect whether the usage of TBB is possible, this include is neccessary
 #include "storm-config.h"
@@ -143,9 +144,18 @@ namespace storm {
         template<typename ValueType>
         void SparseMatrixBuilder<ValueType>::newRowGroup(index_type startingRow) {
             STORM_LOG_THROW(hasCustomRowGrouping, storm::exceptions::InvalidStateException, "Matrix was not created to have a custom row grouping.");
-            STORM_LOG_THROW(rowGroupIndices.empty() || startingRow >= rowGroupIndices.back(), storm::exceptions::InvalidStateException, "Illegal row group with negative size.");
+            STORM_LOG_THROW(startingRow >= lastRow, storm::exceptions::InvalidStateException, "Illegal row group with negative size.");
             rowGroupIndices.push_back(startingRow);
             ++currentRowGroup;
+
+            // Close all rows from the most recent one to the starting row.
+            for (index_type i = lastRow + 1; i <= startingRow; ++i) {
+                rowIndications.push_back(currentEntryCount);
+            }
+
+            // Reset the most recently seen row/column to allow for proper insertion of the following elements.
+            lastRow = startingRow;
+            lastColumn = 0;
         }
         
         template<typename ValueType>
@@ -156,7 +166,7 @@ namespace storm {
                 rowCount = std::max(rowCount, initialRowCount);
             }
             rowCount = std::max(rowCount, overriddenRowCount);
-            
+
             // If the current row count was overridden, we may need to add empty rows.
             for (index_type i = lastRow + 1; i < rowCount; ++i) {
                 rowIndications.push_back(currentEntryCount);
@@ -196,7 +206,7 @@ namespace storm {
                     rowGroupIndices.push_back(rowCount);
                 }
             }
-            
+
             return SparseMatrix<ValueType>(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices), hasCustomRowGrouping);
         }
         
@@ -1163,16 +1173,16 @@ namespace storm {
         // Explicitly instantiate the entry, builder and the matrix.
         // double
         template class MatrixEntry<typename SparseMatrix<double>::index_type, double>;
-        template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, double> const& entry);
+        template std::ostream& operator<<(std::ostream& out, MatrixEntry<typename SparseMatrix<double>::index_type, double> const& entry);
         template class SparseMatrixBuilder<double>;
         template class SparseMatrix<double>;
         template std::ostream& operator<<(std::ostream& out, SparseMatrix<double> const& matrix);
         template std::vector<double> SparseMatrix<double>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<double> const& otherMatrix) const;
         template bool SparseMatrix<double>::isSubmatrixOf(SparseMatrix<double> const& matrix) const;
 
-            // float
+        // float
         template class MatrixEntry<typename SparseMatrix<float>::index_type, float>;
-        template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, float> const& entry);
+        template std::ostream& operator<<(std::ostream& out, MatrixEntry<typename SparseMatrix<float>::index_type, float> const& entry);
         template class SparseMatrixBuilder<float>;
         template class SparseMatrix<float>;
         template std::ostream& operator<<(std::ostream& out, SparseMatrix<float> const& matrix);
@@ -1181,12 +1191,20 @@ namespace storm {
 
         // int
         template class MatrixEntry<typename SparseMatrix<int>::index_type, int>;
-        template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, int> const& entry);
+        template std::ostream& operator<<(std::ostream& out, MatrixEntry<typename SparseMatrix<int>::index_type, int> const& entry);
         template class SparseMatrixBuilder<int>;
         template class SparseMatrix<int>;
         template std::ostream& operator<<(std::ostream& out, SparseMatrix<int> const& matrix);
         template bool SparseMatrix<int>::isSubmatrixOf(SparseMatrix<int> const& matrix) const;
 
+        // state_type
+        template class MatrixEntry<typename SparseMatrix<storm::storage::sparse::state_type>::index_type, storm::storage::sparse::state_type>;
+        template std::ostream& operator<<(std::ostream& out, MatrixEntry<typename SparseMatrix<storm::storage::sparse::state_type>::index_type, storm::storage::sparse::state_type> const& entry);
+        template class SparseMatrixBuilder<storm::storage::sparse::state_type>;
+        template class SparseMatrix<storm::storage::sparse::state_type>;
+        template std::ostream& operator<<(std::ostream& out, SparseMatrix<storm::storage::sparse::state_type> const& matrix);
+        template bool SparseMatrix<int>::isSubmatrixOf(SparseMatrix<storm::storage::sparse::state_type> const& matrix) const;
+
 #ifdef STORM_HAVE_CARL
         // Rat Function
         template class MatrixEntry<typename SparseMatrix<RationalFunction>::index_type, RationalFunction>;

src/storage/prism/Program.cpp

@@ -1011,7 +1011,6 @@ namespace storm {
                     }
                     
                     // Now we are in a position to start the enumeration over all command variables.
-                    uint_fast64_t modelCount = 0;
                     solver->allSat(allCommandVariables, [&] (storm::solver::SmtSolver::ModelReference& modelReference) -> bool {
                         // Now we need to reconstruct the chosen commands from the valuation of the command variables.
                         std::vector<std::vector<std::reference_wrapper<Command const>>> chosenCommands(possibleCommands.size());

src/utility/ConstantsComparator.cpp

@@ -2,6 +2,7 @@
 
 #include <cstdlib>
 #include <cmath>
+#include <src/storage/sparse/StateType.h>
 
 #include "src/utility/constants.h"
 #include "src/settings/SettingsManager.h"
@@ -94,7 +95,8 @@ namespace storm {
         template class ConstantsComparator<double>;
         template class ConstantsComparator<float>;
         template class ConstantsComparator<int>;
-        
+        template class ConstantsComparator<storm::storage::sparse::state_type>;
+
 #ifdef STORM_HAVE_CARL
         template class ConstantsComparator<RationalFunction>;
         template class ConstantsComparator<Polynomial>;

src/utility/constants.cpp

@@ -1,7 +1,7 @@
 #include "src/utility/constants.h"
 
-#include "src/storage/SparseMatrix.h"
 #include "src/storage/sparse/StateType.h"
+#include "src/storage/SparseMatrix.h"
 #include "src/settings/SettingsManager.h"
 #include "src/settings/modules/GeneralSettings.h"
 
@@ -83,27 +83,13 @@ namespace storm {
             return std::pow(value, exponent);
         }
 
-		template<>
-		double simplify(double value) {
-			// In the general case, we don't to anything here, but merely return the value. If something else is
-			// supposed to happen here, the templated function can be specialized for this particular type.
-			return value;
-		}
-
-		template<>
-		float simplify(float value) {
-			// In the general case, we don't to anything here, but merely return the value. If something else is
-			// supposed to happen here, the templated function can be specialized for this particular type.
+		template<typename ValueType>
+		ValueType simplify(ValueType value) {
+            // In the general case, we don't to anything here, but merely return the value. If something else is
+            // supposed to happen here, the templated function can be specialized for this particular type.
 			return value;
 		}
 
-        template<>
-        int simplify(int value) {
-            // In the general case, we don't to anything here, but merely return the value. If something else is
-            // supposed to happen here, the templated function can be specialized for this particular type.
-            return value;
-        }
-        
 #ifdef STORM_HAVE_CARL
         template<>
         RationalFunction& simplify(RationalFunction& value);
@@ -201,7 +187,23 @@ namespace storm {
         template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int> matrixEntry);
         template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>& matrixEntry);
         template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>&& matrixEntry);
-        
+
+        template bool isOne(storm::storage::sparse::state_type const& value);
+        template bool isZero(storm::storage::sparse::state_type const& value);
+        template bool isConstant(storm::storage::sparse::state_type const& value);
+
+        template storm::storage::sparse::state_type one();
+        template storm::storage::sparse::state_type zero();
+        template storm::storage::sparse::state_type infinity();
+
+        template storm::storage::sparse::state_type pow(storm::storage::sparse::state_type const& value, uint_fast64_t exponent);
+
+        template storm::storage::sparse::state_type simplify(storm::storage::sparse::state_type value);
+
+        template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type> matrixEntry);
+        template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>& matrixEntry);
+        template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>&& matrixEntry);
+
 #ifdef STORM_HAVE_CARL
         template bool isOne(RationalFunction const& value);
         template bool isZero(RationalFunction const& value);

src/utility/solver.cpp

@@ -1,13 +1,13 @@
 #include "src/utility/solver.h"
 
-#include "src/solver/SymbolicGameSolver.h"
-
 #include <vector>
 
 #include "src/solver/SymbolicLinearEquationSolver.h"
 #include "src/solver/SymbolicMinMaxLinearEquationSolver.h"
+#include "src/solver/SymbolicGameSolver.h"
 #include "src/solver/NativeLinearEquationSolver.h"
 #include "src/solver/GmmxxLinearEquationSolver.h"
+#include "src/solver/GameSolver.h"
 
 #include "src/solver/NativeMinMaxLinearEquationSolver.h"
 #include "src/solver/GmmxxMinMaxLinearEquationSolver.h"
@@ -102,8 +102,7 @@ namespace storm {
             template<typename ValueType>
             void MinMaxLinearEquationSolverFactory<ValueType>::setPreferredTechnique(storm::solver::MinMaxTechniqueSelection preferredTech) {
                 this->prefTech = preferredTech;
-            } 
-
+            }
             
             template<typename ValueType>
             std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> MinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix, bool trackPolicy) const {
@@ -133,6 +132,10 @@ namespace storm {
                 
             }
 
+            template<typename ValueType>
+            std::unique_ptr<storm::solver::GameSolver<ValueType>> GameSolverFactory<ValueType>::create(storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix, storm::storage::SparseMatrix<ValueType> const& player2Matrix) const {
+                return std::unique_ptr<storm::solver::GameSolver<ValueType>>(new storm::solver::GameSolver<ValueType>(player1Matrix, player2Matrix));
+            }
 
             std::unique_ptr<storm::solver::LpSolver> LpSolverFactory::create(std::string const& name, storm::solver::LpSolverTypeSelection solvT) const {
                 storm::solver::LpSolverType t;
@@ -192,7 +195,7 @@ namespace storm {
             template class GmmxxLinearEquationSolverFactory<double>;
             template class NativeLinearEquationSolverFactory<double>;
             template class MinMaxLinearEquationSolverFactory<double>;
-          
+            template class GameSolverFactory<double>;
         }
     }
 }

src/utility/solver.h

@@ -4,6 +4,7 @@
 #include <set>
 #include <vector>
 #include <memory>
+#include <src/storage/sparse/StateType.h>
 
 #include "src/storage/dd/DdType.h"
 #include "src/solver/SolverSelectionOptions.h"
@@ -13,13 +14,15 @@ namespace storm {
         template<storm::dd::DdType T>  class SymbolicGameSolver;
         template<storm::dd::DdType T, typename V> class SymbolicLinearEquationSolver;
         template<storm::dd::DdType T, typename V> class SymbolicMinMaxLinearEquationSolver;
+        template<typename V> class GameSolver;
         template<typename V> class LinearEquationSolver;
         template<typename V> class MinMaxLinearEquationSolver;
         class LpSolver;
         class SmtSolver;
         
         template<typename ValueType> class NativeLinearEquationSolver;
-        enum class NativeLinearEquationSolverSolutionMethod;
+        enum class
+                NativeLinearEquationSolverSolutionMethod;
     }
 
     namespace storage {
@@ -93,7 +96,7 @@ namespace storm {
             public:
                 MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection solverType = storm::solver::EquationSolverTypeSelection::FROMSETTINGS);
                 /*!
-                 * Creates a new nondeterministic linear equation solver instance with the given matrix.
+                 * Creates a new min/max linear equation solver instance with the given matrix.
                  */
                 virtual std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix, bool trackPolicy = false) const;
                 void setSolverType(storm::solver::EquationSolverTypeSelection solverType);
@@ -106,6 +109,15 @@ namespace storm {
                 /// Notice that we save the selection enum here, which allows different solvers to use different techniques.
                 storm::solver::MinMaxTechniqueSelection prefTech;
             };
+
+            template<typename ValueType>
+            class GameSolverFactory {
+            public:
+                /*!
+                 * Creates a new game solver instance with the given matrices.
+                 */
+                virtual std::unique_ptr<storm::solver::GameSolver<ValueType>> create(storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix, storm::storage::SparseMatrix<ValueType> const& player2Matrix) const;
+            };
            
             class LpSolverFactory {
             public:

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());

test/functional/solver/GameSolverTest.cpp

@@ -0,0 +1,69 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+
+#include "src/storage/SparseMatrix.h"
+
+#include "src/utility/solver.h"
+#include "src/settings/SettingsManager.h"
+
+#include "src/solver/GameSolver.h"
+#include "src/settings/modules/NativeEquationSolverSettings.h"
+
+TEST(GameSolverTest, Solve) {
+    // Construct simple game. Start with player 2 matrix.
+    storm::storage::SparseMatrixBuilder<double> player2MatrixBuilder(0, 0, 0, false, true);
+    player2MatrixBuilder.newRowGroup(0);
+    player2MatrixBuilder.addNextValue(0, 0, 0.4);
+    player2MatrixBuilder.addNextValue(0, 1, 0.6);
+    player2MatrixBuilder.addNextValue(1, 1, 0.2);
+    player2MatrixBuilder.addNextValue(1, 2, 0.8);
+    player2MatrixBuilder.newRowGroup(2);
+    player2MatrixBuilder.addNextValue(2, 2, 0.5);
+    player2MatrixBuilder.addNextValue(2, 3, 0.5);
+    player2MatrixBuilder.addNextValue(3, 0, 1);
+    player2MatrixBuilder.newRowGroup(4);
+    player2MatrixBuilder.newRowGroup(5);
+    player2MatrixBuilder.newRowGroup(6);
+    storm::storage::SparseMatrix<double> player2Matrix = player2MatrixBuilder.build();
+
+    // Now build player 1 matrix.
+    storm::storage::SparseMatrixBuilder<storm::storage::sparse::state_type> player1MatrixBuilder(0, 0, 0, false, true);
+    player1MatrixBuilder.newRowGroup(0);
+    player1MatrixBuilder.addNextValue(0, 0, 1);
+    player1MatrixBuilder.addNextValue(1, 1, 1);
+    player1MatrixBuilder.newRowGroup(2);
+    player1MatrixBuilder.addNextValue(2, 2, 1);
+    player1MatrixBuilder.newRowGroup(3);
+    player1MatrixBuilder.addNextValue(3, 3, 1);
+    player1MatrixBuilder.newRowGroup(4);
+    player1MatrixBuilder.addNextValue(4, 4, 1);
+    storm::storage::SparseMatrix<storm::storage::sparse::state_type> player1Matrix = player1MatrixBuilder.build();
+
+    std::unique_ptr<storm::utility::solver::GameSolverFactory<double>> solverFactory(new storm::utility::solver::GameSolverFactory<double>());
+    std::unique_ptr<storm::solver::GameSolver<double>> solver = solverFactory->create(player1Matrix, player2Matrix);
+
+    // Create solution and target state vector.
+    std::vector<double> result(4);
+    std::vector<double> b(7);
+    b[4] = 1;
+    b[6] = 1;
+
+    // Now solve the game with different strategies for the players.
+    solver->solveGame(storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, result, b);
+    EXPECT_NEAR(0, result[0], storm::settings::nativeEquationSolverSettings().getPrecision());
+
+    result = std::vector<double>(4);
+
+    solver->solveGame(storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, result, b);
+    EXPECT_NEAR(0.5, result[0], storm::settings::nativeEquationSolverSettings().getPrecision());
+
+    result = std::vector<double>(4);
+
+    solver->solveGame(storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, result, b);
+    EXPECT_NEAR(0.2, result[0], storm::settings::nativeEquationSolverSettings().getPrecision());
+
+    result = std::vector<double>(4);
+
+    solver->solveGame(storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, result, b);
+    EXPECT_NEAR(0.99999892625817599, result[0], storm::settings::nativeEquationSolverSettings().getPrecision());
+}