diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp index 3136bc36f..421f3b8cc 100644 --- a/src/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/parser/NondeterministicSparseTransitionParser.cpp @@ -117,15 +117,21 @@ namespace storm { // If we have switched the source state, we possibly need to insert the rows of the last // source state. if (source != lastSource) { - curRow += ((modelInformation.getRowGroupIndices())[lastSource + 1] - (modelInformation.getRowGroupIndices())[lastSource]) -(lastChoice + 1); + curRow += ((modelInformation.getRowGroupIndices())[lastSource + 1] - (modelInformation.getRowGroupIndices())[lastSource]) - (lastChoice + 1); } // If we skipped some states, we need to reserve empty rows for all their nondeterministic - // choices. + // choices and create the row groups. for (uint_fast64_t i = lastSource + 1; i < source; ++i) { + matrixBuilder.newRowGroup(modelInformation.getRowGroupIndices()[i]); curRow += ((modelInformation.getRowGroupIndices())[i + 1] - (modelInformation.getRowGroupIndices())[i]); } + // If we moved to the next source, we need to open the next row group. + if (source != lastSource) { + matrixBuilder.newRowGroup(modelInformation.getRowGroupIndices()[source]); + } + // If we advanced to the next state, but skipped some choices, we have to reserve rows // for them if (source != lastSource) { @@ -155,7 +161,7 @@ namespace storm { } } if (source != lastSource) { - // Add create a new rowGroup for the source, if this is the first choice we encounter for this state. + // Create a new rowGroup for the source, if this is the first choice we encounter for this state. matrixBuilder.newRowGroup(curRow); } } @@ -178,13 +184,8 @@ namespace storm { // Since we assume the transition rewards are for the transitions of the model, we copy the rowGroupIndices. if (isRewardFile) { - // We already have rowGroup 0. - for (uint_fast64_t index = 1; index < modelInformation.getRowGroupIndices().size() - 1; index++) { - matrixBuilder.newRowGroup(modelInformation.getRowGroupIndices()[index]); - } - } else { - for (uint_fast64_t node = lastSource + 1; node <= firstPass.highestStateIndex; node++) { - matrixBuilder.newRowGroup(curRow + 1); + for (uint_fast64_t node = lastSource + 1; node < modelInformation.getRowGroupCount(); node++) { + matrixBuilder.newRowGroup(modelInformation.getRowGroupIndices()[node]); } } diff --git a/src/solver/AbstractGameSolver.cpp b/src/solver/AbstractGameSolver.cpp new file mode 100644 index 000000000..76ea87bd1 --- /dev/null +++ b/src/solver/AbstractGameSolver.cpp @@ -0,0 +1,22 @@ +#include "src/solver/AbstractGameSolver.h" + +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" + +namespace storm { + namespace solver { + AbstractGameSolver::AbstractGameSolver() { + // Get the settings object to customize solving. + storm::settings::modules::NativeEquationSolverSettings const& settings = storm::settings::nativeEquationSolverSettings(); + + // Get appropriate settings. + maximalNumberOfIterations = settings.getMaximalIterationCount(); + precision = settings.getPrecision(); + relative = settings.getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative; + } + + AbstractGameSolver::AbstractGameSolver(double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : precision(precision), maximalNumberOfIterations(maximalNumberOfIterations), relative(relative) { + // Intentionally left empty. + } + } +} \ No newline at end of file diff --git a/src/solver/AbstractGameSolver.h b/src/solver/AbstractGameSolver.h new file mode 100644 index 000000000..693b4defa --- /dev/null +++ b/src/solver/AbstractGameSolver.h @@ -0,0 +1,40 @@ +#ifndef STORM_SOLVER_ABSTRACTGAMESOLVER_H_ +#define STORM_SOLVER_ABSTRACTGAMESOLVER_H_ + +#include + +namespace storm { + namespace solver { + /*! + * The abstract base class for the game solvers. + */ + class AbstractGameSolver { + public: + /*! + * Creates a game solver with the default parameters. + */ + AbstractGameSolver(); + + /*! + * Creates a game solver with the given parameters. + * + * @param precision The precision to achieve. + * @param maximalNumberOfIterations The maximal number of iterations to perform. + * @param relative A flag indicating whether a relative or an absolute stopping criterion is to be used. + */ + AbstractGameSolver(double precision, uint_fast64_t maximalNumberOfIterations, bool relative); + + protected: + // The precision to achieve. + double precision; + + // The maximal number of iterations to perform. + uint_fast64_t maximalNumberOfIterations; + + // A flag indicating whether a relative or an absolute stopping criterion is to be used. + bool relative; + }; + } +} + +#endif /* STORM_SOLVER_ABSTRACTGAMESOLVER_H_ */ diff --git a/src/solver/GameSolver.cpp b/src/solver/GameSolver.cpp new file mode 100644 index 000000000..752328e11 --- /dev/null +++ b/src/solver/GameSolver.cpp @@ -0,0 +1,76 @@ +#include "src/solver/GameSolver.h" + +#include "src/storage/SparseMatrix.h" + +#include "src/utility/vector.h" + +namespace storm { + namespace solver { + template + GameSolver::GameSolver(storm::storage::SparseMatrix const& player1Matrix, storm::storage::SparseMatrix const& player2Matrix) : AbstractGameSolver(), player1Matrix(player1Matrix), player2Matrix(player2Matrix) { + // Intentionally left empty. + } + + template + GameSolver::GameSolver(storm::storage::SparseMatrix const& player1Matrix, storm::storage::SparseMatrix const& player2Matrix, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : AbstractGameSolver(precision, maximalNumberOfIterations, relative), player1Matrix(player1Matrix), player2Matrix(player2Matrix) { + // Intentionally left empty. + } + + template + void GameSolver::solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, std::vector& x, std::vector const& b) const { + // Set up the environment for value iteration. + uint_fast64_t numberOfPlayer1States = x.size(); + + bool converged = false; + 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, precision, relative); + std::swap(x, tmpResult); + + ++iterations; + } while (!converged && iterations < maximalNumberOfIterations); + } + + template class GameSolver; + } +} \ No newline at end of file diff --git a/src/solver/GameSolver.h b/src/solver/GameSolver.h new file mode 100644 index 000000000..8218768cc --- /dev/null +++ b/src/solver/GameSolver.h @@ -0,0 +1,62 @@ +#ifndef STORM_SOLVER_GAMESOLVER_H_ +#define STORM_SOLVER_GAMESOLVER_H_ + +#include + +#include "src/solver/AbstractGameSolver.h" +#include "src/solver/OptimizationDirection.h" + +#include "src/storage/sparse/StateType.h" + +namespace storm { + namespace storage { + template + class SparseMatrix; + } + + namespace solver { + template + class GameSolver : public AbstractGameSolver { + public: + /* + * Constructs a game solver with the given player 1 and player 2 matrices. + * + * @param player1Matrix The matrix defining the choices of player 1. + * @param player2Matrix The matrix defining the choices of player 2. + */ + GameSolver(storm::storage::SparseMatrix 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, double precision, uint_fast64_t maximalNumberOfIterations, bool relative); + + /*! + * Solves the equation system defined by the game matrix. Note that the game matrix has to be given upon + * construction time of the solver object. + * + * @param player1Goal Sets whether player 1 wants to minimize or maximize. + * @param player2Goal Sets whether player 2 wants to minimize or maximize. + * @param x The initial guess of the solution. + * @param b The vector to add after matrix-vector multiplication. + * @return The solution vector in the for of the vector x. + */ + virtual void solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, std::vector& x, std::vector const& b) const; + + private: + // The matrix defining the choices of player 1. + storm::storage::SparseMatrix const& player1Matrix; + + // The matrix defining the choices of player 2. + storm::storage::SparseMatrix const& player2Matrix; + }; + } +} + +#endif /* STORM_SOLVER_GAMESOLVER_H_ */ diff --git a/src/solver/SymbolicGameSolver.cpp b/src/solver/SymbolicGameSolver.cpp index 8faab2914..ab439326c 100644 --- a/src/solver/SymbolicGameSolver.cpp +++ b/src/solver/SymbolicGameSolver.cpp @@ -11,44 +11,36 @@ namespace storm { template SymbolicGameSolver::SymbolicGameSolver(storm::dd::Add const& gameMatrix, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables) : gameMatrix(gameMatrix), allRows(allRows), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables) { - // Get the settings object to customize solving. - storm::settings::modules::NativeEquationSolverSettings const& settings = storm::settings::nativeEquationSolverSettings(); - - // Get appropriate settings. - maximalNumberOfIterations = settings.getMaximalIterationCount(); - precision = settings.getPrecision(); - relative = settings.getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative; + // Intentionally left empty. } template - SymbolicGameSolver::SymbolicGameSolver(storm::dd::Add const& gameMatrix, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : gameMatrix(gameMatrix), allRows(allRows), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables), precision(precision), maximalNumberOfIterations(maximalNumberOfIterations), relative(relative) { + SymbolicGameSolver::SymbolicGameSolver(storm::dd::Add const& gameMatrix, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : AbstractGameSolver(precision, maximalNumberOfIterations, relative), gameMatrix(gameMatrix), allRows(allRows), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables) { // Intentionally left empty. } template - storm::dd::Add SymbolicGameSolver::solveGame(bool player1Min, bool player2Min, storm::dd::Add const& x, storm::dd::Add const& b) const { + storm::dd::Add SymbolicGameSolver::solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, storm::dd::Add const& x, storm::dd::Add const& b) const { // Set up the environment. storm::dd::Add xCopy = x; uint_fast64_t iterations = 0; bool converged = false; - while (!converged && iterations < maximalNumberOfIterations) { + do { // Compute tmp = A * x + b storm::dd::Add xCopyAsColumn = xCopy.swapVariables(this->rowColumnMetaVariablePairs); storm::dd::Add tmp = this->gameMatrix.multiplyMatrix(xCopyAsColumn, this->columnMetaVariables); tmp += b; // Now abstract from player 2 and player 1 variables. - if (player2Min) { - tmp = tmp.minAbstract(this->player2Variables); - } else { - tmp = tmp.maxAbstract(this->player2Variables); + switch (player2Goal) { + case OptimizationDirection::Minimize: tmp = tmp.minAbstract(this->player2Variables); break; + case OptimizationDirection::Maximize: tmp = tmp.maxAbstract(this->player2Variables); break; } - - if (player1Min) { - tmp = tmp.minAbstract(this->player1Variables); - } else { - tmp = tmp.maxAbstract(this->player1Variables); + + switch (player1Goal) { + case OptimizationDirection::Minimize: tmp = tmp.minAbstract(this->player1Variables); break; + case OptimizationDirection::Maximize: tmp = tmp.maxAbstract(this->player1Variables); break; } // Now check if the process already converged within our precision. @@ -60,7 +52,7 @@ namespace storm { } ++iterations; - } + } while (!converged && iterations < maximalNumberOfIterations); return xCopy; } diff --git a/src/solver/SymbolicGameSolver.h b/src/solver/SymbolicGameSolver.h index 6abebee54..ec4c47d68 100644 --- a/src/solver/SymbolicGameSolver.h +++ b/src/solver/SymbolicGameSolver.h @@ -3,8 +3,11 @@ #include #include -#include "src/storage/expressions/Variable.h" +#include "src/solver/AbstractGameSolver.h" +#include "src/solver/OptimizationDirection.h" + +#include "src/storage/expressions/Variable.h" #include "src/storage/dd/Bdd.h" #include "src/storage/dd/Add.h" @@ -15,7 +18,7 @@ namespace storm { * An interface that represents an abstract symbolic game solver. */ template - class SymbolicGameSolver { + class SymbolicGameSolver : public AbstractGameSolver { public: /*! * Constructs a symbolic game solver with the given meta variable sets and pairs. @@ -50,16 +53,16 @@ namespace storm { SymbolicGameSolver(storm::dd::Add const& gameMatrix, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables, double precision, uint_fast64_t maximalNumberOfIterations, bool relative); /*! - * Solves the equation system x = min/max(A*x + b) given by the parameters. Note that the matrix A has - * to be given upon construction time of the solver object. + * Solves the equation system defined by the game matrix. Note that the game matrix has to be given upon + * construction time of the solver object. * - * @param player1Min A flag indicating whether player 1 wants to minimize the result. - * @param player2Min A flag indicating whether player 1 wants to minimize the result. + * @param player1Goal Sets whether player 1 wants to minimize or maximize. + * @param player2Goal Sets whether player 2 wants to minimize or maximize. * @param x The initial guess of the solution. * @param b The vector to add after matrix-vector multiplication. * @return The solution vector. */ - virtual storm::dd::Add solveGame(bool player1Min, bool player2Min, storm::dd::Add const& x, storm::dd::Add const& b) const; + virtual storm::dd::Add solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, storm::dd::Add const& x, storm::dd::Add const& b) const; protected: // The matrix defining the coefficients of the linear equation system. @@ -69,28 +72,19 @@ namespace storm { storm::dd::Bdd const& allRows; // The row variables. - std::set rowMetaVariables; + std::set const& rowMetaVariables; // The column variables. - std::set columnMetaVariables; + std::set const& columnMetaVariables; // The pairs of meta variables used for renaming. std::vector> const& rowColumnMetaVariablePairs; // The player 1 variables. - std::set player1Variables; + std::set const& player1Variables; // The player 2 variables. - std::set player2Variables; - - // The precision to achive. - double precision; - - // The maximal number of iterations to perform. - uint_fast64_t maximalNumberOfIterations; - - // A flag indicating whether a relative or an absolute stopping criterion is to be used. - bool relative; + std::set const& player2Variables; }; } // namespace solver diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 4648950b3..4184109cb 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -1,4 +1,5 @@ #include +#include // To detect whether the usage of TBB is possible, this include is neccessary #include "storm-config.h" @@ -143,9 +144,18 @@ namespace storm { template void SparseMatrixBuilder::newRowGroup(index_type startingRow) { STORM_LOG_THROW(hasCustomRowGrouping, storm::exceptions::InvalidStateException, "Matrix was not created to have a custom row grouping."); - STORM_LOG_THROW(rowGroupIndices.empty() || startingRow >= rowGroupIndices.back(), storm::exceptions::InvalidStateException, "Illegal row group with negative size."); + STORM_LOG_THROW(startingRow >= lastRow, storm::exceptions::InvalidStateException, "Illegal row group with negative size."); rowGroupIndices.push_back(startingRow); ++currentRowGroup; + + // Close all rows from the most recent one to the starting row. + for (index_type i = lastRow + 1; i <= startingRow; ++i) { + rowIndications.push_back(currentEntryCount); + } + + // Reset the most recently seen row/column to allow for proper insertion of the following elements. + lastRow = startingRow; + lastColumn = 0; } template @@ -156,7 +166,7 @@ namespace storm { rowCount = std::max(rowCount, initialRowCount); } rowCount = std::max(rowCount, overriddenRowCount); - + // If the current row count was overridden, we may need to add empty rows. for (index_type i = lastRow + 1; i < rowCount; ++i) { rowIndications.push_back(currentEntryCount); @@ -196,7 +206,7 @@ namespace storm { rowGroupIndices.push_back(rowCount); } } - + return SparseMatrix(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices), hasCustomRowGrouping); } @@ -1163,16 +1173,16 @@ namespace storm { // Explicitly instantiate the entry, builder and the matrix. // double template class MatrixEntry::index_type, double>; - template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); + template std::ostream& operator<<(std::ostream& out, MatrixEntry::index_type, double> const& entry); template class SparseMatrixBuilder; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; - // float + // float template class MatrixEntry::index_type, float>; - template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); + template std::ostream& operator<<(std::ostream& out, MatrixEntry::index_type, float> const& entry); template class SparseMatrixBuilder; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); @@ -1181,12 +1191,20 @@ namespace storm { // int template class MatrixEntry::index_type, int>; - template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); + template std::ostream& operator<<(std::ostream& out, MatrixEntry::index_type, int> const& entry); template class SparseMatrixBuilder; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; + // state_type + template class MatrixEntry::index_type, storm::storage::sparse::state_type>; + template std::ostream& operator<<(std::ostream& out, MatrixEntry::index_type, storm::storage::sparse::state_type> const& entry); + template class SparseMatrixBuilder; + template class SparseMatrix; + template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); + template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; + #ifdef STORM_HAVE_CARL // Rat Function template class MatrixEntry::index_type, RationalFunction>; diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index e62cfc114..9ac73881e 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -1011,7 +1011,6 @@ namespace storm { } // Now we are in a position to start the enumeration over all command variables. - uint_fast64_t modelCount = 0; solver->allSat(allCommandVariables, [&] (storm::solver::SmtSolver::ModelReference& modelReference) -> bool { // Now we need to reconstruct the chosen commands from the valuation of the command variables. std::vector>> chosenCommands(possibleCommands.size()); diff --git a/src/utility/ConstantsComparator.cpp b/src/utility/ConstantsComparator.cpp index aecfa39fb..5923b5284 100644 --- a/src/utility/ConstantsComparator.cpp +++ b/src/utility/ConstantsComparator.cpp @@ -2,6 +2,7 @@ #include #include +#include #include "src/utility/constants.h" #include "src/settings/SettingsManager.h" @@ -94,7 +95,8 @@ namespace storm { template class ConstantsComparator; template class ConstantsComparator; template class ConstantsComparator; - + template class ConstantsComparator; + #ifdef STORM_HAVE_CARL template class ConstantsComparator; template class ConstantsComparator; diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp index f346d2fcc..bba5fd160 100644 --- a/src/utility/constants.cpp +++ b/src/utility/constants.cpp @@ -1,7 +1,7 @@ #include "src/utility/constants.h" -#include "src/storage/SparseMatrix.h" #include "src/storage/sparse/StateType.h" +#include "src/storage/SparseMatrix.h" #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" @@ -83,27 +83,13 @@ namespace storm { return std::pow(value, exponent); } - template<> - double simplify(double value) { - // In the general case, we don't to anything here, but merely return the value. If something else is - // supposed to happen here, the templated function can be specialized for this particular type. - return value; - } - - template<> - float simplify(float value) { - // In the general case, we don't to anything here, but merely return the value. If something else is - // supposed to happen here, the templated function can be specialized for this particular type. + template + ValueType simplify(ValueType value) { + // In the general case, we don't to anything here, but merely return the value. If something else is + // supposed to happen here, the templated function can be specialized for this particular type. return value; } - template<> - int simplify(int value) { - // In the general case, we don't to anything here, but merely return the value. If something else is - // supposed to happen here, the templated function can be specialized for this particular type. - return value; - } - #ifdef STORM_HAVE_CARL template<> RationalFunction& simplify(RationalFunction& value); @@ -201,7 +187,23 @@ namespace storm { template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); - + + template bool isOne(storm::storage::sparse::state_type const& value); + template bool isZero(storm::storage::sparse::state_type const& value); + template bool isConstant(storm::storage::sparse::state_type const& value); + + template storm::storage::sparse::state_type one(); + template storm::storage::sparse::state_type zero(); + template storm::storage::sparse::state_type infinity(); + + template storm::storage::sparse::state_type pow(storm::storage::sparse::state_type const& value, uint_fast64_t exponent); + + template storm::storage::sparse::state_type simplify(storm::storage::sparse::state_type value); + + template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); + template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); + template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); + #ifdef STORM_HAVE_CARL template bool isOne(RationalFunction const& value); template bool isZero(RationalFunction const& value); diff --git a/src/utility/solver.cpp b/src/utility/solver.cpp index ef3744ff9..15d8a71ac 100644 --- a/src/utility/solver.cpp +++ b/src/utility/solver.cpp @@ -1,13 +1,13 @@ #include "src/utility/solver.h" -#include "src/solver/SymbolicGameSolver.h" - #include #include "src/solver/SymbolicLinearEquationSolver.h" #include "src/solver/SymbolicMinMaxLinearEquationSolver.h" +#include "src/solver/SymbolicGameSolver.h" #include "src/solver/NativeLinearEquationSolver.h" #include "src/solver/GmmxxLinearEquationSolver.h" +#include "src/solver/GameSolver.h" #include "src/solver/NativeMinMaxLinearEquationSolver.h" #include "src/solver/GmmxxMinMaxLinearEquationSolver.h" @@ -102,8 +102,7 @@ namespace storm { template void MinMaxLinearEquationSolverFactory::setPreferredTechnique(storm::solver::MinMaxTechniqueSelection preferredTech) { this->prefTech = preferredTech; - } - + } template std::unique_ptr> MinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix, bool trackPolicy) const { @@ -133,6 +132,10 @@ namespace storm { } + 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; @@ -192,7 +195,7 @@ namespace storm { template class GmmxxLinearEquationSolverFactory; template class NativeLinearEquationSolverFactory; template class MinMaxLinearEquationSolverFactory; - + template class GameSolverFactory; } } } \ No newline at end of file diff --git a/src/utility/solver.h b/src/utility/solver.h index 81e2d1d23..ed7528915 100644 --- a/src/utility/solver.h +++ b/src/utility/solver.h @@ -4,6 +4,7 @@ #include #include #include +#include #include "src/storage/dd/DdType.h" #include "src/solver/SolverSelectionOptions.h" @@ -13,13 +14,15 @@ namespace storm { template class SymbolicGameSolver; template class SymbolicLinearEquationSolver; template class SymbolicMinMaxLinearEquationSolver; + template class GameSolver; template class LinearEquationSolver; template class MinMaxLinearEquationSolver; class LpSolver; class SmtSolver; template class NativeLinearEquationSolver; - enum class NativeLinearEquationSolverSolutionMethod; + enum class + NativeLinearEquationSolverSolutionMethod; } namespace storage { @@ -93,7 +96,7 @@ namespace storm { public: MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection solverType = storm::solver::EquationSolverTypeSelection::FROMSETTINGS); /*! - * Creates a new nondeterministic linear equation solver instance with the given matrix. + * Creates a new min/max linear equation solver instance with the given matrix. */ virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix, bool trackPolicy = false) const; void setSolverType(storm::solver::EquationSolverTypeSelection solverType); @@ -106,6 +109,15 @@ namespace storm { /// Notice that we save the selection enum here, which allows different solvers to use different techniques. storm::solver::MinMaxTechniqueSelection prefTech; }; + + template + 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: diff --git a/test/functional/solver/FullySymbolicGameSolverTest.cpp b/test/functional/solver/FullySymbolicGameSolverTest.cpp index ce9e21798..dd48ad678 100644 --- a/test/functional/solver/FullySymbolicGameSolverTest.cpp +++ b/test/functional/solver/FullySymbolicGameSolverTest.cpp @@ -45,25 +45,25 @@ TEST(FullySymbolicGameSolverTest, Solve) { storm::dd::Add b = manager->getEncoding(state.first, 2).toAdd() + manager->getEncoding(state.first, 4).toAdd(); // Now solve the game with different strategies for the players. - storm::dd::Add result = solver->solveGame(true, true, x, b); + storm::dd::Add result = solver->solveGame(storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, x, b); result *= manager->getEncoding(state.first, 1).toAdd(); result = result.sumAbstract({state.first}); EXPECT_NEAR(0, result.getValue(), storm::settings::nativeEquationSolverSettings().getPrecision()); x = manager->getAddZero(); - result = solver->solveGame(true, false, x, b); + result = solver->solveGame(storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, x, b); result *= manager->getEncoding(state.first, 1).toAdd(); result = result.sumAbstract({state.first}); EXPECT_NEAR(0.5, result.getValue(), storm::settings::nativeEquationSolverSettings().getPrecision()); x = manager->getAddZero(); - result = solver->solveGame(false, true, x, b); + result = solver->solveGame(storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, x, b); result *= manager->getEncoding(state.first, 1).toAdd(); result = result.sumAbstract({state.first}); EXPECT_NEAR(0.2, result.getValue(), storm::settings::nativeEquationSolverSettings().getPrecision()); x = manager->getAddZero(); - result = solver->solveGame(false, false, x, b); + result = solver->solveGame(storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, x, b); result *= manager->getEncoding(state.first, 1).toAdd(); result = result.sumAbstract({state.first}); EXPECT_NEAR(0.99999892625817599, result.getValue(), storm::settings::nativeEquationSolverSettings().getPrecision()); diff --git a/test/functional/solver/GameSolverTest.cpp b/test/functional/solver/GameSolverTest.cpp new file mode 100644 index 000000000..7c73d90f4 --- /dev/null +++ b/test/functional/solver/GameSolverTest.cpp @@ -0,0 +1,69 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "src/storage/SparseMatrix.h" + +#include "src/utility/solver.h" +#include "src/settings/SettingsManager.h" + +#include "src/solver/GameSolver.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" + +TEST(GameSolverTest, Solve) { + // Construct simple game. Start with player 2 matrix. + storm::storage::SparseMatrixBuilder player2MatrixBuilder(0, 0, 0, false, true); + player2MatrixBuilder.newRowGroup(0); + player2MatrixBuilder.addNextValue(0, 0, 0.4); + player2MatrixBuilder.addNextValue(0, 1, 0.6); + player2MatrixBuilder.addNextValue(1, 1, 0.2); + player2MatrixBuilder.addNextValue(1, 2, 0.8); + player2MatrixBuilder.newRowGroup(2); + player2MatrixBuilder.addNextValue(2, 2, 0.5); + player2MatrixBuilder.addNextValue(2, 3, 0.5); + player2MatrixBuilder.addNextValue(3, 0, 1); + player2MatrixBuilder.newRowGroup(4); + player2MatrixBuilder.newRowGroup(5); + player2MatrixBuilder.newRowGroup(6); + storm::storage::SparseMatrix player2Matrix = player2MatrixBuilder.build(); + + // Now build player 1 matrix. + storm::storage::SparseMatrixBuilder player1MatrixBuilder(0, 0, 0, false, true); + player1MatrixBuilder.newRowGroup(0); + player1MatrixBuilder.addNextValue(0, 0, 1); + player1MatrixBuilder.addNextValue(1, 1, 1); + player1MatrixBuilder.newRowGroup(2); + player1MatrixBuilder.addNextValue(2, 2, 1); + player1MatrixBuilder.newRowGroup(3); + player1MatrixBuilder.addNextValue(3, 3, 1); + player1MatrixBuilder.newRowGroup(4); + player1MatrixBuilder.addNextValue(4, 4, 1); + storm::storage::SparseMatrix player1Matrix = player1MatrixBuilder.build(); + + std::unique_ptr> solverFactory(new storm::utility::solver::GameSolverFactory()); + std::unique_ptr> solver = solverFactory->create(player1Matrix, player2Matrix); + + // Create solution and target state vector. + std::vector result(4); + std::vector b(7); + b[4] = 1; + b[6] = 1; + + // Now solve the game with different strategies for the players. + solver->solveGame(storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, result, b); + EXPECT_NEAR(0, result[0], storm::settings::nativeEquationSolverSettings().getPrecision()); + + result = std::vector(4); + + solver->solveGame(storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, result, b); + EXPECT_NEAR(0.5, result[0], storm::settings::nativeEquationSolverSettings().getPrecision()); + + result = std::vector(4); + + solver->solveGame(storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, result, b); + EXPECT_NEAR(0.2, result[0], storm::settings::nativeEquationSolverSettings().getPrecision()); + + result = std::vector(4); + + solver->solveGame(storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, result, b); + EXPECT_NEAR(0.99999892625817599, result[0], storm::settings::nativeEquationSolverSettings().getPrecision()); +} \ No newline at end of file