diff --git a/src/storm/solver/AbstractGameSolver.cpp b/src/storm/solver/AbstractGameSolver.cpp index b2cd637ba..3b2079fe9 100644 --- a/src/storm/solver/AbstractGameSolver.cpp +++ b/src/storm/solver/AbstractGameSolver.cpp @@ -2,6 +2,7 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/NativeEquationSolverSettings.h" +#include "storm/adapters/CarlAdapter.h" #include "storm/exceptions/InvalidSettingsException.h" @@ -14,12 +15,12 @@ namespace storm { // Get appropriate settings. maximalNumberOfIterations = settings.getMaximalIterationCount(); - precision = settings.getPrecision(); + precision = storm::utility::convertNumber<ValueType>(settings.getPrecision()); relative = settings.getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative; } template <typename ValueType> - AbstractGameSolver<ValueType>::AbstractGameSolver(double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : precision(precision), maximalNumberOfIterations(maximalNumberOfIterations), relative(relative) { + AbstractGameSolver<ValueType>::AbstractGameSolver(ValueType precision, uint_fast64_t maximalNumberOfIterations, bool relative) : precision(precision), maximalNumberOfIterations(maximalNumberOfIterations), relative(relative) { // Intentionally left empty. } @@ -52,7 +53,7 @@ namespace storm { template <typename ValueType> - double AbstractGameSolver<ValueType>::getPrecision() const { + ValueType AbstractGameSolver<ValueType>::getPrecision() const { return precision; } @@ -83,6 +84,7 @@ namespace storm { } template class AbstractGameSolver<double>; + template class AbstractGameSolver<storm::RationalNumber>; } } diff --git a/src/storm/solver/AbstractGameSolver.h b/src/storm/solver/AbstractGameSolver.h index 37935c911..a7bcebd4f 100644 --- a/src/storm/solver/AbstractGameSolver.h +++ b/src/storm/solver/AbstractGameSolver.h @@ -31,7 +31,7 @@ namespace storm { * @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); + AbstractGameSolver(ValueType precision, uint_fast64_t maximalNumberOfIterations, bool relative); /*! * Sets schedulers that might be considered by the solver as an initial guess @@ -49,12 +49,12 @@ namespace storm { storm::storage::TotalScheduler const& getPlayer1Scheduler() const; storm::storage::TotalScheduler const& getPlayer2Scheduler() const; - double getPrecision() const; + ValueType getPrecision() const; bool getRelative() const; protected: // The precision to achieve. - double precision; + ValueType precision; // The maximal number of iterations to perform. uint_fast64_t maximalNumberOfIterations; diff --git a/src/storm/solver/GameSolver.cpp b/src/storm/solver/GameSolver.cpp index b3e0db4e4..64d490e7c 100644 --- a/src/storm/solver/GameSolver.cpp +++ b/src/storm/solver/GameSolver.cpp @@ -20,7 +20,7 @@ namespace storm { } template <typename ValueType> - GameSolver<ValueType>::GameSolver(storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix, storm::storage::SparseMatrix<ValueType> const& player2Matrix, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : AbstractGameSolver<ValueType>(precision, maximalNumberOfIterations, relative), player1Matrix(player1Matrix), player2Matrix(player2Matrix) { + GameSolver<ValueType>::GameSolver(storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix, storm::storage::SparseMatrix<ValueType> const& player2Matrix, ValueType precision, uint_fast64_t maximalNumberOfIterations, bool relative) : AbstractGameSolver<ValueType>(precision, maximalNumberOfIterations, relative), player1Matrix(player1Matrix), player2Matrix(player2Matrix) { // Intentionally left empty. } @@ -202,5 +202,6 @@ namespace storm { } template class GameSolver<double>; + template class GameSolver<storm::RationalNumber>; } } diff --git a/src/storm/solver/GameSolver.h b/src/storm/solver/GameSolver.h index f4f3dcf6d..b21b19ca8 100644 --- a/src/storm/solver/GameSolver.h +++ b/src/storm/solver/GameSolver.h @@ -36,7 +36,7 @@ namespace storm { * @param maximalNumberOfIterations The maximal number of iterations. * @param relative Sets whether or not to detect convergence with a relative or absolute criterion. */ - GameSolver(storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix, storm::storage::SparseMatrix<ValueType> const& player2Matrix, double precision, uint_fast64_t maximalNumberOfIterations, bool relative); + GameSolver(storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix, storm::storage::SparseMatrix<ValueType> const& player2Matrix, ValueType precision, uint_fast64_t maximalNumberOfIterations, bool relative); /*! * Solves the equation system defined by the game matrices. Note that the game matrices have to be given upon diff --git a/src/storm/solver/SymbolicGameSolver.cpp b/src/storm/solver/SymbolicGameSolver.cpp index 996c7fc72..bfbe008e7 100644 --- a/src/storm/solver/SymbolicGameSolver.cpp +++ b/src/storm/solver/SymbolicGameSolver.cpp @@ -20,7 +20,7 @@ namespace storm { } template<storm::dd::DdType Type, typename ValueType> - SymbolicGameSolver<Type, ValueType>::SymbolicGameSolver(storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, storm::dd::Bdd<Type> const& illegalPlayer1Mask, storm::dd::Bdd<Type> const& illegalPlayer2Mask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : AbstractGameSolver<ValueType>(precision, maximalNumberOfIterations, relative), A(A), allRows(allRows), illegalPlayer1Mask(illegalPlayer1Mask.ite(A.getDdManager().getConstant(storm::utility::infinity<ValueType>()), A.getDdManager().template getAddZero<ValueType>())), illegalPlayer2Mask(illegalPlayer2Mask.ite(A.getDdManager().getConstant(storm::utility::infinity<ValueType>()), A.getDdManager().template getAddZero<ValueType>())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables), generatePlayer1Strategy(false), generatePlayer2Strategy(false) { + SymbolicGameSolver<Type, ValueType>::SymbolicGameSolver(storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, storm::dd::Bdd<Type> const& illegalPlayer1Mask, storm::dd::Bdd<Type> const& illegalPlayer2Mask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables, ValueType precision, uint_fast64_t maximalNumberOfIterations, bool relative) : AbstractGameSolver<ValueType>(precision, maximalNumberOfIterations, relative), A(A), allRows(allRows), illegalPlayer1Mask(illegalPlayer1Mask.ite(A.getDdManager().getConstant(storm::utility::infinity<ValueType>()), A.getDdManager().template getAddZero<ValueType>())), illegalPlayer2Mask(illegalPlayer2Mask.ite(A.getDdManager().getConstant(storm::utility::infinity<ValueType>()), A.getDdManager().template getAddZero<ValueType>())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables), generatePlayer1Strategy(false), generatePlayer2Strategy(false) { // Intentionally left empty. } diff --git a/src/storm/solver/SymbolicGameSolver.h b/src/storm/solver/SymbolicGameSolver.h index 3d525d495..7e7d25531 100644 --- a/src/storm/solver/SymbolicGameSolver.h +++ b/src/storm/solver/SymbolicGameSolver.h @@ -54,7 +54,7 @@ namespace storm { * equation system iteratively. * @param relative Sets whether or not to use a relativ stopping criterion rather than an absolute one. */ - SymbolicGameSolver(storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, storm::dd::Bdd<Type> const& illegalPlayer1Mask, storm::dd::Bdd<Type> const& illegalPlayer2Mask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables, double precision, uint_fast64_t maximalNumberOfIterations, bool relative); + SymbolicGameSolver(storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, storm::dd::Bdd<Type> const& illegalPlayer1Mask, storm::dd::Bdd<Type> const& illegalPlayer2Mask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables, ValueType precision, uint_fast64_t maximalNumberOfIterations, bool relative); /*! * Solves the equation system defined by the game matrix. Note that the game matrix has to be given upon diff --git a/src/storm/utility/solver.cpp b/src/storm/utility/solver.cpp index 5a8785781..12a6add0b 100644 --- a/src/storm/utility/solver.cpp +++ b/src/storm/utility/solver.cpp @@ -110,6 +110,7 @@ namespace storm { template class SymbolicGameSolverFactory<storm::dd::DdType::CUDD, double>; template class SymbolicGameSolverFactory<storm::dd::DdType::Sylvan, double>; template class GameSolverFactory<double>; + template class GameSolverFactory<storm::RationalNumber>; } } }