Refactored GameSolver. It is now analogous to the MinMaxLinearEquationSolver.

src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp

@@ -8,7 +8,6 @@
 #include "storm/models/sparse/StandardRewardModel.h"
 #include "storm/utility/vector.h"
 #include "storm/utility/graph.h"
-#include "storm/solver/GameSolver.h"
 #include "storm/logic/FragmentSpecification.h"
 
 #include "storm/exceptions/InvalidArgumentException.h"
@@ -20,11 +19,11 @@ namespace storm {
         namespace parametric {
             
             template <typename SparseModelType, typename ConstantType>
-            SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel) : SparseParameterLiftingModelChecker<SparseModelType, ConstantType>(parametricModel), solverFactory(std::make_unique<storm::utility::solver::GameSolverFactory<ConstantType>>()) {
+            SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel) : SparseParameterLiftingModelChecker<SparseModelType, ConstantType>(parametricModel), solverFactory(std::make_unique<storm::solver::GameSolverFactory<ConstantType>>()) {
             }
             
             template <typename SparseModelType, typename ConstantType>
-            SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr<storm::utility::solver::GameSolverFactory<ConstantType>>&& solverFactory) : SparseParameterLiftingModelChecker<SparseModelType, ConstantType>(parametricModel), solverFactory(std::move(solverFactory)) {
+            SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr<storm::solver::GameSolverFactory<ConstantType>>&& solverFactory) : SparseParameterLiftingModelChecker<SparseModelType, ConstantType>(parametricModel), solverFactory(std::move(solverFactory)) {
             }
     
             template <typename SparseModelType, typename ConstantType>
@@ -212,10 +211,10 @@ namespace storm {
                 if(lowerResultBound) solver->setLowerBound(lowerResultBound.get());
                 if(upperResultBound) solver->setUpperBound(upperResultBound.get());
                 if(applyPreviousResultAsHint) {
-                    solver->setTrackScheduler(true);
+                    solver->setTrackSchedulers(true);
                     x.resize(maybeStates.getNumberOfSetBits(), storm::utility::zero<ConstantType>());
-                    if(storm::solver::minimize(dirForParameters) && minSched && player1Sched) solver->setSchedulerHint(std::move(player1Sched.get()), std::move(minSched.get()));
-                    if(storm::solver::maximize(dirForParameters) && maxSched && player1Sched) solver->setSchedulerHint(std::move(player1Sched.get()), std::move(maxSched.get()));
+                    if(storm::solver::minimize(dirForParameters) && minSched && player1Sched) solver->setSchedulerHints(std::move(player1Sched.get()), std::move(minSched.get()));
+                    if(storm::solver::maximize(dirForParameters) && maxSched && player1Sched) solver->setSchedulerHints(std::move(player1Sched.get()), std::move(maxSched.get()));
                 } else {
                     x.assign(maybeStates.getNumberOfSetBits(), storm::utility::zero<ConstantType>());
                 }
@@ -241,11 +240,11 @@ namespace storm {
                     solver->solveGame(this->currentCheckTask->getOptimizationDirection(), dirForParameters, x, parameterLifter->getVector());
                     if(applyPreviousResultAsHint) {
                         if(storm::solver::minimize(dirForParameters)) {
-                            minSched = solver->getPlayer2Scheduler();
+                            minSched = std::move(*solver->getPlayer2Scheduler());
                         } else {
-                            maxSched = solver->getPlayer2Scheduler();
+                            maxSched = std::move(*solver->getPlayer2Scheduler());
                         }
-                        player1Sched = solver->getPlayer1Scheduler();
+                        player1Sched = std::move(*solver->getPlayer1Scheduler());
                     }
                 }
                 

src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h

@@ -8,7 +8,7 @@
 #include "storm/storage/BitVector.h"
 #include "storm/storage/SparseMatrix.h"
 #include "storm/storage/sparse/StateType.h"
-#include "storm/utility/solver.h"
+#include "storm/solver/GameSolver.h"
 #include "storm/transformer/ParameterLifter.h"
 #include "storm/storage/TotalScheduler.h"
 
@@ -20,7 +20,7 @@ namespace storm {
             class SparseMdpParameterLiftingModelChecker : public SparseParameterLiftingModelChecker<SparseModelType, ConstantType> {
             public:
                 SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel);
-                SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr<storm::utility::solver::GameSolverFactory<ConstantType>>&& solverFactory);
+                SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr<storm::solver::GameSolverFactory<ConstantType>>&& solverFactory);
                 
                 virtual bool canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const override;
                 
@@ -49,7 +49,7 @@ namespace storm {
                 
                 storm::storage::SparseMatrix<storm::storage::sparse::state_type> player1Matrix;
                 std::unique_ptr<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>> parameterLifter;
-                std::unique_ptr<storm::utility::solver::GameSolverFactory<ConstantType>> solverFactory;
+                std::unique_ptr<storm::solver::GameSolverFactory<ConstantType>> solverFactory;
                 
                 // Results from the most recent solver call.
                 boost::optional<storm::storage::TotalScheduler> minSched, maxSched;

src/storm/settings/SettingsManager.cpp

@@ -25,6 +25,7 @@
 #include "storm/settings/modules/NativeEquationSolverSettings.h"
 #include "storm/settings/modules/EliminationSettings.h"
 #include "storm/settings/modules/MinMaxEquationSolverSettings.h"
+#include "storm/settings/modules/GameSolverSettings.h"
 #include "storm/settings/modules/BisimulationSettings.h"
 #include "storm/settings/modules/GlpkSettings.h"
 #include "storm/settings/modules/GurobiSettings.h"
@@ -521,6 +522,7 @@ namespace storm {
             storm::settings::addModule<storm::settings::modules::NativeEquationSolverSettings>();
             storm::settings::addModule<storm::settings::modules::EliminationSettings>();
             storm::settings::addModule<storm::settings::modules::MinMaxEquationSolverSettings>();
+            storm::settings::addModule<storm::settings::modules::GameSolverSettings>();
             storm::settings::addModule<storm::settings::modules::BisimulationSettings>();
             storm::settings::addModule<storm::settings::modules::GlpkSettings>();
             storm::settings::addModule<storm::settings::modules::GurobiSettings>();

src/storm/settings/modules/GameSolverSettings.cpp

@@ -0,0 +1,73 @@
+#include "storm/settings/modules/GameSolverSettings.h"
+
+#include "storm/settings/Option.h"
+#include "storm/settings/ArgumentBuilder.h"
+#include "storm/settings/OptionBuilder.h"
+
+#include "storm/utility/macros.h"
+#include "storm/exceptions/IllegalArgumentValueException.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            const std::string GameSolverSettings::moduleName = "game";
+            const std::string GameSolverSettings::solvingMethodOptionName = "method";
+            const std::string GameSolverSettings::maximalIterationsOptionName = "maxiter";
+            const std::string GameSolverSettings::maximalIterationsOptionShortName = "i";
+            const std::string GameSolverSettings::precisionOptionName = "precision";
+            const std::string GameSolverSettings::absoluteOptionName = "absolute";
+
+            GameSolverSettings::GameSolverSettings() : ModuleSettings(moduleName) {
+                std::vector<std::string> gameSolvingTechniques = {"vi", "value-iteration", "pi", "policy-iteration"};
+                this->addOption(storm::settings::OptionBuilder(moduleName, solvingMethodOptionName, false, "Sets which game solving technique is preferred.")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of a game solving technique.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(gameSolvingTechniques)).setDefaultValueString("vi").build()).build());
+                
+                this->addOption(storm::settings::OptionBuilder(moduleName, maximalIterationsOptionName, false, "The maximal number of iterations to perform before iterative solving is aborted.").setShortName(maximalIterationsOptionShortName).addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").setDefaultValueUnsignedInteger(20000).build()).build());
+                
+                this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
+
+                this->addOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, false, "Sets whether the relative or the absolute error is considered for detecting convergence.").build());
+            }
+            
+            storm::solver::GameMethod GameSolverSettings::getGameSolvingMethod() const {
+                std::string gameSolvingTechnique = this->getOption(solvingMethodOptionName).getArgumentByName("name").getValueAsString();
+                if (gameSolvingTechnique == "value-iteration" || gameSolvingTechnique == "vi") {
+                    return storm::solver::GameMethod::ValueIteration;
+                } else if (gameSolvingTechnique == "policy-iteration" || gameSolvingTechnique == "pi") {
+                    return storm::solver::GameMethod::PolicyIteration;
+                }
+                STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown game solving technique '" << gameSolvingTechnique << "'.");
+            }
+            
+            bool GameSolverSettings::isGameSolvingMethodSet() const {
+                return this->getOption(solvingMethodOptionName).getHasOptionBeenSet();
+            }
+            
+            bool GameSolverSettings::isMaximalIterationCountSet() const {
+                return this->getOption(maximalIterationsOptionName).getHasOptionBeenSet();
+            }
+            
+            uint_fast64_t GameSolverSettings::getMaximalIterationCount() const {
+                return this->getOption(maximalIterationsOptionName).getArgumentByName("count").getValueAsUnsignedInteger();
+            }
+            
+            bool GameSolverSettings::isPrecisionSet() const {
+                return this->getOption(precisionOptionName).getHasOptionBeenSet();
+            }
+            
+            double GameSolverSettings::getPrecision() const {
+                return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble();
+            }
+            
+            bool GameSolverSettings::isConvergenceCriterionSet() const {
+                return this->getOption(absoluteOptionName).getHasOptionBeenSet();
+            }
+            
+            GameSolverSettings::ConvergenceCriterion GameSolverSettings::getConvergenceCriterion() const {
+                return this->getOption(absoluteOptionName).getHasOptionBeenSet() ? GameSolverSettings::ConvergenceCriterion::Absolute : GameSolverSettings::ConvergenceCriterion::Relative;
+            }
+            
+        }
+    }
+}

src/storm/settings/modules/GameSolverSettings.h

@@ -0,0 +1,91 @@
+#pragma once
+
+#include "storm-config.h"
+#include "storm/settings/modules/ModuleSettings.h"
+
+#include "storm/solver/SolverSelectionOptions.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            /*!
+             * This class represents the game solver settings.
+             */
+            class GameSolverSettings : public ModuleSettings {
+            public:
+                // An enumeration of all available convergence criteria.
+                enum class ConvergenceCriterion { Absolute, Relative };
+                
+                GameSolverSettings();
+              
+                /*!
+                 * Retrieves whether a game solving technique has been set.
+                 *
+                 * @return True iff an equation solving technique has been set.
+                 */
+                bool isGameSolvingMethodSet() const;
+                
+                /*!
+                 * Retrieves the selected game solving technique.
+                 *
+                 * @return The selected game solving technique.
+                 */
+                storm::solver::GameMethod getGameSolvingMethod() const;
+                
+                /*!
+                 * Retrieves whether the maximal iteration count has been set.
+                 *
+                 * @return True iff the maximal iteration count has been set.
+                 */
+                bool isMaximalIterationCountSet() const;
+                
+                /*!
+                 * Retrieves the maximal number of iterations to perform until giving up on converging.
+                 *
+                 * @return The maximal iteration count.
+                 */
+                uint_fast64_t getMaximalIterationCount() const;
+                
+                /*!
+                 * Retrieves whether the precision has been set.
+                 *
+                 * @return True iff the precision has been set.
+                 */
+                bool isPrecisionSet() const;
+                
+                /*!
+                 * Retrieves the precision that is used for detecting convergence.
+                 *
+                 * @return The precision to use for detecting convergence.
+                 */
+                double getPrecision() const;
+                
+                /*!
+                 * Retrieves whether the convergence criterion has been set.
+                 *
+                 * @return True iff the convergence criterion has been set.
+                 */
+                bool isConvergenceCriterionSet() const;
+                
+                /*!
+                 * Retrieves the selected convergence criterion.
+                 *
+                 * @return The selected convergence criterion.
+                 */
+                ConvergenceCriterion getConvergenceCriterion() const;
+                
+                // The name of the module.
+                static const std::string moduleName;
+                
+            private:
+                static const std::string solvingMethodOptionName;
+                static const std::string maximalIterationsOptionName;
+                static const std::string maximalIterationsOptionShortName;
+                static const std::string precisionOptionName;
+                static const std::string absoluteOptionName;
+            };
+            
+        }
+    }
+}

src/storm/solver/AbstractGameSolver.cpp

@@ -1,90 +0,0 @@
-#include "storm/solver/AbstractGameSolver.h"
-
-#include "storm/settings/SettingsManager.h"
-#include "storm/settings/modules/NativeEquationSolverSettings.h"
-#include "storm/adapters/CarlAdapter.h"
-
-#include "storm/exceptions/InvalidSettingsException.h"
-
-namespace storm {
-    namespace solver {
-        template <typename ValueType>
-        AbstractGameSolver<ValueType>::AbstractGameSolver() {
-            // Get the settings object to customize solving.
-            storm::settings::modules::NativeEquationSolverSettings const& settings = storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>();
-
-            // Get appropriate settings.
-            maximalNumberOfIterations = settings.getMaximalIterationCount();
-            precision = storm::utility::convertNumber<ValueType>(settings.getPrecision());
-            relative = settings.getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative;
-        }
-
-        template <typename ValueType>
-        AbstractGameSolver<ValueType>::AbstractGameSolver(ValueType precision, uint_fast64_t maximalNumberOfIterations, bool relative) : precision(precision), maximalNumberOfIterations(maximalNumberOfIterations), relative(relative) {
-            // Intentionally left empty.
-        }
-        
-        template <typename ValueType>
-        void AbstractGameSolver<ValueType>::setTrackScheduler(bool trackScheduler){
-            this->trackScheduler = trackScheduler;
-        }
-        
-        template<typename ValueType>
-        bool AbstractGameSolver<ValueType>::hasScheduler() const {
-            return (static_cast<bool>(player1Scheduler) && static_cast<bool>(player2Scheduler));
-        }
-        
-        template<typename ValueType>
-        bool AbstractGameSolver<ValueType>::isTrackSchedulerSet() const {
-            return this->trackScheduler;
-        }
-        
-        template<typename ValueType>
-        storm::storage::TotalScheduler const& AbstractGameSolver<ValueType>::getPlayer1Scheduler() const {
-            STORM_LOG_THROW(player1Scheduler, storm::exceptions::InvalidSettingsException, "Cannot retrieve scheduler, because none was generated.");
-            return *player1Scheduler.get();
-        }
-        
-        template<typename ValueType>
-        storm::storage::TotalScheduler const& AbstractGameSolver<ValueType>::getPlayer2Scheduler() const {
-            STORM_LOG_THROW(player2Scheduler, storm::exceptions::InvalidSettingsException, "Cannot retrieve scheduler, because none was generated.");
-            return *player2Scheduler.get();
-        }
-
-        
-        template <typename ValueType>
-        ValueType AbstractGameSolver<ValueType>::getPrecision() const {
-            return precision;
-        }
-        
-        template <typename ValueType>
-        bool AbstractGameSolver<ValueType>::getRelative() const {
-            return relative;
-        }
-    
-        template <typename ValueType>
-        void AbstractGameSolver<ValueType>::setSchedulerHint(storm::storage::TotalScheduler&& player1Scheduler, storm::storage::TotalScheduler&& player2Scheduler) {
-            player1SchedulerHint = player1Scheduler;
-            player2SchedulerHint = player2Scheduler;
-        }
-    
-        template <typename ValueType>
-        bool AbstractGameSolver<ValueType>::hasSchedulerHints() const {
-            return player1SchedulerHint.is_initialized() && player2SchedulerHint.is_initialized();
-        }
-    
-        template <typename ValueType>
-        void AbstractGameSolver<ValueType>::setLowerBound(ValueType const& value) {
-            this->lowerBound = value;
-        }
-    
-        template <typename ValueType>
-        void AbstractGameSolver<ValueType>::setUpperBound(ValueType const& value) {
-            this->upperBound = value;
-        }
-    
-        template class AbstractGameSolver<double>;
-        template class AbstractGameSolver<storm::RationalNumber>;
-        
-    }
-}

src/storm/solver/AbstractGameSolver.h

@@ -1,85 +0,0 @@
-#ifndef STORM_SOLVER_ABSTRACTGAMESOLVER_H_
-#define STORM_SOLVER_ABSTRACTGAMESOLVER_H_
-
-#include <cstdint>
-#include <memory>
-
-#include <boost/optional.hpp>
-
-#include "storm/storage/sparse/StateType.h"
-#include "storm/utility/vector.h"
-#include "storm/solver/AbstractEquationSolver.h"
-#include "storm/storage/TotalScheduler.h"
-
-namespace storm {
-    namespace solver {
-        /*!
-         * The abstract base class for the game solvers.
-         */
-        template< typename ValueType>
-        class AbstractGameSolver : public AbstractEquationSolver<ValueType>{
-        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(ValueType precision, uint_fast64_t maximalNumberOfIterations, bool relative);
-            
-            /*!
-             * Sets schedulers that might be considered by the solver as an initial guess
-             */
-            void setSchedulerHint(storm::storage::TotalScheduler&& player1Scheduler, storm::storage::TotalScheduler&& player2Scheduler);
-            bool hasSchedulerHints() const;
-            
-            void setLowerBound(ValueType const& value);
-            void setUpperBound(ValueType const& value);
-            
-            void setTrackScheduler(bool trackScheduler = true);
-            bool isTrackSchedulerSet() const;
-            bool hasScheduler() const;
-            
-            storm::storage::TotalScheduler const& getPlayer1Scheduler() const;
-            storm::storage::TotalScheduler const& getPlayer2Scheduler() const;
-            
-            ValueType getPrecision() const;
-            bool getRelative() const;
-
-        protected:
-            // The precision to achieve.
-            ValueType 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;
-            
-            // Whether we generate a scheduler during solving.
-            bool trackScheduler;
-            
-            // The scheduler for the corresponding players (if it could be successfully generated).
-            mutable boost::optional<std::unique_ptr<storm::storage::TotalScheduler>> player1Scheduler;
-            mutable boost::optional<std::unique_ptr<storm::storage::TotalScheduler>> player2Scheduler;
-            
-            // schedulers that might be considered by the solver as an initial guess
-            boost::optional<storm::storage::TotalScheduler> player1SchedulerHint;
-            boost::optional<storm::storage::TotalScheduler> player2SchedulerHint;
-            
-            boost::optional<ValueType> lowerBound;
-            boost::optional<ValueType> upperBound;
-            
-            
-            
-        };
-    }
-}
-
-#endif /* STORM_SOLVER_ABSTRACTGAMESOLVER_H_ */

src/storm/solver/GameSolver.cpp

@@ -1,206 +1,122 @@
 #include "storm/solver/GameSolver.h"
 
 #include "storm/solver/LinearEquationSolver.h"
-#include "storm/utility/solver.h"
-#include "storm/storage/SparseMatrix.h"
-#include "storm/utility/vector.h"
-#include "storm/utility/graph.h"
+#include "storm/solver/StandardGameSolver.h"
 
-#include "storm/solver/GmmxxLinearEquationSolver.h"
-#include "storm/solver/EigenLinearEquationSolver.h"
-#include "storm/solver/NativeLinearEquationSolver.h"
-#include "storm/solver/EliminationLinearEquationSolver.h"
+#include "storm/utility/macros.h"
+#include "storm/exceptions/IllegalFunctionCallException.h"
 
-#include "storm/exceptions/NotImplementedException.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<ValueType>(), player1Matrix(player1Matrix), player2Matrix(player2Matrix) {
-            // Intentionally left empty.
+        void GameSolver<ValueType>::setTrackSchedulers(bool value) {
+            trackSchedulers = value;
+            if (!trackSchedulers) {
+                player1Scheduler = boost::none;
+                player2Scheduler = boost::none;
+            }
         }
         
         template<typename ValueType>
-        GameSolver<ValueType>::GameSolver(storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix, storm::storage::SparseMatrix<ValueType> const& player2Matrix, ValueType precision, uint_fast64_t maximalNumberOfIterations, bool relative) : AbstractGameSolver<ValueType>(precision, maximalNumberOfIterations, relative), player1Matrix(player1Matrix), player2Matrix(player2Matrix) {
-            // Intentionally left empty.
+        bool GameSolver<ValueType>::isTrackSchedulersSet() const {
+            return trackSchedulers;
         }
         
         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.
-            bool converged = false;
-            uint_fast64_t numberOfPlayer1States = x.size();
-            std::vector<ValueType> tmpResult(numberOfPlayer1States);
-            std::vector<ValueType> nondetResult(player2Matrix.getRowCount());
-            std::vector<ValueType> player2Result(player2Matrix.getRowGroupCount());
-            
-            // check if we have a scheduler hint to apply
-            if(this->hasSchedulerHints()) {
-                //Get the rows of the player2matrix that are selected by the schedulers
-                //Note that rows can be selected more then once and in an arbitrary order.
-                std::vector<storm::storage::sparse::state_type> selectedRows(numberOfPlayer1States);
-                for (uint_fast64_t pl1State = 0; pl1State < numberOfPlayer1States; ++pl1State){
-                    auto const& pl1Row = player1Matrix.getRow(pl1State, this->player1SchedulerHint->getChoice(pl1State));
-                    STORM_LOG_ASSERT(pl1Row.getNumberOfEntries()==1, "We assume that rows of player one have one entry.");
-                    uint_fast64_t pl2State = pl1Row.begin()->getColumn();
-                    selectedRows[pl1State] = player2Matrix.getRowGroupIndices()[pl2State] + this->player2SchedulerHint->getChoice(pl2State);
+        bool GameSolver<ValueType>::hasSchedulers() const {
+            return player1Scheduler.is_initialized() && player2Scheduler.is_initialized();
         }
-                //Get the matrix and the vector induced by this selection
-                auto inducedMatrix = player2Matrix.selectRowsFromRowIndexSequence(selectedRows, true);
-                inducedMatrix.convertToEquationSystem();
-                storm::utility::vector::selectVectorValues<ValueType>(tmpResult, selectedRows, b);
         
-                // Solve the resulting equation system.
-                auto submatrixSolver = storm::solver::GeneralLinearEquationSolverFactory<ValueType>().create(std::move(inducedMatrix));
-                submatrixSolver->setCachingEnabled(true);
-                if (this->lowerBound) { submatrixSolver->setLowerBound(this->lowerBound.get()); }
-                if (this->upperBound) { submatrixSolver->setUpperBound(this->upperBound.get()); }
-                // invoke the solver
-                submatrixSolver->solveEquations(x, tmpResult);
+        template<typename ValueType>
+        storm::storage::TotalScheduler const& GameSolver<ValueType>::getPlayer1Scheduler() const {
+            STORM_LOG_THROW(player1Scheduler, storm::exceptions::IllegalFunctionCallException, "Cannot retrieve player 1 scheduler, because none was generated.");
+            return *player1Scheduler.get();
         }
         
-            // 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());
+        template<typename ValueType>
+        storm::storage::TotalScheduler const& GameSolver<ValueType>::getPlayer2Scheduler() const {
+            STORM_LOG_THROW(player2Scheduler, storm::exceptions::IllegalFunctionCallException, "Cannot retrieve player 2 scheduler, because none was generated.");
+            return *player2Scheduler.get();
         }
         
-                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>();
-                    }
+        template<typename ValueType>
+        std::unique_ptr<storm::storage::TotalScheduler> GameSolver<ValueType>::getPlayer1Scheduler() {
+            STORM_LOG_THROW(player1Scheduler, storm::exceptions::IllegalFunctionCallException, "Cannot retrieve player 1 scheduler, because none was generated.");
+            return std::move(player1Scheduler.get());
         }
         
-                // Check if the process converged and set up the new iteration in case we are not done.
-                converged = storm::utility::vector::equalModuloPrecision(x, tmpResult, this->precision, this->relative);
-                converged = converged || (this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(x));
-                std::swap(x, tmpResult);
-
-                ++iterations;
-            } while (!converged && iterations < this->maximalNumberOfIterations);
-            
-            STORM_LOG_WARN_COND(converged, "Iterative solver for stochastic two player games did not converge after " << iterations << " iterations.");
-            
-            if(this->trackScheduler){
-                std::vector<uint_fast64_t> player2Choices(player2Matrix.getRowGroupCount());
-                storm::utility::vector::reduceVectorMinOrMax(player2Goal, nondetResult, player2Result, player2Matrix.getRowGroupIndices(), &player2Choices);
-                this->player2Scheduler = std::make_unique<storm::storage::TotalScheduler>(std::move(player2Choices));
-
-                std::vector<uint_fast64_t> player1Choices(numberOfPlayer1States, 0);
-                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;
-                        storm::storage::sparse::state_type localChoice = 1;
-                        // Now iterate through the different values and pick the extremal one.
-                        if (player1Goal == OptimizationDirection::Minimize) {
-                            for (; it != ite; ++it, ++localChoice) {
-                                if(player2Result[it->getColumn()] < tmpResult[pl1State]){
-                                    tmpResult[pl1State] = player2Result[it->getColumn()];
-                                    player1Choices[pl1State] = localChoice;
-                                }
-                            }
-                        } else {
-                            for (; it != ite; ++it, ++localChoice) {
-                                if(player2Result[it->getColumn()] > tmpResult[pl1State]){
-                                    tmpResult[pl1State] = player2Result[it->getColumn()];
-                                    player1Choices[pl1State] = localChoice;
-                                }
-                            }
+        template<typename ValueType>
+        std::unique_ptr<storm::storage::TotalScheduler> GameSolver<ValueType>::getPlayer2Scheduler() {
+            STORM_LOG_THROW(player2Scheduler, storm::exceptions::IllegalFunctionCallException, "Cannot retrieve player 2 scheduler, because none was generated.");
+            return std::move(player2Scheduler.get());
         }
-                    } else {
-                        STORM_LOG_ERROR("There is no choice for Player 1 at state " << pl1State << " in the stochastic two player game. This is not expected!");
+        
+        template<typename ValueType>
+        void GameSolver<ValueType>::setSchedulerHints(storm::storage::TotalScheduler&& player1Scheduler, storm::storage::TotalScheduler&& player2Scheduler) {
+            this->player1SchedulerHint = std::move(player1Scheduler);
+            this->player2SchedulerHint = std::move(player2Scheduler);
         }
+
+        template<typename ValueType>
+        bool GameSolver<ValueType>::hasSchedulerHints() const {
+            return player1SchedulerHint.is_initialized() && player2SchedulerHint.is_initialized();
         }
-                this->player1Scheduler = std::make_unique<storm::storage::TotalScheduler>(std::move(player1Choices));
+        
+        template<typename ValueType>
+        void GameSolver<ValueType>::setCachingEnabled(bool value) {
+            if(cachingEnabled && !value) {
+                // caching will be turned off. Hence we clear the cache at this point
+                clearCache();
             }
+            cachingEnabled = value;
         }
         
         template<typename ValueType>
-        void GameSolver<ValueType>::repeatedMultiply(OptimizationDirection player1Goal, OptimizationDirection player2Goal, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n) const {
-            // Set up the environment for iterations
-            uint_fast64_t numberOfPlayer1States = x.size();
-            std::vector<ValueType> tmpResult(numberOfPlayer1States);
-            std::vector<ValueType> nondetResult(player2Matrix.getRowCount());
-            std::vector<ValueType> player2Result(player2Matrix.getRowGroupCount());
-            
-            for (uint_fast64_t iteration = 0; iteration < n; ++iteration) {
-                player2Matrix.multiplyWithVector(x, nondetResult);
-                
-                if(b != nullptr) {
-                    storm::utility::vector::addVectors(*b, nondetResult, nondetResult);
+        bool GameSolver<ValueType>::isCachingEnabled() const {
+            return cachingEnabled;
         }
         
-                storm::utility::vector::reduceVectorMinOrMax(player2Goal, 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()]);
-                            }
+        template<typename ValueType>
+        void GameSolver<ValueType>::clearCache() const {
+            // Intentionally left empty.
         }
-                    } else {
-                        tmpResult[pl1State] = storm::utility::zero<ValueType>();
+        
+        template<typename ValueType>
+        void GameSolver<ValueType>::setLowerBound(ValueType const& value) {
+            lowerBound = value;
         }
+        
+        template<typename ValueType>
+        void GameSolver<ValueType>::setUpperBound(ValueType const& value) {
+            upperBound = value;
         }
-                std::swap(x, tmpResult);
+        
+        template<typename ValueType>
+        void GameSolver<ValueType>::setBounds(ValueType const& lower, ValueType const& upper) {
+            setLowerBound(lower);
+            setUpperBound(upper);
         }
+        
+        template<typename ValueType>
+        GameSolverFactory<ValueType>::GameSolverFactory() {
+            // Intentionally left empty.
         }
         
         template<typename ValueType>
-        storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& GameSolver<ValueType>::getPlayer1Matrix() const {
-            return player1Matrix;
+        std::unique_ptr<GameSolver<ValueType>> GameSolverFactory<ValueType>::create(storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix, storm::storage::SparseMatrix<ValueType> const& player2Matrix) const {
+            return std::make_unique<StandardGameSolver<ValueType>>(player1Matrix, player2Matrix, std::make_unique<GeneralLinearEquationSolverFactory<ValueType>>());
         }
                 
         template<typename ValueType>
-        storm::storage::SparseMatrix<ValueType> const& GameSolver<ValueType>::getPlayer2Matrix() const {
-            return player2Matrix;
+        std::unique_ptr<GameSolver<ValueType>> GameSolverFactory<ValueType>::create(storm::storage::SparseMatrix<storm::storage::sparse::state_type>&& player1Matrix, storm::storage::SparseMatrix<ValueType>&& player2Matrix) const {
+            return std::make_unique<StandardGameSolver<ValueType>>(std::move(player1Matrix), std::move(player2Matrix), std::make_unique<GeneralLinearEquationSolverFactory<ValueType>>());
         }
         
         template class GameSolver<double>;
         template class GameSolver<storm::RationalNumber>;
+        
+        template class GameSolverFactory<double>;
+        template class GameSolverFactory<storm::RationalNumber>;
     }
 }

src/storm/solver/GameSolver.h

@@ -1,78 +1,178 @@
-#ifndef STORM_SOLVER_GAMESOLVER_H_
-#define STORM_SOLVER_GAMESOLVER_H_
+#pragma once
 
 #include <vector>
+#include <memory>
+#include <boost/optional.hpp>
 
-#include "storm/solver/AbstractGameSolver.h"
-#include "storm/solver/TerminationCondition.h"
+#include "storm/solver/AbstractEquationSolver.h"
 #include "storm/solver/OptimizationDirection.h"
-
 #include "storm/storage/sparse/StateType.h"
+#include "storm/storage/TotalScheduler.h"
+#include "storm/utility/macros.h"
+
+#include "storm/exceptions/InvalidSettingsException.h"
 
 namespace storm {
     namespace storage {
-        template<typename ValueType>
-        class SparseMatrix;
+        template<typename T> class SparseMatrix;
     }
     
     namespace solver {
-        template<typename ValueType>
-        class GameSolver : public AbstractGameSolver<ValueType> {
-        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.
+        /*!
+         * A class representing the interface that all game solvers shall implement.
          */
-            GameSolver(storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix, storm::storage::SparseMatrix<ValueType> const& player2Matrix, ValueType precision, uint_fast64_t maximalNumberOfIterations, bool relative);
+        template<class ValueType>
+        class GameSolver : public AbstractEquationSolver<ValueType> {
+        public:
 
             /*!
              * Solves the equation system defined by the game matrices. Note that the game matrices have 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 player1Dir Sets whether player 1 wants to minimize or maximize.
+             * @param player2Dir Sets whether player 2 wants to minimize or maximize.
              * @param x The initial guess of the solution. For correctness, the guess has to be less (or equal) to the final solution (unless both players minimize)
              * @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;
+            virtual bool solveGame(OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const = 0;
             
             /*!
-             * Performs n multiplications of the form
-             *  reduce(player1Matrix * reduce(player2Matrix * x + b))
+             * Performs (repeated) matrix-vector multiplication with the given parameters, i.e. computes
+             * x[i+1] = min/max(player1Matrix*(min/max(player2Matrix*x[i] + b))) until x[n], where x[0] = x. After each multiplication and addition, the
+             * minimal/maximal value out of each row group is selected to reduce the resulting vector to obtain the
+             * vector for the next iteration. Note that the player1Matrix and the player2Matrix 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. For correctness, the guess has to be less (or equal) to the final solution (unless both players minimize)
-             * @param b The vector to add after matrix-vector multiplication.
-             * @param n The number of times we perform the multiplication
+             * @param player1Dir Sets whether player 1 wants to minimize or maximize.
+             * @param player2Dir Sets whether player 2 wants to minimize or maximize.
+             * @param x The initial vector that is to be multiplied with the matrix. This is also the output parameter,
+             * i.e. after the method returns, this vector will contain the computed values.
+             * @param b If not null, this vector is added after each multiplication.
+             * @param n Specifies the number of iterations the matrix-vector multiplication is performed.
              */
-            virtual void repeatedMultiply(OptimizationDirection player1Goal, OptimizationDirection player2Goal, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n) const;
+            virtual void repeatedMultiply(OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n = 1) const = 0;
             
-            storm::storage::SparseMatrix<ValueType> const& getPlayer2Matrix() const;
-            storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& getPlayer1Matrix() const;
+            /*!
+             * Sets whether schedulers are generated when solving equation systems. If the argument is false, the currently
+             * stored schedulers (if any) are deleted.
+             */
+            void setTrackSchedulers(bool value = true);
+
+            /*!
+             * Retrieves whether this solver is set to generate schedulers.
+             */
+            bool isTrackSchedulersSet() const;
+
+            /*!
+             * Retrieves whether the solver generated a scheduler.
+             */
+            bool hasSchedulers() const;
+
+            /*!
+             * Retrieves the generated schedulers. Note: it is only legal to call this function if schedulers were generated.
+             */
+            storm::storage::TotalScheduler const& getPlayer1Scheduler() const;
+            storm::storage::TotalScheduler const& getPlayer2Scheduler() const;
+
+            /*!
+             * Retrieves the generated schedulers and takes ownership of it. Note: it is only legal to call this functions
+             * if scheduler were generated and after calling this methods, the solver will not contain the corresponding scheduler
+             * any more (i.e. it is illegal to call this methods again until new schedulers have been generated).
+             */
+            std::unique_ptr<storm::storage::TotalScheduler> getPlayer1Scheduler();
+            std::unique_ptr<storm::storage::TotalScheduler> getPlayer2Scheduler();
+
+            /*!
+             * Sets scheduler hints that might be considered by the solver as an initial guess
+             */
+            void setSchedulerHints(storm::storage::TotalScheduler&& player1Scheduler, storm::storage::TotalScheduler&& player2Scheduler);
+            
+            /*!
+             * Returns whether Scheduler hints are available
+             */
+            bool hasSchedulerHints() const;
+            
+            /**
+             * Gets the precision after which the solver takes two numbers as equal.
+             *
+             * @see getRelative()
+             */
+            virtual ValueType getPrecision() const = 0;
+
+            /**
+             *  Gets whether the precision is taken to be absolute or relative
+             */
+            virtual bool getRelative() const = 0;
+            
+            /*!
+             * Sets whether some of the generated data during solver calls should be cached.
+             * This possibly decreases the runtime of subsequent calls but also increases memory consumption.
+             */
+            void setCachingEnabled(bool value);
+            
+            /*!
+             * Retrieves whether some of the generated data during solver calls should be cached.
+             */
+            bool isCachingEnabled() const;
+
+            /*
+             * Clears the currently cached data that has been stored during previous calls of the solver.
+             */
+            virtual void clearCache() const;
+
+            /*!
+             * Sets a lower bound for the solution that can potentially used by the solver.
+             */
+            void setLowerBound(ValueType const& value);
+            
+            /*!
+             * Sets an upper bound for the solution that can potentially used by the solver.
+             */
+            void setUpperBound(ValueType const& value);
+            
+            /*!
+             * Sets bounds for the solution that can potentially used by the solver.
+             */
+            void setBounds(ValueType const& lower, ValueType const& upper);
+
+        protected:
+            /// Whether we generate schedulers during solving.
+            bool trackSchedulers;
+
+            /// The schedulers (if they could be successfully generated).
+            mutable boost::optional<std::unique_ptr<storm::storage::TotalScheduler>> player1Scheduler;
+            mutable boost::optional<std::unique_ptr<storm::storage::TotalScheduler>> player2Scheduler;
+            
+            // A lower bound if one was set.
+            boost::optional<ValueType> lowerBound;
+            
+            // An upper bound if one was set.
+            boost::optional<ValueType> upperBound;
+            
+            // schedulers that might be considered by the solver as an initial guess
+            boost::optional<storm::storage::TotalScheduler> player1SchedulerHint;
+            boost::optional<storm::storage::TotalScheduler> player2SchedulerHint;
             
         private:
-            // The matrix defining the choices of player 1.
-            storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix;
+            /// Whether some of the generated data during solver calls should be cached.
+            bool cachingEnabled;
             
-            // The matrix defining the choices of player 2.
-            storm::storage::SparseMatrix<ValueType> const& player2Matrix;
         };
-    }
-}
 
-#endif /* STORM_SOLVER_GAMESOLVER_H_ */
+        template<typename ValueType>
+        class GameSolverFactory {
+        public:
+            GameSolverFactory();
+
+            virtual std::unique_ptr<GameSolver<ValueType>> create(storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix, storm::storage::SparseMatrix<ValueType> const& player2Matrix) const;
+            virtual std::unique_ptr<GameSolver<ValueType>> create(storm::storage::SparseMatrix<storm::storage::sparse::state_type>&& player1Matrix, storm::storage::SparseMatrix<ValueType>&& player2Matrix) const;
+
+        private:
+            bool trackScheduler;
+
+        };
+        
+    } // namespace solver
+} // namespace storm
+

src/storm/solver/StandardGameSolver.cpp

@@ -0,0 +1,607 @@
+#include "storm/solver/StandardGameSolver.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/GameSolverSettings.h"
+
+#include "storm/solver/GmmxxLinearEquationSolver.h"
+#include "storm/solver/EigenLinearEquationSolver.h"
+#include "storm/solver/NativeLinearEquationSolver.h"
+#include "storm/solver/EliminationLinearEquationSolver.h"
+
+#include "storm/utility/vector.h"
+#include "storm/utility/macros.h"
+#include "storm/exceptions/InvalidSettingsException.h"
+#include "storm/exceptions/InvalidStateException.h"
+#include "storm/exceptions/NotImplementedException.h"
+namespace storm {
+    namespace solver {
+        
+        template<typename ValueType>
+        StandardGameSolverSettings<ValueType>::StandardGameSolverSettings() {
+            // Get the settings object to customize game solving.
+            storm::settings::modules::GameSolverSettings const& settings = storm::settings::getModule<storm::settings::modules::GameSolverSettings>();
+            
+            maximalNumberOfIterations = settings.getMaximalIterationCount();
+            precision = storm::utility::convertNumber<ValueType>(settings.getPrecision());
+            relative = settings.getConvergenceCriterion() == storm::settings::modules::GameSolverSettings::ConvergenceCriterion::Relative;
+            
+            auto method = settings.getGameSolvingMethod();
+            switch (method) {
+                case GameMethod::ValueIteration: this->solutionMethod = SolutionMethod::ValueIteration; break;
+                case GameMethod::PolicyIteration: this->solutionMethod = SolutionMethod::PolicyIteration; break;
+                default:
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique.");
+            }
+        }
+        
+        template<typename ValueType>
+        void StandardGameSolverSettings<ValueType>::setSolutionMethod(SolutionMethod const& solutionMethod) {
+            this->solutionMethod = solutionMethod;
+        }
+        
+        template<typename ValueType>
+        void StandardGameSolverSettings<ValueType>::setMaximalNumberOfIterations(uint64_t maximalNumberOfIterations) {
+            this->maximalNumberOfIterations = maximalNumberOfIterations;
+        }
+        
+        template<typename ValueType>
+        void StandardGameSolverSettings<ValueType>::setRelativeTerminationCriterion(bool value) {
+            this->relative = value;
+        }
+        
+        template<typename ValueType>
+        void StandardGameSolverSettings<ValueType>::setPrecision(ValueType precision) {
+            this->precision = precision;
+        }
+        
+        template<typename ValueType>
+        typename StandardGameSolverSettings<ValueType>::SolutionMethod const& StandardGameSolverSettings<ValueType>::getSolutionMethod() const {
+            return solutionMethod;
+        }
+        
+        template<typename ValueType>
+        uint64_t StandardGameSolverSettings<ValueType>::getMaximalNumberOfIterations() const {
+            return maximalNumberOfIterations;
+        }
+        
+        template<typename ValueType>
+        ValueType StandardGameSolverSettings<ValueType>::getPrecision() const {
+            return precision;
+        }
+        
+        template<typename ValueType>
+        bool StandardGameSolverSettings<ValueType>::getRelativeTerminationCriterion() const {
+            return relative;
+        }
+        
+        template<typename ValueType>
+        StandardGameSolver<ValueType>::StandardGameSolver(storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix, storm::storage::SparseMatrix<ValueType> const& player2Matrix, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, StandardGameSolverSettings<ValueType> const& settings) : settings(settings), linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localP1Matrix(nullptr), localP2Matrix(nullptr), player1Matrix(player1Matrix), player2Matrix(player2Matrix) {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType>
+        StandardGameSolver<ValueType>::StandardGameSolver(storm::storage::SparseMatrix<storm::storage::sparse::state_type>&& player1Matrix, storm::storage::SparseMatrix<ValueType>&& player2Matrix, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, StandardGameSolverSettings<ValueType> const& settings) : settings(settings), linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localP1Matrix(std::make_unique<storm::storage::SparseMatrix<storm::storage::sparse::state_type>>(std::move(player1Matrix))), localP2Matrix(std::make_unique<storm::storage::SparseMatrix<ValueType>>(std::move(player2Matrix))), player1Matrix(*localP1Matrix), player2Matrix(*localP2Matrix) {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType>
+        bool StandardGameSolver<ValueType>::solveGame(OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
+            switch (this->getSettings().getSolutionMethod()) {
+                case StandardGameSolverSettings<ValueType>::SolutionMethod::ValueIteration:
+                    return solveGameValueIteration(player1Dir, player2Dir, x, b);
+                case StandardGameSolverSettings<ValueType>::SolutionMethod::PolicyIteration:
+                    return solveGamePolicyIteration(player1Dir, player2Dir, x, b);
+            }
+            return true;
+        }
+        
+        template<typename ValueType>
+        bool StandardGameSolver<ValueType>::solveGamePolicyIteration(OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
+            
+
+            
+            
+            
+           /* // Create the initial scheduler.
+            std::vector<storm::storage::sparse::state_type> scheduler = this->schedulerHint ? this->schedulerHint->getChoices() : std::vector<storm::storage::sparse::state_type>(this->A.getRowGroupCount());
+            
+            // Get a vector for storing the right-hand side of the inner equation system.
+            if(!auxiliaryRowGroupVector) {
+                auxiliaryRowGroupVector = std::make_unique<std::vector<ValueType>>(this->A.getRowGroupCount());
+            }
+            std::vector<ValueType>& subB = *auxiliaryRowGroupVector;
+
+            // Resolve the nondeterminism according to the current scheduler.
+            storm::storage::SparseMatrix<ValueType> submatrix = this->A.selectRowsFromRowGroups(scheduler, true);
+            submatrix.convertToEquationSystem();
+            storm::utility::vector::selectVectorValues<ValueType>(subB, scheduler, this->A.getRowGroupIndices(), b);
+
+            // Create a solver that we will use throughout the procedure. We will modify the matrix in each iteration.
+            auto solver = linearEquationSolverFactory->create(std::move(submatrix));
+            if (this->lowerBound) {
+                solver->setLowerBound(this->lowerBound.get());
+            }
+            if (this->upperBound) {
+                solver->setUpperBound(this->upperBound.get());
+            }
+            solver->setCachingEnabled(true);
+            
+            Status status = Status::InProgress;
+            uint64_t iterations = 0;
+            do {
+                // Solve the equation system for the 'DTMC'.
+                // FIXME: we need to remove the 0- and 1- states to make the solution unique.
+                // HOWEVER: if we start with a valid scheduler, then we will never get an illegal one, because staying
+                // within illegal MECs will never strictly improve the value. Is this true?
+                solver->solveEquations(x, subB);
+                
+                // Go through the multiplication result and see whether we can improve any of the choices.
+                bool schedulerImproved = false;
+                for (uint_fast64_t group = 0; group < this->A.getRowGroupCount(); ++group) {
+                    for (uint_fast64_t choice = this->A.getRowGroupIndices()[group]; choice < this->A.getRowGroupIndices()[group + 1]; ++choice) {
+                        // If the choice is the currently selected one, we can skip it.
+                        if (choice - this->A.getRowGroupIndices()[group] == scheduler[group]) {
+                            continue;
+                        }
+                        
+                        // Create the value of the choice.
+                        ValueType choiceValue = storm::utility::zero<ValueType>();
+                        for (auto const& entry : this->A.getRow(choice)) {
+                            choiceValue += entry.getValue() * x[entry.getColumn()];
+                        }
+                        choiceValue += b[choice];
+                        
+                        // If the value is strictly better than the solution of the inner system, we need to improve the scheduler.
+                        // TODO: If the underlying solver is not precise, this might run forever (i.e. when a state has two choices where the (exact) values are equal).
+                        // only changing the scheduler if the values are not equal (modulo precision) would make this unsound.
+                        if (valueImproved(dir, x[group], choiceValue)) {
+                            schedulerImproved = true;
+                            scheduler[group] = choice - this->A.getRowGroupIndices()[group];
+                        }
+                    }
+                }
+                
+                // If the scheduler did not improve, we are done.
+                if (!schedulerImproved) {
+                    status = Status::Converged;
+                } else {
+                    // Update the scheduler and the solver.
+                    submatrix = this->A.selectRowsFromRowGroups(scheduler, true);
+                    submatrix.convertToEquationSystem();
+                    storm::utility::vector::selectVectorValues<ValueType>(subB, scheduler, this->A.getRowGroupIndices(), b);
+                    solver->setMatrix(std::move(submatrix));
+                }
+                
+                // Update environment variables.
+                ++iterations;
+                status = updateStatusIfNotConverged(status, x, iterations);
+            } while (status == Status::InProgress);
+            
+            reportStatus(status, iterations);
+            
+            // If requested, we store the scheduler for retrieval.
+            if (this->isTrackSchedulerSet()) {
+                this->scheduler = std::make_unique<storm::storage::TotalScheduler>(std::move(scheduler));
+            }
+            
+            if(!this->isCachingEnabled()) {
+                clearCache();
+            }
+            
+            if(status == Status::Converged || status == Status::TerminatedEarly) {
+                return true;
+            } else{
+                return false;
+            }*/
+        }
+        
+        template<typename ValueType>
+        bool StandardGameSolver<ValueType>::valueImproved(OptimizationDirection dir, ValueType const& value1, ValueType const& value2) const {
+            if (dir == OptimizationDirection::Minimize) {
+                return value1 > value2;
+            } else {
+                return value1 < value2;
+            }
+        }
+
+        template<typename ValueType>
+        ValueType StandardGameSolver<ValueType>::getPrecision() const {
+            return this->getSettings().getPrecision();
+        }
+
+        template<typename ValueType>
+        bool StandardGameSolver<ValueType>::getRelative() const {
+            return this->getSettings().getRelativeTerminationCriterion();
+        }
+
+        template<typename ValueType>
+        bool StandardGameSolver<ValueType>::solveGameValueIteration(OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
+                         
+            if(!linEqSolverPlayer2Matrix) {
+                linEqSolverPlayer2Matrix = linearEquationSolverFactory->create(player2Matrix);
+                linEqSolverPlayer2Matrix->setCachingEnabled(true);
+            }
+            
+            if (!auxiliaryP2RowVector.get()) {
+                auxiliaryP2RowVector = std::make_unique<std::vector<ValueType>>(player2Matrix.getRowCount());
+            }
+               
+            if (!auxiliaryP2RowGroupVector.get()) {
+                auxiliaryP2RowGroupVector = std::make_unique<std::vector<ValueType>>(player2Matrix.getRowGroupCount());
+            }
+             
+            if (!auxiliaryP1RowGroupVector.get()) {
+                auxiliaryP1RowGroupVector = std::make_unique<std::vector<ValueType>>(player1Matrix.getRowGroupCount());
+            }
+             
+            std::vector<ValueType>& multiplyResult = *auxiliaryP2RowVector;
+            std::vector<ValueType>& reducedMultiplyResult = *auxiliaryP2RowGroupVector;
+             
+             
+            // if this->schedulerHint ...
+             
+             
+            std::vector<ValueType>* newX = auxiliaryP1RowGroupVector.get();
+            std::vector<ValueType>* currentX = &x;
+             
+            // Proceed with the iterations as long as the method did not converge or reach the maximum number of iterations.
+            uint64_t iterations = 0;
+            
+            Status status = Status::InProgress;
+            while (status == Status::InProgress) {
+                multiplyAndReduce(player1Dir, player2Dir, *currentX, &b, *linEqSolverPlayer2Matrix, multiplyResult, reducedMultiplyResult, *newX);
+
+                // Determine whether the method converged.
+                if (storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *newX, this->getSettings().getPrecision(), this->getSettings().getRelativeTerminationCriterion())) {
+                    status = Status::Converged;
+                }
+                
+                // Update environment variables.
+                std::swap(currentX, newX);
+                ++iterations;
+                status = updateStatusIfNotConverged(status, *currentX, iterations);
+            }
+                        
+            reportStatus(status, iterations);
+            
+            // If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result
+            // is currently stored in currentX, but x is the output vector.
+            if (currentX == auxiliaryP1RowGroupVector.get()) {
+                std::swap(x, *currentX);
+            }
+            
+            // If requested, we store the scheduler for retrieval.
+            if (this->isTrackSchedulersSet()) {
+                std::vector<uint_fast64_t> player1Choices(player1Matrix.getRowGroupCount(), 0);
+                std::vector<uint_fast64_t> player2Choices(player2Matrix.getRowGroupCount(), 0);
+                multiplyAndReduce(player1Dir, player2Dir, x, &b, *linEqSolverPlayer2Matrix, multiplyResult, reducedMultiplyResult, *auxiliaryP1RowGroupVector, &player1Choices, &player2Choices);
+                this->player1Scheduler = std::make_unique<storm::storage::TotalScheduler>(std::move(player1Choices));
+                this->player2Scheduler = std::make_unique<storm::storage::TotalScheduler>(std::move(player2Choices));
+ 
+            }
+            
+            if(!this->isCachingEnabled()) {
+                clearCache();
+            }
+            
+            if(status == Status::Converged || status == Status::TerminatedEarly) {
+                return true;
+            } else{
+                return false;
+            }
+             
+             
+             
+             
+                         /*      // Set up the environment for value iteration.
+            bool converged = false;
+            uint_fast64_t numberOfPlayer1States = x.size();
+            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, this->precision, this->relative);
+                std::swap(x, tmpResult);
+
+                ++iterations;
+            } while (!converged && iterations < this->maximalNumberOfIterations && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(x)));
+            
+            STORM_LOG_WARN_COND(converged, "Iterative solver for stochastic two player games did not converge after " << iterations << " iterations.");
+            
+            if(this->trackScheduler){
+                std::vector<uint_fast64_t> player2Choices(player2Matrix.getRowGroupCount());
+                storm::utility::vector::reduceVectorMinOrMax(player2Goal, nondetResult, player2Result, player2Matrix.getRowGroupIndices(), &player2Choices);
+                this->player2Scheduler = std::make_unique<storm::storage::TotalScheduler>(std::move(player2Choices));
+
+                std::vector<uint_fast64_t> player1Choices(numberOfPlayer1States, 0);
+                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;
+                        storm::storage::sparse::state_type localChoice = 1;
+                        // Now iterate through the different values and pick the extremal one.
+                        if (player1Goal == OptimizationDirection::Minimize) {
+                            for (; it != ite; ++it, ++localChoice) {
+                                if(player2Result[it->getColumn()] < tmpResult[pl1State]){
+                                    tmpResult[pl1State] = player2Result[it->getColumn()];
+                                    player1Choices[pl1State] = localChoice;
+                                }
+                            }
+                        } else {
+                            for (; it != ite; ++it, ++localChoice) {
+                                if(player2Result[it->getColumn()] > tmpResult[pl1State]){
+                                    tmpResult[pl1State] = player2Result[it->getColumn()];
+                                    player1Choices[pl1State] = localChoice;
+                                }
+                            }
+                        }
+                    } else {
+                        STORM_LOG_ERROR("There is no choice for Player 1 at state " << pl1State << " in the stochastic two player game. This is not expected!");
+                    }
+                }
+                this->player1Scheduler = std::make_unique<storm::storage::TotalScheduler>(std::move(player1Choices));
+            }
+            
+             
+             
+             * if(!linEqSolverA) {
+                linEqSolverA = linearEquationSolverFactory->create(A);
+                linEqSolverA->setCachingEnabled(true);
+            }
+            
+            if (!auxiliaryRowVector.get()) {
+                auxiliaryRowVector = std::make_unique<std::vector<ValueType>>(A.getRowCount());
+            }
+            std::vector<ValueType>& multiplyResult = *auxiliaryRowVector;
+            
+            if (!auxiliaryRowGroupVector.get()) {
+                auxiliaryRowGroupVector = std::make_unique<std::vector<ValueType>>(A.getRowGroupCount());
+            }
+            
+            if(this->schedulerHint) {
+                // Resolve the nondeterminism according to the scheduler hint
+                storm::storage::SparseMatrix<ValueType> submatrix = this->A.selectRowsFromRowGroups(this->schedulerHint->getChoices(), true);
+                submatrix.convertToEquationSystem();
+                storm::utility::vector::selectVectorValues<ValueType>(*auxiliaryRowGroupVector, this->schedulerHint->getChoices(), this->A.getRowGroupIndices(), b);
+
+                // Solve the resulting equation system.
+                // Note that the linEqSolver might consider a slightly different interpretation of "equalModuloPrecision". Hence, we iteratively increase its precision.
+                auto submatrixSolver = linearEquationSolverFactory->create(std::move(submatrix));
+                submatrixSolver->setCachingEnabled(true);
+                if (this->lowerBound) { submatrixSolver->setLowerBound(this->lowerBound.get()); }
+                if (this->upperBound) { submatrixSolver->setUpperBound(this->upperBound.get()); }
+                submatrixSolver->solveEquations(x, *auxiliaryRowGroupVector);
+            }
+            
+            std::vector<ValueType>* newX = auxiliaryRowGroupVector.get();
+            
+            std::vector<ValueType>* currentX = &x;
+            
+            // Proceed with the iterations as long as the method did not converge or reach the maximum number of iterations.
+            uint64_t iterations = 0;
+            
+            Status status = Status::InProgress;
+            while (status == Status::InProgress) {
+                // Compute x' = A*x + b.
+                linEqSolverA->multiply(*currentX, &b, multiplyResult);
+                
+                // Reduce the vector x' by applying min/max for all non-deterministic choices.
+                storm::utility::vector::reduceVectorMinOrMax(dir, multiplyResult, *newX, this->A.getRowGroupIndices());
+                
+                // Determine whether the method converged.
+                if (storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *newX, this->getSettings().getPrecision(), this->getSettings().getRelativeTerminationCriterion())) {
+                    status = Status::Converged;
+                }
+                
+                // Update environment variables.
+                std::swap(currentX, newX);
+                ++iterations;
+                status = updateStatusIfNotConverged(status, *currentX, iterations);
+            }
+            
+            reportStatus(status, iterations);
+            
+            // If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result
+            // is currently stored in currentX, but x is the output vector.
+            if (currentX == auxiliaryRowGroupVector.get()) {
+                std::swap(x, *currentX);
+            }
+            
+            // If requested, we store the scheduler for retrieval.
+            if (this->isTrackSchedulerSet()) {
+                // Due to a custom termination condition, it may be the case that no iterations are performed. In this
+                // case we need to compute x'= A*x+b once.
+                if (iterations==0) {
+                    linEqSolverA->multiply(x, &b, multiplyResult);
+                }
+                std::vector<storm::storage::sparse::state_type> choices(this->A.getRowGroupCount());
+                // Reduce the multiplyResult and keep track of the choices made
+                storm::utility::vector::reduceVectorMinOrMax(dir, multiplyResult, x, this->A.getRowGroupIndices(), &choices);
+                this->scheduler = std::make_unique<storm::storage::TotalScheduler>(std::move(choices));
+            }
+
+            if(!this->isCachingEnabled()) {
+                clearCache();
+            }
+            
+            if(status == Status::Converged || status == Status::TerminatedEarly) {
+                return true;
+            } else{
+                return false;
+            }
+             */
+        }
+        
+        template<typename ValueType>
+        void StandardGameSolver<ValueType>::repeatedMultiply(OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n) const {
+            
+            if(!linEqSolverPlayer2Matrix) {
+                linEqSolverPlayer2Matrix = linearEquationSolverFactory->create(player2Matrix);
+                linEqSolverPlayer2Matrix->setCachingEnabled(true);
+            }
+            
+            if (!auxiliaryP2RowVector.get()) {
+                auxiliaryP2RowVector = std::make_unique<std::vector<ValueType>>(player2Matrix.getRowCount());
+            }
+               
+            if (!auxiliaryP2RowGroupVector.get()) {
+                auxiliaryP2RowGroupVector = std::make_unique<std::vector<ValueType>>(player2Matrix.getRowGroupCount());
+            }
+            std::vector<ValueType>& multiplyResult = *auxiliaryP2RowVector;
+            std::vector<ValueType>& reducedMultiplyResult = *auxiliaryP2RowGroupVector;
+            
+            for (uint_fast64_t iteration = 0; iteration < n; ++iteration) {
+                multiplyAndReduce(player1Dir, player2Dir, x, b, *linEqSolverPlayer2Matrix, multiplyResult, reducedMultiplyResult, x);
+            }
+            
+            if(!this->isCachingEnabled()) {
+                clearCache();
+            }
+        }
+        
+        template<typename ValueType>
+        void StandardGameSolver<ValueType>::multiplyAndReduce(OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, storm::solver::LinearEquationSolver<ValueType>& linEqSolver, std::vector<ValueType>& multiplyResult, std::vector<ValueType>& p2ReducedMultiplyResult, std::vector<ValueType>& p1ReducedMultiplyResult, std::vector<uint_fast64_t>* player1Choices, std::vector<uint_fast64_t>* player2Choices) const {
+            
+            linEqSolver.multiply(x, b, multiplyResult);
+                
+            storm::utility::vector::reduceVectorMinOrMax(player2Dir, multiplyResult, p2ReducedMultiplyResult, player2Matrix.getRowGroupIndices(), player2Choices);
+
+            uint_fast64_t pl1State = 0;
+            std::vector<uint_fast64_t>::iterator choiceIt;
+            if (player1Choices) {
+                choiceIt = player1Choices->begin();
+            }
+            for (auto& result : p1ReducedMultiplyResult) {
+                storm::storage::SparseMatrix<storm::storage::sparse::state_type>::const_rows relevantRows = player1Matrix.getRowGroup(pl1State);
+                STORM_LOG_ASSERT(relevantRows.getNumberOfEntries() != 0, "There is a choice of player 1 that does not lead to any player 2 choice");
+                auto it = relevantRows.begin();
+                auto ite = relevantRows.end();
+
+                // Set the first value.
+                result = p2ReducedMultiplyResult[it->getColumn()];
+                if (player1Choices) {
+                    *choiceIt = 0;
+                }
+                uint_fast64_t localChoice = 1;
+                ++it;
+                
+                // Now iterate through the different values and pick the extremal one.
+                if (player1Dir == OptimizationDirection::Minimize) {
+                    for (; it != ite; ++it, ++localChoice) {
+                        ValueType& val = p2ReducedMultiplyResult[it->getColumn()];
+                        if (val < result) {
+                            result = val;
+                            if (player1Choices) {
+                                *choiceIt = localChoice;
+                            }
+                        }
+                    }
+                } else {
+                    for (; it != ite; ++it, ++localChoice) {
+                        ValueType& val = p2ReducedMultiplyResult[it->getColumn()];
+                        if (val > result) {
+                            result = val;
+                            if (player1Choices) {
+                                *choiceIt = localChoice;
+                            }
+                        }
+                    }
+                }
+                ++pl1State;
+                if (player1Choices) {
+                    ++choiceIt;
+                }
+            }
+        }
+
+        
+        template<typename ValueType>
+        typename StandardGameSolver<ValueType>::Status StandardGameSolver<ValueType>::updateStatusIfNotConverged(Status status, std::vector<ValueType> const& x, uint64_t iterations) const {
+            if (status != Status::Converged) {
+                if (this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(x)) {
+                    status = Status::TerminatedEarly;
+                } else if (iterations >= this->getSettings().getMaximalNumberOfIterations()) {
+                    status = Status::MaximalIterationsExceeded;
+                }
+            }
+            return status;
+        }
+        
+        template<typename ValueType>
+        void StandardGameSolver<ValueType>::reportStatus(Status status, uint64_t iterations) const {
+            switch (status) {
+                case Status::Converged: STORM_LOG_INFO("Iterative solver converged after " << iterations << " iterations."); break;
+                case Status::TerminatedEarly: STORM_LOG_INFO("Iterative solver terminated early after " << iterations << " iterations."); break;
+                case Status::MaximalIterationsExceeded: STORM_LOG_WARN("Iterative solver did not converge after " << iterations << " iterations."); break;
+                default:
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Iterative solver terminated unexpectedly.");
+            }
+        }
+        
+        template<typename ValueType>
+        StandardGameSolverSettings<ValueType> const& StandardGameSolver<ValueType>::getSettings() const {
+            return settings;
+        }
+        
+        template<typename ValueType>
+        void StandardGameSolver<ValueType>::setSettings(StandardGameSolverSettings<ValueType> const& newSettings) {
+            settings = newSettings;
+        }
+        
+        template<typename ValueType>
+        void StandardGameSolver<ValueType>::clearCache() const {
+            linEqSolverPlayer2Matrix.reset();
+            auxiliaryP2RowVector.reset();
+            auxiliaryP2RowGroupVector.reset();
+            auxiliaryP1RowGroupVector.reset();
+            GameSolver<ValueType>::clearCache();
+        }
+        
+        template class StandardGameSolverSettings<double>;
+        template class StandardGameSolver<double>;
+        template class StandardGameSolverSettings<storm::RationalNumber>;
+        template class StandardGameSolver<storm::RationalNumber>;
+    }
+}

src/storm/solver/StandardGameSolver.h

@@ -0,0 +1,93 @@
+#pragma once
+
+#include "storm/solver/LinearEquationSolver.h"
+#include "storm/solver/GameSolver.h"
+
+namespace storm {
+    namespace solver {
+        
+        template<typename ValueType>
+        class StandardGameSolverSettings {
+        public:
+            StandardGameSolverSettings();
+            
+            enum class SolutionMethod {
+                ValueIteration, PolicyIteration
+            };
+            
+            void setSolutionMethod(SolutionMethod const& solutionMethod);
+            void setMaximalNumberOfIterations(uint64_t maximalNumberOfIterations);
+            void setRelativeTerminationCriterion(bool value);
+            void setPrecision(ValueType precision);
+
+            SolutionMethod const& getSolutionMethod() const;
+            uint64_t getMaximalNumberOfIterations() const;
+            ValueType getPrecision() const;
+            bool getRelativeTerminationCriterion() const;
+
+        private:
+            SolutionMethod solutionMethod;
+            uint64_t maximalNumberOfIterations;
+            ValueType precision;
+            bool relative;
+        };
+       
+        template<typename ValueType>
+        class StandardGameSolver : public GameSolver<ValueType> {
+        public:
+            StandardGameSolver(storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix, storm::storage::SparseMatrix<ValueType> const& player2Matrix, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, StandardGameSolverSettings<ValueType> const& settings = StandardGameSolverSettings<ValueType>());
+            
+            StandardGameSolver(storm::storage::SparseMatrix<storm::storage::sparse::state_type>&& player1Matrix, storm::storage::SparseMatrix<ValueType>&& player2Matrix, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, StandardGameSolverSettings<ValueType> const& settings = StandardGameSolverSettings<ValueType>());
+            
+            virtual bool solveGame(OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const override;
+            virtual void repeatedMultiply(OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n = 1) const override;
+
+            StandardGameSolverSettings<ValueType> const& getSettings() const;
+            void setSettings(StandardGameSolverSettings<ValueType> const& newSettings);
+            
+            virtual void clearCache() const override;
+
+            virtual ValueType getPrecision() const override;
+            virtual bool getRelative() const override;
+            
+        private:
+            bool solveGamePolicyIteration(OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
+            bool solveGameValueIteration(OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
+
+            void multiplyAndReduce(OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const* b,
+                                   storm::solver::LinearEquationSolver<ValueType>& linEqSolver, std::vector<ValueType>& multiplyResult, std::vector<ValueType>& p2ReducedMultiplyResult, std::vector<ValueType>& p1ReducedMultiplyResult, std::vector<uint_fast64_t>* player1Choices = nullptr, std::vector<uint_fast64_t>* player2Choices = nullptr) const;
+            
+            bool valueImproved(OptimizationDirection dir, ValueType const& value1, ValueType const& value2) const;
+            
+            enum class Status {
+                Converged, TerminatedEarly, MaximalIterationsExceeded, InProgress
+            };
+            
+            // possibly cached data
+            mutable std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> linEqSolverPlayer2Matrix;
+            mutable std::unique_ptr<std::vector<ValueType>> auxiliaryP2RowVector; // player2Matrix.rowCount() entries
+            mutable std::unique_ptr<std::vector<ValueType>> auxiliaryP2RowGroupVector; // player2Matrix.rowGroupCount() entries
+            mutable std::unique_ptr<std::vector<ValueType>> auxiliaryP1RowGroupVector; // player1Matrix.rowGroupCount() entries
+
+            Status updateStatusIfNotConverged(Status status, std::vector<ValueType> const& x, uint64_t iterations) const;
+            void reportStatus(Status status, uint64_t iterations) const;
+            
+            /// The settings of this solver.
+            StandardGameSolverSettings<ValueType> settings;
+            
+            /// The factory used to obtain linear equation solvers.
+            std::unique_ptr<LinearEquationSolverFactory<ValueType>> linearEquationSolverFactory;
+            
+            // If the solver takes posession of the matrix, we store the moved matrix in this member, so it gets deleted
+            // when the solver is destructed.
+            std::unique_ptr<storm::storage::SparseMatrix<storm::storage::sparse::state_type>> localP1Matrix;
+            std::unique_ptr<storm::storage::SparseMatrix<ValueType>> localP2Matrix;
+            
+            // A reference to the original sparse matrix given to this solver. If the solver takes posession of the matrix
+            // the reference refers to localA.
+            storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix;
+            storm::storage::SparseMatrix<ValueType> const& player2Matrix;
+            
+        };
+    }
+}

src/storm/solver/SymbolicGameSolver.cpp

@@ -15,12 +15,16 @@ namespace storm {
     namespace solver {
         
         template<storm::dd::DdType Type, typename ValueType>
-        SymbolicGameSolver<Type, ValueType>::SymbolicGameSolver(storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, storm::dd::Bdd<Type> const& illegalPlayer1Mask, storm::dd::Bdd<Type> const& illegalPlayer2Mask, 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) : AbstractGameSolver<ValueType>(), A(A), allRows(allRows), illegalPlayer1Mask(illegalPlayer1Mask.ite(A.getDdManager().getConstant(storm::utility::infinity<ValueType>()), A.getDdManager().template getAddZero<ValueType>())), illegalPlayer2Mask(illegalPlayer2Mask.ite(A.getDdManager().getConstant(storm::utility::infinity<ValueType>()), A.getDdManager().template getAddZero<ValueType>())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables), generatePlayer1Strategy(false), generatePlayer2Strategy(false) {
-            // Intentionally left empty.
+        SymbolicGameSolver<Type, ValueType>::SymbolicGameSolver(storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, storm::dd::Bdd<Type> const& illegalPlayer1Mask, storm::dd::Bdd<Type> const& illegalPlayer2Mask, 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) : A(A), allRows(allRows), illegalPlayer1Mask(illegalPlayer1Mask.ite(A.getDdManager().getConstant(storm::utility::infinity<ValueType>()), A.getDdManager().template getAddZero<ValueType>())), illegalPlayer2Mask(illegalPlayer2Mask.ite(A.getDdManager().getConstant(storm::utility::infinity<ValueType>()), A.getDdManager().template getAddZero<ValueType>())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables), generatePlayer1Strategy(false), generatePlayer2Strategy(false) {
+            // Get the default settings
+            storm::settings::modules::NativeEquationSolverSettings const& settings = storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>();
+            maximalNumberOfIterations = settings.getMaximalIterationCount();
+            precision = storm::utility::convertNumber<ValueType>(settings.getPrecision());
+            relative = settings.getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative;
         }
         
         template<storm::dd::DdType Type, typename ValueType>
-        SymbolicGameSolver<Type, ValueType>::SymbolicGameSolver(storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, storm::dd::Bdd<Type> const& illegalPlayer1Mask, storm::dd::Bdd<Type> const& illegalPlayer2Mask, 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, ValueType precision, uint_fast64_t maximalNumberOfIterations, bool relative) : AbstractGameSolver<ValueType>(precision, maximalNumberOfIterations, relative), A(A), allRows(allRows), illegalPlayer1Mask(illegalPlayer1Mask.ite(A.getDdManager().getConstant(storm::utility::infinity<ValueType>()), A.getDdManager().template getAddZero<ValueType>())), illegalPlayer2Mask(illegalPlayer2Mask.ite(A.getDdManager().getConstant(storm::utility::infinity<ValueType>()), A.getDdManager().template getAddZero<ValueType>())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables), generatePlayer1Strategy(false), generatePlayer2Strategy(false) {
+        SymbolicGameSolver<Type, ValueType>::SymbolicGameSolver(storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, storm::dd::Bdd<Type> const& illegalPlayer1Mask, storm::dd::Bdd<Type> const& illegalPlayer2Mask, 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, ValueType precision, uint_fast64_t maximalNumberOfIterations, bool relative) : A(A), allRows(allRows), illegalPlayer1Mask(illegalPlayer1Mask.ite(A.getDdManager().getConstant(storm::utility::infinity<ValueType>()), A.getDdManager().template getAddZero<ValueType>())), illegalPlayer2Mask(illegalPlayer2Mask.ite(A.getDdManager().getConstant(storm::utility::infinity<ValueType>()), A.getDdManager().template getAddZero<ValueType>())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables), generatePlayer1Strategy(false), generatePlayer2Strategy(false), precision(precision), maximalNumberOfIterations(maximalNumberOfIterations), relative(relative) {
             // Intentionally left empty.
         }
         
@@ -113,7 +117,7 @@ namespace storm {
                 
                 ++iterations;
             } while (!converged && iterations < this->maximalNumberOfIterations);
-            STORM_LOG_TRACE("Numerically solving the game took " << iterations << " iterations.");
+            STORM_LOG_INFO("Numerically solving the game took " << iterations << " iterations.");
             
             return xCopy;
         }

src/storm/solver/SymbolicGameSolver.h

@@ -4,7 +4,6 @@
 #include <set>
 #include <vector>
 
-#include "storm/solver/AbstractGameSolver.h"
 #include "storm/solver/OptimizationDirection.h"
 
 #include "storm/storage/expressions/Variable.h"
@@ -18,7 +17,7 @@ namespace storm {
          * An interface that represents an abstract symbolic game solver.
          */
         template<storm::dd::DdType Type, typename ValueType = double>
-        class SymbolicGameSolver : public AbstractGameSolver<ValueType> {
+        class SymbolicGameSolver {
         public:
             /*!
              * Constructs a symbolic game solver with the given meta variable sets and pairs.
@@ -121,6 +120,14 @@ namespace storm {
             // A player 1 strategy if one was generated.
             boost::optional<storm::dd::Bdd<Type>> player2Strategy;
             
+            // The precision to achieve.
+            ValueType 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

src/storm/utility/solver.cpp

@@ -4,11 +4,8 @@
 
 #include "storm/solver/SymbolicNativeLinearEquationSolver.h"
 #include "storm/solver/SymbolicEliminationLinearEquationSolver.h"
-#include "storm/solver/SymbolicMinMaxLinearEquationSolver.h"
 #include "storm/solver/SymbolicGameSolver.h"
-#include "storm/solver/GameSolver.h"
 
-#include "storm/solver/TopologicalMinMaxLinearEquationSolver.h"
 
 #include "storm/solver/GurobiLpSolver.h"
 #include "storm/solver/Z3LpSolver.h"
@@ -30,11 +27,6 @@ namespace storm {
                 return std::unique_ptr<storm::solver::SymbolicGameSolver<Type, ValueType>>(new storm::solver::SymbolicGameSolver<Type, ValueType>(A, allRows, illegalPlayer1Mask, illegalPlayer2Mask, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables, player2Variables));
             }
             
-            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;
                 if(solvT == storm::solver::LpSolverTypeSelection::FROMSETTINGS) {
@@ -95,8 +87,6 @@ namespace storm {
             
             template class SymbolicGameSolverFactory<storm::dd::DdType::CUDD, double>;
             template class SymbolicGameSolverFactory<storm::dd::DdType::Sylvan, double>;
-            template class GameSolverFactory<double>;
-            template class GameSolverFactory<storm::RationalNumber>;
         }
     }
 }

src/storm/utility/solver.h

@@ -24,9 +24,6 @@ namespace storm {
         template<storm::dd::DdType T, typename V>
         class SymbolicMinMaxLinearEquationSolver;
         
-        template<typename V>
-        class GameSolver;
-        
         template<typename V>
         class LinearEquationSolver;
         
@@ -63,15 +60,6 @@ namespace storm {
                 virtual std::unique_ptr<storm::solver::SymbolicGameSolver<Type, ValueType>> create(storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, storm::dd::Bdd<Type> const& illegalPlayer1Mask, storm::dd::Bdd<Type> const& illegalPlayer2Mask, 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 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:
                 /*!