Browse Source

introducing solver formats to enable linear equation solvers to take the fixed point rather than the equation system formulation

tempestpy_adaptions
dehnert 7 years ago
parent
commit
ec61e110f2
  1. 13
      src/storm/exceptions/FormatUnsupportedBySolverException.h
  2. 5
      src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
  3. 22
      src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
  4. 28
      src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
  5. 21
      src/storm/settings/modules/NativeEquationSolverSettings.cpp
  6. 12
      src/storm/settings/modules/NativeEquationSolverSettings.h
  7. 21
      src/storm/solver/EigenLinearEquationSolver.cpp
  8. 10
      src/storm/solver/EigenLinearEquationSolver.h
  9. 38
      src/storm/solver/EliminationLinearEquationSolver.cpp
  10. 8
      src/storm/solver/EliminationLinearEquationSolver.h
  11. 19
      src/storm/solver/GmmxxLinearEquationSolver.cpp
  12. 8
      src/storm/solver/GmmxxLinearEquationSolver.h
  13. 14
      src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
  14. 59
      src/storm/solver/LinearEquationSolver.cpp
  15. 57
      src/storm/solver/LinearEquationSolver.h
  16. 15
      src/storm/solver/LinearEquationSolverProblemFormat.cpp
  17. 15
      src/storm/solver/LinearEquationSolverProblemFormat.h
  18. 66
      src/storm/solver/NativeLinearEquationSolver.cpp
  19. 18
      src/storm/solver/NativeLinearEquationSolver.h
  20. 10
      src/storm/solver/StandardGameSolver.cpp
  21. 2
      src/storm/storage/SparseMatrix.cpp

13
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

5
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<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(std::move(bsccEquationSystem));
solver->solveEquations(bsccEquationSystemSolution, bsccEquationSystemRightSide);
}
@ -557,6 +560,8 @@ namespace storm {
rewardSolution = std::vector<ValueType>(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<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(std::move(rewardEquationSystemMatrix));
solver->solveEquations(rewardSolution, rewardRightSide);
}

22
src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp

@ -59,11 +59,16 @@ namespace storm {
prob1StatesAsColumn = prob1StatesAsColumn.swapVariables(model.getRowColumnMetaVariablePairs());
storm::dd::Add<DdType, ValueType> 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<ValueType> x(maybeStates.getNonZeroCount(), storm::utility::convertNumber<ValueType>(0.5));
@ -224,10 +229,15 @@ namespace storm {
// Then compute the state reward vector to use in the computation.
storm::dd::Add<DdType, ValueType> 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<ValueType> x(maybeStates.getNonZeroCount(), storm::utility::convertNumber<ValueType>(0.5));

28
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<ValueType> 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<ValueType> 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<ValueType>(result, maybeStates, storm::utility::one<ValueType>());
} 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<ValueType> 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<ValueType> 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.

21
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<std::string> methods = { "jacobi", "gaussseidel", "sor", "walkerchae", "power" };
std::vector<std::string> 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<std::string> 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();

12
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

21
src/storm/solver/EigenLinearEquationSolver.cpp

@ -106,10 +106,15 @@ namespace storm {
#endif
template<typename ValueType>
EigenLinearEquationSolver<ValueType>::EigenLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, EigenLinearEquationSolverSettings<ValueType> const& settings) : eigenA(storm::adapters::EigenAdapter::toEigenSparseMatrix<ValueType>(A)), settings(settings) {
EigenLinearEquationSolver<ValueType>::EigenLinearEquationSolver(EigenLinearEquationSolverSettings<ValueType> const& settings) : settings(settings) {
// Intentionally left empty.
}
template<typename ValueType>
EigenLinearEquationSolver<ValueType>::EigenLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, EigenLinearEquationSolverSettings<ValueType> const& settings) : settings(settings) {
this->setMatrix(A);
}
template<typename ValueType>
EigenLinearEquationSolver<ValueType>::EigenLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, EigenLinearEquationSolverSettings<ValueType> const& settings) : settings(settings) {
this->setMatrix(std::move(A));
@ -299,6 +304,11 @@ namespace storm {
return settings;
}
template<typename ValueType>
LinearEquationSolverProblemFormat EigenLinearEquationSolver<ValueType>::getEquationProblemFormat() const {
LinearEquationSolverProblemFormat::EquationSystem;
}
template<typename ValueType>
EigenLinearEquationSolverSettings<ValueType> const& EigenLinearEquationSolver<ValueType>::getSettings() const {
return settings;
@ -347,13 +357,8 @@ namespace storm {
#endif
template<typename ValueType>
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> EigenLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const {
return std::make_unique<storm::solver::EigenLinearEquationSolver<ValueType>>(matrix, settings);
}
template<typename ValueType>
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> EigenLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType>&& matrix) const {
return std::make_unique<storm::solver::EigenLinearEquationSolver<ValueType>>(std::move(matrix), settings);
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> EigenLinearEquationSolverFactory<ValueType>::create() const {
return std::make_unique<storm::solver::EigenLinearEquationSolver<ValueType>>(settings);
}
template<typename ValueType>

10
src/storm/solver/EigenLinearEquationSolver.h

@ -60,6 +60,7 @@ namespace storm {
template<typename ValueType>
class EigenLinearEquationSolver : public LinearEquationSolver<ValueType> {
public:
EigenLinearEquationSolver(EigenLinearEquationSolverSettings<ValueType> const& settings = EigenLinearEquationSolverSettings<ValueType>());
EigenLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, EigenLinearEquationSolverSettings<ValueType> const& settings = EigenLinearEquationSolverSettings<ValueType>());
EigenLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, EigenLinearEquationSolverSettings<ValueType> const& settings = EigenLinearEquationSolverSettings<ValueType>());
@ -71,7 +72,9 @@ namespace storm {
EigenLinearEquationSolverSettings<ValueType>& getSettings();
EigenLinearEquationSolverSettings<ValueType> 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<typename ValueType>
class EigenLinearEquationSolverFactory : public LinearEquationSolverFactory<ValueType> {
public:
virtual std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const override;
virtual std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType>&& matrix) const override;
using LinearEquationSolverFactory<ValueType>::create;
virtual std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> create() const override;
EigenLinearEquationSolverSettings<ValueType>& getSettings();
EigenLinearEquationSolverSettings<ValueType> const& getSettings() const;

38
src/storm/solver/EliminationLinearEquationSolver.cpp

@ -33,6 +33,11 @@ namespace storm {
return order;
}
template<typename ValueType>
EliminationLinearEquationSolver<ValueType>::EliminationLinearEquationSolver(EliminationLinearEquationSolverSettings<ValueType> const& settings) : settings(settings) {
// Intentionally left empty.
}
template<typename ValueType>
EliminationLinearEquationSolver<ValueType>::EliminationLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, EliminationLinearEquationSolverSettings<ValueType> 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<ValueType> locallyConvertedMatrix;
if (localA) {
localA->convertToEquationSystem();
} else {
locallyConvertedMatrix = *A;
locallyConvertedMatrix.convertToEquationSystem();
}
storm::storage::SparseMatrix<ValueType> const& transitionMatrix = localA ? *localA : locallyConvertedMatrix;
storm::storage::SparseMatrix<ValueType> const& transitionMatrix = localA ? *localA : *A;
storm::storage::SparseMatrix<ValueType> 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<typename ValueType>
LinearEquationSolverProblemFormat EliminationLinearEquationSolver<ValueType>::getEquationProblemFormat() const {
return LinearEquationSolverProblemFormat::FixedPointSystem;
}
template<typename ValueType>
uint64_t EliminationLinearEquationSolver<ValueType>::getMatrixRowCount() const {
return this->A->getRowCount();
@ -152,13 +147,8 @@ namespace storm {
}
template<typename ValueType>
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> EliminationLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const {
return std::make_unique<storm::solver::EliminationLinearEquationSolver<ValueType>>(matrix, settings);
}
template<typename ValueType>
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> EliminationLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType>&& matrix) const {
return std::make_unique<storm::solver::EliminationLinearEquationSolver<ValueType>>(std::move(matrix), settings);
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> EliminationLinearEquationSolverFactory<ValueType>::create() const {
return std::make_unique<storm::solver::EliminationLinearEquationSolver<ValueType>>(settings);
}
template<typename ValueType>

8
src/storm/solver/EliminationLinearEquationSolver.h

@ -26,6 +26,7 @@ namespace storm {
template<typename ValueType>
class EliminationLinearEquationSolver : public LinearEquationSolver<ValueType> {
public:
EliminationLinearEquationSolver(EliminationLinearEquationSolverSettings<ValueType> const& settings = EliminationLinearEquationSolverSettings<ValueType>());
EliminationLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, EliminationLinearEquationSolverSettings<ValueType> const& settings = EliminationLinearEquationSolverSettings<ValueType>());
EliminationLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, EliminationLinearEquationSolverSettings<ValueType> const& settings = EliminationLinearEquationSolverSettings<ValueType>());
@ -38,6 +39,8 @@ namespace storm {
EliminationLinearEquationSolverSettings<ValueType>& getSettings();
EliminationLinearEquationSolverSettings<ValueType> const& getSettings() const;
virtual LinearEquationSolverProblemFormat getEquationProblemFormat() const override;
private:
void initializeSettings();
@ -59,8 +62,9 @@ namespace storm {
template<typename ValueType>
class EliminationLinearEquationSolverFactory : public LinearEquationSolverFactory<ValueType> {
public:
virtual std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const override;
virtual std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType>&& matrix) const override;
using LinearEquationSolverFactory<ValueType>::create;
virtual std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> create() const override;
EliminationLinearEquationSolverSettings<ValueType>& getSettings();
EliminationLinearEquationSolverSettings<ValueType> const& getSettings() const;

19
src/storm/solver/GmmxxLinearEquationSolver.cpp

@ -101,6 +101,11 @@ namespace storm {
return restart;
}
template<typename ValueType>
GmmxxLinearEquationSolver<ValueType>::GmmxxLinearEquationSolver(GmmxxLinearEquationSolverSettings<ValueType> const& settings) : settings(settings) {
// Intentionally left empty.
}
template<typename ValueType>
GmmxxLinearEquationSolver<ValueType>::GmmxxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, GmmxxLinearEquationSolverSettings<ValueType> const& settings) : settings(settings) {
this->setMatrix(A);
@ -227,6 +232,11 @@ namespace storm {
return settings;
}
template<typename ValueType>
LinearEquationSolverProblemFormat GmmxxLinearEquationSolver<ValueType>::getEquationProblemFormat() const {
return LinearEquationSolverProblemFormat::EquationSystem;
}
template<typename ValueType>
void GmmxxLinearEquationSolver<ValueType>::clearCache() const {
iluPreconditioner.reset();
@ -245,13 +255,8 @@ namespace storm {
}
template<typename ValueType>
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> GmmxxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const {
return std::make_unique<storm::solver::GmmxxLinearEquationSolver<ValueType>>(matrix, settings);
}
template<typename ValueType>
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> GmmxxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType>&& matrix) const {
return std::make_unique<storm::solver::GmmxxLinearEquationSolver<ValueType>>(std::move(matrix), settings);
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> GmmxxLinearEquationSolverFactory<ValueType>::create() const {
return std::make_unique<storm::solver::GmmxxLinearEquationSolver<ValueType>>(settings);
}
template<typename ValueType>

8
src/storm/solver/GmmxxLinearEquationSolver.h

@ -81,6 +81,7 @@ namespace storm {
template<typename ValueType>
class GmmxxLinearEquationSolver : public LinearEquationSolver<ValueType> {
public:
GmmxxLinearEquationSolver(GmmxxLinearEquationSolverSettings<ValueType> const& settings = GmmxxLinearEquationSolverSettings<ValueType>());
GmmxxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, GmmxxLinearEquationSolverSettings<ValueType> const& settings = GmmxxLinearEquationSolverSettings<ValueType>());
GmmxxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, GmmxxLinearEquationSolverSettings<ValueType> const& settings = GmmxxLinearEquationSolverSettings<ValueType>());
@ -97,6 +98,8 @@ namespace storm {
void setSettings(GmmxxLinearEquationSolverSettings<ValueType> const& newSettings);
GmmxxLinearEquationSolverSettings<ValueType> const& getSettings() const;
virtual LinearEquationSolverProblemFormat getEquationProblemFormat() const override;
virtual void clearCache() const override;
private:
@ -120,8 +123,9 @@ namespace storm {
template<typename ValueType>
class GmmxxLinearEquationSolverFactory : public LinearEquationSolverFactory<ValueType> {
public:
virtual std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const override;
virtual std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType>&& matrix) const override;
using LinearEquationSolverFactory<ValueType>::create;
virtual std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> create() const override;
GmmxxLinearEquationSolverSettings<ValueType>& getSettings();
GmmxxLinearEquationSolverSettings<ValueType> const& getSettings() const;

14
src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp

@ -127,8 +127,11 @@ namespace storm {
std::vector<ValueType>& subB = *auxiliaryRowGroupVector;
// Resolve the nondeterminism according to the current scheduler.
storm::storage::SparseMatrix<ValueType> submatrix = this->A->selectRowsFromRowGroups(scheduler, true);
submatrix.convertToEquationSystem();
bool convertToEquationSystem = this->linearEquationSolverFactory->getEquationProblemFormat() == LinearEquationSolverProblemFormat::EquationSystem;
storm::storage::SparseMatrix<ValueType> submatrix = this->A->selectRowsFromRowGroups(scheduler, convertToEquationSystem);
if (convertToEquationSystem) {
submatrix.convertToEquationSystem();
}
storm::utility::vector::selectVectorValues<ValueType>(subB, scheduler, this->A->getRowGroupIndices(), b);
// Create a solver that we will use throughout the procedure. We will modify the matrix in each iteration.
@ -256,8 +259,11 @@ namespace storm {
if (this->hasInitialScheduler()) {
// Resolve the nondeterminism according to the initial scheduler.
storm::storage::SparseMatrix<ValueType> submatrix = this->A->selectRowsFromRowGroups(this->getInitialScheduler(), true);
submatrix.convertToEquationSystem();
bool convertToEquationSystem = this->linearEquationSolverFactory->getEquationProblemFormat() == LinearEquationSolverProblemFormat::EquationSystem;
storm::storage::SparseMatrix<ValueType> submatrix = this->A->selectRowsFromRowGroups(this->getInitialScheduler(), convertToEquationSystem);
if (convertToEquationSystem) {
submatrix.convertToEquationSystem();
}
storm::utility::vector::selectVectorValues<ValueType>(*auxiliaryRowGroupVector, this->getInitialScheduler(), this->A->getRowGroupIndices(), b);
// Solve the resulting equation system.

59
src/storm/solver/LinearEquationSolver.cpp

@ -137,30 +137,33 @@ namespace storm {
}
template<typename ValueType>
std::unique_ptr<LinearEquationSolver<ValueType>> LinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType>&& matrix) const {
return create(matrix);
std::unique_ptr<LinearEquationSolver<ValueType>> LinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const {
std::unique_ptr<LinearEquationSolver<ValueType>> solver = this->create();
solver->setMatrix(matrix);
return solver;
}
template<typename ValueType>
std::unique_ptr<LinearEquationSolver<ValueType>> GeneralLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const {
return selectSolver(matrix);
std::unique_ptr<LinearEquationSolver<ValueType>> LinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType>&& matrix) const {
std::unique_ptr<LinearEquationSolver<ValueType>> solver = this->create();
solver->setMatrix(std::move(matrix));
return solver;
}
template<typename ValueType>
std::unique_ptr<LinearEquationSolver<ValueType>> GeneralLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType>&& matrix) const {
return selectSolver(std::move(matrix));
LinearEquationSolverProblemFormat LinearEquationSolverFactory<ValueType>::getEquationProblemFormat() const {
return this->create()->getEquationProblemFormat();
}
template<typename ValueType>
template<typename MatrixType>
std::unique_ptr<LinearEquationSolver<ValueType>> GeneralLinearEquationSolverFactory<ValueType>::selectSolver(MatrixType&& matrix) const {
std::unique_ptr<LinearEquationSolver<ValueType>> GeneralLinearEquationSolverFactory<ValueType>::create() const {
EquationSolverType equationSolver = storm::settings::getModule<storm::settings::modules::CoreSettings>().getEquationSolver();
switch (equationSolver) {
case EquationSolverType::Gmmxx: return std::make_unique<GmmxxLinearEquationSolver<ValueType>>(std::forward<MatrixType>(matrix));
case EquationSolverType::Native: return std::make_unique<NativeLinearEquationSolver<ValueType>>(std::forward<MatrixType>(matrix));
case EquationSolverType::Eigen: return std::make_unique<EigenLinearEquationSolver<ValueType>>(std::forward<MatrixType>(matrix));
case EquationSolverType::Elimination: return std::make_unique<EliminationLinearEquationSolver<ValueType>>(std::forward<MatrixType>(matrix));
default: return std::make_unique<GmmxxLinearEquationSolver<ValueType>>(std::forward<MatrixType>(matrix));
case EquationSolverType::Gmmxx: return std::make_unique<GmmxxLinearEquationSolver<ValueType>>();
case EquationSolverType::Native: return std::make_unique<NativeLinearEquationSolver<ValueType>>();
case EquationSolverType::Eigen: return std::make_unique<EigenLinearEquationSolver<ValueType>>();
case EquationSolverType::Elimination: return std::make_unique<EliminationLinearEquationSolver<ValueType>>();
default: return std::make_unique<GmmxxLinearEquationSolver<ValueType>>();
}
}
@ -170,20 +173,11 @@ namespace storm {
}
#ifdef STORM_HAVE_CARL
std::unique_ptr<LinearEquationSolver<storm::RationalNumber>> GeneralLinearEquationSolverFactory<storm::RationalNumber>::create(storm::storage::SparseMatrix<storm::RationalNumber> const& matrix) const {
return selectSolver(matrix);
}
std::unique_ptr<LinearEquationSolver<storm::RationalNumber>> GeneralLinearEquationSolverFactory<storm::RationalNumber>::create(storm::storage::SparseMatrix<storm::RationalNumber>&& matrix) const {
return selectSolver(std::move(matrix));
}
template<typename MatrixType>
std::unique_ptr<LinearEquationSolver<storm::RationalNumber>> GeneralLinearEquationSolverFactory<storm::RationalNumber>::selectSolver(MatrixType&& matrix) const {
std::unique_ptr<LinearEquationSolver<storm::RationalNumber>> GeneralLinearEquationSolverFactory<storm::RationalNumber>::create() const {
EquationSolverType equationSolver = storm::settings::getModule<storm::settings::modules::CoreSettings>().getEquationSolver();
switch (equationSolver) {
case EquationSolverType::Elimination: return std::make_unique<EliminationLinearEquationSolver<storm::RationalNumber>>(std::forward<MatrixType>(matrix));
default: return std::make_unique<EigenLinearEquationSolver<storm::RationalNumber>>(std::forward<MatrixType>(matrix));
case EquationSolverType::Elimination: return std::make_unique<EliminationLinearEquationSolver<storm::RationalNumber>>();
default: return std::make_unique<EigenLinearEquationSolver<storm::RationalNumber>>();
}
}
@ -191,20 +185,11 @@ namespace storm {
return std::make_unique<GeneralLinearEquationSolverFactory<storm::RationalNumber>>(*this);
}
std::unique_ptr<LinearEquationSolver<storm::RationalFunction>> GeneralLinearEquationSolverFactory<storm::RationalFunction>::create(storm::storage::SparseMatrix<storm::RationalFunction> const& matrix) const {
return selectSolver(matrix);
}
std::unique_ptr<LinearEquationSolver<storm::RationalFunction>> GeneralLinearEquationSolverFactory<storm::RationalFunction>::create(storm::storage::SparseMatrix<storm::RationalFunction>&& matrix) const {
return selectSolver(std::move(matrix));
}
template<typename MatrixType>
std::unique_ptr<LinearEquationSolver<storm::RationalFunction>> GeneralLinearEquationSolverFactory<storm::RationalFunction>::selectSolver(MatrixType&& matrix) const {
std::unique_ptr<LinearEquationSolver<storm::RationalFunction>> GeneralLinearEquationSolverFactory<storm::RationalFunction>::create() const {
EquationSolverType equationSolver = storm::settings::getModule<storm::settings::modules::CoreSettings>().getEquationSolver();
switch (equationSolver) {
case EquationSolverType::Elimination: return std::make_unique<EliminationLinearEquationSolver<storm::RationalFunction>>(std::forward<MatrixType>(matrix));
default: return std::make_unique<EigenLinearEquationSolver<storm::RationalFunction>>(std::forward<MatrixType>(matrix));
case EquationSolverType::Elimination: return std::make_unique<EliminationLinearEquationSolver<storm::RationalFunction>>();
default: return std::make_unique<EigenLinearEquationSolver<storm::RationalFunction>>();
}
}

57
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<ValueType>&& 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<ValueType>& x, std::vector<ValueType> 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<LinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const = 0;
std::unique_ptr<LinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> 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<LinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType>&& matrix) const;
std::unique_ptr<LinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType>&& matrix) const;
/*!
* Creates an equation solver with the current settings, but without a matrix.
*/
virtual std::unique_ptr<LinearEquationSolver<ValueType>> create() const = 0;
/*!
* Creates a copy of this factory.
*/
virtual std::unique_ptr<LinearEquationSolverFactory<ValueType>> clone() const = 0;
/*!
* Retrieves the problem format that the solver expects if it was created with the current settings.
*/
virtual LinearEquationSolverProblemFormat getEquationProblemFormat() const;
};
template<typename ValueType>
class GeneralLinearEquationSolverFactory : public LinearEquationSolverFactory<ValueType> {
public:
virtual std::unique_ptr<LinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const override;
virtual std::unique_ptr<LinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType>&& matrix) const override;
using LinearEquationSolverFactory<ValueType>::create;
virtual std::unique_ptr<LinearEquationSolverFactory<ValueType>> clone() const override;
virtual std::unique_ptr<LinearEquationSolver<ValueType>> create() const override;
private:
template<typename MatrixType>
std::unique_ptr<LinearEquationSolver<ValueType>> selectSolver(MatrixType&& matrix) const;
virtual std::unique_ptr<LinearEquationSolverFactory<ValueType>> clone() const override;
};
#ifdef STORM_HAVE_CARL
template<>
class GeneralLinearEquationSolverFactory<storm::RationalNumber> : public LinearEquationSolverFactory<storm::RationalNumber> {
public:
virtual std::unique_ptr<LinearEquationSolver<storm::RationalNumber>> create(storm::storage::SparseMatrix<storm::RationalNumber> const& matrix) const override;
virtual std::unique_ptr<LinearEquationSolver<storm::RationalNumber>> create(storm::storage::SparseMatrix<storm::RationalNumber>&& matrix) const override;
using LinearEquationSolverFactory<storm::RationalNumber>::create;
virtual std::unique_ptr<LinearEquationSolverFactory<storm::RationalNumber>> clone() const override;
virtual std::unique_ptr<LinearEquationSolver<storm::RationalNumber>> create() const override;
private:
template<typename MatrixType>
std::unique_ptr<LinearEquationSolver<storm::RationalNumber>> selectSolver(MatrixType&& matrix) const;
virtual std::unique_ptr<LinearEquationSolverFactory<storm::RationalNumber>> clone() const override;
};
template<>
class GeneralLinearEquationSolverFactory<storm::RationalFunction> : public LinearEquationSolverFactory<storm::RationalFunction> {
public:
virtual std::unique_ptr<LinearEquationSolver<storm::RationalFunction>> create(storm::storage::SparseMatrix<storm::RationalFunction> const& matrix) const override;
virtual std::unique_ptr<LinearEquationSolver<storm::RationalFunction>> create(storm::storage::SparseMatrix<storm::RationalFunction>&& matrix) const override;
using LinearEquationSolverFactory<storm::RationalFunction>::create;
virtual std::unique_ptr<LinearEquationSolverFactory<storm::RationalFunction>> clone() const override;
virtual std::unique_ptr<LinearEquationSolver<storm::RationalFunction>> create() const override;
private:
template<typename MatrixType>
std::unique_ptr<LinearEquationSolver<storm::RationalFunction>> selectSolver(MatrixType&& matrix) const;
virtual std::unique_ptr<LinearEquationSolverFactory<storm::RationalFunction>> clone() const override;
};
#endif
} // namespace solver

15
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;
}
}
}

15
src/storm/solver/LinearEquationSolverProblemFormat.h

@ -0,0 +1,15 @@
#pragma once
#include <iostream>
namespace storm {
namespace solver {
enum class LinearEquationSolverProblemFormat {
EquationSystem, FixedPointSystem
};
std::ostream& operator<<(std::ostream& out, LinearEquationSolverProblemFormat const& format);
}
}

66
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<storm::settings::modules::NativeEquationSolverSettings>().getOmega();
omega = settings.getOmega();
multiplicationStyle = settings.getPowerMethodMultiplicationStyle();
}
template<typename ValueType>
@ -63,6 +66,11 @@ namespace storm {
this->omega = omega;
}
template<typename ValueType>
void NativeLinearEquationSolverSettings<ValueType>::setPowerMethodMultiplicationStyle(MultiplicationStyle value) {
this->multiplicationStyle = value;
}
template<typename ValueType>
typename NativeLinearEquationSolverSettings<ValueType>::SolutionMethod NativeLinearEquationSolverSettings<ValueType>::getSolutionMethod() const {
return method;
@ -88,6 +96,16 @@ namespace storm {
return omega;
}
template<typename ValueType>
MultiplicationStyle NativeLinearEquationSolverSettings<ValueType>::getPowerMethodMultiplicationStyle() const {
return multiplicationStyle;
}
template<typename ValueType>
NativeLinearEquationSolver<ValueType>::NativeLinearEquationSolver(NativeLinearEquationSolverSettings<ValueType> const& settings) : localA(nullptr), A(nullptr), settings(settings) {
// Intentionally left empty.
}
template<typename ValueType>
NativeLinearEquationSolver<ValueType>::NativeLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, NativeLinearEquationSolverSettings<ValueType> const& settings) : localA(nullptr), A(nullptr), settings(settings) {
this->setMatrix(A);
@ -344,22 +362,8 @@ namespace storm {
template<typename ValueType>
bool NativeLinearEquationSolver<ValueType>::solveEquationsPower(std::vector<ValueType>& x, std::vector<ValueType> 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<ValueType> locallyConvertedMatrix;
if (localA) {
localA->convertToEquationSystem();
} else {
locallyConvertedMatrix = *A;
locallyConvertedMatrix.convertToEquationSystem();
}
storm::storage::SparseMatrix<ValueType> const& transitionMatrix = localA ? *localA : locallyConvertedMatrix;
if (!this->cachedRowVector) {
this->cachedRowVector = std::make_unique<std::vector<ValueType>>(getMatrixRowCount());
}
@ -367,10 +371,17 @@ namespace storm {
std::vector<ValueType>* currentX = &x;
std::vector<ValueType>* 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<ValueType>(*currentX, *nextX, static_cast<ValueType>(this->getSettings().getPrecision()), this->getSettings().getRelativeTerminationCriterion());
@ -397,6 +408,11 @@ namespace storm {
return converged;
}
template<typename ValueType>
bool NativeLinearEquationSolver<ValueType>::solveEquationsSoundPower(std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
// TODO
}
template<typename ValueType>
bool NativeLinearEquationSolver<ValueType>::solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
if (this->getSettings().getSolutionMethod() == NativeLinearEquationSolverSettings<ValueType>::SolutionMethod::SOR || this->getSettings().getSolutionMethod() == NativeLinearEquationSolverSettings<ValueType>::SolutionMethod::GaussSeidel) {
@ -477,6 +493,15 @@ namespace storm {
return settings;
}
template<typename ValueType>
LinearEquationSolverProblemFormat NativeLinearEquationSolver<ValueType>::getEquationProblemFormat() const {
if (this->getSettings().getSolutionMethod() == NativeLinearEquationSolverSettings<ValueType>::SolutionMethod::Power || this->getSettings().getSolutionMethod() == NativeLinearEquationSolverSettings<ValueType>::SolutionMethod::SoundPower) {
return LinearEquationSolverProblemFormat::FixedPointSystem;
} else {
return LinearEquationSolverProblemFormat::EquationSystem;
}
}
template<typename ValueType>
void NativeLinearEquationSolver<ValueType>::clearCache() const {
jacobiDecomposition.reset();
@ -495,13 +520,8 @@ namespace storm {
}
template<typename ValueType>
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> NativeLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const {
return std::make_unique<storm::solver::NativeLinearEquationSolver<ValueType>>(matrix, settings);
}
template<typename ValueType>
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> NativeLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType>&& matrix) const {
return std::make_unique<storm::solver::NativeLinearEquationSolver<ValueType>>(std::move(matrix), settings);
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> NativeLinearEquationSolverFactory<ValueType>::create() const {
return std::make_unique<storm::solver::NativeLinearEquationSolver<ValueType>>(settings);
}
template<typename ValueType>

18
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<typename ValueType>
class NativeLinearEquationSolver : public LinearEquationSolver<ValueType> {
public:
NativeLinearEquationSolver(NativeLinearEquationSolverSettings<ValueType> const& settings = NativeLinearEquationSolverSettings<ValueType>());
NativeLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, NativeLinearEquationSolverSettings<ValueType> const& settings = NativeLinearEquationSolverSettings<ValueType>());
NativeLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, NativeLinearEquationSolverSettings<ValueType> const& settings = NativeLinearEquationSolverSettings<ValueType>());
@ -61,6 +65,8 @@ namespace storm {
void setSettings(NativeLinearEquationSolverSettings<ValueType> const& newSettings);
NativeLinearEquationSolverSettings<ValueType> 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<ValueType>& x, std::vector<ValueType> const& b) const;
virtual bool solveEquationsWalkerChae(std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
virtual bool solveEquationsPower(std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
virtual bool solveEquationsSoundPower(std::vector<ValueType>& x, std::vector<ValueType> 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<typename ValueType>
class NativeLinearEquationSolverFactory : public LinearEquationSolverFactory<ValueType> {
public:
virtual std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const override;
virtual std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType>&& matrix) const override;
using LinearEquationSolverFactory<ValueType>::create;
virtual std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> create() const override;
NativeLinearEquationSolverSettings<ValueType>& getSettings();
NativeLinearEquationSolverSettings<ValueType> const& getSettings() const;

10
src/storm/solver/StandardGameSolver.cpp

@ -115,7 +115,9 @@ namespace storm {
// Solve the equation system induced by the two schedulers.
storm::storage::SparseMatrix<ValueType> 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<ValueType> 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<storm::RationalNumber>;
template class StandardGameSolver<storm::RationalNumber>;
}
}
}

2
src/storm/storage/SparseMatrix.cpp

@ -1369,7 +1369,7 @@ namespace storm {
*resultIterator = storm::utility::zero<ValueType>();
}
for (ite = this->begin() + *rowIterator - 1; it != ite; ++it) {
for (ite = this->begin() + *rowIterator - 1; it != ite; --it) {
*resultIterator += it->getValue() * vector[it->getColumn()];
}
}

Loading…
Cancel
Save