diff --git a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp index fddb32ae1..2808123b4 100644 --- a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp +++ b/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 - SparseMdpParameterLiftingModelChecker::SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel) : SparseParameterLiftingModelChecker(parametricModel), solverFactory(std::make_unique>()) { + SparseMdpParameterLiftingModelChecker::SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel) : SparseParameterLiftingModelChecker(parametricModel), solverFactory(std::make_unique>()) { } template - SparseMdpParameterLiftingModelChecker::SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr>&& solverFactory) : SparseParameterLiftingModelChecker(parametricModel), solverFactory(std::move(solverFactory)) { + SparseMdpParameterLiftingModelChecker::SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr>&& solverFactory) : SparseParameterLiftingModelChecker(parametricModel), solverFactory(std::move(solverFactory)) { } template @@ -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()); - 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()); } @@ -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()); } } diff --git a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h index ab96f4d13..0e2c4a3c4 100644 --- a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h +++ b/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 { public: SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel); - SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr>&& solverFactory); + SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr>&& solverFactory); virtual bool canHandle(CheckTask const& checkTask) const override; @@ -49,7 +49,7 @@ namespace storm { storm::storage::SparseMatrix player1Matrix; std::unique_ptr> parameterLifter; - std::unique_ptr> solverFactory; + std::unique_ptr> solverFactory; // Results from the most recent solver call. boost::optional minSched, maxSched; diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp index 307e68dc0..77c1e9150 100644 --- a/src/storm/settings/SettingsManager.cpp +++ b/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::addModule(); storm::settings::addModule(); + storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); diff --git a/src/storm/settings/modules/GameSolverSettings.cpp b/src/storm/settings/modules/GameSolverSettings.cpp new file mode 100644 index 000000000..11da56920 --- /dev/null +++ b/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 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; + } + + } + } +} diff --git a/src/storm/settings/modules/GameSolverSettings.h b/src/storm/settings/modules/GameSolverSettings.h new file mode 100644 index 000000000..9c17b4334 --- /dev/null +++ b/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; + }; + + } + } +} diff --git a/src/storm/solver/AbstractGameSolver.cpp b/src/storm/solver/AbstractGameSolver.cpp deleted file mode 100644 index 3b2079fe9..000000000 --- a/src/storm/solver/AbstractGameSolver.cpp +++ /dev/null @@ -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 - AbstractGameSolver::AbstractGameSolver() { - // Get the settings object to customize solving. - storm::settings::modules::NativeEquationSolverSettings const& settings = storm::settings::getModule(); - - // Get appropriate settings. - maximalNumberOfIterations = settings.getMaximalIterationCount(); - precision = storm::utility::convertNumber(settings.getPrecision()); - relative = settings.getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative; - } - - template - AbstractGameSolver::AbstractGameSolver(ValueType precision, uint_fast64_t maximalNumberOfIterations, bool relative) : precision(precision), maximalNumberOfIterations(maximalNumberOfIterations), relative(relative) { - // Intentionally left empty. - } - - template - void AbstractGameSolver::setTrackScheduler(bool trackScheduler){ - this->trackScheduler = trackScheduler; - } - - template - bool AbstractGameSolver::hasScheduler() const { - return (static_cast(player1Scheduler) && static_cast(player2Scheduler)); - } - - template - bool AbstractGameSolver::isTrackSchedulerSet() const { - return this->trackScheduler; - } - - template - storm::storage::TotalScheduler const& AbstractGameSolver::getPlayer1Scheduler() const { - STORM_LOG_THROW(player1Scheduler, storm::exceptions::InvalidSettingsException, "Cannot retrieve scheduler, because none was generated."); - return *player1Scheduler.get(); - } - - template - storm::storage::TotalScheduler const& AbstractGameSolver::getPlayer2Scheduler() const { - STORM_LOG_THROW(player2Scheduler, storm::exceptions::InvalidSettingsException, "Cannot retrieve scheduler, because none was generated."); - return *player2Scheduler.get(); - } - - - template - ValueType AbstractGameSolver::getPrecision() const { - return precision; - } - - template - bool AbstractGameSolver::getRelative() const { - return relative; - } - - template - void AbstractGameSolver::setSchedulerHint(storm::storage::TotalScheduler&& player1Scheduler, storm::storage::TotalScheduler&& player2Scheduler) { - player1SchedulerHint = player1Scheduler; - player2SchedulerHint = player2Scheduler; - } - - template - bool AbstractGameSolver::hasSchedulerHints() const { - return player1SchedulerHint.is_initialized() && player2SchedulerHint.is_initialized(); - } - - template - void AbstractGameSolver::setLowerBound(ValueType const& value) { - this->lowerBound = value; - } - - template - void AbstractGameSolver::setUpperBound(ValueType const& value) { - this->upperBound = value; - } - - template class AbstractGameSolver; - template class AbstractGameSolver; - - } -} diff --git a/src/storm/solver/AbstractGameSolver.h b/src/storm/solver/AbstractGameSolver.h deleted file mode 100644 index a7bcebd4f..000000000 --- a/src/storm/solver/AbstractGameSolver.h +++ /dev/null @@ -1,85 +0,0 @@ -#ifndef STORM_SOLVER_ABSTRACTGAMESOLVER_H_ -#define STORM_SOLVER_ABSTRACTGAMESOLVER_H_ - -#include -#include - -#include - -#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{ - 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> player1Scheduler; - mutable boost::optional> player2Scheduler; - - // schedulers that might be considered by the solver as an initial guess - boost::optional player1SchedulerHint; - boost::optional player2SchedulerHint; - - boost::optional lowerBound; - boost::optional upperBound; - - - - }; - } -} - -#endif /* STORM_SOLVER_ABSTRACTGAMESOLVER_H_ */ diff --git a/src/storm/solver/GameSolver.cpp b/src/storm/solver/GameSolver.cpp index 4b27fca14..f0c0e3417 100644 --- a/src/storm/solver/GameSolver.cpp +++ b/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 - GameSolver::GameSolver(storm::storage::SparseMatrix const& player1Matrix, storm::storage::SparseMatrix const& player2Matrix) : AbstractGameSolver(), player1Matrix(player1Matrix), player2Matrix(player2Matrix) { - // Intentionally left empty. + + template + void GameSolver::setTrackSchedulers(bool value) { + trackSchedulers = value; + if (!trackSchedulers) { + player1Scheduler = boost::none; + player2Scheduler = boost::none; + } } - - template - GameSolver::GameSolver(storm::storage::SparseMatrix const& player1Matrix, storm::storage::SparseMatrix const& player2Matrix, ValueType precision, uint_fast64_t maximalNumberOfIterations, bool relative) : AbstractGameSolver(precision, maximalNumberOfIterations, relative), player1Matrix(player1Matrix), player2Matrix(player2Matrix) { - // Intentionally left empty. + + template + bool GameSolver::isTrackSchedulersSet() const { + return trackSchedulers; } - - template - void GameSolver::solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, std::vector& x, std::vector const& b) const { - - // Set up the environment for value iteration. - bool converged = false; - uint_fast64_t numberOfPlayer1States = x.size(); - std::vector tmpResult(numberOfPlayer1States); - std::vector nondetResult(player2Matrix.getRowCount()); - std::vector 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 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); - } - //Get the matrix and the vector induced by this selection - auto inducedMatrix = player2Matrix.selectRowsFromRowIndexSequence(selectedRows, true); - inducedMatrix.convertToEquationSystem(); - storm::utility::vector::selectVectorValues(tmpResult, selectedRows, b); - - // Solve the resulting equation system. - auto submatrixSolver = storm::solver::GeneralLinearEquationSolverFactory().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); - } - - // 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::const_rows relevantRows = player1Matrix.getRowGroup(pl1State); - if (relevantRows.getNumberOfEntries() > 0) { - storm::storage::SparseMatrix::const_iterator it = relevantRows.begin(); - storm::storage::SparseMatrix::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(); - } - } - - // 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 player2Choices(player2Matrix.getRowGroupCount()); - storm::utility::vector::reduceVectorMinOrMax(player2Goal, nondetResult, player2Result, player2Matrix.getRowGroupIndices(), &player2Choices); - this->player2Scheduler = std::make_unique(std::move(player2Choices)); - - std::vector player1Choices(numberOfPlayer1States, 0); - for (uint_fast64_t pl1State = 0; pl1State < numberOfPlayer1States; ++pl1State) { - storm::storage::SparseMatrix::const_rows relevantRows = player1Matrix.getRowGroup(pl1State); - if (relevantRows.getNumberOfEntries() > 0) { - storm::storage::SparseMatrix::const_iterator it = relevantRows.begin(); - storm::storage::SparseMatrix::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(std::move(player1Choices)); - } + + template + bool GameSolver::hasSchedulers() const { + return player1Scheduler.is_initialized() && player2Scheduler.is_initialized(); + } + + template + storm::storage::TotalScheduler const& GameSolver::getPlayer1Scheduler() const { + STORM_LOG_THROW(player1Scheduler, storm::exceptions::IllegalFunctionCallException, "Cannot retrieve player 1 scheduler, because none was generated."); + return *player1Scheduler.get(); + } + + template + storm::storage::TotalScheduler const& GameSolver::getPlayer2Scheduler() const { + STORM_LOG_THROW(player2Scheduler, storm::exceptions::IllegalFunctionCallException, "Cannot retrieve player 2 scheduler, because none was generated."); + return *player2Scheduler.get(); + } + + template + std::unique_ptr GameSolver::getPlayer1Scheduler() { + STORM_LOG_THROW(player1Scheduler, storm::exceptions::IllegalFunctionCallException, "Cannot retrieve player 1 scheduler, because none was generated."); + return std::move(player1Scheduler.get()); + } + + template + std::unique_ptr GameSolver::getPlayer2Scheduler() { + STORM_LOG_THROW(player2Scheduler, storm::exceptions::IllegalFunctionCallException, "Cannot retrieve player 2 scheduler, because none was generated."); + return std::move(player2Scheduler.get()); + } + + template + void GameSolver::setSchedulerHints(storm::storage::TotalScheduler&& player1Scheduler, storm::storage::TotalScheduler&& player2Scheduler) { + this->player1SchedulerHint = std::move(player1Scheduler); + this->player2SchedulerHint = std::move(player2Scheduler); } - - template - void GameSolver::repeatedMultiply(OptimizationDirection player1Goal, OptimizationDirection player2Goal, std::vector& x, std::vector const* b, uint_fast64_t n) const { - // Set up the environment for iterations - uint_fast64_t numberOfPlayer1States = x.size(); - std::vector tmpResult(numberOfPlayer1States); - std::vector nondetResult(player2Matrix.getRowCount()); - std::vector 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); - } - - storm::utility::vector::reduceVectorMinOrMax(player2Goal, nondetResult, player2Result, player2Matrix.getRowGroupIndices()); - - for (uint_fast64_t pl1State = 0; pl1State < numberOfPlayer1States; ++pl1State) { - storm::storage::SparseMatrix::const_rows relevantRows = player1Matrix.getRowGroup(pl1State); - if (relevantRows.getNumberOfEntries() > 0) { - storm::storage::SparseMatrix::const_iterator it = relevantRows.begin(); - storm::storage::SparseMatrix::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(); - } - } - std::swap(x, tmpResult); + template + bool GameSolver::hasSchedulerHints() const { + return player1SchedulerHint.is_initialized() && player2SchedulerHint.is_initialized(); + } + + template + void GameSolver::setCachingEnabled(bool value) { + if(cachingEnabled && !value) { + // caching will be turned off. Hence we clear the cache at this point + clearCache(); } + cachingEnabled = value; + } + + template + bool GameSolver::isCachingEnabled() const { + return cachingEnabled; } - template - storm::storage::SparseMatrix const& GameSolver::getPlayer1Matrix() const { - return player1Matrix; + template + void GameSolver::clearCache() const { + // Intentionally left empty. } - template - storm::storage::SparseMatrix const& GameSolver::getPlayer2Matrix() const { - return player2Matrix; + template + void GameSolver::setLowerBound(ValueType const& value) { + lowerBound = value; } - + + template + void GameSolver::setUpperBound(ValueType const& value) { + upperBound = value; + } + + template + void GameSolver::setBounds(ValueType const& lower, ValueType const& upper) { + setLowerBound(lower); + setUpperBound(upper); + } + + template + GameSolverFactory::GameSolverFactory() { + // Intentionally left empty. + } + + template + std::unique_ptr> GameSolverFactory::create(storm::storage::SparseMatrix const& player1Matrix, storm::storage::SparseMatrix const& player2Matrix) const { + return std::make_unique>(player1Matrix, player2Matrix, std::make_unique>()); + } + + template + std::unique_ptr> GameSolverFactory::create(storm::storage::SparseMatrix&& player1Matrix, storm::storage::SparseMatrix&& player2Matrix) const { + return std::make_unique>(std::move(player1Matrix), std::move(player2Matrix), std::make_unique>()); + } + template class GameSolver; template class GameSolver; + + template class GameSolverFactory; + template class GameSolverFactory; } } diff --git a/src/storm/solver/GameSolver.h b/src/storm/solver/GameSolver.h index b21b19ca8..e4756c24f 100644 --- a/src/storm/solver/GameSolver.h +++ b/src/storm/solver/GameSolver.h @@ -1,78 +1,178 @@ -#ifndef STORM_SOLVER_GAMESOLVER_H_ -#define STORM_SOLVER_GAMESOLVER_H_ +#pragma once #include +#include +#include -#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 - class SparseMatrix; + template class SparseMatrix; } - + namespace solver { - template - class GameSolver : public AbstractGameSolver { + + /*! + * A class representing the interface that all game solvers shall implement. + */ + template + class GameSolver : public AbstractEquationSolver { public: - /* - * Constructs a game solver with the given player 1 and player 2 matrices. - * - * @param player1Matrix The matrix defining the choices of player 1. - * @param player2Matrix The matrix defining the choices of player 2. - */ - GameSolver(storm::storage::SparseMatrix const& player1Matrix, storm::storage::SparseMatrix const& player2Matrix); - - /* - * Constructs a game solver with the given player 1 and player 2 matrices and options. - * - * @param player1Matrix The matrix defining the choices of player 1. - * @param player2Matrix The matrix defining the choices of player 2. - * @param precision The precision that is used to detect convergence. - * @param maximalNumberOfIterations The maximal number of iterations. - * @param relative Sets whether or not to detect convergence with a relative or absolute criterion. - */ - GameSolver(storm::storage::SparseMatrix const& player1Matrix, storm::storage::SparseMatrix const& player2Matrix, ValueType precision, uint_fast64_t maximalNumberOfIterations, bool relative); /*! * 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& x, std::vector const& b) const; + virtual bool solveGame(OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector 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 player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const* b, uint_fast64_t n = 1) const = 0; + + /*! + * 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 getPlayer1Scheduler(); + std::unique_ptr 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 */ - virtual void repeatedMultiply(OptimizationDirection player1Goal, OptimizationDirection player2Goal, std::vector& x, std::vector const* b, uint_fast64_t n) const; + bool hasSchedulerHints() const; + + /** + * Gets the precision after which the solver takes two numbers as equal. + * + * @see getRelative() + */ + virtual ValueType getPrecision() const = 0; - storm::storage::SparseMatrix const& getPlayer2Matrix() const; - storm::storage::SparseMatrix const& getPlayer1Matrix() const; + /** + * Gets whether the precision is taken to be absolute or relative + */ + virtual bool getRelative() const = 0; - private: - // The matrix defining the choices of player 1. - storm::storage::SparseMatrix const& player1Matrix; + /*! + * 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; - // The matrix defining the choices of player 2. - storm::storage::SparseMatrix const& player2Matrix; + /* + * 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> player1Scheduler; + mutable boost::optional> player2Scheduler; + + // A lower bound if one was set. + boost::optional lowerBound; + + // An upper bound if one was set. + boost::optional upperBound; + + // schedulers that might be considered by the solver as an initial guess + boost::optional player1SchedulerHint; + boost::optional player2SchedulerHint; + + private: + /// Whether some of the generated data during solver calls should be cached. + bool cachingEnabled; + }; - } -} -#endif /* STORM_SOLVER_GAMESOLVER_H_ */ + template + class GameSolverFactory { + public: + GameSolverFactory(); + + virtual std::unique_ptr> create(storm::storage::SparseMatrix const& player1Matrix, storm::storage::SparseMatrix const& player2Matrix) const; + virtual std::unique_ptr> create(storm::storage::SparseMatrix&& player1Matrix, storm::storage::SparseMatrix&& player2Matrix) const; + + private: + bool trackScheduler; + + }; + + } // namespace solver +} // namespace storm + diff --git a/src/storm/solver/SolverSelectionOptions.h b/src/storm/solver/SolverSelectionOptions.h index b93014053..32af0a4eb 100644 --- a/src/storm/solver/SolverSelectionOptions.h +++ b/src/storm/solver/SolverSelectionOptions.h @@ -8,7 +8,7 @@ namespace storm { namespace solver { ExtendEnumsWithSelectionField(MinMaxMethod, PolicyIteration, ValueIteration, Topological) ExtendEnumsWithSelectionField(GameMethod, PolicyIteration, ValueIteration) - + ExtendEnumsWithSelectionField(LpSolverType, Gurobi, Glpk, Z3) ExtendEnumsWithSelectionField(EquationSolverType, Native, Gmmxx, Eigen, Elimination) ExtendEnumsWithSelectionField(SmtSolverType, Z3, Mathsat) diff --git a/src/storm/solver/StandardGameSolver.cpp b/src/storm/solver/StandardGameSolver.cpp new file mode 100644 index 000000000..45df1688e --- /dev/null +++ b/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 + StandardGameSolverSettings::StandardGameSolverSettings() { + // Get the settings object to customize game solving. + storm::settings::modules::GameSolverSettings const& settings = storm::settings::getModule(); + + maximalNumberOfIterations = settings.getMaximalIterationCount(); + precision = storm::utility::convertNumber(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 + void StandardGameSolverSettings::setSolutionMethod(SolutionMethod const& solutionMethod) { + this->solutionMethod = solutionMethod; + } + + template + void StandardGameSolverSettings::setMaximalNumberOfIterations(uint64_t maximalNumberOfIterations) { + this->maximalNumberOfIterations = maximalNumberOfIterations; + } + + template + void StandardGameSolverSettings::setRelativeTerminationCriterion(bool value) { + this->relative = value; + } + + template + void StandardGameSolverSettings::setPrecision(ValueType precision) { + this->precision = precision; + } + + template + typename StandardGameSolverSettings::SolutionMethod const& StandardGameSolverSettings::getSolutionMethod() const { + return solutionMethod; + } + + template + uint64_t StandardGameSolverSettings::getMaximalNumberOfIterations() const { + return maximalNumberOfIterations; + } + + template + ValueType StandardGameSolverSettings::getPrecision() const { + return precision; + } + + template + bool StandardGameSolverSettings::getRelativeTerminationCriterion() const { + return relative; + } + + template + StandardGameSolver::StandardGameSolver(storm::storage::SparseMatrix const& player1Matrix, storm::storage::SparseMatrix const& player2Matrix, std::unique_ptr>&& linearEquationSolverFactory, StandardGameSolverSettings const& settings) : settings(settings), linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localP1Matrix(nullptr), localP2Matrix(nullptr), player1Matrix(player1Matrix), player2Matrix(player2Matrix) { + // Intentionally left empty. + } + + template + StandardGameSolver::StandardGameSolver(storm::storage::SparseMatrix&& player1Matrix, storm::storage::SparseMatrix&& player2Matrix, std::unique_ptr>&& linearEquationSolverFactory, StandardGameSolverSettings const& settings) : settings(settings), linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localP1Matrix(std::make_unique>(std::move(player1Matrix))), localP2Matrix(std::make_unique>(std::move(player2Matrix))), player1Matrix(*localP1Matrix), player2Matrix(*localP2Matrix) { + // Intentionally left empty. + } + + template + bool StandardGameSolver::solveGame(OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const& b) const { + switch (this->getSettings().getSolutionMethod()) { + case StandardGameSolverSettings::SolutionMethod::ValueIteration: + return solveGameValueIteration(player1Dir, player2Dir, x, b); + case StandardGameSolverSettings::SolutionMethod::PolicyIteration: + return solveGamePolicyIteration(player1Dir, player2Dir, x, b); + } + return true; + } + + template + bool StandardGameSolver::solveGamePolicyIteration(OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const& b) const { + + + + + + /* // Create the initial scheduler. + std::vector scheduler = this->schedulerHint ? this->schedulerHint->getChoices() : std::vector(this->A.getRowGroupCount()); + + // Get a vector for storing the right-hand side of the inner equation system. + if(!auxiliaryRowGroupVector) { + auxiliaryRowGroupVector = std::make_unique>(this->A.getRowGroupCount()); + } + std::vector& subB = *auxiliaryRowGroupVector; + + // Resolve the nondeterminism according to the current scheduler. + storm::storage::SparseMatrix submatrix = this->A.selectRowsFromRowGroups(scheduler, true); + submatrix.convertToEquationSystem(); + storm::utility::vector::selectVectorValues(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(); + 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(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(std::move(scheduler)); + } + + if(!this->isCachingEnabled()) { + clearCache(); + } + + if(status == Status::Converged || status == Status::TerminatedEarly) { + return true; + } else{ + return false; + }*/ + } + + template + bool StandardGameSolver::valueImproved(OptimizationDirection dir, ValueType const& value1, ValueType const& value2) const { + if (dir == OptimizationDirection::Minimize) { + return value1 > value2; + } else { + return value1 < value2; + } + } + + template + ValueType StandardGameSolver::getPrecision() const { + return this->getSettings().getPrecision(); + } + + template + bool StandardGameSolver::getRelative() const { + return this->getSettings().getRelativeTerminationCriterion(); + } + + template + bool StandardGameSolver::solveGameValueIteration(OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const& b) const { + + if(!linEqSolverPlayer2Matrix) { + linEqSolverPlayer2Matrix = linearEquationSolverFactory->create(player2Matrix); + linEqSolverPlayer2Matrix->setCachingEnabled(true); + } + + if (!auxiliaryP2RowVector.get()) { + auxiliaryP2RowVector = std::make_unique>(player2Matrix.getRowCount()); + } + + if (!auxiliaryP2RowGroupVector.get()) { + auxiliaryP2RowGroupVector = std::make_unique>(player2Matrix.getRowGroupCount()); + } + + if (!auxiliaryP1RowGroupVector.get()) { + auxiliaryP1RowGroupVector = std::make_unique>(player1Matrix.getRowGroupCount()); + } + + std::vector& multiplyResult = *auxiliaryP2RowVector; + std::vector& reducedMultiplyResult = *auxiliaryP2RowGroupVector; + + + // if this->schedulerHint ... + + + std::vector* newX = auxiliaryP1RowGroupVector.get(); + std::vector* 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(*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 player1Choices(player1Matrix.getRowGroupCount(), 0); + std::vector player2Choices(player2Matrix.getRowGroupCount(), 0); + multiplyAndReduce(player1Dir, player2Dir, x, &b, *linEqSolverPlayer2Matrix, multiplyResult, reducedMultiplyResult, *auxiliaryP1RowGroupVector, &player1Choices, &player2Choices); + this->player1Scheduler = std::make_unique(std::move(player1Choices)); + this->player2Scheduler = std::make_unique(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 tmpResult(numberOfPlayer1States); + std::vector nondetResult(player2Matrix.getRowCount()); + std::vector 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::const_rows relevantRows = player1Matrix.getRowGroup(pl1State); + if (relevantRows.getNumberOfEntries() > 0) { + storm::storage::SparseMatrix::const_iterator it = relevantRows.begin(); + storm::storage::SparseMatrix::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(); + } + } + + // 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 player2Choices(player2Matrix.getRowGroupCount()); + storm::utility::vector::reduceVectorMinOrMax(player2Goal, nondetResult, player2Result, player2Matrix.getRowGroupIndices(), &player2Choices); + this->player2Scheduler = std::make_unique(std::move(player2Choices)); + + std::vector player1Choices(numberOfPlayer1States, 0); + for (uint_fast64_t pl1State = 0; pl1State < numberOfPlayer1States; ++pl1State) { + storm::storage::SparseMatrix::const_rows relevantRows = player1Matrix.getRowGroup(pl1State); + if (relevantRows.getNumberOfEntries() > 0) { + storm::storage::SparseMatrix::const_iterator it = relevantRows.begin(); + storm::storage::SparseMatrix::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(std::move(player1Choices)); + } + + + + * if(!linEqSolverA) { + linEqSolverA = linearEquationSolverFactory->create(A); + linEqSolverA->setCachingEnabled(true); + } + + if (!auxiliaryRowVector.get()) { + auxiliaryRowVector = std::make_unique>(A.getRowCount()); + } + std::vector& multiplyResult = *auxiliaryRowVector; + + if (!auxiliaryRowGroupVector.get()) { + auxiliaryRowGroupVector = std::make_unique>(A.getRowGroupCount()); + } + + if(this->schedulerHint) { + // Resolve the nondeterminism according to the scheduler hint + storm::storage::SparseMatrix submatrix = this->A.selectRowsFromRowGroups(this->schedulerHint->getChoices(), true); + submatrix.convertToEquationSystem(); + storm::utility::vector::selectVectorValues(*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* newX = auxiliaryRowGroupVector.get(); + + std::vector* 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(*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 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(std::move(choices)); + } + + if(!this->isCachingEnabled()) { + clearCache(); + } + + if(status == Status::Converged || status == Status::TerminatedEarly) { + return true; + } else{ + return false; + } + */ + } + + template + void StandardGameSolver::repeatedMultiply(OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const* b, uint_fast64_t n) const { + + if(!linEqSolverPlayer2Matrix) { + linEqSolverPlayer2Matrix = linearEquationSolverFactory->create(player2Matrix); + linEqSolverPlayer2Matrix->setCachingEnabled(true); + } + + if (!auxiliaryP2RowVector.get()) { + auxiliaryP2RowVector = std::make_unique>(player2Matrix.getRowCount()); + } + + if (!auxiliaryP2RowGroupVector.get()) { + auxiliaryP2RowGroupVector = std::make_unique>(player2Matrix.getRowGroupCount()); + } + std::vector& multiplyResult = *auxiliaryP2RowVector; + std::vector& 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 + void StandardGameSolver::multiplyAndReduce(OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const* b, storm::solver::LinearEquationSolver& linEqSolver, std::vector& multiplyResult, std::vector& p2ReducedMultiplyResult, std::vector& p1ReducedMultiplyResult, std::vector* player1Choices, std::vector* player2Choices) const { + + linEqSolver.multiply(x, b, multiplyResult); + + storm::utility::vector::reduceVectorMinOrMax(player2Dir, multiplyResult, p2ReducedMultiplyResult, player2Matrix.getRowGroupIndices(), player2Choices); + + uint_fast64_t pl1State = 0; + std::vector::iterator choiceIt; + if (player1Choices) { + choiceIt = player1Choices->begin(); + } + for (auto& result : p1ReducedMultiplyResult) { + storm::storage::SparseMatrix::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 StandardGameSolver::Status StandardGameSolver::updateStatusIfNotConverged(Status status, std::vector 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 + void StandardGameSolver::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 + StandardGameSolverSettings const& StandardGameSolver::getSettings() const { + return settings; + } + + template + void StandardGameSolver::setSettings(StandardGameSolverSettings const& newSettings) { + settings = newSettings; + } + + template + void StandardGameSolver::clearCache() const { + linEqSolverPlayer2Matrix.reset(); + auxiliaryP2RowVector.reset(); + auxiliaryP2RowGroupVector.reset(); + auxiliaryP1RowGroupVector.reset(); + GameSolver::clearCache(); + } + + template class StandardGameSolverSettings; + template class StandardGameSolver; + template class StandardGameSolverSettings; + template class StandardGameSolver; + } +} \ No newline at end of file diff --git a/src/storm/solver/StandardGameSolver.h b/src/storm/solver/StandardGameSolver.h new file mode 100644 index 000000000..f30a79fc8 --- /dev/null +++ b/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 + 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 + class StandardGameSolver : public GameSolver { + public: + StandardGameSolver(storm::storage::SparseMatrix const& player1Matrix, storm::storage::SparseMatrix const& player2Matrix, std::unique_ptr>&& linearEquationSolverFactory, StandardGameSolverSettings const& settings = StandardGameSolverSettings()); + + StandardGameSolver(storm::storage::SparseMatrix&& player1Matrix, storm::storage::SparseMatrix&& player2Matrix, std::unique_ptr>&& linearEquationSolverFactory, StandardGameSolverSettings const& settings = StandardGameSolverSettings()); + + virtual bool solveGame(OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const& b) const override; + virtual void repeatedMultiply(OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const* b, uint_fast64_t n = 1) const override; + + StandardGameSolverSettings const& getSettings() const; + void setSettings(StandardGameSolverSettings 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& x, std::vector const& b) const; + bool solveGameValueIteration(OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const& b) const; + + void multiplyAndReduce(OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const* b, + storm::solver::LinearEquationSolver& linEqSolver, std::vector& multiplyResult, std::vector& p2ReducedMultiplyResult, std::vector& p1ReducedMultiplyResult, std::vector* player1Choices = nullptr, std::vector* 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> linEqSolverPlayer2Matrix; + mutable std::unique_ptr> auxiliaryP2RowVector; // player2Matrix.rowCount() entries + mutable std::unique_ptr> auxiliaryP2RowGroupVector; // player2Matrix.rowGroupCount() entries + mutable std::unique_ptr> auxiliaryP1RowGroupVector; // player1Matrix.rowGroupCount() entries + + Status updateStatusIfNotConverged(Status status, std::vector const& x, uint64_t iterations) const; + void reportStatus(Status status, uint64_t iterations) const; + + /// The settings of this solver. + StandardGameSolverSettings settings; + + /// The factory used to obtain linear equation solvers. + std::unique_ptr> 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> localP1Matrix; + std::unique_ptr> 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 const& player1Matrix; + storm::storage::SparseMatrix const& player2Matrix; + + }; + } +} diff --git a/src/storm/solver/SymbolicGameSolver.cpp b/src/storm/solver/SymbolicGameSolver.cpp index bfbe008e7..9f9c54ac7 100644 --- a/src/storm/solver/SymbolicGameSolver.cpp +++ b/src/storm/solver/SymbolicGameSolver.cpp @@ -15,12 +15,16 @@ namespace storm { namespace solver { template - SymbolicGameSolver::SymbolicGameSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalPlayer1Mask, storm::dd::Bdd const& illegalPlayer2Mask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables) : AbstractGameSolver(), A(A), allRows(allRows), illegalPlayer1Mask(illegalPlayer1Mask.ite(A.getDdManager().getConstant(storm::utility::infinity()), A.getDdManager().template getAddZero())), illegalPlayer2Mask(illegalPlayer2Mask.ite(A.getDdManager().getConstant(storm::utility::infinity()), A.getDdManager().template getAddZero())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables), generatePlayer1Strategy(false), generatePlayer2Strategy(false) { - // Intentionally left empty. + SymbolicGameSolver::SymbolicGameSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalPlayer1Mask, storm::dd::Bdd const& illegalPlayer2Mask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables) : A(A), allRows(allRows), illegalPlayer1Mask(illegalPlayer1Mask.ite(A.getDdManager().getConstant(storm::utility::infinity()), A.getDdManager().template getAddZero())), illegalPlayer2Mask(illegalPlayer2Mask.ite(A.getDdManager().getConstant(storm::utility::infinity()), A.getDdManager().template getAddZero())), 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(); + maximalNumberOfIterations = settings.getMaximalIterationCount(); + precision = storm::utility::convertNumber(settings.getPrecision()); + relative = settings.getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative; } template - SymbolicGameSolver::SymbolicGameSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalPlayer1Mask, storm::dd::Bdd const& illegalPlayer2Mask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables, ValueType precision, uint_fast64_t maximalNumberOfIterations, bool relative) : AbstractGameSolver(precision, maximalNumberOfIterations, relative), A(A), allRows(allRows), illegalPlayer1Mask(illegalPlayer1Mask.ite(A.getDdManager().getConstant(storm::utility::infinity()), A.getDdManager().template getAddZero())), illegalPlayer2Mask(illegalPlayer2Mask.ite(A.getDdManager().getConstant(storm::utility::infinity()), A.getDdManager().template getAddZero())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables), generatePlayer1Strategy(false), generatePlayer2Strategy(false) { + SymbolicGameSolver::SymbolicGameSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalPlayer1Mask, storm::dd::Bdd const& illegalPlayer2Mask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables, ValueType precision, uint_fast64_t maximalNumberOfIterations, bool relative) : A(A), allRows(allRows), illegalPlayer1Mask(illegalPlayer1Mask.ite(A.getDdManager().getConstant(storm::utility::infinity()), A.getDdManager().template getAddZero())), illegalPlayer2Mask(illegalPlayer2Mask.ite(A.getDdManager().getConstant(storm::utility::infinity()), A.getDdManager().template getAddZero())), 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; } diff --git a/src/storm/solver/SymbolicGameSolver.h b/src/storm/solver/SymbolicGameSolver.h index 7e7d25531..f4154b00b 100644 --- a/src/storm/solver/SymbolicGameSolver.h +++ b/src/storm/solver/SymbolicGameSolver.h @@ -4,7 +4,6 @@ #include #include -#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 - class SymbolicGameSolver : public AbstractGameSolver { + class SymbolicGameSolver { public: /*! * Constructs a symbolic game solver with the given meta variable sets and pairs. @@ -120,7 +119,15 @@ namespace storm { // A player 1 strategy if one was generated. boost::optional> 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 diff --git a/src/storm/utility/solver.cpp b/src/storm/utility/solver.cpp index a111ec64b..fcee52548 100644 --- a/src/storm/utility/solver.cpp +++ b/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>(new storm::solver::SymbolicGameSolver(A, allRows, illegalPlayer1Mask, illegalPlayer2Mask, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables, player2Variables)); } - template - std::unique_ptr> GameSolverFactory::create(storm::storage::SparseMatrix const& player1Matrix, storm::storage::SparseMatrix const& player2Matrix) const { - return std::unique_ptr>(new storm::solver::GameSolver(player1Matrix, player2Matrix)); - } - std::unique_ptr 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; template class SymbolicGameSolverFactory; - template class GameSolverFactory; - template class GameSolverFactory; } } } diff --git a/src/storm/utility/solver.h b/src/storm/utility/solver.h index 074d2c9bd..5748c60d2 100644 --- a/src/storm/utility/solver.h +++ b/src/storm/utility/solver.h @@ -24,9 +24,6 @@ namespace storm { template class SymbolicMinMaxLinearEquationSolver; - template - class GameSolver; - template class LinearEquationSolver; @@ -63,15 +60,6 @@ namespace storm { virtual std::unique_ptr> create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalPlayer1Mask, storm::dd::Bdd const& illegalPlayer2Mask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables) const; }; - template - class GameSolverFactory { - public: - /*! - * Creates a new game solver instance with the given matrices. - */ - virtual std::unique_ptr> create(storm::storage::SparseMatrix const& player1Matrix, storm::storage::SparseMatrix const& player2Matrix) const; - }; - class LpSolverFactory { public: /*!