diff --git a/src/storm/exceptions/FormatUnsupportedBySolverException.h b/src/storm/exceptions/FormatUnsupportedBySolverException.h new file mode 100644 index 000000000..2f7d2bf65 --- /dev/null +++ b/src/storm/exceptions/FormatUnsupportedBySolverException.h @@ -0,0 +1,13 @@ +#pragma once + +#include "storm/exceptions/BaseException.h" +#include "storm/exceptions/ExceptionMacros.h" + +namespace storm { + namespace exceptions { + + STORM_NEW_EXCEPTION(FormatUnsupportedBySolverException) + + } // namespace exceptions +} // namespace storm + diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index b574cabd1..b59c13897 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -22,6 +22,7 @@ #include "storm/exceptions/InvalidOperationException.h" #include "storm/exceptions/InvalidStateException.h" #include "storm/exceptions/InvalidPropertyException.h" +#include "storm/exceptions/FormatUnsupportedBySolverException.h" namespace storm { namespace modelchecker { @@ -489,6 +490,8 @@ namespace storm { bsccEquationSystem = builder.build(); { + // Check whether we have the right input format for the solver. + STORM_LOG_THROW(linearEquationSolverFactory.getEquationProblemFormat() == storm::solver::LinearEquationSolverProblemFormat::EquationSystem, storm::exceptions::FormatUnsupportedBySolverException, "The selected solver does not support the required format."); std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(bsccEquationSystem)); solver->solveEquations(bsccEquationSystemSolution, bsccEquationSystemRightSide); } @@ -557,6 +560,8 @@ namespace storm { rewardSolution = std::vector(rewardEquationSystemMatrix.getColumnCount(), one); { + // Check whether we have the right input format for the solver. + STORM_LOG_THROW(linearEquationSolverFactory.getEquationProblemFormat() == storm::solver::LinearEquationSolverProblemFormat::EquationSystem, storm::exceptions::FormatUnsupportedBySolverException, "The selected solver does not support the required format."); std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(rewardEquationSystemMatrix)); solver->solveEquations(rewardSolution, rewardRightSide); } diff --git a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp index 3daaee646..2a7e8672e 100644 --- a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp @@ -59,11 +59,16 @@ namespace storm { prob1StatesAsColumn = prob1StatesAsColumn.swapVariables(model.getRowColumnMetaVariablePairs()); storm::dd::Add subvector = submatrix * prob1StatesAsColumn; subvector = subvector.sumAbstract(model.getColumnVariables()); + + // Check whether we need to create an equation system. + bool convertToEquationSystem = linearEquationSolverFactory.getEquationProblemFormat() == storm::solver::LinearEquationSolverProblemFormat::EquationSystem; - // Finally cut away all columns targeting non-maybe states and convert the matrix into the matrix needed - // for solving the equation system (i.e. compute (I-A)). + // Finally cut away all columns targeting non-maybe states and potentially convert the matrix + // into the matrix needed for solving the equation system (i.e. compute (I-A)). submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); - submatrix = (model.getRowColumnIdentity() * maybeStatesAdd) - submatrix; + if (convertToEquationSystem) { + submatrix = (model.getRowColumnIdentity() * maybeStatesAdd) - submatrix; + } // Create the solution vector. std::vector x(maybeStates.getNonZeroCount(), storm::utility::convertNumber(0.5)); @@ -224,10 +229,15 @@ namespace storm { // Then compute the state reward vector to use in the computation. storm::dd::Add subvector = rewardModel.getTotalRewardVector(maybeStatesAdd, submatrix, model.getColumnVariables()); - // Finally cut away all columns targeting non-maybe states and convert the matrix into the matrix needed - // for solving the equation system (i.e. compute (I-A)). + // Check whether we need to create an equation system. + bool convertToEquationSystem = linearEquationSolverFactory.getEquationProblemFormat() == storm::solver::LinearEquationSolverProblemFormat::EquationSystem; + + // Finally cut away all columns targeting non-maybe states and potentially convert the matrix + // into the matrix needed for solving the equation system (i.e. compute (I-A)). submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); - submatrix = (model.getRowColumnIdentity() * maybeStatesAdd) - submatrix; + if (convertToEquationSystem) { + submatrix = (model.getRowColumnIdentity() * maybeStatesAdd) - submatrix; + } // Create the solution vector. std::vector x(maybeStates.getNonZeroCount(), storm::utility::convertNumber(0.5)); diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 6d219bda6..0fc234c83 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -106,12 +106,16 @@ namespace storm { if (!maybeStates.empty()) { // In this case we have have to compute the probabilities. - // We can eliminate the rows and columns from the original transition probability matrix. - storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, true); + // Check whether we need to convert the input to equation system format. + bool convertToEquationSystem = linearEquationSolverFactory.getEquationProblemFormat() == storm::solver::LinearEquationSolverProblemFormat::EquationSystem; - // Converting the matrix from the fixpoint notation to the form needed for the equation - // system. That is, we go from x = A*x + b to (I-A)x = b. - submatrix.convertToEquationSystem(); + // We can eliminate the rows and columns from the original transition probability matrix. + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, convertToEquationSystem); + if (convertToEquationSystem) { + // Converting the matrix from the fixpoint notation to the form needed for the equation + // system. That is, we go from x = A*x + b to (I-A)x = b. + submatrix.convertToEquationSystem(); + } // Initialize the x vector with the hint (if available) or with 0.5 for each element. // This is the initial guess for the iterative solvers. It should be safe as for all @@ -237,13 +241,17 @@ namespace storm { storm::utility::vector::setVectorValues(result, maybeStates, storm::utility::one()); } else { if (!maybeStates.empty()) { + // Check whether we need to convert the input to equation system format. + bool convertToEquationSystem = linearEquationSolverFactory.getEquationProblemFormat() == storm::solver::LinearEquationSolverProblemFormat::EquationSystem; + // In this case we have to compute the reward values for the remaining states. // We can eliminate the rows and columns from the original transition probability matrix. - storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, true); - - // Converting the matrix from the fixpoint notation to the form needed for the equation - // system. That is, we go from x = A*x + b to (I-A)x = b. - submatrix.convertToEquationSystem(); + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, convertToEquationSystem); + if (convertToEquationSystem) { + // Converting the matrix from the fixpoint notation to the form needed for the equation + // system. That is, we go from x = A*x + b to (I-A)x = b. + submatrix.convertToEquationSystem(); + } // Initialize the x vector with the hint (if available) or with 1 for each element. // This is the initial guess for the iterative solvers. diff --git a/src/storm/settings/modules/NativeEquationSolverSettings.cpp b/src/storm/settings/modules/NativeEquationSolverSettings.cpp index aa8ca37a9..7b17808f1 100644 --- a/src/storm/settings/modules/NativeEquationSolverSettings.cpp +++ b/src/storm/settings/modules/NativeEquationSolverSettings.cpp @@ -22,9 +22,10 @@ namespace storm { const std::string NativeEquationSolverSettings::maximalIterationsOptionShortName = "i"; const std::string NativeEquationSolverSettings::precisionOptionName = "precision"; const std::string NativeEquationSolverSettings::absoluteOptionName = "absolute"; - + const std::string NativeEquationSolverSettings::powerMethodMultiplicationStyleOptionName = "powmult"; + NativeEquationSolverSettings::NativeEquationSolverSettings() : ModuleSettings(moduleName) { - std::vector methods = { "jacobi", "gaussseidel", "sor", "walkerchae", "power" }; + std::vector methods = { "jacobi", "gaussseidel", "sor", "walkerchae", "power", "spower" }; this->addOption(storm::settings::OptionBuilder(moduleName, techniqueOptionName, true, "The method to be used for solving linear equation systems with the native engine.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods)).setDefaultValueString("jacobi").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()); @@ -34,6 +35,10 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, omegaOptionName, false, "The omega used for SOR.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The value of the SOR parameter.").setDefaultValueDouble(0.9).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()); + + std::vector multiplicationStyles = {"gaussseidel", "regular", "gs", "r"}; + this->addOption(storm::settings::OptionBuilder(moduleName, powerMethodMultiplicationStyleOptionName, false, "Sets which method multiplication style to prefer for the power method.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of a multiplication style.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(multiplicationStyles)).setDefaultValueString("gaussseidel").build()).build()); } bool NativeEquationSolverSettings::isLinearEquationSystemTechniqueSet() const { @@ -56,6 +61,8 @@ namespace storm { return NativeEquationSolverSettings::LinearEquationMethod::WalkerChae; } else if (linearEquationSystemTechniqueAsString == "power") { return NativeEquationSolverSettings::LinearEquationMethod::Power; + } else if (linearEquationSystemTechniqueAsString == "spower") { + return NativeEquationSolverSettings::LinearEquationMethod::SoundPower; } STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown solution technique '" << linearEquationSystemTechniqueAsString << "' selected."); } @@ -88,6 +95,16 @@ namespace storm { return this->getOption(absoluteOptionName).getHasOptionBeenSet() ? NativeEquationSolverSettings::ConvergenceCriterion::Absolute : NativeEquationSolverSettings::ConvergenceCriterion::Relative; } + storm::solver::MultiplicationStyle NativeEquationSolverSettings::getPowerMethodMultiplicationStyle() const { + std::string multiplicationStyleString = this->getOption(powerMethodMultiplicationStyleOptionName).getArgumentByName("name").getValueAsString(); + if (multiplicationStyleString == "gaussseidel" || multiplicationStyleString == "gs") { + return storm::solver::MultiplicationStyle::GaussSeidel; + } else if (multiplicationStyleString == "regular" || multiplicationStyleString == "r") { + return storm::solver::MultiplicationStyle::Regular; + } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown multiplication style '" << multiplicationStyleString << "'."); + } + bool NativeEquationSolverSettings::check() const { // This list does not include the precision, because this option is shared with other modules. bool optionSet = isLinearEquationSystemTechniqueSet() || isMaximalIterationCountSet() || isConvergenceCriterionSet(); diff --git a/src/storm/settings/modules/NativeEquationSolverSettings.h b/src/storm/settings/modules/NativeEquationSolverSettings.h index 12ee6716f..ccedfbdc6 100644 --- a/src/storm/settings/modules/NativeEquationSolverSettings.h +++ b/src/storm/settings/modules/NativeEquationSolverSettings.h @@ -3,6 +3,8 @@ #include "storm/settings/modules/ModuleSettings.h" +#include "storm/solver/MultiplicationStyle.h" + namespace storm { namespace settings { namespace modules { @@ -13,7 +15,7 @@ namespace storm { class NativeEquationSolverSettings : public ModuleSettings { public: // An enumeration of all available methods for solving linear equations. - enum class LinearEquationMethod { Jacobi, GaussSeidel, SOR, WalkerChae, Power }; + enum class LinearEquationMethod { Jacobi, GaussSeidel, SOR, WalkerChae, Power, SoundPower }; // An enumeration of all available convergence criteria. enum class ConvergenceCriterion { Absolute, Relative }; @@ -93,6 +95,13 @@ namespace storm { */ ConvergenceCriterion getConvergenceCriterion() const; + /*! + * Retrieves the multiplication style to use in the power method. + * + * @return The multiplication style. + */ + storm::solver::MultiplicationStyle getPowerMethodMultiplicationStyle() const; + bool check() const override; // The name of the module. @@ -106,6 +115,7 @@ namespace storm { static const std::string maximalIterationsOptionShortName; static const std::string precisionOptionName; static const std::string absoluteOptionName; + static const std::string powerMethodMultiplicationStyleOptionName; }; } // namespace modules diff --git a/src/storm/solver/EigenLinearEquationSolver.cpp b/src/storm/solver/EigenLinearEquationSolver.cpp index d82994e50..5f0a001a9 100644 --- a/src/storm/solver/EigenLinearEquationSolver.cpp +++ b/src/storm/solver/EigenLinearEquationSolver.cpp @@ -106,10 +106,15 @@ namespace storm { #endif template - EigenLinearEquationSolver::EigenLinearEquationSolver(storm::storage::SparseMatrix const& A, EigenLinearEquationSolverSettings const& settings) : eigenA(storm::adapters::EigenAdapter::toEigenSparseMatrix(A)), settings(settings) { + EigenLinearEquationSolver::EigenLinearEquationSolver(EigenLinearEquationSolverSettings const& settings) : settings(settings) { // Intentionally left empty. } + template + EigenLinearEquationSolver::EigenLinearEquationSolver(storm::storage::SparseMatrix const& A, EigenLinearEquationSolverSettings const& settings) : settings(settings) { + this->setMatrix(A); + } + template EigenLinearEquationSolver::EigenLinearEquationSolver(storm::storage::SparseMatrix&& A, EigenLinearEquationSolverSettings const& settings) : settings(settings) { this->setMatrix(std::move(A)); @@ -299,6 +304,11 @@ namespace storm { return settings; } + template + LinearEquationSolverProblemFormat EigenLinearEquationSolver::getEquationProblemFormat() const { + LinearEquationSolverProblemFormat::EquationSystem; + } + template EigenLinearEquationSolverSettings const& EigenLinearEquationSolver::getSettings() const { return settings; @@ -347,13 +357,8 @@ namespace storm { #endif template - std::unique_ptr> EigenLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - return std::make_unique>(matrix, settings); - } - - template - std::unique_ptr> EigenLinearEquationSolverFactory::create(storm::storage::SparseMatrix&& matrix) const { - return std::make_unique>(std::move(matrix), settings); + std::unique_ptr> EigenLinearEquationSolverFactory::create() const { + return std::make_unique>(settings); } template diff --git a/src/storm/solver/EigenLinearEquationSolver.h b/src/storm/solver/EigenLinearEquationSolver.h index 6c214cd5a..951258a76 100644 --- a/src/storm/solver/EigenLinearEquationSolver.h +++ b/src/storm/solver/EigenLinearEquationSolver.h @@ -60,6 +60,7 @@ namespace storm { template class EigenLinearEquationSolver : public LinearEquationSolver { public: + EigenLinearEquationSolver(EigenLinearEquationSolverSettings const& settings = EigenLinearEquationSolverSettings()); EigenLinearEquationSolver(storm::storage::SparseMatrix const& A, EigenLinearEquationSolverSettings const& settings = EigenLinearEquationSolverSettings()); EigenLinearEquationSolver(storm::storage::SparseMatrix&& A, EigenLinearEquationSolverSettings const& settings = EigenLinearEquationSolverSettings()); @@ -71,7 +72,9 @@ namespace storm { EigenLinearEquationSolverSettings& getSettings(); EigenLinearEquationSolverSettings const& getSettings() const; - + + virtual LinearEquationSolverProblemFormat getEquationProblemFormat() const override; + private: virtual uint64_t getMatrixRowCount() const override; virtual uint64_t getMatrixColumnCount() const override; @@ -86,8 +89,9 @@ namespace storm { template class EigenLinearEquationSolverFactory : public LinearEquationSolverFactory { public: - virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const override; - virtual std::unique_ptr> create(storm::storage::SparseMatrix&& matrix) const override; + using LinearEquationSolverFactory::create; + + virtual std::unique_ptr> create() const override; EigenLinearEquationSolverSettings& getSettings(); EigenLinearEquationSolverSettings const& getSettings() const; diff --git a/src/storm/solver/EliminationLinearEquationSolver.cpp b/src/storm/solver/EliminationLinearEquationSolver.cpp index 6bfac7031..94aba88f5 100644 --- a/src/storm/solver/EliminationLinearEquationSolver.cpp +++ b/src/storm/solver/EliminationLinearEquationSolver.cpp @@ -33,6 +33,11 @@ namespace storm { return order; } + template + EliminationLinearEquationSolver::EliminationLinearEquationSolver(EliminationLinearEquationSolverSettings const& settings) : settings(settings) { + // Intentionally left empty. + } + template EliminationLinearEquationSolver::EliminationLinearEquationSolver(storm::storage::SparseMatrix const& A, EliminationLinearEquationSolverSettings const& settings) : localA(nullptr), A(nullptr), settings(settings) { this->setMatrix(A); @@ -64,18 +69,8 @@ namespace storm { // but arbitrary matrices require pivoting, which is not currently implemented. STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with elimination"); - - // We need to revert the transformation into an equation system matrix, because the elimination procedure - // and the distance computation is based on the probability matrix instead. - storm::storage::SparseMatrix locallyConvertedMatrix; - if (localA) { - localA->convertToEquationSystem(); - } else { - locallyConvertedMatrix = *A; - locallyConvertedMatrix.convertToEquationSystem(); - } - - storm::storage::SparseMatrix const& transitionMatrix = localA ? *localA : locallyConvertedMatrix; + + storm::storage::SparseMatrix const& transitionMatrix = localA ? *localA : *A; storm::storage::SparseMatrix backwardTransitions = transitionMatrix.transpose(); // Initialize the solution to the right-hand side of the equation system. @@ -106,11 +101,6 @@ namespace storm { eliminator.eliminateState(state, false); } - // After having solved the system, we need to revert the transition system if we kept it local. - if (localA) { - localA->convertToEquationSystem(); - } - return true; } @@ -141,6 +131,11 @@ namespace storm { return settings; } + template + LinearEquationSolverProblemFormat EliminationLinearEquationSolver::getEquationProblemFormat() const { + return LinearEquationSolverProblemFormat::FixedPointSystem; + } + template uint64_t EliminationLinearEquationSolver::getMatrixRowCount() const { return this->A->getRowCount(); @@ -152,13 +147,8 @@ namespace storm { } template - std::unique_ptr> EliminationLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - return std::make_unique>(matrix, settings); - } - - template - std::unique_ptr> EliminationLinearEquationSolverFactory::create(storm::storage::SparseMatrix&& matrix) const { - return std::make_unique>(std::move(matrix), settings); + std::unique_ptr> EliminationLinearEquationSolverFactory::create() const { + return std::make_unique>(settings); } template diff --git a/src/storm/solver/EliminationLinearEquationSolver.h b/src/storm/solver/EliminationLinearEquationSolver.h index a2a59e97a..30d0277b0 100644 --- a/src/storm/solver/EliminationLinearEquationSolver.h +++ b/src/storm/solver/EliminationLinearEquationSolver.h @@ -26,6 +26,7 @@ namespace storm { template class EliminationLinearEquationSolver : public LinearEquationSolver { public: + EliminationLinearEquationSolver(EliminationLinearEquationSolverSettings const& settings = EliminationLinearEquationSolverSettings()); EliminationLinearEquationSolver(storm::storage::SparseMatrix const& A, EliminationLinearEquationSolverSettings const& settings = EliminationLinearEquationSolverSettings()); EliminationLinearEquationSolver(storm::storage::SparseMatrix&& A, EliminationLinearEquationSolverSettings const& settings = EliminationLinearEquationSolverSettings()); @@ -38,6 +39,8 @@ namespace storm { EliminationLinearEquationSolverSettings& getSettings(); EliminationLinearEquationSolverSettings const& getSettings() const; + virtual LinearEquationSolverProblemFormat getEquationProblemFormat() const override; + private: void initializeSettings(); @@ -59,8 +62,9 @@ namespace storm { template class EliminationLinearEquationSolverFactory : public LinearEquationSolverFactory { public: - virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const override; - virtual std::unique_ptr> create(storm::storage::SparseMatrix&& matrix) const override; + using LinearEquationSolverFactory::create; + + virtual std::unique_ptr> create() const override; EliminationLinearEquationSolverSettings& getSettings(); EliminationLinearEquationSolverSettings const& getSettings() const; diff --git a/src/storm/solver/GmmxxLinearEquationSolver.cpp b/src/storm/solver/GmmxxLinearEquationSolver.cpp index b922a1b9c..f7aea79a9 100644 --- a/src/storm/solver/GmmxxLinearEquationSolver.cpp +++ b/src/storm/solver/GmmxxLinearEquationSolver.cpp @@ -101,6 +101,11 @@ namespace storm { return restart; } + template + GmmxxLinearEquationSolver::GmmxxLinearEquationSolver(GmmxxLinearEquationSolverSettings const& settings) : settings(settings) { + // Intentionally left empty. + } + template GmmxxLinearEquationSolver::GmmxxLinearEquationSolver(storm::storage::SparseMatrix const& A, GmmxxLinearEquationSolverSettings const& settings) : settings(settings) { this->setMatrix(A); @@ -227,6 +232,11 @@ namespace storm { return settings; } + template + LinearEquationSolverProblemFormat GmmxxLinearEquationSolver::getEquationProblemFormat() const { + return LinearEquationSolverProblemFormat::EquationSystem; + } + template void GmmxxLinearEquationSolver::clearCache() const { iluPreconditioner.reset(); @@ -245,13 +255,8 @@ namespace storm { } template - std::unique_ptr> GmmxxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - return std::make_unique>(matrix, settings); - } - - template - std::unique_ptr> GmmxxLinearEquationSolverFactory::create(storm::storage::SparseMatrix&& matrix) const { - return std::make_unique>(std::move(matrix), settings); + std::unique_ptr> GmmxxLinearEquationSolverFactory::create() const { + return std::make_unique>(settings); } template diff --git a/src/storm/solver/GmmxxLinearEquationSolver.h b/src/storm/solver/GmmxxLinearEquationSolver.h index cce3a6369..95cb10757 100644 --- a/src/storm/solver/GmmxxLinearEquationSolver.h +++ b/src/storm/solver/GmmxxLinearEquationSolver.h @@ -81,6 +81,7 @@ namespace storm { template class GmmxxLinearEquationSolver : public LinearEquationSolver { public: + GmmxxLinearEquationSolver(GmmxxLinearEquationSolverSettings const& settings = GmmxxLinearEquationSolverSettings()); GmmxxLinearEquationSolver(storm::storage::SparseMatrix const& A, GmmxxLinearEquationSolverSettings const& settings = GmmxxLinearEquationSolverSettings()); GmmxxLinearEquationSolver(storm::storage::SparseMatrix&& A, GmmxxLinearEquationSolverSettings const& settings = GmmxxLinearEquationSolverSettings()); @@ -97,6 +98,8 @@ namespace storm { void setSettings(GmmxxLinearEquationSolverSettings const& newSettings); GmmxxLinearEquationSolverSettings const& getSettings() const; + virtual LinearEquationSolverProblemFormat getEquationProblemFormat() const override; + virtual void clearCache() const override; private: @@ -120,8 +123,9 @@ namespace storm { template class GmmxxLinearEquationSolverFactory : public LinearEquationSolverFactory { public: - virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const override; - virtual std::unique_ptr> create(storm::storage::SparseMatrix&& matrix) const override; + using LinearEquationSolverFactory::create; + + virtual std::unique_ptr> create() const override; GmmxxLinearEquationSolverSettings& getSettings(); GmmxxLinearEquationSolverSettings const& getSettings() const; diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index 606946402..6abfaf270 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -127,8 +127,11 @@ namespace storm { std::vector& subB = *auxiliaryRowGroupVector; // Resolve the nondeterminism according to the current scheduler. - storm::storage::SparseMatrix submatrix = this->A->selectRowsFromRowGroups(scheduler, true); - submatrix.convertToEquationSystem(); + bool convertToEquationSystem = this->linearEquationSolverFactory->getEquationProblemFormat() == LinearEquationSolverProblemFormat::EquationSystem; + storm::storage::SparseMatrix submatrix = this->A->selectRowsFromRowGroups(scheduler, convertToEquationSystem); + if (convertToEquationSystem) { + 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. @@ -256,8 +259,11 @@ namespace storm { if (this->hasInitialScheduler()) { // Resolve the nondeterminism according to the initial scheduler. - storm::storage::SparseMatrix submatrix = this->A->selectRowsFromRowGroups(this->getInitialScheduler(), true); - submatrix.convertToEquationSystem(); + bool convertToEquationSystem = this->linearEquationSolverFactory->getEquationProblemFormat() == LinearEquationSolverProblemFormat::EquationSystem; + storm::storage::SparseMatrix submatrix = this->A->selectRowsFromRowGroups(this->getInitialScheduler(), convertToEquationSystem); + if (convertToEquationSystem) { + submatrix.convertToEquationSystem(); + } storm::utility::vector::selectVectorValues(*auxiliaryRowGroupVector, this->getInitialScheduler(), this->A->getRowGroupIndices(), b); // Solve the resulting equation system. diff --git a/src/storm/solver/LinearEquationSolver.cpp b/src/storm/solver/LinearEquationSolver.cpp index bdcc4041e..2efc90f8f 100644 --- a/src/storm/solver/LinearEquationSolver.cpp +++ b/src/storm/solver/LinearEquationSolver.cpp @@ -137,30 +137,33 @@ namespace storm { } template - std::unique_ptr> LinearEquationSolverFactory::create(storm::storage::SparseMatrix&& matrix) const { - return create(matrix); + std::unique_ptr> LinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { + std::unique_ptr> solver = this->create(); + solver->setMatrix(matrix); + return solver; } template - std::unique_ptr> GeneralLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - return selectSolver(matrix); + std::unique_ptr> LinearEquationSolverFactory::create(storm::storage::SparseMatrix&& matrix) const { + std::unique_ptr> solver = this->create(); + solver->setMatrix(std::move(matrix)); + return solver; } template - std::unique_ptr> GeneralLinearEquationSolverFactory::create(storm::storage::SparseMatrix&& matrix) const { - return selectSolver(std::move(matrix)); + LinearEquationSolverProblemFormat LinearEquationSolverFactory::getEquationProblemFormat() const { + return this->create()->getEquationProblemFormat(); } template - template - std::unique_ptr> GeneralLinearEquationSolverFactory::selectSolver(MatrixType&& matrix) const { + std::unique_ptr> GeneralLinearEquationSolverFactory::create() const { EquationSolverType equationSolver = storm::settings::getModule().getEquationSolver(); switch (equationSolver) { - case EquationSolverType::Gmmxx: return std::make_unique>(std::forward(matrix)); - case EquationSolverType::Native: return std::make_unique>(std::forward(matrix)); - case EquationSolverType::Eigen: return std::make_unique>(std::forward(matrix)); - case EquationSolverType::Elimination: return std::make_unique>(std::forward(matrix)); - default: return std::make_unique>(std::forward(matrix)); + case EquationSolverType::Gmmxx: return std::make_unique>(); + case EquationSolverType::Native: return std::make_unique>(); + case EquationSolverType::Eigen: return std::make_unique>(); + case EquationSolverType::Elimination: return std::make_unique>(); + default: return std::make_unique>(); } } @@ -170,20 +173,11 @@ namespace storm { } #ifdef STORM_HAVE_CARL - std::unique_ptr> GeneralLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - return selectSolver(matrix); - } - - std::unique_ptr> GeneralLinearEquationSolverFactory::create(storm::storage::SparseMatrix&& matrix) const { - return selectSolver(std::move(matrix)); - } - - template - std::unique_ptr> GeneralLinearEquationSolverFactory::selectSolver(MatrixType&& matrix) const { + std::unique_ptr> GeneralLinearEquationSolverFactory::create() const { EquationSolverType equationSolver = storm::settings::getModule().getEquationSolver(); switch (equationSolver) { - case EquationSolverType::Elimination: return std::make_unique>(std::forward(matrix)); - default: return std::make_unique>(std::forward(matrix)); + case EquationSolverType::Elimination: return std::make_unique>(); + default: return std::make_unique>(); } } @@ -191,20 +185,11 @@ namespace storm { return std::make_unique>(*this); } - std::unique_ptr> GeneralLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - return selectSolver(matrix); - } - - std::unique_ptr> GeneralLinearEquationSolverFactory::create(storm::storage::SparseMatrix&& matrix) const { - return selectSolver(std::move(matrix)); - } - - template - std::unique_ptr> GeneralLinearEquationSolverFactory::selectSolver(MatrixType&& matrix) const { + std::unique_ptr> GeneralLinearEquationSolverFactory::create() const { EquationSolverType equationSolver = storm::settings::getModule().getEquationSolver(); switch (equationSolver) { - case EquationSolverType::Elimination: return std::make_unique>(std::forward(matrix)); - default: return std::make_unique>(std::forward(matrix)); + case EquationSolverType::Elimination: return std::make_unique>(); + default: return std::make_unique>(); } } diff --git a/src/storm/solver/LinearEquationSolver.h b/src/storm/solver/LinearEquationSolver.h index 1d3eb5a83..aa14226bf 100644 --- a/src/storm/solver/LinearEquationSolver.h +++ b/src/storm/solver/LinearEquationSolver.h @@ -6,6 +6,7 @@ #include "storm/solver/AbstractEquationSolver.h" #include "storm/solver/MultiplicationStyle.h" +#include "storm/solver/LinearEquationSolverProblemFormat.h" #include "storm/solver/OptimizationDirection.h" #include "storm/utility/VectorHelper.h" @@ -36,12 +37,13 @@ namespace storm { virtual void setMatrix(storm::storage::SparseMatrix&& A) = 0; /*! - * Solves the equation system A*x = b. The matrix A is required to be square and have a unique solution. - * The solution of the set of linear equations will be written to the vector x. Note that the matrix A has - * to be given upon construction time of the solver object. + * If the solver expects the equation system format, it solves Ax = b. If it it expects a fixed point + * format, it solves Ax + b = x. In both versions, the matrix A is required to be square and the problem + * is required to have a unique solution. The solution will be written to the vector x. Note that the matrix + * A has to be given upon construction time of the solver object. * * @param x The solution vector that has to be computed. Its length must be equal to the number of rows of A. - * @param b The right-hand side of the equation system. Its length must be equal to the number of rows of A. + * @param b The vector b. Its length must be equal to the number of rows of A. * * @return true */ @@ -119,6 +121,12 @@ namespace storm { */ void repeatedMultiply(std::vector& x, std::vector const* b, uint_fast64_t n) const; + /*! + * Retrieves the format in which this solver expects to solve equations. If the solver expects the equation + * system format, it solves Ax = b. If it it expects a fixed point format, it solves Ax + b = x. + */ + virtual LinearEquationSolverProblemFormat getEquationProblemFormat() const = 0; + /*! * Sets whether some of the generated data during solver calls should be cached. * This possibly increases the runtime of subsequent calls but also increases memory consumption. @@ -187,7 +195,7 @@ namespace storm { * @param matrix The matrix that defines the equation system. * @return A pointer to the newly created solver. */ - virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const = 0; + std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const; /*! * Creates a new linear equation solver instance with the given matrix. The caller gives up posession of the @@ -196,52 +204,53 @@ namespace storm { * @param matrix The matrix that defines the equation system. * @return A pointer to the newly created solver. */ - virtual std::unique_ptr> create(storm::storage::SparseMatrix&& matrix) const; + std::unique_ptr> create(storm::storage::SparseMatrix&& matrix) const; + + /*! + * Creates an equation solver with the current settings, but without a matrix. + */ + virtual std::unique_ptr> create() const = 0; /*! * Creates a copy of this factory. */ virtual std::unique_ptr> clone() const = 0; + + /*! + * Retrieves the problem format that the solver expects if it was created with the current settings. + */ + virtual LinearEquationSolverProblemFormat getEquationProblemFormat() const; }; template class GeneralLinearEquationSolverFactory : public LinearEquationSolverFactory { public: - virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const override; - virtual std::unique_ptr> create(storm::storage::SparseMatrix&& matrix) const override; + using LinearEquationSolverFactory::create; - virtual std::unique_ptr> clone() const override; + virtual std::unique_ptr> create() const override; - private: - template - std::unique_ptr> selectSolver(MatrixType&& matrix) const; + virtual std::unique_ptr> clone() const override; }; #ifdef STORM_HAVE_CARL template<> class GeneralLinearEquationSolverFactory : public LinearEquationSolverFactory { public: - virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const override; - virtual std::unique_ptr> create(storm::storage::SparseMatrix&& matrix) const override; + using LinearEquationSolverFactory::create; - virtual std::unique_ptr> clone() const override; + virtual std::unique_ptr> create() const override; - private: - template - std::unique_ptr> selectSolver(MatrixType&& matrix) const; + virtual std::unique_ptr> clone() const override; }; template<> class GeneralLinearEquationSolverFactory : public LinearEquationSolverFactory { public: - virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const override; - virtual std::unique_ptr> create(storm::storage::SparseMatrix&& matrix) const override; + using LinearEquationSolverFactory::create; - virtual std::unique_ptr> clone() const override; + virtual std::unique_ptr> create() const override; - private: - template - std::unique_ptr> selectSolver(MatrixType&& matrix) const; + virtual std::unique_ptr> clone() const override; }; #endif } // namespace solver diff --git a/src/storm/solver/LinearEquationSolverProblemFormat.cpp b/src/storm/solver/LinearEquationSolverProblemFormat.cpp new file mode 100644 index 000000000..9c7756cd4 --- /dev/null +++ b/src/storm/solver/LinearEquationSolverProblemFormat.cpp @@ -0,0 +1,15 @@ +#include "storm/solver/LinearEquationSolverProblemFormat.h" + +namespace storm { + namespace solver { + + std::ostream& operator<<(std::ostream& out, LinearEquationSolverProblemFormat const& format) { + switch (format) { + case LinearEquationSolverProblemFormat::EquationSystem: out << "equation system"; break; + case LinearEquationSolverProblemFormat::FixedPointSystem: out << "fixed point system"; break; + } + return out; + } + + } +} diff --git a/src/storm/solver/LinearEquationSolverProblemFormat.h b/src/storm/solver/LinearEquationSolverProblemFormat.h new file mode 100644 index 000000000..c15d4c9cd --- /dev/null +++ b/src/storm/solver/LinearEquationSolverProblemFormat.h @@ -0,0 +1,15 @@ +#pragma once + +#include + +namespace storm { + namespace solver { + + enum class LinearEquationSolverProblemFormat { + EquationSystem, FixedPointSystem + }; + + std::ostream& operator<<(std::ostream& out, LinearEquationSolverProblemFormat const& format); + + } +} diff --git a/src/storm/solver/NativeLinearEquationSolver.cpp b/src/storm/solver/NativeLinearEquationSolver.cpp index 05dc06515..fa2dbc237 100644 --- a/src/storm/solver/NativeLinearEquationSolver.cpp +++ b/src/storm/solver/NativeLinearEquationSolver.cpp @@ -28,6 +28,8 @@ namespace storm { method = SolutionMethod::WalkerChae; } else if (methodAsSetting == storm::settings::modules::NativeEquationSolverSettings::LinearEquationMethod::Power) { method = SolutionMethod::Power; + } else if (methodAsSetting == storm::settings::modules::NativeEquationSolverSettings::LinearEquationMethod::SoundPower) { + method = SolutionMethod::SoundPower; } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The selected solution technique is invalid for this solver."); } @@ -35,7 +37,8 @@ namespace storm { maximalNumberOfIterations = settings.getMaximalIterationCount(); precision = settings.getPrecision(); relative = settings.getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative; - omega = storm::settings::getModule().getOmega(); + omega = settings.getOmega(); + multiplicationStyle = settings.getPowerMethodMultiplicationStyle(); } template @@ -63,6 +66,11 @@ namespace storm { this->omega = omega; } + template + void NativeLinearEquationSolverSettings::setPowerMethodMultiplicationStyle(MultiplicationStyle value) { + this->multiplicationStyle = value; + } + template typename NativeLinearEquationSolverSettings::SolutionMethod NativeLinearEquationSolverSettings::getSolutionMethod() const { return method; @@ -88,6 +96,16 @@ namespace storm { return omega; } + template + MultiplicationStyle NativeLinearEquationSolverSettings::getPowerMethodMultiplicationStyle() const { + return multiplicationStyle; + } + + template + NativeLinearEquationSolver::NativeLinearEquationSolver(NativeLinearEquationSolverSettings const& settings) : localA(nullptr), A(nullptr), settings(settings) { + // Intentionally left empty. + } + template NativeLinearEquationSolver::NativeLinearEquationSolver(storm::storage::SparseMatrix const& A, NativeLinearEquationSolverSettings const& settings) : localA(nullptr), A(nullptr), settings(settings) { this->setMatrix(A); @@ -344,22 +362,8 @@ namespace storm { template bool NativeLinearEquationSolver::solveEquationsPower(std::vector& x, std::vector const& b) const { - // FIXME: This solver will not work for all input systems. More concretely, the current implementation will - // not work for systems that have a 0 on the diagonal. This is not a restriction of this technique in general - // but arbitrary matrices require pivoting, which is not currently implemented. STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with NativeLinearEquationSolver (Power)"); - // We need to revert the transformation into an equation system matrix, because the elimination procedure - // and the distance computation is based on the probability matrix instead. - storm::storage::SparseMatrix locallyConvertedMatrix; - if (localA) { - localA->convertToEquationSystem(); - } else { - locallyConvertedMatrix = *A; - locallyConvertedMatrix.convertToEquationSystem(); - } - storm::storage::SparseMatrix const& transitionMatrix = localA ? *localA : locallyConvertedMatrix; - if (!this->cachedRowVector) { this->cachedRowVector = std::make_unique>(getMatrixRowCount()); } @@ -367,10 +371,17 @@ namespace storm { std::vector* currentX = &x; std::vector* nextX = this->cachedRowVector.get(); + bool useGaussSeidelMultiplication = this->getSettings().getPowerMethodMultiplicationStyle() == storm::solver::MultiplicationStyle::GaussSeidel; + bool converged = false; uint64_t iterations = 0; while (!converged && iterations < this->getSettings().getMaximalNumberOfIterations() && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) { - this->multiplier.multAdd(transitionMatrix, *currentX, &b, *nextX); + if (useGaussSeidelMultiplication) { + *nextX = *currentX; + this->multiplier.multAddGaussSeidelBackward(*this->A, *nextX, &b); + } else { + this->multiplier.multAdd(*this->A, *currentX, &b, *nextX); + } // Now check if the process already converged within our precision. converged = storm::utility::vector::equalModuloPrecision(*currentX, *nextX, static_cast(this->getSettings().getPrecision()), this->getSettings().getRelativeTerminationCriterion()); @@ -397,6 +408,11 @@ namespace storm { return converged; } + template + bool NativeLinearEquationSolver::solveEquationsSoundPower(std::vector& x, std::vector const& b) const { + // TODO + } + template bool NativeLinearEquationSolver::solveEquations(std::vector& x, std::vector const& b) const { if (this->getSettings().getSolutionMethod() == NativeLinearEquationSolverSettings::SolutionMethod::SOR || this->getSettings().getSolutionMethod() == NativeLinearEquationSolverSettings::SolutionMethod::GaussSeidel) { @@ -477,6 +493,15 @@ namespace storm { return settings; } + template + LinearEquationSolverProblemFormat NativeLinearEquationSolver::getEquationProblemFormat() const { + if (this->getSettings().getSolutionMethod() == NativeLinearEquationSolverSettings::SolutionMethod::Power || this->getSettings().getSolutionMethod() == NativeLinearEquationSolverSettings::SolutionMethod::SoundPower) { + return LinearEquationSolverProblemFormat::FixedPointSystem; + } else { + return LinearEquationSolverProblemFormat::EquationSystem; + } + } + template void NativeLinearEquationSolver::clearCache() const { jacobiDecomposition.reset(); @@ -495,13 +520,8 @@ namespace storm { } template - std::unique_ptr> NativeLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - return std::make_unique>(matrix, settings); - } - - template - std::unique_ptr> NativeLinearEquationSolverFactory::create(storm::storage::SparseMatrix&& matrix) const { - return std::make_unique>(std::move(matrix), settings); + std::unique_ptr> NativeLinearEquationSolverFactory::create() const { + return std::make_unique>(settings); } template diff --git a/src/storm/solver/NativeLinearEquationSolver.h b/src/storm/solver/NativeLinearEquationSolver.h index 8985e95f5..678aab555 100644 --- a/src/storm/solver/NativeLinearEquationSolver.h +++ b/src/storm/solver/NativeLinearEquationSolver.h @@ -14,7 +14,7 @@ namespace storm { class NativeLinearEquationSolverSettings { public: enum class SolutionMethod { - Jacobi, GaussSeidel, SOR, WalkerChae, Power + Jacobi, GaussSeidel, SOR, WalkerChae, Power, SoundPower }; NativeLinearEquationSolverSettings(); @@ -24,19 +24,22 @@ namespace storm { void setMaximalNumberOfIterations(uint64_t maximalNumberOfIterations); void setRelativeTerminationCriterion(bool value); void setOmega(ValueType omega); - + void setPowerMethodMultiplicationStyle(MultiplicationStyle value); + SolutionMethod getSolutionMethod() const; ValueType getPrecision() const; uint64_t getMaximalNumberOfIterations() const; uint64_t getRelativeTerminationCriterion() const; ValueType getOmega() const; - + MultiplicationStyle getPowerMethodMultiplicationStyle() const; + private: SolutionMethod method; double precision; bool relative; uint_fast64_t maximalNumberOfIterations; ValueType omega; + MultiplicationStyle multiplicationStyle; }; /*! @@ -45,6 +48,7 @@ namespace storm { template class NativeLinearEquationSolver : public LinearEquationSolver { public: + NativeLinearEquationSolver(NativeLinearEquationSolverSettings const& settings = NativeLinearEquationSolverSettings()); NativeLinearEquationSolver(storm::storage::SparseMatrix const& A, NativeLinearEquationSolverSettings const& settings = NativeLinearEquationSolverSettings()); NativeLinearEquationSolver(storm::storage::SparseMatrix&& A, NativeLinearEquationSolverSettings const& settings = NativeLinearEquationSolverSettings()); @@ -61,6 +65,8 @@ namespace storm { void setSettings(NativeLinearEquationSolverSettings const& newSettings); NativeLinearEquationSolverSettings const& getSettings() const; + virtual LinearEquationSolverProblemFormat getEquationProblemFormat() const override; + virtual void clearCache() const override; private: @@ -71,6 +77,7 @@ namespace storm { virtual bool solveEquationsJacobi(std::vector& x, std::vector const& b) const; virtual bool solveEquationsWalkerChae(std::vector& x, std::vector const& b) const; virtual bool solveEquationsPower(std::vector& x, std::vector const& b) const; + virtual bool solveEquationsSoundPower(std::vector& x, std::vector const& b) const; // 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. @@ -110,8 +117,9 @@ namespace storm { template class NativeLinearEquationSolverFactory : public LinearEquationSolverFactory { public: - virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const override; - virtual std::unique_ptr> create(storm::storage::SparseMatrix&& matrix) const override; + using LinearEquationSolverFactory::create; + + virtual std::unique_ptr> create() const override; NativeLinearEquationSolverSettings& getSettings(); NativeLinearEquationSolverSettings const& getSettings() const; diff --git a/src/storm/solver/StandardGameSolver.cpp b/src/storm/solver/StandardGameSolver.cpp index af38b7a8c..f522b3ffa 100644 --- a/src/storm/solver/StandardGameSolver.cpp +++ b/src/storm/solver/StandardGameSolver.cpp @@ -115,7 +115,9 @@ namespace storm { // Solve the equation system induced by the two schedulers. storm::storage::SparseMatrix submatrix; getInducedMatrixVector(x, b, player1Choices, player2Choices, submatrix, subB); - submatrix.convertToEquationSystem(); + if (this->linearEquationSolverFactory->getEquationProblemFormat() == LinearEquationSolverProblemFormat::EquationSystem) { + submatrix.convertToEquationSystem(); + } auto submatrixSolver = linearEquationSolverFactory->create(std::move(submatrix)); if (this->lowerBound) { submatrixSolver->setLowerBound(this->lowerBound.get()); } if (this->upperBound) { submatrixSolver->setUpperBound(this->upperBound.get()); } @@ -206,7 +208,9 @@ namespace storm { // Solve the equation system induced by the two schedulers. storm::storage::SparseMatrix submatrix; getInducedMatrixVector(x, b, this->player1ChoicesHint.get(), this->player2ChoicesHint.get(), submatrix, *auxiliaryP1RowGroupVector); - submatrix.convertToEquationSystem(); + if (this->linearEquationSolverFactory->getEquationProblemFormat() == LinearEquationSolverProblemFormat::EquationSystem) { + submatrix.convertToEquationSystem(); + } auto submatrixSolver = linearEquationSolverFactory->create(std::move(submatrix)); if (this->lowerBound) { submatrixSolver->setLowerBound(this->lowerBound.get()); } if (this->upperBound) { submatrixSolver->setUpperBound(this->upperBound.get()); } @@ -443,4 +447,4 @@ namespace storm { template class StandardGameSolverSettings; template class StandardGameSolver; } -} \ No newline at end of file +} diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 258493bd6..e2e15b7bc 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -1369,7 +1369,7 @@ namespace storm { *resultIterator = storm::utility::zero(); } - for (ite = this->begin() + *rowIterator - 1; it != ite; ++it) { + for (ite = this->begin() + *rowIterator - 1; it != ite; --it) { *resultIterator += it->getValue() * vector[it->getColumn()]; } }