From 00d331ebb4f8e25cbd635427a82b7562b9f4596b Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 23 Jun 2016 18:13:06 +0200 Subject: [PATCH] moved linear equation solver factories to the respective solver files (and away from utility). restructured settings in factories and the way they are forwarded to the linear equation solvers. fixed all resulting errors Former-commit-id: 27e1ae2466e71174ef11c2754c774f76e1670e98 --- .../csl/HybridCtmcCslModelChecker.cpp | 4 +- .../csl/HybridCtmcCslModelChecker.h | 6 +- .../csl/SparseCtmcCslModelChecker.cpp | 4 +- .../csl/SparseCtmcCslModelChecker.h | 6 +- .../csl/helper/HybridCtmcCslHelper.cpp | 12 +- .../csl/helper/HybridCtmcCslHelper.h | 14 +- .../csl/helper/SparseCtmcCslHelper.cpp | 28 +-- .../csl/helper/SparseCtmcCslHelper.h | 20 +-- .../prctl/HybridDtmcPrctlModelChecker.cpp | 4 +- .../prctl/HybridDtmcPrctlModelChecker.h | 6 +- .../prctl/SparseDtmcPrctlModelChecker.cpp | 4 +- .../prctl/SparseDtmcPrctlModelChecker.h | 4 +- .../prctl/helper/HybridDtmcPrctlHelper.cpp | 12 +- .../prctl/helper/HybridDtmcPrctlHelper.h | 14 +- .../prctl/helper/SparseDtmcPrctlHelper.cpp | 26 +-- .../prctl/helper/SparseDtmcPrctlHelper.h | 28 +-- src/solver/EigenLinearEquationSolver.cpp | 151 ++++++++++++---- src/solver/EigenLinearEquationSolver.h | 103 +++++------ .../EliminationLinearEquationSolver.cpp | 82 ++++++++- src/solver/EliminationLinearEquationSolver.h | 53 +++++- src/solver/GmmxxLinearEquationSolver.cpp | 170 +++++++++++++----- src/solver/GmmxxLinearEquationSolver.h | 152 ++++++++++------ .../GmmxxMinMaxLinearEquationSolver.cpp | 5 +- src/solver/LinearEquationSolver.cpp | 87 +++++++++ src/solver/LinearEquationSolver.h | 54 ++++++ src/solver/NativeLinearEquationSolver.cpp | 138 +++++++++++--- src/solver/NativeLinearEquationSolver.h | 93 +++++----- .../NativeMinMaxLinearEquationSolver.cpp | 1 - src/solver/SolveGoal.cpp | 8 +- src/solver/SolveGoal.h | 6 +- .../TopologicalMinMaxLinearEquationSolver.cpp | 1 - src/utility/solver.cpp | 125 ------------- src/utility/solver.h | 86 --------- .../EigenDtmcPrctlModelCheckerTest.cpp | 22 +-- .../GmmxxCtmcCslModelCheckerTest.cpp | 8 +- .../GmmxxDtmcPrctlModelCheckerTest.cpp | 18 +- .../GmmxxHybridCtmcCslModelCheckerTest.cpp | 18 +- .../GmmxxHybridDtmcPrctlModelCheckerTest.cpp | 14 +- .../NativeCtmcCslModelCheckerTest.cpp | 10 +- .../NativeDtmcPrctlModelCheckerTest.cpp | 32 ++-- .../NativeHybridCtmcCslModelCheckerTest.cpp | 18 +- .../NativeHybridDtmcPrctlModelCheckerTest.cpp | 14 +- .../solver/EigenLinearEquationSolverTest.cpp | 40 +++-- .../solver/GmmxxLinearEquationSolverTest.cpp | 59 ++++-- .../GmmxxDtmcPrctModelCheckerTest.cpp | 4 +- .../NativeDtmcPrctlModelCheckerTest.cpp | 4 +- 46 files changed, 1062 insertions(+), 706 deletions(-) create mode 100644 src/solver/LinearEquationSolver.cpp diff --git a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp index b4c59bb0f..ade2717b0 100644 --- a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -15,12 +15,12 @@ namespace storm { namespace modelchecker { template - HybridCtmcCslModelChecker::HybridCtmcCslModelChecker(storm::models::symbolic::Ctmc const& model) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::make_unique>()) { + HybridCtmcCslModelChecker::HybridCtmcCslModelChecker(storm::models::symbolic::Ctmc const& model) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::make_unique>()) { // Intentionally left empty. } template - HybridCtmcCslModelChecker::HybridCtmcCslModelChecker(storm::models::symbolic::Ctmc const& model, std::unique_ptr>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { + HybridCtmcCslModelChecker::HybridCtmcCslModelChecker(storm::models::symbolic::Ctmc const& model, std::unique_ptr>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { // Intentionally left empty. } diff --git a/src/modelchecker/csl/HybridCtmcCslModelChecker.h b/src/modelchecker/csl/HybridCtmcCslModelChecker.h index 5bfe49405..0d69f5220 100644 --- a/src/modelchecker/csl/HybridCtmcCslModelChecker.h +++ b/src/modelchecker/csl/HybridCtmcCslModelChecker.h @@ -5,7 +5,7 @@ #include "src/models/symbolic/Ctmc.h" -#include "src/utility/solver.h" +#include "src/solver/LinearEquationSolver.h" namespace storm { namespace modelchecker { @@ -14,7 +14,7 @@ namespace storm { class HybridCtmcCslModelChecker : public SymbolicPropositionalModelChecker { public: explicit HybridCtmcCslModelChecker(storm::models::symbolic::Ctmc const& model); - explicit HybridCtmcCslModelChecker(storm::models::symbolic::Ctmc const& model, std::unique_ptr>&& linearEquationSolverFactory); + explicit HybridCtmcCslModelChecker(storm::models::symbolic::Ctmc const& model, std::unique_ptr>&& linearEquationSolverFactory); // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(CheckTask const& checkTask) const override; @@ -31,7 +31,7 @@ namespace storm { private: // An object that is used for solving linear equations and performing matrix-vector multiplication. - std::unique_ptr> linearEquationSolverFactory; + std::unique_ptr> linearEquationSolverFactory; }; } // namespace modelchecker diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp index abf21fe01..f376e19e7 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -24,12 +24,12 @@ namespace storm { namespace modelchecker { template - SparseCtmcCslModelChecker::SparseCtmcCslModelChecker(SparseCtmcModelType const& model) : SparsePropositionalModelChecker(model), linearEquationSolverFactory(std::make_unique>()) { + SparseCtmcCslModelChecker::SparseCtmcCslModelChecker(SparseCtmcModelType const& model) : SparsePropositionalModelChecker(model), linearEquationSolverFactory(std::make_unique>()) { // Intentionally left empty. } template - SparseCtmcCslModelChecker::SparseCtmcCslModelChecker(SparseCtmcModelType const& model, std::unique_ptr>&& linearEquationSolverFactory) : SparsePropositionalModelChecker(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { + SparseCtmcCslModelChecker::SparseCtmcCslModelChecker(SparseCtmcModelType const& model, std::unique_ptr>&& linearEquationSolverFactory) : SparsePropositionalModelChecker(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { // Intentionally left empty. } diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.h b/src/modelchecker/csl/SparseCtmcCslModelChecker.h index 802841dee..070f81ffd 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.h +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.h @@ -5,7 +5,7 @@ #include "src/models/sparse/Ctmc.h" -#include "src/utility/solver.h" +#include "src/solver/LinearEquationSolver.h" namespace storm { namespace modelchecker { @@ -17,7 +17,7 @@ namespace storm { typedef typename SparseCtmcModelType::RewardModelType RewardModelType; explicit SparseCtmcCslModelChecker(SparseCtmcModelType const& model); - explicit SparseCtmcCslModelChecker(SparseCtmcModelType const& model, std::unique_ptr>&& linearEquationSolverFactory); + explicit SparseCtmcCslModelChecker(SparseCtmcModelType const& model, std::unique_ptr>&& linearEquationSolverFactory); // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(CheckTask const& checkTask) const override; @@ -32,7 +32,7 @@ namespace storm { private: // An object that is used for solving linear equations and performing matrix-vector multiplication. - std::unique_ptr> linearEquationSolverFactory; + std::unique_ptr> linearEquationSolverFactory; }; } // namespace modelchecker diff --git a/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp b/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp index e59523866..91581e987 100644 --- a/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp +++ b/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp @@ -26,7 +26,7 @@ namespace storm { namespace helper { template - std::unique_ptr HybridCtmcCslHelper::computeReachabilityRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr HybridCtmcCslHelper::computeReachabilityRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { return HybridDtmcPrctlHelper::computeReachabilityRewards(model, computeProbabilityMatrix(model, rateMatrix, exitRateVector), rewardModel.divideStateRewardVector(exitRateVector), targetStates, qualitative, linearEquationSolverFactory); } @@ -37,12 +37,12 @@ namespace storm { } template - std::unique_ptr HybridCtmcCslHelper::computeUntilProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr HybridCtmcCslHelper::computeUntilProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { return HybridDtmcPrctlHelper::computeUntilProbabilities(model, computeProbabilityMatrix(model, rateMatrix, exitRateVector), phiStates, psiStates, qualitative, linearEquationSolverFactory); } template - std::unique_ptr HybridCtmcCslHelper::computeBoundedUntilProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr HybridCtmcCslHelper::computeBoundedUntilProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // If the time bounds are [0, inf], we rather call untimed reachability. if (storm::utility::isZero(lowerBound) && upperBound == storm::utility::infinity()) { @@ -218,7 +218,7 @@ namespace storm { } template - std::unique_ptr HybridCtmcCslHelper::computeInstantaneousRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr HybridCtmcCslHelper::computeInstantaneousRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if the model has a state-based reward model. STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -244,7 +244,7 @@ namespace storm { } template - std::unique_ptr HybridCtmcCslHelper::computeCumulativeRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr HybridCtmcCslHelper::computeCumulativeRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if the model has a state-based reward model. STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -276,7 +276,7 @@ namespace storm { } template - std::unique_ptr HybridCtmcCslHelper::computeLongRunAverageProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr HybridCtmcCslHelper::computeLongRunAverageProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { storm::dd::Add probabilityMatrix = computeProbabilityMatrix(model, rateMatrix, exitRateVector); // Create ODD for the translation. diff --git a/src/modelchecker/csl/helper/HybridCtmcCslHelper.h b/src/modelchecker/csl/helper/HybridCtmcCslHelper.h index ca7d7aa35..e2e0667c0 100644 --- a/src/modelchecker/csl/helper/HybridCtmcCslHelper.h +++ b/src/modelchecker/csl/helper/HybridCtmcCslHelper.h @@ -7,7 +7,7 @@ #include "src/modelchecker/results/CheckResult.h" -#include "src/utility/solver.h" +#include "src/solver/LinearEquationSolver.h" namespace storm { namespace modelchecker { @@ -18,17 +18,17 @@ namespace storm { public: typedef typename storm::models::symbolic::Model::RewardModelType RewardModelType; - static std::unique_ptr computeBoundedUntilProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeBoundedUntilProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeInstantaneousRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeInstantaneousRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeCumulativeRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeCumulativeRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeUntilProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeUntilProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeReachabilityRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeReachabilityRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeLongRunAverageProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeLongRunAverageProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); static std::unique_ptr computeNextProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& nextStates); diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 12bb227b9..0dddea5cb 100644 --- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -26,7 +26,7 @@ namespace storm { namespace modelchecker { namespace helper { template - std::vector SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { uint_fast64_t numberOfStates = rateMatrix.getRowCount(); @@ -191,7 +191,7 @@ namespace storm { } template - std::vector SparseCtmcCslHelper::computeUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseCtmcCslHelper::computeUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { return SparseDtmcPrctlHelper::computeUntilProbabilities(computeProbabilityMatrix(rateMatrix, exitRateVector), backwardTransitions, phiStates, psiStates, qualitative, linearEquationSolverFactory); } @@ -202,7 +202,7 @@ namespace storm { } template - std::vector SparseCtmcCslHelper::computeNextProbabilities(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseCtmcCslHelper::computeNextProbabilities(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { return SparseDtmcPrctlHelper::computeNextProbabilities(computeProbabilityMatrix(rateMatrix, exitRateVector), nextStates, linearEquationSolverFactory); } @@ -235,7 +235,7 @@ namespace storm { template template - std::vector SparseCtmcCslHelper::computeTransientProbabilities(storm::storage::SparseMatrix const& uniformizedMatrix, std::vector const* addVector, ValueType timeBound, ValueType uniformizationRate, std::vector values, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseCtmcCslHelper::computeTransientProbabilities(storm::storage::SparseMatrix const& uniformizedMatrix, std::vector const* addVector, ValueType timeBound, ValueType uniformizationRate, std::vector values, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { ValueType lambda = timeBound * uniformizationRate; @@ -314,7 +314,7 @@ namespace storm { template template - std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if the model has a state-based reward this->getModel(). STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -341,7 +341,7 @@ namespace storm { template template - std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if the model has a state-based reward this->getModel(). STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -373,7 +373,7 @@ namespace storm { template template - std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); storm::storage::SparseMatrix probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector); @@ -432,7 +432,7 @@ namespace storm { } template - std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // If there are no goal states, we avoid the computation and directly return zero. uint_fast64_t numberOfStates = probabilityMatrix.getRowCount(); if (psiStates.empty()) { @@ -656,7 +656,7 @@ namespace storm { } template - std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Compute expected time on CTMC by reduction to DTMC with rewards. storm::storage::SparseMatrix probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector); @@ -698,16 +698,16 @@ namespace storm { } template class SparseCtmcCslHelper; - template std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeUntilProbabilitiesElimination(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative); template std::vector SparseCtmcCslHelper::computeReachabilityTimesElimination(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative); - template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); } } } diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.h b/src/modelchecker/csl/helper/SparseCtmcCslHelper.h index 2b4dd6043..8485b2501 100644 --- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.h +++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.h @@ -3,7 +3,7 @@ #include "src/storage/BitVector.h" -#include "src/utility/solver.h" +#include "src/solver/LinearEquationSolver.h" namespace storm { namespace modelchecker { @@ -11,25 +11,25 @@ namespace storm { template class SparseCtmcCslHelper { public: - static std::vector computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::vector computeNextProbabilities(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeNextProbabilities(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::vector computeUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); static std::vector computeUntilProbabilitiesElimination(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative); template - static std::vector computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template - static std::vector computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template - static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::vector computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::vector computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); static std::vector computeReachabilityTimesElimination(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative); /*! @@ -58,7 +58,7 @@ namespace storm { * @return The vector of transient probabilities. */ template - static std::vector computeTransientProbabilities(storm::storage::SparseMatrix const& uniformizedMatrix, std::vector const* addVector, ValueType timeBound, ValueType uniformizationRate, std::vector values, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeTransientProbabilities(storm::storage::SparseMatrix const& uniformizedMatrix, std::vector const* addVector, ValueType timeBound, ValueType uniformizationRate, std::vector values, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); /*! * Converts the given rate-matrix into a time-abstract probability matrix. diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp index 75f651e8a..f0cd46154 100644 --- a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp @@ -26,12 +26,12 @@ namespace storm { namespace modelchecker { template - HybridDtmcPrctlModelChecker::HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc const& model, std::unique_ptr>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { + HybridDtmcPrctlModelChecker::HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc const& model, std::unique_ptr>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { // Intentionally left empty. } template - HybridDtmcPrctlModelChecker::HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc const& model) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::make_unique>()) { + HybridDtmcPrctlModelChecker::HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc const& model) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::make_unique>()) { // Intentionally left empty. } diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h index 3489e74e8..620aa2952 100644 --- a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h @@ -5,7 +5,7 @@ #include "src/models/symbolic/Dtmc.h" -#include "src/utility/solver.h" +#include "src/solver/LinearEquationSolver.h" namespace storm { namespace modelchecker { @@ -14,7 +14,7 @@ namespace storm { class HybridDtmcPrctlModelChecker : public SymbolicPropositionalModelChecker { public: explicit HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc const& model); - explicit HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc const& model, std::unique_ptr>&& linearEquationSolverFactory); + explicit HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc const& model, std::unique_ptr>&& linearEquationSolverFactory); // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(CheckTask const& checkTask) const override; @@ -32,7 +32,7 @@ namespace storm { private: // An object that is used for retrieving linear equation solvers. - std::unique_ptr> linearEquationSolverFactory; + std::unique_ptr> linearEquationSolverFactory; }; } // namespace modelchecker diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 75fdaca64..92ec6d2be 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -24,12 +24,12 @@ namespace storm { namespace modelchecker { template - SparseDtmcPrctlModelChecker::SparseDtmcPrctlModelChecker(SparseDtmcModelType const& model, std::unique_ptr>&& linearEquationSolverFactory) : SparsePropositionalModelChecker(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { + SparseDtmcPrctlModelChecker::SparseDtmcPrctlModelChecker(SparseDtmcModelType const& model, std::unique_ptr>&& linearEquationSolverFactory) : SparsePropositionalModelChecker(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { // Intentionally left empty. } template - SparseDtmcPrctlModelChecker::SparseDtmcPrctlModelChecker(SparseDtmcModelType const& model) : SparsePropositionalModelChecker(model), linearEquationSolverFactory(std::make_unique>()) { + SparseDtmcPrctlModelChecker::SparseDtmcPrctlModelChecker(SparseDtmcModelType const& model) : SparsePropositionalModelChecker(model), linearEquationSolverFactory(std::make_unique>()) { // Intentionally left empty. } diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index 6b94f6642..d577676b0 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -16,7 +16,7 @@ namespace storm { typedef typename SparseDtmcModelType::RewardModelType RewardModelType; explicit SparseDtmcPrctlModelChecker(SparseDtmcModelType const& model); - explicit SparseDtmcPrctlModelChecker(SparseDtmcModelType const& model, std::unique_ptr>&& linearEquationSolverFactory); + explicit SparseDtmcPrctlModelChecker(SparseDtmcModelType const& model, std::unique_ptr>&& linearEquationSolverFactory); // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(CheckTask const& checkTask) const override; @@ -34,7 +34,7 @@ namespace storm { private: // An object that is used for retrieving linear equation solvers. - std::unique_ptr> linearEquationSolverFactory; + std::unique_ptr> linearEquationSolverFactory; }; } // namespace modelchecker diff --git a/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp index 869242db4..73bd63088 100644 --- a/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp @@ -24,7 +24,7 @@ namespace storm { namespace helper { template - std::unique_ptr HybridDtmcPrctlHelper::computeUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr HybridDtmcPrctlHelper::computeUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // We need to identify the states which have to be taken out of the matrix, i.e. all states that have // probability 0 and 1 of satisfying the until-formula. std::pair, storm::dd::Bdd> statesWithProbability01 = storm::utility::graph::performProb01(model, transitionMatrix, phiStates, psiStates); @@ -83,7 +83,7 @@ namespace storm { } template - std::unique_ptr HybridDtmcPrctlHelper::computeGloballyProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr HybridDtmcPrctlHelper::computeGloballyProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { std::unique_ptr result = computeUntilProbabilities(model, transitionMatrix, model.getReachableStates(), !psiStates && model.getReachableStates(), qualitative, linearEquationSolverFactory); result->asQuantitativeCheckResult().oneMinus(); return result; @@ -96,7 +96,7 @@ namespace storm { } template - std::unique_ptr HybridDtmcPrctlHelper::computeBoundedUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr HybridDtmcPrctlHelper::computeBoundedUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, uint_fast64_t stepBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // We need to identify the states which have to be taken out of the matrix, i.e. all states that have // probability 0 or 1 of satisfying the until-formula. storm::dd::Bdd statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(model, transitionMatrix.notZero(), phiStates, psiStates, stepBound); @@ -141,7 +141,7 @@ namespace storm { template - std::unique_ptr HybridDtmcPrctlHelper::computeInstantaneousRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr HybridDtmcPrctlHelper::computeInstantaneousRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if the model has at least one reward this->getModel(). STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -163,7 +163,7 @@ namespace storm { } template - std::unique_ptr HybridDtmcPrctlHelper::computeCumulativeRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr HybridDtmcPrctlHelper::computeCumulativeRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if the model has at least one reward this->getModel(). STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -189,7 +189,7 @@ namespace storm { } template - std::unique_ptr HybridDtmcPrctlHelper::computeReachabilityRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr HybridDtmcPrctlHelper::computeReachabilityRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if there is at least one reward model. STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); diff --git a/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.h b/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.h index 9cbfa83d3..6296802ae 100644 --- a/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.h +++ b/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.h @@ -6,7 +6,7 @@ #include "src/storage/dd/Add.h" #include "src/storage/dd/Bdd.h" -#include "src/utility/solver.h" +#include "src/solver/LinearEquationSolver.h" namespace storm { namespace modelchecker { @@ -20,19 +20,19 @@ namespace storm { public: typedef typename storm::models::symbolic::Model::RewardModelType RewardModelType; - static std::unique_ptr computeBoundedUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeBoundedUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, uint_fast64_t stepBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); static std::unique_ptr computeNextProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& nextStates); - static std::unique_ptr computeUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeGloballyProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeGloballyProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeCumulativeRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeCumulativeRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeInstantaneousRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeInstantaneousRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeReachabilityRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeReachabilityRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); }; } diff --git a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 857da9a6f..7e9d03c6d 100644 --- a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -17,7 +17,7 @@ namespace storm { namespace modelchecker { namespace helper { template - std::vector SparseDtmcPrctlHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseDtmcPrctlHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { std::vector result(transitionMatrix.getRowCount(), storm::utility::zero()); // If we identify the states that have probability 0 of reaching the target states, we can exclude them in the further analysis. @@ -48,7 +48,7 @@ namespace storm { } template - std::vector SparseDtmcPrctlHelper::computeUntilProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseDtmcPrctlHelper::computeUntilProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // We need to identify the states which have to be taken out of the matrix, i.e. // all states that have probability 0 and 1 of satisfying the until-formula. std::pair statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiStates, psiStates); @@ -105,7 +105,7 @@ namespace storm { } template - std::vector SparseDtmcPrctlHelper::computeGloballyProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseDtmcPrctlHelper::computeGloballyProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { std::vector result = computeUntilProbabilities(transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowCount(), true), ~psiStates, qualitative, linearEquationSolverFactory); for (auto& entry : result) { entry = storm::utility::one() - entry; @@ -114,7 +114,7 @@ namespace storm { } template - std::vector SparseDtmcPrctlHelper::computeNextProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseDtmcPrctlHelper::computeNextProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Create the vector with which to multiply and initialize it correctly. std::vector result(transitionMatrix.getRowCount()); storm::utility::vector::setVectorValues(result, nextStates, storm::utility::one()); @@ -126,7 +126,7 @@ namespace storm { } template - std::vector SparseDtmcPrctlHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseDtmcPrctlHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Initialize result to the null vector. std::vector result(transitionMatrix.getRowCount()); @@ -141,7 +141,7 @@ namespace storm { } template - std::vector SparseDtmcPrctlHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseDtmcPrctlHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if the model has a state-based reward this->getModel(). STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -156,12 +156,12 @@ namespace storm { } template - std::vector SparseDtmcPrctlHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseDtmcPrctlHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { return computeReachabilityRewards(transitionMatrix, backwardTransitions, [&] (uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates) { return rewardModel.getTotalRewardVector(numberOfRows, transitionMatrix, maybeStates); }, targetStates, qualitative, linearEquationSolverFactory); } template - std::vector SparseDtmcPrctlHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& totalStateRewardVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseDtmcPrctlHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& totalStateRewardVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { return computeReachabilityRewards(transitionMatrix, backwardTransitions, [&] (uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates) { std::vector result(numberOfRows); @@ -172,7 +172,7 @@ namespace storm { } template - std::vector SparseDtmcPrctlHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseDtmcPrctlHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Determine which states have a reward of infinity by definition. storm::storage::BitVector trueStates(transitionMatrix.getRowCount(), true); @@ -224,12 +224,12 @@ namespace storm { } template - std::vector SparseDtmcPrctlHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseDtmcPrctlHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { return SparseCtmcCslHelper::computeLongRunAverageProbabilities(transitionMatrix, psiStates, nullptr, qualitative, linearEquationSolverFactory); } template - typename SparseDtmcPrctlHelper::BaierTransformedModel SparseDtmcPrctlHelper::computeBaierTransformation(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, boost::optional> const& stateRewards, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + typename SparseDtmcPrctlHelper::BaierTransformedModel SparseDtmcPrctlHelper::computeBaierTransformation(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, boost::optional> const& stateRewards, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { BaierTransformedModel result; @@ -349,7 +349,7 @@ namespace storm { } template - std::vector SparseDtmcPrctlHelper::computeConditionalProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseDtmcPrctlHelper::computeConditionalProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Prepare result vector. std::vector result(transitionMatrix.getRowCount(), storm::utility::infinity()); @@ -376,7 +376,7 @@ namespace storm { } template - std::vector SparseDtmcPrctlHelper::computeConditionalRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseDtmcPrctlHelper::computeConditionalRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Prepare result vector. std::vector result(transitionMatrix.getRowCount(), storm::utility::infinity()); diff --git a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h index 0be762298..80e4321ba 100644 --- a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h +++ b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h @@ -8,7 +8,7 @@ #include "src/storage/SparseMatrix.h" #include "src/storage/BitVector.h" -#include "src/utility/solver.h" +#include "src/solver/LinearEquationSolver.h" namespace storm { namespace modelchecker { @@ -19,30 +19,30 @@ namespace storm { template > class SparseDtmcPrctlHelper { public: - static std::vector computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::vector computeNextProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeNextProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::vector computeUntilProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeUntilProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::vector computeGloballyProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeGloballyProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::vector computeCumulativeRewards(storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeCumulativeRewards(storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::vector computeInstantaneousRewards(storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeInstantaneousRewards(storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& totalStateRewardVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& totalStateRewardVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::vector computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::vector computeConditionalProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeConditionalProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::vector computeConditionalRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeConditionalRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); private: - static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); struct BaierTransformedModel { BaierTransformedModel() : noTargetStates(false) { @@ -56,7 +56,7 @@ namespace storm { bool noTargetStates; }; - static BaierTransformedModel computeBaierTransformation(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, boost::optional> const& stateRewards, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static BaierTransformedModel computeBaierTransformation(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, boost::optional> const& stateRewards, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); }; } diff --git a/src/solver/EigenLinearEquationSolver.cpp b/src/solver/EigenLinearEquationSolver.cpp index d7328f8f9..3d5f5a857 100644 --- a/src/solver/EigenLinearEquationSolver.cpp +++ b/src/solver/EigenLinearEquationSolver.cpp @@ -5,16 +5,14 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/EigenEquationSolverSettings.h" +#include "src/utility/macros.h" +#include "src/exceptions/InvalidSettingsException.h" + namespace storm { namespace solver { template - EigenLinearEquationSolver::EigenLinearEquationSolver(storm::storage::SparseMatrix const& A, SolutionMethod method, double precision, uint64_t maximalNumberOfIterations, Preconditioner preconditioner) : originalA(&A), eigenA(storm::adapters::EigenAdapter::toEigenSparseMatrix(A)), method(method), precision(precision), maximalNumberOfIterations(maximalNumberOfIterations), preconditioner(preconditioner) { - // Intentionally left empty. - } - - template - EigenLinearEquationSolver::EigenLinearEquationSolver(storm::storage::SparseMatrix const& A) : originalA(&A), eigenA(storm::adapters::EigenAdapter::toEigenSparseMatrix(A)) { + EigenLinearEquationSolverSettings::EigenLinearEquationSolverSettings() { // Get the settings object to customize linear solving. storm::settings::modules::EigenEquationSolverSettings const& settings = storm::settings::getModule(); @@ -41,6 +39,65 @@ namespace storm { } } + template + void EigenLinearEquationSolverSettings::setSolutionMethod(SolutionMethod const& method) { + this->method = method; + } + + template + void EigenLinearEquationSolverSettings::setPreconditioner(Preconditioner const& preconditioner) { + this->preconditioner = preconditioner; + } + + template + void EigenLinearEquationSolverSettings::setPrecision(ValueType precision) { + this->precision = precision; + } + + template + void EigenLinearEquationSolverSettings::setMaximalNumberOfIterations(uint64_t maximalNumberOfIterations) { + this->maximalNumberOfIterations = maximalNumberOfIterations; + } + + template + typename EigenLinearEquationSolverSettings::SolutionMethod EigenLinearEquationSolverSettings::getSolutionMethod() const { + return this->method; + } + + template + typename EigenLinearEquationSolverSettings::Preconditioner EigenLinearEquationSolverSettings::getPreconditioner() const { + return this->preconditioner; + } + + template + ValueType EigenLinearEquationSolverSettings::getPrecision() const { + return this->precision; + } + + template + uint64_t EigenLinearEquationSolverSettings::getMaximalNumberOfIterations() const { + return this->maximalNumberOfIterations; + } + + EigenLinearEquationSolverSettings::EigenLinearEquationSolverSettings() { + // Intentionally left empty. + } + + EigenLinearEquationSolverSettings::EigenLinearEquationSolverSettings() { + // Intentionally left empty. + } + + template + EigenLinearEquationSolver::EigenLinearEquationSolver(storm::storage::SparseMatrix const& A, EigenLinearEquationSolverSettings const& settings) : eigenA(storm::adapters::EigenAdapter::toEigenSparseMatrix(A)), settings(settings) { + // Intentionally left empty. + } + + template + EigenLinearEquationSolver::EigenLinearEquationSolver(storm::storage::SparseMatrix&& A, EigenLinearEquationSolverSettings const& settings) : settings(settings) { + storm::storage::SparseMatrix localA(std::move(A)); + eigenA = storm::adapters::EigenAdapter::toEigenSparseMatrix(localA); + } + template void EigenLinearEquationSolver::solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult) const { // Translate the vectors x and b into Eigen's format. @@ -54,25 +111,25 @@ namespace storm { eigenX[index] = x[index]; } - if (method == SolutionMethod::SparseLU) { + if (this->getSettings().getSolutionMethod() == EigenLinearEquationSolverSettings::SolutionMethod::SparseLU) { Eigen::SparseLU, Eigen::COLAMDOrdering> solver; - solver.compute(*eigenA); + solver.compute(*this->eigenA); if (solver.info() != Eigen::Success) { std::cout << solver.lastErrorMessage() << std::endl; } solver._solve_impl(eigenB, eigenX); } else { - if (preconditioner == Preconditioner::Ilu) { + if (this->getSettings().getPreconditioner() == EigenLinearEquationSolverSettings::Preconditioner::Ilu) { Eigen::BiCGSTAB, Eigen::IncompleteLUT> solver; - solver.compute(*eigenA); + solver.compute(*this->eigenA); solver.solveWithGuess(eigenB, eigenX); - } else if (preconditioner == Preconditioner::Diagonal) { + } else if (this->getSettings().getPreconditioner() == EigenLinearEquationSolverSettings::Preconditioner::Diagonal) { Eigen::BiCGSTAB, Eigen::DiagonalPreconditioner> solver; - solver.compute(*eigenA); + solver.compute(*this->eigenA); solver.solveWithGuess(eigenB, eigenX); } else { Eigen::BiCGSTAB, Eigen::IdentityPreconditioner> solver; - solver.compute(*eigenA); + solver.compute(*this->eigenA); solver.solveWithGuess(eigenB, eigenX); } } @@ -100,7 +157,7 @@ namespace storm { // Perform n matrix-vector multiplications. for (uint64_t iteration = 0; iteration < n; ++iteration) { - eigenX = *eigenA * eigenX; + eigenX = *this->eigenA * eigenX; if (eigenB != nullptr) { eigenX += *eigenB; } @@ -112,12 +169,19 @@ namespace storm { } } - // Specialization form storm::RationalNumber + template + EigenLinearEquationSolverSettings& EigenLinearEquationSolver::getSettings() { + return settings; + } - EigenLinearEquationSolver::EigenLinearEquationSolver(storm::storage::SparseMatrix const& A, SolutionMethod method) : originalA(&A), eigenA(storm::adapters::EigenAdapter::toEigenSparseMatrix(A)), method(method) { - // Intentionally left empty. + template + EigenLinearEquationSolverSettings const& EigenLinearEquationSolver::getSettings() const { + return settings; } + // Specialization form storm::RationalNumber + + template<> void EigenLinearEquationSolver::solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult) const { // Translate the vectors x and b into Eigen's format. Eigen::Matrix eigenB(b.size()); @@ -130,11 +194,9 @@ namespace storm { eigenX[index] = x[index]; } - if (method == SolutionMethod::SparseLU) { - Eigen::SparseLU, Eigen::COLAMDOrdering> solver; - solver.compute(*eigenA); - solver._solve_impl(eigenB, eigenX); - } + Eigen::SparseLU, Eigen::COLAMDOrdering> solver; + solver.compute(*eigenA); + solver._solve_impl(eigenB, eigenX); // Translate the solution from Eigen's format into our representation. for (uint64_t index = 0; index < eigenX.size(); ++index) { @@ -142,6 +204,7 @@ namespace storm { } } + template<> void EigenLinearEquationSolver::performMatrixVectorMultiplication(std::vector& x, std::vector const* b, uint_fast64_t n, std::vector* multiplyResult) const { // Translate the vectors x and b into Eigen's format. std::unique_ptr> eigenB; @@ -172,10 +235,7 @@ namespace storm { // Specialization form storm::RationalFunction - EigenLinearEquationSolver::EigenLinearEquationSolver(storm::storage::SparseMatrix const& A, SolutionMethod method) : originalA(&A), eigenA(storm::adapters::EigenAdapter::toEigenSparseMatrix(A)), method(method) { - // Intentionally left empty. - } - + template<> void EigenLinearEquationSolver::solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult) const { // Translate the vectors x and b into Eigen's format. Eigen::Matrix eigenB(b.size()); @@ -188,11 +248,9 @@ namespace storm { eigenX[index] = x[index]; } - if (method == SolutionMethod::SparseLU) { - Eigen::SparseLU, Eigen::COLAMDOrdering> solver; - solver.compute(*eigenA); - solver._solve_impl(eigenB, eigenX); - } + Eigen::SparseLU, Eigen::COLAMDOrdering> solver; + solver.compute(*eigenA); + solver._solve_impl(eigenB, eigenX); // Translate the solution from Eigen's format into our representation. for (uint64_t index = 0; index < eigenX.size(); ++index) { @@ -200,6 +258,7 @@ namespace storm { } } + template<> void EigenLinearEquationSolver::performMatrixVectorMultiplication(std::vector& x, std::vector const* b, uint_fast64_t n, std::vector* multiplyResult) const { // Translate the vectors x and b into Eigen's format. std::unique_ptr> eigenB; @@ -228,9 +287,37 @@ namespace storm { } } + 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); + } + + template + EigenLinearEquationSolverSettings& EigenLinearEquationSolverFactory::getSettings() { + return settings; + } + + template + EigenLinearEquationSolverSettings const& EigenLinearEquationSolverFactory::getSettings() const { + return settings; + } + + template class EigenLinearEquationSolverSettings; + template class EigenLinearEquationSolverSettings; + template class EigenLinearEquationSolverSettings; + template class EigenLinearEquationSolver; template class EigenLinearEquationSolver; -// template class EigenLinearEquationSolver; + template class EigenLinearEquationSolver; + + template class EigenLinearEquationSolverFactory; + template class EigenLinearEquationSolverFactory; + template class EigenLinearEquationSolverFactory; } } \ No newline at end of file diff --git a/src/solver/EigenLinearEquationSolver.h b/src/solver/EigenLinearEquationSolver.h index 924a2af74..6aa770d7e 100644 --- a/src/solver/EigenLinearEquationSolver.h +++ b/src/solver/EigenLinearEquationSolver.h @@ -7,11 +7,8 @@ namespace storm { namespace solver { - /*! - * A class that uses the Eigen library to implement the LinearEquationSolver interface. - */ template - class EigenLinearEquationSolver : public LinearEquationSolver { + class EigenLinearEquationSolverSettings { public: enum class SolutionMethod { SparseLU, Bicgstab @@ -21,80 +18,72 @@ namespace storm { Ilu, Diagonal, None }; - EigenLinearEquationSolver(storm::storage::SparseMatrix const& A, SolutionMethod method, double precision, uint64_t maximalNumberOfIterations, Preconditioner preconditioner); - - EigenLinearEquationSolver(storm::storage::SparseMatrix const& A); + EigenLinearEquationSolverSettings(); - virtual void solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr) const override; + void setSolutionMethod(SolutionMethod const& method); + void setPreconditioner(Preconditioner const& preconditioner); + void setPrecision(ValueType precision); + void setMaximalNumberOfIterations(uint64_t maximalNumberOfIterations); - virtual void performMatrixVectorMultiplication(std::vector& x, std::vector const* b, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const override; + SolutionMethod getSolutionMethod() const; + Preconditioner getPreconditioner() const; + ValueType getPrecision() const; + uint64_t getMaximalNumberOfIterations() const; private: - // A pointer to the original sparse matrix given to this solver. - storm::storage::SparseMatrix const* originalA; - - // The (eigen) matrix associated with this equation solver. - std::unique_ptr> eigenA; - - // The method to use for solving linear equation systems. SolutionMethod method; - - // The required precision for the iterative methods. - double precision; - - // The maximal number of iterations to do before iteration is aborted. - uint_fast64_t maximalNumberOfIterations; - - // The preconditioner to use when solving the linear equation system. Preconditioner preconditioner; + double precision; + uint64_t maximalNumberOfIterations; }; template<> - class EigenLinearEquationSolver : public LinearEquationSolver { + class EigenLinearEquationSolverSettings { public: - enum class SolutionMethod { - SparseLU - }; + EigenLinearEquationSolverSettings(); + }; + + template<> + class EigenLinearEquationSolverSettings { + public: + EigenLinearEquationSolverSettings(); + }; + + /*! + * A class that uses the Eigen library to implement the LinearEquationSolver interface. + */ + template + class EigenLinearEquationSolver : public LinearEquationSolver { + public: + EigenLinearEquationSolver(storm::storage::SparseMatrix const& A, EigenLinearEquationSolverSettings const& settings = EigenLinearEquationSolverSettings()); + EigenLinearEquationSolver(storm::storage::SparseMatrix&& A, EigenLinearEquationSolverSettings const& settings = EigenLinearEquationSolverSettings()); - EigenLinearEquationSolver(storm::storage::SparseMatrix const& A, SolutionMethod method = SolutionMethod::SparseLU); + virtual void solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr) const override; - virtual void solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr) const override; + virtual void performMatrixVectorMultiplication(std::vector& x, std::vector const* b, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const override; - virtual void performMatrixVectorMultiplication(std::vector& x, std::vector const* b, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const override; + EigenLinearEquationSolverSettings& getSettings(); + EigenLinearEquationSolverSettings const& getSettings() const; private: - // A pointer to the original sparse matrix given to this solver. - storm::storage::SparseMatrix const* originalA; - // The (eigen) matrix associated with this equation solver. - std::unique_ptr> eigenA; - - // The method to use for solving linear equation systems. - SolutionMethod method; + std::unique_ptr> eigenA; + + // The settings used by the solver. + EigenLinearEquationSolverSettings settings; }; - template<> - class EigenLinearEquationSolver : public LinearEquationSolver { + template + class EigenLinearEquationSolverFactory : public LinearEquationSolverFactory { public: - enum class SolutionMethod { - SparseLU - }; - - EigenLinearEquationSolver(storm::storage::SparseMatrix const& A, SolutionMethod method = SolutionMethod::SparseLU); - - virtual void solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr) const override; - - virtual void performMatrixVectorMultiplication(std::vector& x, std::vector const* b, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const override; + virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const override; + virtual std::unique_ptr> create(storm::storage::SparseMatrix&& matrix) const override; + EigenLinearEquationSolverSettings& getSettings(); + EigenLinearEquationSolverSettings const& getSettings() const; + private: - // A pointer to the original sparse matrix given to this solver. - storm::storage::SparseMatrix const* originalA; - - // The (eigen) matrix associated with this equation solver. - std::unique_ptr> eigenA; - - // The method to use for solving linear equation systems. - SolutionMethod method; + EigenLinearEquationSolverSettings settings; }; } } \ No newline at end of file diff --git a/src/solver/EliminationLinearEquationSolver.cpp b/src/solver/EliminationLinearEquationSolver.cpp index 52a355fbd..e250257ff 100644 --- a/src/solver/EliminationLinearEquationSolver.cpp +++ b/src/solver/EliminationLinearEquationSolver.cpp @@ -3,7 +3,6 @@ #include #include "src/settings/SettingsManager.h" -#include "src/settings/modules/EliminationSettings.h" #include "src/solver/stateelimination/StatePriorityQueue.h" #include "src/solver/stateelimination/PrioritizedStateEliminator.h" @@ -20,10 +19,30 @@ namespace storm { using namespace storm::utility::stateelimination; template - EliminationLinearEquationSolver::EliminationLinearEquationSolver(storm::storage::SparseMatrix const& A) : A(A) { - // Intentionally left empty. + EliminationLinearEquationSolverSettings::EliminationLinearEquationSolverSettings() { + order = storm::settings::getModule().getEliminationOrder(); } + template + void EliminationLinearEquationSolverSettings::setEliminationOrder(storm::settings::modules::EliminationSettings::EliminationOrder const& order) { + this->order = order; + } + + template + storm::settings::modules::EliminationSettings::EliminationOrder EliminationLinearEquationSolverSettings::getEliminationOrder() const { + return order; + } + + template + EliminationLinearEquationSolver::EliminationLinearEquationSolver(storm::storage::SparseMatrix const& A, EliminationLinearEquationSolverSettings const& settings) : localA(nullptr), A(A), settings(settings) { + // Intentionally left empty. + } + + template + EliminationLinearEquationSolver::EliminationLinearEquationSolver(storm::storage::SparseMatrix&& A, EliminationLinearEquationSolverSettings const& settings) : localA(std::make_unique>(std::move(A))), A(*localA), settings(settings) { + // Intentionally left empty. + } + template void EliminationLinearEquationSolver::solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult) const { STORM_LOG_WARN_COND(multiplyResult == nullptr, "Providing scratch memory will not improve the performance of this solver."); @@ -36,10 +55,15 @@ namespace storm { // 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 transitionMatrix(A); - - transitionMatrix.convertToEquationSystem(); + storm::storage::SparseMatrix locallyConvertedMatrix; + if (localA) { + localA->convertToEquationSystem(); + } else { + locallyConvertedMatrix = A; + locallyConvertedMatrix.convertToEquationSystem(); + } + storm::storage::SparseMatrix const& transitionMatrix = localA ? *localA : locallyConvertedMatrix; storm::storage::SparseMatrix backwardTransitions = transitionMatrix.transpose(); // Initialize the solution to the right-hand side of the equation system. @@ -49,8 +73,8 @@ namespace storm { storm::storage::FlexibleSparseMatrix flexibleMatrix(transitionMatrix, false); storm::storage::FlexibleSparseMatrix flexibleBackwardTransitions(backwardTransitions, true); - storm::settings::modules::EliminationSettings::EliminationOrder order = storm::settings::getModule().getEliminationOrder(); boost::optional> distanceBasedPriorities; + auto order = this->getSettings().getEliminationOrder(); if (eliminationOrderNeedsDistances(order)) { // Since we have no initial states at this point, we determine a representative of every BSCC regarding // the backward transitions, because this means that every row is reachable from this set of rows, which @@ -69,6 +93,11 @@ namespace storm { auto state = priorityQueue->pop(); 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(); + }; } template @@ -108,10 +137,47 @@ namespace storm { } } + template + EliminationLinearEquationSolverSettings& EliminationLinearEquationSolver::getSettings() { + return settings; + } + + template + EliminationLinearEquationSolverSettings const& EliminationLinearEquationSolver::getSettings() const { + return settings; + } + + 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); + } + + template + EliminationLinearEquationSolverSettings& EliminationLinearEquationSolverFactory::getSettings() { + return settings; + } + + template + EliminationLinearEquationSolverSettings const& EliminationLinearEquationSolverFactory::getSettings() const { + return settings; + } + + template class EliminationLinearEquationSolverSettings; + template class EliminationLinearEquationSolverSettings; + template class EliminationLinearEquationSolverSettings; + template class EliminationLinearEquationSolver; template class EliminationLinearEquationSolver; template class EliminationLinearEquationSolver; - + + template class EliminationLinearEquationSolverFactory; + template class EliminationLinearEquationSolverFactory; + template class EliminationLinearEquationSolverFactory; } } diff --git a/src/solver/EliminationLinearEquationSolver.h b/src/solver/EliminationLinearEquationSolver.h index 25dffa651..dfab51b50 100644 --- a/src/solver/EliminationLinearEquationSolver.h +++ b/src/solver/EliminationLinearEquationSolver.h @@ -3,30 +3,65 @@ #include "src/solver/LinearEquationSolver.h" +#include "src/settings/modules/EliminationSettings.h" + namespace storm { namespace solver { + template + class EliminationLinearEquationSolverSettings { + public: + EliminationLinearEquationSolverSettings(); + + void setEliminationOrder(storm::settings::modules::EliminationSettings::EliminationOrder const& order); + + storm::settings::modules::EliminationSettings::EliminationOrder getEliminationOrder() const; + + private: + storm::settings::modules::EliminationSettings::EliminationOrder order; + }; + /*! - * A class that uses gaussian elimination to implement the LinearEquationSolver interface. In particular + * A class that uses gaussian elimination to implement the LinearEquationSolver interface. */ template class EliminationLinearEquationSolver : public LinearEquationSolver { public: - - /*! - * Constructs a linear equation solver. - * - * @param A The matrix defining the coefficients of the linear equation system. - */ - EliminationLinearEquationSolver(storm::storage::SparseMatrix const& A); + EliminationLinearEquationSolver(storm::storage::SparseMatrix const& A, EliminationLinearEquationSolverSettings const& settings = EliminationLinearEquationSolverSettings()); + EliminationLinearEquationSolver(storm::storage::SparseMatrix&& A, EliminationLinearEquationSolverSettings const& settings = EliminationLinearEquationSolverSettings()); virtual void solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr) const override; virtual void performMatrixVectorMultiplication(std::vector& x, std::vector const* b, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const override; + EliminationLinearEquationSolverSettings& getSettings(); + EliminationLinearEquationSolverSettings const& getSettings() const; + private: - // A reference to the original matrix used for this equation solver. + void initializeSettings(); + + // If the solver takes posession of the matrix, we store the moved matrix in this member, so it gets deleted + // when the solver is destructed. + std::unique_ptr> localA; + + // A reference to the original sparse matrix given to this solver. If the solver takes posession of the matrix + // the reference refers to localA. storm::storage::SparseMatrix const& A; + // The settings used by the solver. + EliminationLinearEquationSolverSettings settings; + }; + + 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; + + EliminationLinearEquationSolverSettings& getSettings(); + EliminationLinearEquationSolverSettings const& getSettings() const; + + private: + EliminationLinearEquationSolverSettings settings; }; } } diff --git a/src/solver/GmmxxLinearEquationSolver.cpp b/src/solver/GmmxxLinearEquationSolver.cpp index 7a0dfdc33..0564938d5 100644 --- a/src/solver/GmmxxLinearEquationSolver.cpp +++ b/src/solver/GmmxxLinearEquationSolver.cpp @@ -16,14 +16,8 @@ namespace storm { namespace solver { - - template - GmmxxLinearEquationSolver::GmmxxLinearEquationSolver(storm::storage::SparseMatrix const& A, SolutionMethod method, double precision, uint_fast64_t maximalNumberOfIterations, Preconditioner preconditioner, bool relative, uint_fast64_t restart) : originalA(&A), gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(A)), method(method), precision(precision), maximalNumberOfIterations(maximalNumberOfIterations), preconditioner(preconditioner), relative(relative), restart(restart) { - // Intentionally left empty. - } - template - GmmxxLinearEquationSolver::GmmxxLinearEquationSolver(storm::storage::SparseMatrix const& A) : originalA(&A), gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(A)) { + GmmxxLinearEquationSolverSettings::GmmxxLinearEquationSolverSettings() { // Get the settings object to customize linear solving. storm::settings::modules::GmmxxEquationSolverSettings const& settings = storm::settings::getModule(); @@ -56,40 +50,112 @@ namespace storm { } } + template + void GmmxxLinearEquationSolverSettings::setSolutionMethod(SolutionMethod const& method) { + this->method = method; + } + + template + void GmmxxLinearEquationSolverSettings::setPreconditioner(Preconditioner const& preconditioner) { + this->preconditioner = preconditioner; + } + + template + void GmmxxLinearEquationSolverSettings::setPrecision(ValueType precision) { + this->precision = precision; + } + + template + void GmmxxLinearEquationSolverSettings::setMaximalNumberOfIterations(uint64_t maximalNumberOfIterations) { + this->maximalNumberOfIterations = maximalNumberOfIterations; + } + + template + void GmmxxLinearEquationSolverSettings::setRelativeTerminationCriterion(bool value) { + this->relative = value; + } + + template + void GmmxxLinearEquationSolverSettings::setNumberOfIterationsUntilRestart(uint64_t restart) { + this->restart = restart; + } + + template + typename GmmxxLinearEquationSolverSettings::SolutionMethod GmmxxLinearEquationSolverSettings::getSolutionMethod() const { + return method; + } + + template + typename GmmxxLinearEquationSolverSettings::Preconditioner GmmxxLinearEquationSolverSettings::getPreconditioner() const { + return preconditioner; + } + + template + ValueType GmmxxLinearEquationSolverSettings::getPrecision() const { + return precision; + } + + template + uint64_t GmmxxLinearEquationSolverSettings::getMaximalNumberOfIterations() const { + return maximalNumberOfIterations; + } + + template + bool GmmxxLinearEquationSolverSettings::getRelativeTerminationCriterion() const { + return relative; + } + + template + uint64_t GmmxxLinearEquationSolverSettings::getNumberOfIterationsUntilRestart() const { + return restart; + } + + template + GmmxxLinearEquationSolver::GmmxxLinearEquationSolver(storm::storage::SparseMatrix const& A, GmmxxLinearEquationSolverSettings const& settings) : localA(nullptr), A(A), gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(A)), settings(settings) { + // Intentionally left empty. + } + + template + GmmxxLinearEquationSolver::GmmxxLinearEquationSolver(storm::storage::SparseMatrix&& A, GmmxxLinearEquationSolverSettings const& settings) : localA(std::make_unique>(std::move(A))), A(*localA), gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(*localA)), settings(settings) { + // Intentionally left empty. + } + template void GmmxxLinearEquationSolver::solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult) const { - STORM_LOG_INFO("Using method '" << methodToString() << "' with preconditioner '" << preconditionerToString() << "' (max. " << maximalNumberOfIterations << " iterations)."); - if (method == SolutionMethod::Jacobi && preconditioner != Preconditioner::None) { + auto method = this->getSettings().getSolutionMethod(); + auto preconditioner = this->getSettings().getPreconditioner(); + STORM_LOG_INFO("Using method '" << method << "' with preconditioner '" << preconditioner << "' (max. " << this->getSettings().getMaximalNumberOfIterations() << " iterations)."); + if (method == GmmxxLinearEquationSolverSettings::SolutionMethod::Jacobi && preconditioner != GmmxxLinearEquationSolverSettings::Preconditioner::None) { STORM_LOG_WARN("Jacobi method currently does not support preconditioners. The requested preconditioner will be ignored."); } - if (method == SolutionMethod::Bicgstab || method == SolutionMethod::Qmr || method == SolutionMethod::Gmres) { + if (method == GmmxxLinearEquationSolverSettings::SolutionMethod::Bicgstab || method == GmmxxLinearEquationSolverSettings::SolutionMethod::Qmr || method == GmmxxLinearEquationSolverSettings::SolutionMethod::Gmres) { // Prepare an iteration object that determines the accuracy and the maximum number of iterations. - gmm::iteration iter(precision, 0, maximalNumberOfIterations); + gmm::iteration iter(this->getSettings().getPrecision(), 0, this->getSettings().getMaximalNumberOfIterations()); - if (method == SolutionMethod::Bicgstab) { - if (preconditioner == Preconditioner::Ilu) { + if (method == GmmxxLinearEquationSolverSettings::SolutionMethod::Bicgstab) { + if (preconditioner == GmmxxLinearEquationSolverSettings::Preconditioner::Ilu) { gmm::bicgstab(*gmmxxMatrix, x, b, gmm::ilu_precond>(*gmmxxMatrix), iter); - } else if (preconditioner == Preconditioner::Diagonal) { + } else if (preconditioner == GmmxxLinearEquationSolverSettings::Preconditioner::Diagonal) { gmm::bicgstab(*gmmxxMatrix, x, b, gmm::diagonal_precond>(*gmmxxMatrix), iter); - } else if (preconditioner == Preconditioner::None) { + } else if (preconditioner == GmmxxLinearEquationSolverSettings::Preconditioner::None) { gmm::bicgstab(*gmmxxMatrix, x, b, gmm::identity_matrix(), iter); } - } else if (method == SolutionMethod::Qmr) { - if (preconditioner == Preconditioner::Ilu) { + } else if (method == GmmxxLinearEquationSolverSettings::SolutionMethod::Qmr) { + if (preconditioner == GmmxxLinearEquationSolverSettings::Preconditioner::Ilu) { gmm::qmr(*gmmxxMatrix, x, b, gmm::ilu_precond>(*gmmxxMatrix), iter); - } else if (preconditioner == Preconditioner::Diagonal) { + } else if (preconditioner == GmmxxLinearEquationSolverSettings::Preconditioner::Diagonal) { gmm::qmr(*gmmxxMatrix, x, b, gmm::diagonal_precond>(*gmmxxMatrix), iter); - } else if (preconditioner == Preconditioner::None) { + } else if (preconditioner == GmmxxLinearEquationSolverSettings::Preconditioner::None) { gmm::qmr(*gmmxxMatrix, x, b, gmm::identity_matrix(), iter); } - } else if (method == SolutionMethod::Gmres) { - if (preconditioner == Preconditioner::Ilu) { - gmm::gmres(*gmmxxMatrix, x, b, gmm::ilu_precond>(*gmmxxMatrix), restart, iter); - } else if (preconditioner == Preconditioner::Diagonal) { - gmm::gmres(*gmmxxMatrix, x, b, gmm::diagonal_precond>(*gmmxxMatrix), restart, iter); - } else if (preconditioner == Preconditioner::None) { - gmm::gmres(*gmmxxMatrix, x, b, gmm::identity_matrix(), restart, iter); + } else if (method == GmmxxLinearEquationSolverSettings::SolutionMethod::Gmres) { + if (preconditioner == GmmxxLinearEquationSolverSettings::Preconditioner::Ilu) { + gmm::gmres(*gmmxxMatrix, x, b, gmm::ilu_precond>(*gmmxxMatrix), this->getSettings().getNumberOfIterationsUntilRestart(), iter); + } else if (preconditioner == GmmxxLinearEquationSolverSettings::Preconditioner::Diagonal) { + gmm::gmres(*gmmxxMatrix, x, b, gmm::diagonal_precond>(*gmmxxMatrix), this->getSettings().getNumberOfIterationsUntilRestart(), iter); + } else if (preconditioner == GmmxxLinearEquationSolverSettings::Preconditioner::None) { + gmm::gmres(*gmmxxMatrix, x, b, gmm::identity_matrix(), this->getSettings().getNumberOfIterationsUntilRestart(), iter); } } @@ -99,11 +165,11 @@ namespace storm { } else { STORM_LOG_WARN("Iterative solver did not converge."); } - } else if (method == SolutionMethod::Jacobi) { - uint_fast64_t iterations = solveLinearEquationSystemWithJacobi(*originalA, x, b, multiplyResult); + } else if (method == GmmxxLinearEquationSolverSettings::SolutionMethod::Jacobi) { + uint_fast64_t iterations = solveLinearEquationSystemWithJacobi(A, x, b, multiplyResult); // Check if the solver converged and issue a warning otherwise. - if (iterations < maximalNumberOfIterations) { + if (iterations < this->getSettings().getMaximalNumberOfIterations()) { STORM_LOG_INFO("Iterative solver converged after " << iterations << " iterations."); } else { STORM_LOG_WARN("Iterative solver did not converge."); @@ -173,14 +239,14 @@ namespace storm { uint_fast64_t iterationCount = 0; bool converged = false; - while (!converged && iterationCount < maximalNumberOfIterations && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) { + while (!converged && iterationCount < this->getSettings().getMaximalNumberOfIterations() && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) { // Compute D^-1 * (b - LU * x) and store result in nextX. gmm::mult(*gmmLU, *currentX, tmpX); gmm::add(b, gmm::scaled(tmpX, -storm::utility::one()), tmpX); storm::utility::vector::multiplyVectorsPointwise(jacobiDecomposition.second, tmpX, *nextX); // Now check if the process already converged within our precision. - converged = storm::utility::vector::equalModuloPrecision(*currentX, *nextX, precision, relative); + converged = storm::utility::vector::equalModuloPrecision(*currentX, *nextX, this->getSettings().getPrecision(), this->getSettings().getRelativeTerminationCriterion()); // Swap the two pointers as a preparation for the next iteration. std::swap(nextX, currentX); @@ -204,27 +270,39 @@ namespace storm { } template - std::string GmmxxLinearEquationSolver::methodToString() const { - switch (method) { - case SolutionMethod::Bicgstab: return "bicgstab"; - case SolutionMethod::Qmr: return "qmr"; - case SolutionMethod::Gmres: return "gmres"; - case SolutionMethod::Jacobi: return "jacobi"; - default: return "invalid"; - } + GmmxxLinearEquationSolverSettings& GmmxxLinearEquationSolver::getSettings() { + return settings; + } + + template + GmmxxLinearEquationSolverSettings const& GmmxxLinearEquationSolver::getSettings() const { + return settings; } template - std::string GmmxxLinearEquationSolver::preconditionerToString() const { - switch (preconditioner) { - case Preconditioner::Ilu: return "ilu"; - case Preconditioner::Diagonal: return "diagonal"; - case Preconditioner::None: return "none"; - default: return "invalid"; - } + 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); + } + + template + GmmxxLinearEquationSolverSettings& GmmxxLinearEquationSolverFactory::getSettings() { + return settings; + } + + template + GmmxxLinearEquationSolverSettings const& GmmxxLinearEquationSolverFactory::getSettings() const { + return settings; } // Explicitly instantiate the solver. + template class GmmxxLinearEquationSolverSettings; template class GmmxxLinearEquationSolver; + template class GmmxxLinearEquationSolverFactory; + } } \ No newline at end of file diff --git a/src/solver/GmmxxLinearEquationSolver.h b/src/solver/GmmxxLinearEquationSolver.h index a6c402f89..89448e4f3 100644 --- a/src/solver/GmmxxLinearEquationSolver.h +++ b/src/solver/GmmxxLinearEquationSolver.h @@ -1,6 +1,8 @@ #ifndef STORM_SOLVER_GMMXXLINEAREQUATIONSOLVER_H_ #define STORM_SOLVER_GMMXXLINEAREQUATIONSOLVER_H_ +#include + #include "src/utility/gmm.h" #include "LinearEquationSolver.h" @@ -8,48 +10,92 @@ namespace storm { namespace solver { - /*! - * A class that uses the gmm++ library to implement the LinearEquationSolver interface. - */ template - class GmmxxLinearEquationSolver : public LinearEquationSolver { + class GmmxxLinearEquationSolverSettings { public: // An enumeration specifying the available preconditioners. enum class Preconditioner { Ilu, Diagonal, None }; + + friend std::ostream& operator<<(std::ostream& out, Preconditioner const& preconditioner) { + switch (preconditioner) { + case GmmxxLinearEquationSolverSettings::Preconditioner::Ilu: out << "ilu"; break; + case GmmxxLinearEquationSolverSettings::Preconditioner::Diagonal: out << "diagonal"; break; + case GmmxxLinearEquationSolverSettings::Preconditioner::None: out << "none"; break; + } + return out; + } + // An enumeration specifying the available solution methods. enum class SolutionMethod { Bicgstab, Qmr, Gmres, Jacobi }; - /*! - * Constructs a linear equation solver with the given parameters. - * - * @param A The matrix defining the coefficients of the linear equation system. - * @param method The method to use for linear equation solving. - * @param precision The precision to use for convergence detection. - * @param maximalNumberOfIterations The maximal number of iterations do perform before iteration is aborted. - * @param preconditioner The preconditioner to use when solving linear equation systems. - * @param relative If set, the relative error rather than the absolute error is considered for convergence - * detection. - * @param restart An optional argument that specifies after how many iterations restarted methods are - * supposed to actually to a restart. - */ - GmmxxLinearEquationSolver(storm::storage::SparseMatrix const& A, SolutionMethod method, double precision, uint_fast64_t maximalNumberOfIterations, Preconditioner preconditioner, bool relative = true, uint_fast64_t restart = 0); + friend std::ostream& operator<<(std::ostream& out, SolutionMethod const& method) { + switch (method) { + case GmmxxLinearEquationSolverSettings::SolutionMethod::Bicgstab: out << "BiCGSTAB"; break; + case GmmxxLinearEquationSolverSettings::SolutionMethod::Qmr: out << "QMR"; break; + case GmmxxLinearEquationSolverSettings::SolutionMethod::Gmres: out << "GMRES"; break; + case GmmxxLinearEquationSolverSettings::SolutionMethod::Jacobi: out << "Jacobi"; break; + } + return out; + } + + GmmxxLinearEquationSolverSettings(); + + void setSolutionMethod(SolutionMethod const& method); + void setPreconditioner(Preconditioner const& preconditioner); + void setPrecision(ValueType precision); + void setMaximalNumberOfIterations(uint64_t maximalNumberOfIterations); + void setRelativeTerminationCriterion(bool value); + void setNumberOfIterationsUntilRestart(uint64_t restart); + + SolutionMethod getSolutionMethod() const; + Preconditioner getPreconditioner() const; + ValueType getPrecision() const; + uint64_t getMaximalNumberOfIterations() const; + bool getRelativeTerminationCriterion() const; + uint64_t getNumberOfIterationsUntilRestart() const; + + private: + // The method to use for solving linear equation systems. + SolutionMethod method; + + // The required precision for the iterative methods. + double precision; + + // The maximal number of iterations to do before iteration is aborted. + uint_fast64_t maximalNumberOfIterations; + + // The preconditioner to use when solving the linear equation system. + Preconditioner preconditioner; + + // Sets whether the relative or absolute error is to be considered for convergence detection. Note that this + // only applies to the Jacobi method for this solver. + bool relative; + + // A restart value that determines when restarted methods shall do so. + uint_fast64_t restart; + }; + + /*! + * A class that uses the gmm++ library to implement the LinearEquationSolver interface. + */ + template + class GmmxxLinearEquationSolver : public LinearEquationSolver { + public: + GmmxxLinearEquationSolver(storm::storage::SparseMatrix const& A, GmmxxLinearEquationSolverSettings const& settings = GmmxxLinearEquationSolverSettings()); + GmmxxLinearEquationSolver(storm::storage::SparseMatrix&& A, GmmxxLinearEquationSolverSettings const& settings = GmmxxLinearEquationSolverSettings()); - /*! - * Constructs a linear equation solver with parameters being set according to the settings object. - * - * @param A The matrix defining the coefficients of the linear equation system. - */ - GmmxxLinearEquationSolver(storm::storage::SparseMatrix const& A); - virtual void solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr) const override; virtual void performMatrixVectorMultiplication(std::vector& x, std::vector const* b, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const override; + GmmxxLinearEquationSolverSettings& getSettings(); + GmmxxLinearEquationSolverSettings const& getSettings() const; + private: /*! * Solves the linear equation system A*x = b given by the parameters using the Jacobi method. @@ -65,44 +111,32 @@ namespace storm { */ uint_fast64_t solveLinearEquationSystemWithJacobi(storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr) const; - /*! - * Retrieves the string representation of the solution method associated with this solver. - * - * @return The string representation of the solution method associated with this solver. - */ - std::string methodToString() const; - - /*! - * Retrieves the string representation of the preconditioner associated with this solver. - * - * @return The string representation of the preconditioner associated with this solver. - */ - std::string preconditionerToString() const; - - // A pointer to the original sparse matrix given to this solver. - storm::storage::SparseMatrix const* originalA; + // If the solver takes posession of the matrix, we store the moved matrix in this member, so it gets deleted + // when the solver is destructed. + std::unique_ptr> localA; + + // A reference to the original sparse matrix given to this solver. If the solver takes posession of the matrix + // the reference refers to localA. + storm::storage::SparseMatrix const& A; // The (gmm++) matrix associated with this equation solver. std::unique_ptr> gmmxxMatrix; - // The method to use for solving linear equation systems. - SolutionMethod method; - - // The required precision for the iterative methods. - double precision; - - // The maximal number of iterations to do before iteration is aborted. - uint_fast64_t maximalNumberOfIterations; - - // The preconditioner to use when solving the linear equation system. - Preconditioner preconditioner; - - // Sets whether the relative or absolute error is to be considered for convergence detection. Note that this - // only applies to the Jacobi method for this solver. - bool relative; - - // A restart value that determines when restarted methods shall do so. - uint_fast64_t restart; + // The settings used by the solver. + GmmxxLinearEquationSolverSettings settings; + }; + + 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; + + GmmxxLinearEquationSolverSettings& getSettings(); + GmmxxLinearEquationSolverSettings const& getSettings() const; + + private: + GmmxxLinearEquationSolverSettings settings; }; } // namespace solver diff --git a/src/solver/GmmxxMinMaxLinearEquationSolver.cpp b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp index e616f8d62..02835670f 100644 --- a/src/solver/GmmxxMinMaxLinearEquationSolver.cpp +++ b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp @@ -122,14 +122,15 @@ namespace storm { storm::storage::SparseMatrix submatrix = this->A.selectRowsFromRowGroups(scheduler, true); submatrix.convertToEquationSystem(); - GmmxxLinearEquationSolver gmmLinearEquationSolver(submatrix, storm::solver::GmmxxLinearEquationSolver::SolutionMethod::Gmres, this->precision, this->maximalNumberOfIterations, storm::solver::GmmxxLinearEquationSolver::Preconditioner::Ilu, this->relative, 50); + GmmxxLinearEquationSolver gmmxxLinearEquationSolver(submatrix); + storm::utility::vector::selectVectorValues(subB, scheduler, rowGroupIndices, b); // Copy X since we will overwrite it std::copy(currentX->begin(), currentX->end(), newX->begin()); // Solve the resulting linear equation system - gmmLinearEquationSolver.solveEquationSystem(*newX, subB, &deterministicMultiplyResult); + gmmxxLinearEquationSolver.solveEquationSystem(*newX, subB, &deterministicMultiplyResult); // Compute x' = A*x + b. This step is necessary to allow the choosing of the optimal policy for the next iteration. gmm::mult(*gmmxxMatrix, *newX, *multiplyResult); diff --git a/src/solver/LinearEquationSolver.cpp b/src/solver/LinearEquationSolver.cpp new file mode 100644 index 000000000..801855765 --- /dev/null +++ b/src/solver/LinearEquationSolver.cpp @@ -0,0 +1,87 @@ +#include "src/solver/LinearEquationSolver.h" + +#include "src/solver/SolverSelectionOptions.h" + +#include "src/solver/GmmxxLinearEquationSolver.h" +#include "src/solver/NativeLinearEquationSolver.h" +#include "src/solver/EigenLinearEquationSolver.h" +#include "src/solver/EliminationLinearEquationSolver.h" + +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/MarkovChainSettings.h" + +namespace storm { + namespace solver { + + template + std::unique_ptr> LinearEquationSolverFactory::create(storm::storage::SparseMatrix&& matrix) const { + return create(matrix); + } + + template + std::unique_ptr> GeneralLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { + return selectSolver(matrix); + } + + template + std::unique_ptr> GeneralLinearEquationSolverFactory::create(storm::storage::SparseMatrix&& matrix) const { + return selectSolver(std::move(matrix)); + } + + template + template + std::unique_ptr> GeneralLinearEquationSolverFactory::selectSolver(MatrixType&& matrix) const { + storm::solver::EquationSolverType equationSolver = storm::settings::getModule().getEquationSolver(); + switch (equationSolver) { + case storm::solver::EquationSolverType::Gmmxx: return std::make_unique>(std::forward(matrix)); + case storm::solver::EquationSolverType::Native: return std::make_unique>(std::forward(matrix)); + case storm::solver::EquationSolverType::Eigen: return std::make_unique>(std::forward(matrix)); + case storm::solver::EquationSolverType::Elimination: return std::make_unique>(std::forward(matrix)); + default: return std::make_unique>(std::forward(matrix)); + } + } + + 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 { + storm::solver::EquationSolverType equationSolver = storm::settings::getModule().getEquationSolver(); + switch (equationSolver) { + case storm::solver::EquationSolverType::Elimination: return std::make_unique>(matrix); + default: return std::make_unique>(matrix); + } + } + + 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 { + storm::solver::EquationSolverType equationSolver = storm::settings::getModule().getEquationSolver(); + switch (equationSolver) { + case storm::solver::EquationSolverType::Elimination: return std::make_unique>(matrix); + default: return std::make_unique>(matrix); + } + } + + template class LinearEquationSolverFactory; + template class LinearEquationSolverFactory; + template class LinearEquationSolverFactory; + + template class GeneralLinearEquationSolverFactory; + template class GeneralLinearEquationSolverFactory; + template class GeneralLinearEquationSolverFactory; + + } +} \ No newline at end of file diff --git a/src/solver/LinearEquationSolver.h b/src/solver/LinearEquationSolver.h index e85fe3cce..833a48229 100644 --- a/src/solver/LinearEquationSolver.h +++ b/src/solver/LinearEquationSolver.h @@ -48,6 +48,60 @@ namespace storm { virtual void performMatrixVectorMultiplication(std::vector& x, std::vector const* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const = 0; }; + template + class LinearEquationSolverFactory { + public: + /*! + * Creates a new linear equation solver instance with the given matrix. + * + * @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; + + /*! + * Creates a new linear equation solver instance with the given matrix. The caller gives up posession of the + * matrix by calling this function. + * + * @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; + }; + + 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; + + private: + template + std::unique_ptr> selectSolver(MatrixType&& matrix) 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; + + private: + template + std::unique_ptr> selectSolver(MatrixType&& matrix) 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; + + private: + template + std::unique_ptr> selectSolver(MatrixType&& matrix) const; + }; + } // namespace solver } // namespace storm diff --git a/src/solver/NativeLinearEquationSolver.cpp b/src/solver/NativeLinearEquationSolver.cpp index 9c402255b..bcfaf4782 100644 --- a/src/solver/NativeLinearEquationSolver.cpp +++ b/src/solver/NativeLinearEquationSolver.cpp @@ -7,31 +7,97 @@ #include "src/utility/vector.h" #include "src/exceptions/InvalidStateException.h" +#include "src/exceptions/InvalidSettingsException.h" namespace storm { namespace solver { - - template - NativeLinearEquationSolver::NativeLinearEquationSolver(storm::storage::SparseMatrix const& A, NativeLinearEquationSolverSolutionMethod method, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : A(A), method(method), precision(precision), relative(relative), maximalNumberOfIterations(maximalNumberOfIterations) { - // Intentionally left empty. - } - + template - NativeLinearEquationSolver::NativeLinearEquationSolver(storm::storage::SparseMatrix const& A, NativeLinearEquationSolverSolutionMethod method) : A(A), method(method) { - // Get the settings object to customize linear solving. + NativeLinearEquationSolverSettings::NativeLinearEquationSolverSettings() { storm::settings::modules::NativeEquationSolverSettings const& settings = storm::settings::getModule(); - // Get appropriate settings. + storm::settings::modules::NativeEquationSolverSettings::LinearEquationMethod methodAsSetting = settings.getLinearEquationSystemMethod(); + if (methodAsSetting == storm::settings::modules::NativeEquationSolverSettings::LinearEquationMethod::GaussSeidel) { + method = SolutionMethod::GaussSeidel; + } else if (methodAsSetting == storm::settings::modules::NativeEquationSolverSettings::LinearEquationMethod::Jacobi) { + method = SolutionMethod::Jacobi; + } else if (methodAsSetting == storm::settings::modules::NativeEquationSolverSettings::LinearEquationMethod::SOR) { + method = SolutionMethod::SOR; + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The selected solution technique is invalid for this solver."); + } + maximalNumberOfIterations = settings.getMaximalIterationCount(); precision = settings.getPrecision(); relative = settings.getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative; + omega = storm::settings::getModule().getOmega(); } - + + template + void NativeLinearEquationSolverSettings::setSolutionMethod(SolutionMethod const& method) { + this->method = method; + } + + template + void NativeLinearEquationSolverSettings::setPrecision(ValueType precision) { + this->precision = precision; + } + + template + void NativeLinearEquationSolverSettings::setMaximalNumberOfIterations(uint64_t maximalNumberOfIterations) { + this->maximalNumberOfIterations = maximalNumberOfIterations; + } + + template + void NativeLinearEquationSolverSettings::setRelativeTerminationCriterion(bool value) { + this->relative = value; + } + + template + void NativeLinearEquationSolverSettings::setOmega(ValueType omega) { + this->omega = omega; + } + + template + typename NativeLinearEquationSolverSettings::SolutionMethod NativeLinearEquationSolverSettings::getSolutionMethod() const { + return method; + } + + template + ValueType NativeLinearEquationSolverSettings::getPrecision() const { + return precision; + } + + template + uint64_t NativeLinearEquationSolverSettings::getMaximalNumberOfIterations() const { + return maximalNumberOfIterations; + } + + template + uint64_t NativeLinearEquationSolverSettings::getRelativeTerminationCriterion() const { + return relative; + } + + template + ValueType NativeLinearEquationSolverSettings::getOmega() const { + return omega; + } + + template + NativeLinearEquationSolver::NativeLinearEquationSolver(storm::storage::SparseMatrix const& A, NativeLinearEquationSolverSettings const& settings) : localA(nullptr), A(A), settings(settings) { + // Intentionally left empty. + } + + template + NativeLinearEquationSolver::NativeLinearEquationSolver(storm::storage::SparseMatrix&& A, NativeLinearEquationSolverSettings const& settings) : localA(std::make_unique>(std::move(A))), A(*localA), settings(settings) { + // Intentionally left empty. + } + template void NativeLinearEquationSolver::solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult) const { - if (method == NativeLinearEquationSolverSolutionMethod::SOR || method == NativeLinearEquationSolverSolutionMethod::GaussSeidel) { + if (this->getSettings().getSolutionMethod() == NativeLinearEquationSolverSettings::SolutionMethod::SOR || this->getSettings().getSolutionMethod() == NativeLinearEquationSolverSettings::SolutionMethod::GaussSeidel) { // Define the omega used for SOR. - ValueType omega = method == NativeLinearEquationSolverSolutionMethod::SOR ? storm::settings::getModule().getOmega() : storm::utility::one(); + ValueType omega = this->getSettings().getSolutionMethod() == NativeLinearEquationSolverSettings::SolutionMethod::SOR ? this->getSettings().getOmega() : storm::utility::one(); // To avoid copying the contents of the vector in the loop, we create a temporary x to swap with. bool tmpXProvided = true; @@ -47,11 +113,11 @@ namespace storm { uint_fast64_t iterationCount = 0; bool converged = false; - while (!converged && iterationCount < maximalNumberOfIterations) { + while (!converged && iterationCount < this->getSettings().getMaximalNumberOfIterations()) { A.performSuccessiveOverRelaxationStep(omega, x, b); // Now check if the process already converged within our precision. - converged = storm::utility::vector::equalModuloPrecision(x, *tmpX, static_cast(precision), relative) || (this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(x)); + converged = storm::utility::vector::equalModuloPrecision(x, *tmpX, static_cast(this->getSettings().getPrecision()), this->getSettings().getRelativeTerminationCriterion()) || (this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(x)); // If we did not yet converge, we need to copy the contents of x to *tmpX. if (!converged) { @@ -87,7 +153,7 @@ namespace storm { uint_fast64_t iterationCount = 0; bool converged = false; - while (!converged && iterationCount < maximalNumberOfIterations && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) { + while (!converged && iterationCount < this->getSettings().getMaximalNumberOfIterations() && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) { // Compute D^-1 * (b - LU * x) and store result in nextX. jacobiDecomposition.first.multiplyWithVector(*currentX, tmpX); storm::utility::vector::subtractVectors(b, tmpX, tmpX); @@ -97,7 +163,7 @@ namespace storm { std::swap(nextX, currentX); // Now check if the process already converged within our precision. - converged = storm::utility::vector::equalModuloPrecision(*currentX, *nextX, static_cast(precision), relative); + converged = storm::utility::vector::equalModuloPrecision(*currentX, *nextX, static_cast(this->getSettings().getPrecision()), this->getSettings().getRelativeTerminationCriterion()); // Increase iteration count so we can abort if convergence is too slow. ++iterationCount; @@ -152,20 +218,40 @@ namespace storm { delete copyX; } } - - + template - std::string NativeLinearEquationSolver::methodToString() const { - switch (method) { - case NativeLinearEquationSolverSolutionMethod::Jacobi: return "jacobi"; - case NativeLinearEquationSolverSolutionMethod::GaussSeidel: return "gauss-seidel"; - case NativeLinearEquationSolverSolutionMethod::SOR: return "sor"; - default: return "invalid"; - } + NativeLinearEquationSolverSettings& NativeLinearEquationSolver::getSettings() { + return settings; + } + + template + NativeLinearEquationSolverSettings const& NativeLinearEquationSolver::getSettings() const { + return settings; + } + + 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); + } + + template + NativeLinearEquationSolverSettings& NativeLinearEquationSolverFactory::getSettings() { + return settings; + } + + template + NativeLinearEquationSolverSettings const& NativeLinearEquationSolverFactory::getSettings() const { + return settings; } // Explicitly instantiate the linear equation solver. + template class NativeLinearEquationSolverSettings; template class NativeLinearEquationSolver; - template class NativeLinearEquationSolver; + template class NativeLinearEquationSolverFactory; } } \ No newline at end of file diff --git a/src/solver/NativeLinearEquationSolver.h b/src/solver/NativeLinearEquationSolver.h index 9dabd4e65..98abc4264 100644 --- a/src/solver/NativeLinearEquationSolver.h +++ b/src/solver/NativeLinearEquationSolver.h @@ -8,66 +8,75 @@ namespace storm { namespace solver { - // An enumeration specifying the available solution methods. - enum class NativeLinearEquationSolverSolutionMethod { - Jacobi, GaussSeidel, SOR + template + class NativeLinearEquationSolverSettings { + public: + enum class SolutionMethod { + Jacobi, GaussSeidel, SOR + }; + + NativeLinearEquationSolverSettings(); + + void setSolutionMethod(SolutionMethod const& method); + void setPrecision(ValueType precision); + void setMaximalNumberOfIterations(uint64_t maximalNumberOfIterations); + void setRelativeTerminationCriterion(bool value); + void setOmega(ValueType omega); + + SolutionMethod getSolutionMethod() const; + ValueType getPrecision() const; + uint64_t getMaximalNumberOfIterations() const; + uint64_t getRelativeTerminationCriterion() const; + ValueType getOmega() const; + + private: + SolutionMethod method; + double precision; + bool relative; + uint_fast64_t maximalNumberOfIterations; + ValueType omega; }; - std::ostream& operator<<(std::ostream& out, NativeLinearEquationSolverSolutionMethod const& method); - /*! * A class that uses Storm's native matrix operations to implement the LinearEquationSolver interface. */ template class NativeLinearEquationSolver : public LinearEquationSolver { public: + NativeLinearEquationSolver(storm::storage::SparseMatrix const& A, NativeLinearEquationSolverSettings const& settings = NativeLinearEquationSolverSettings()); + NativeLinearEquationSolver(storm::storage::SparseMatrix&& A, NativeLinearEquationSolverSettings const& settings = NativeLinearEquationSolverSettings()); - /*! - * Constructs a linear equation solver with parameters being set according to the settings object. - * - * @param A The matrix defining the coefficients of the linear equation system. - * @param method The method to use for solving linear equations. - */ - NativeLinearEquationSolver(storm::storage::SparseMatrix const& A, NativeLinearEquationSolverSolutionMethod method = NativeLinearEquationSolverSolutionMethod::GaussSeidel); - - /*! - * Constructs a linear equation solver with the given parameters. - * - * @param A The matrix defining the coefficients of the linear equation system. - * @param method The method to use for linear equation solving. - * @param precision The precision to use for convergence detection. - * @param maximalNumberOfIterations The maximal number of iterations do perform before iteration is aborted. - * @param relative If set, the relative error rather than the absolute error is considered for convergence - * detection. - */ - NativeLinearEquationSolver(storm::storage::SparseMatrix const& A, NativeLinearEquationSolverSolutionMethod method, double precision, uint_fast64_t maximalNumberOfIterations, bool relative = true); - virtual void solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr) const override; virtual void performMatrixVectorMultiplication(std::vector& x, std::vector const* b, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const override; + NativeLinearEquationSolverSettings& getSettings(); + NativeLinearEquationSolverSettings const& getSettings() const; + private: - /*! - * Retrieves the string representation of the solution method associated with this solver. - * - * @return The string representation of the solution method associated with this solver. - */ - std::string methodToString() 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. + std::unique_ptr> localA; - // A reference to the matrix the gives the coefficients of the linear equation system. + // A reference to the original sparse matrix given to this solver. If the solver takes posession of the matrix + // the reference refers to localA. storm::storage::SparseMatrix const& A; + + // The settings used by the solver. + NativeLinearEquationSolverSettings settings; + }; + + 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; - // The method to use for solving linear equation systems. - NativeLinearEquationSolverSolutionMethod method; - - // The required precision for the iterative methods. - double precision; - - // Sets whether the relative or absolute error is to be considered for convergence detection. - bool relative; + NativeLinearEquationSolverSettings& getSettings(); + NativeLinearEquationSolverSettings const& getSettings() const; - // The maximal number of iterations to do before iteration is aborted. - uint_fast64_t maximalNumberOfIterations; + private: + NativeLinearEquationSolverSettings settings; }; } } diff --git a/src/solver/NativeMinMaxLinearEquationSolver.cpp b/src/solver/NativeMinMaxLinearEquationSolver.cpp index 544840898..26d34f991 100644 --- a/src/solver/NativeMinMaxLinearEquationSolver.cpp +++ b/src/solver/NativeMinMaxLinearEquationSolver.cpp @@ -205,6 +205,5 @@ namespace storm { // Explicitly instantiate the solver. template class NativeMinMaxLinearEquationSolver; - template class NativeMinMaxLinearEquationSolver; } // namespace solver } // namespace storm diff --git a/src/solver/SolveGoal.cpp b/src/solver/SolveGoal.cpp index 642077c05..24ca63ea8 100644 --- a/src/solver/SolveGoal.cpp +++ b/src/solver/SolveGoal.cpp @@ -32,14 +32,14 @@ namespace storm { } template - std::unique_ptr> configureLinearEquationSolver(BoundedGoal const& goal, storm::utility::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { + std::unique_ptr> configureLinearEquationSolver(BoundedGoal const& goal, storm::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { std::unique_ptr> solver = factory.create(matrix); solver->setTerminationCondition(std::make_unique>(goal.relevantValues(), goal.thresholdValue(), goal.boundIsStrict(), goal.minimize())); return solver; } template - std::unique_ptr> configureLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { + std::unique_ptr> configureLinearEquationSolver(SolveGoal const& goal, storm::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { if (goal.isBounded()) { return configureLinearEquationSolver(static_cast const&>(goal), factory, matrix); } @@ -48,8 +48,8 @@ namespace storm { template std::unique_ptr> configureMinMaxLinearEquationSolver(BoundedGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); template std::unique_ptr> configureMinMaxLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); - template std::unique_ptr> configureLinearEquationSolver(BoundedGoal const& goal, storm::utility::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); - template std::unique_ptr> configureLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); + template std::unique_ptr> configureLinearEquationSolver(BoundedGoal const& goal, storm::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); + template std::unique_ptr> configureLinearEquationSolver(SolveGoal const& goal, storm::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); } } diff --git a/src/solver/SolveGoal.h b/src/solver/SolveGoal.h index fb28dfbb3..2dab69c4f 100644 --- a/src/solver/SolveGoal.h +++ b/src/solver/SolveGoal.h @@ -8,6 +8,8 @@ #include "src/logic/Bound.h" #include "src/storage/BitVector.h" +#include "src/solver/LinearEquationSolver.h" + namespace storm { namespace storage { template class SparseMatrix; @@ -101,10 +103,10 @@ namespace storm { std::unique_ptr> configureMinMaxLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); template - std::unique_ptr> configureLinearEquationSolver(BoundedGoal const& goal, storm::utility::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); + std::unique_ptr> configureLinearEquationSolver(BoundedGoal const& goal, storm::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); template - std::unique_ptr> configureLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); + std::unique_ptr> configureLinearEquationSolver(SolveGoal const& goal, storm::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); } } diff --git a/src/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/solver/TopologicalMinMaxLinearEquationSolver.cpp index 0140fec1d..2f6e51de1 100644 --- a/src/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -429,6 +429,5 @@ namespace storm { // Explicitly instantiate the solver. template class TopologicalMinMaxLinearEquationSolver; - template class TopologicalMinMaxLinearEquationSolver; } // namespace solver } // namespace storm diff --git a/src/utility/solver.cpp b/src/utility/solver.cpp index 242078c9e..cafe63565 100644 --- a/src/utility/solver.cpp +++ b/src/utility/solver.cpp @@ -45,119 +45,7 @@ namespace storm { std::unique_ptr> SymbolicGameSolverFactory::create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables) const { return std::unique_ptr>(new storm::solver::SymbolicGameSolver(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables, player2Variables)); } - - template - std::unique_ptr> LinearEquationSolverFactory::create(storm::storage::SparseMatrix&& matrix) const { - return create(matrix); - } - - template - std::unique_ptr> GeneralLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - return selectSolver(matrix); - } - - template - std::unique_ptr> GeneralLinearEquationSolverFactory::create(storm::storage::SparseMatrix&& matrix) const { - return selectSolver(std::move(matrix)); - } - - template - template - std::unique_ptr> GeneralLinearEquationSolverFactory::selectSolver(MatrixType&& matrix) const { - storm::solver::EquationSolverType equationSolver = storm::settings::getModule().getEquationSolver(); - switch (equationSolver) { - case storm::solver::EquationSolverType::Gmmxx: return std::make_unique>(std::forward(matrix)); - case storm::solver::EquationSolverType::Native: return std::make_unique>(std::forward(matrix)); - case storm::solver::EquationSolverType::Eigen: return std::make_unique>(std::forward(matrix)); - case storm::solver::EquationSolverType::Elimination: return std::make_unique>(std::forward(matrix)); - default: return std::make_unique>(std::forward(matrix)); - } - } - - 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 { - storm::solver::EquationSolverType equationSolver = storm::settings::getModule().getEquationSolver(); - switch (equationSolver) { - case storm::solver::EquationSolverType::Elimination: return std::make_unique>(matrix); - default: return std::make_unique>(matrix); - } - } - - 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 { - storm::solver::EquationSolverType equationSolver = storm::settings::getModule().getEquationSolver(); - switch (equationSolver) { - case storm::solver::EquationSolverType::Elimination: return std::make_unique>(matrix); - default: return std::make_unique>(matrix); - } - } - - template - std::unique_ptr> GmmxxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - return std::make_unique>(matrix); - } - - template - std::unique_ptr> GmmxxLinearEquationSolverFactory::create(storm::storage::SparseMatrix&& matrix) const { - return std::make_unique>(std::move(matrix)); - } - - template - std::unique_ptr> EigenLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - return std::make_unique>(matrix); - } - - template - std::unique_ptr> EigenLinearEquationSolverFactory::create(storm::storage::SparseMatrix&& matrix) const { - return std::make_unique>(std::move(matrix)); - } - - template - NativeLinearEquationSolverFactory::NativeLinearEquationSolverFactory() { - switch (storm::settings::getModule().getLinearEquationSystemMethod()) { - case settings::modules::NativeEquationSolverSettings::LinearEquationMethod::Jacobi: - this->method = storm::solver::NativeLinearEquationSolverSolutionMethod::Jacobi; - break; - case settings::modules::NativeEquationSolverSettings::LinearEquationMethod::GaussSeidel: - this->method = storm::solver::NativeLinearEquationSolverSolutionMethod::GaussSeidel; - break; - case settings::modules::NativeEquationSolverSettings::LinearEquationMethod::SOR: - this->method = storm::solver::NativeLinearEquationSolverSolutionMethod::SOR; - break; - } - } - - template - NativeLinearEquationSolverFactory::NativeLinearEquationSolverFactory(typename storm::solver::NativeLinearEquationSolverSolutionMethod method) : method(method) { - // Intentionally left empty. - } - - template - std::unique_ptr> NativeLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - return std::make_unique>(matrix, method); - } - - template - std::unique_ptr> NativeLinearEquationSolverFactory::create(storm::storage::SparseMatrix&& matrix) const { - return std::make_unique>(std::move(matrix), method); - } - template MinMaxLinearEquationSolverFactory::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection solver) { @@ -269,21 +157,8 @@ namespace storm { template class SymbolicMinMaxLinearEquationSolverFactory; template class SymbolicGameSolverFactory; template class SymbolicGameSolverFactory; - template class LinearEquationSolverFactory; - template class GeneralLinearEquationSolverFactory; - template class GmmxxLinearEquationSolverFactory; - template class EigenLinearEquationSolverFactory; - template class NativeLinearEquationSolverFactory; template class MinMaxLinearEquationSolverFactory; template class GameSolverFactory; - - template class LinearEquationSolverFactory; - template class GeneralLinearEquationSolverFactory; - template class EigenLinearEquationSolverFactory; - - template class LinearEquationSolverFactory; - template class GeneralLinearEquationSolverFactory; - template class EigenLinearEquationSolverFactory; } } } diff --git a/src/utility/solver.h b/src/utility/solver.h index a5fab02c7..d47c304a7 100644 --- a/src/utility/solver.h +++ b/src/utility/solver.h @@ -33,11 +33,6 @@ namespace storm { class LpSolver; class SmtSolver; - - template - class NativeLinearEquationSolver; - - enum class NativeLinearEquationSolverSolutionMethod; } namespace storage { @@ -77,87 +72,6 @@ namespace storm { public: virtual std::unique_ptr> create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables) const; }; - - template - class LinearEquationSolverFactory { - public: - /*! - * Creates a new linear equation solver instance with the given matrix. - * - * @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; - - /*! - * Creates a new linear equation solver instance with the given matrix. The caller gives up posession of the - * matrix by calling this function. - * - * @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; - }; - - 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; - - private: - template - std::unique_ptr> selectSolver(MatrixType&& matrix) 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; - - private: - template - std::unique_ptr> selectSolver(MatrixType&& matrix) 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; - - private: - template - std::unique_ptr> selectSolver(MatrixType&& matrix) const; - }; - - template - class NativeLinearEquationSolverFactory : public LinearEquationSolverFactory { - public: - NativeLinearEquationSolverFactory(); - NativeLinearEquationSolverFactory(storm::solver::NativeLinearEquationSolverSolutionMethod method); - - virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const override; - virtual std::unique_ptr> create(storm::storage::SparseMatrix&& matrix) const override; - - private: - storm::solver::NativeLinearEquationSolverSolutionMethod method; - }; - - 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; - }; - - 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; - }; template class MinMaxLinearEquationSolverFactory { diff --git a/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp index 113d0b1ba..8caa788bb 100644 --- a/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp @@ -3,7 +3,7 @@ #include "src/parser/FormulaParser.h" #include "src/logic/Formulas.h" -#include "src/utility/solver.h" +#include "src/solver/EigenLinearEquationSolver.h" #include "src/models/sparse/StandardRewardModel.h" #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" @@ -29,7 +29,7 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die) { ASSERT_EQ(dtmc->getNumberOfStates(), 13ull); ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::EigenLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); @@ -77,7 +77,7 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalNumber) { ASSERT_EQ(dtmc->getNumberOfStates(), 13ull); ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); @@ -129,7 +129,7 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalFunction) { ASSERT_EQ(variables.size(), 1ull); instantiation.emplace(*variables.begin(), storm::RationalNumber(1) / storm::RationalNumber(2)); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); @@ -174,7 +174,7 @@ TEST(EigenDtmcPrctlModelCheckerTest, Crowds) { ASSERT_EQ(8607ull, dtmc->getNumberOfStates()); ASSERT_EQ(15113ull, dtmc->getNumberOfTransitions()); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::EigenLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::EigenLinearEquationSolverFactory())); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); @@ -211,7 +211,7 @@ TEST(EigenDtmcPrctlModelCheckerTest, SynchronousLeader) { ASSERT_EQ(12400ull, dtmc->getNumberOfStates()); ASSERT_EQ(16495ull, dtmc->getNumberOfTransitions()); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::EigenLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); @@ -254,7 +254,7 @@ TEST(EigenDtmcPrctlModelCheckerTest, LRASingleBscc) { dtmc.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap)); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); @@ -278,7 +278,7 @@ TEST(EigenDtmcPrctlModelCheckerTest, LRASingleBscc) { dtmc.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap)); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); @@ -302,7 +302,7 @@ TEST(EigenDtmcPrctlModelCheckerTest, LRASingleBscc) { dtmc.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap)); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::EigenLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); @@ -365,7 +365,7 @@ TEST(EigenDtmcPrctlModelCheckerTest, LRA) { dtmc.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap)); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::EigenLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); @@ -394,7 +394,7 @@ TEST(EigenDtmcPrctlModelCheckerTest, Conditional) { std::shared_ptr> dtmc = model->as>(); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::EigenLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; diff --git a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp index 25763b37f..8f6814ded 100644 --- a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp @@ -35,7 +35,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Cluster) { uint_fast64_t initialState = *ctmc->getInitialStates().begin(); // Create model checker. - storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::make_unique>()); // Start checking properties. formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=100 !\"minimum\"]"); @@ -111,7 +111,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Embedded) { uint_fast64_t initialState = *ctmc->getInitialStates().begin(); // Create model checker. - storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::make_unique>()); // Start checking properties. formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10000 \"down\"]"); @@ -173,7 +173,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Polling) { uint_fast64_t initialState = *ctmc->getInitialStates().begin(); // Create model checker. - storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::make_unique>()); // Start checking properties. formula = formulaParser.parseSingleFormulaFromString("P=?[ F<=10 \"target\"]"); @@ -214,7 +214,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Tandem) { uint_fast64_t initialState = *ctmc->getInitialStates().begin(); // Create model checker. - storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::make_unique>()); // Start checking properties. formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"network_full\" ]"); diff --git a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp index bb96f4511..2290a1cec 100644 --- a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp @@ -3,7 +3,7 @@ #include "src/parser/FormulaParser.h" #include "src/logic/Formulas.h" -#include "src/utility/solver.h" +#include "src/solver/GmmxxLinearEquationSolver.h" #include "src/models/sparse/StandardRewardModel.h" #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" @@ -29,7 +29,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) { ASSERT_EQ(dtmc->getNumberOfStates(), 13ull); ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); @@ -73,7 +73,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { ASSERT_EQ(8607ull, dtmc->getNumberOfStates()); ASSERT_EQ(15113ull, dtmc->getNumberOfTransitions()); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); @@ -110,7 +110,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { ASSERT_EQ(12400ull, dtmc->getNumberOfStates()); ASSERT_EQ(16495ull, dtmc->getNumberOfTransitions()); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); @@ -153,7 +153,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) { dtmc.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap)); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); @@ -177,7 +177,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) { dtmc.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap)); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); @@ -201,7 +201,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) { dtmc.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap)); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); @@ -264,7 +264,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRA) { dtmc.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap)); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); @@ -291,7 +291,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Conditional) { std::shared_ptr> dtmc = model->as>(); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; diff --git a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp index 52196371d..b5e26c9ca 100644 --- a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp @@ -7,7 +7,7 @@ #include "src/builder/DdPrismModelBuilder.h" #include "src/storage/dd/DdType.h" -#include "src/utility/solver.h" +#include "src/solver/GmmxxLinearEquationSolver.h" #include "src/models/symbolic/StandardRewardModel.h" #include "src/modelchecker/csl/HybridCtmcCslModelChecker.h" #include "src/modelchecker/results/HybridQuantitativeCheckResult.h" @@ -43,7 +43,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Cudd) { std::shared_ptr> ctmc = model->as>(); // Create model checker. - storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::make_unique>()); // Start checking properties. formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=100 !\"minimum\"]"); @@ -140,7 +140,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Sylvan) { std::shared_ptr> ctmc = model->as>(); // Create model checker. - storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::make_unique>()); // Start checking properties. formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=100 !\"minimum\"]"); @@ -237,7 +237,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Cudd) { std::shared_ptr> ctmc = model->as>(); // Create model checker. - storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::make_unique>()); // Start checking properties. formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10000 \"down\"]"); @@ -316,7 +316,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Sylvan) { std::shared_ptr> ctmc = model->as>(); // Create model checker. - storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::make_unique>()); // Start checking properties. formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10000 \"down\"]"); @@ -388,7 +388,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Cudd) { std::shared_ptr> ctmc = model->as>(); // Create model checker. - storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::make_unique>()); // Start checking properties. formula = formulaParser.parseSingleFormulaFromString("P=?[ F<=10 \"target\"]"); @@ -424,7 +424,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Sylvan) { std::shared_ptr> ctmc = model->as>(); // Create model checker. - storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::make_unique>()); // Start checking properties. formula = formulaParser.parseSingleFormulaFromString("P=?[ F<=10 \"target\"]"); @@ -474,7 +474,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Cudd) { std::shared_ptr> ctmc = model->as>(); // Create model checker. - storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::make_unique>()); // Start checking properties. formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"network_full\" ]"); @@ -562,7 +562,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Sylvan) { std::shared_ptr> ctmc = model->as>(); // Create model checker. - storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::make_unique>()); // Start checking properties. formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"network_full\" ]"); diff --git a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp index 0c4679382..a8a0857ad 100644 --- a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp @@ -3,7 +3,7 @@ #include "src/parser/FormulaParser.h" #include "src/logic/Formulas.h" -#include "src/utility/solver.h" +#include "src/solver/GmmxxLinearEquationSolver.h" #include "src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h" #include "src/modelchecker/results/HybridQuantitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" @@ -40,7 +40,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Cudd) { std::shared_ptr> dtmc = model->as>(); - storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::make_unique>()); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); @@ -101,7 +101,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Sylvan) { std::shared_ptr> dtmc = model->as>(); - storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::make_unique>()); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); @@ -154,7 +154,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Cudd) { std::shared_ptr> dtmc = model->as>(); - storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::make_unique>()); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); @@ -198,7 +198,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) { std::shared_ptr> dtmc = model->as>(); - storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::make_unique>()); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); @@ -250,7 +250,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) { std::shared_ptr> dtmc = model->as>(); - storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::make_unique>()); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); @@ -302,7 +302,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) { std::shared_ptr> dtmc = model->as>(); - storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::make_unique>()); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); diff --git a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp index 65d58c19f..29a937a5e 100644 --- a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp @@ -6,7 +6,7 @@ #include "src/logic/Formulas.h" #include "src/builder/ExplicitModelBuilder.h" -#include "src/utility/solver.h" +#include "src/solver/NativeLinearEquationSolver.h" #include "src/models/sparse/StandardRewardModel.h" #include "src/modelchecker/csl/SparseCtmcCslModelChecker.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" @@ -32,7 +32,7 @@ TEST(NativeCtmcCslModelCheckerTest, Cluster) { uint_fast64_t initialState = *ctmc->getInitialStates().begin(); // Create model checker. - storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::make_unique>()); // Start checking properties. formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=100 !\"minimum\"]"); @@ -103,7 +103,7 @@ TEST(NativeCtmcCslModelCheckerTest, Embedded) { uint_fast64_t initialState = *ctmc->getInitialStates().begin(); // Create model checker. - storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::make_unique>()); // Start checking properties. formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10000 \"down\"]"); @@ -158,7 +158,7 @@ TEST(NativeCtmcCslModelCheckerTest, Polling) { uint_fast64_t initialState = *ctmc->getInitialStates().begin(); // Create model checker. - storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::make_unique>()); // Start checking properties. formula = formulaParser.parseSingleFormulaFromString("P=?[ F<=10 \"target\"]"); @@ -192,7 +192,7 @@ TEST(NativeCtmcCslModelCheckerTest, Tandem) { uint_fast64_t initialState = *ctmc->getInitialStates().begin(); // Create model checker. - storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::make_unique>()); // Start checking properties. formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"network_full\" ]"); diff --git a/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp index b53c080e2..b8b5bda5a 100644 --- a/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp @@ -4,7 +4,7 @@ #include "src/parser/FormulaParser.h" #include "src/settings/SettingMemento.h" #include "src/logic/Formulas.h" -#include "src/utility/solver.h" +#include "src/solver/NativeLinearEquationSolver.h" #include "src/models/sparse/StandardRewardModel.h" #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" @@ -29,7 +29,7 @@ TEST(NativeDtmcPrctlModelCheckerTest, Die) { ASSERT_EQ(dtmc->getNumberOfStates(), 13ull); ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); @@ -73,7 +73,7 @@ TEST(NativeDtmcPrctlModelCheckerTest, Crowds) { ASSERT_EQ(8607ull, dtmc->getNumberOfStates()); ASSERT_EQ(15113ull, dtmc->getNumberOfTransitions()); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); @@ -110,7 +110,7 @@ TEST(NativeDtmcPrctlModelCheckerTest, SynchronousLeader) { ASSERT_EQ(12400ull, dtmc->getNumberOfStates()); ASSERT_EQ(16495ull, dtmc->getNumberOfTransitions()); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); @@ -153,7 +153,10 @@ TEST(NativeDtmcPrctlModelCheckerTest, LRASingleBscc) { dtmc.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap)); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory(storm::solver::NativeLinearEquationSolverSolutionMethod::SOR, 0.9))); + auto factory = std::make_unique>(); + factory->getSettings().setSolutionMethod(storm::solver::NativeLinearEquationSolverSettings::SolutionMethod::SOR); + factory->getSettings().setOmega(0.9); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::move(factory)); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); @@ -177,7 +180,10 @@ TEST(NativeDtmcPrctlModelCheckerTest, LRASingleBscc) { dtmc.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap)); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory(storm::solver::NativeLinearEquationSolverSolutionMethod::SOR, 0.9))); + auto factory = std::make_unique>(); + factory->getSettings().setSolutionMethod(storm::solver::NativeLinearEquationSolverSettings::SolutionMethod::SOR); + factory->getSettings().setOmega(0.9); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::move(factory)); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); @@ -201,7 +207,10 @@ TEST(NativeDtmcPrctlModelCheckerTest, LRASingleBscc) { dtmc.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap)); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory(storm::solver::NativeLinearEquationSolverSolutionMethod::SOR, 0.9))); + auto factory = std::make_unique>(); + factory->getSettings().setSolutionMethod(storm::solver::NativeLinearEquationSolverSettings::SolutionMethod::SOR); + factory->getSettings().setOmega(0.9); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::move(factory)); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); @@ -216,7 +225,7 @@ TEST(NativeDtmcPrctlModelCheckerTest, LRASingleBscc) { TEST(NativeDtmcPrctlModelCheckerTest, LRA) { storm::storage::SparseMatrixBuilder matrixBuilder; - std::shared_ptr> mdp; + std::shared_ptr> dtmc; // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -262,9 +271,12 @@ TEST(NativeDtmcPrctlModelCheckerTest, LRA) { ap.addLabelToState("a", 13); ap.addLabelToState("a", 14); - mdp.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap)); + dtmc.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap)); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory(storm::solver::NativeLinearEquationSolverSolutionMethod::SOR, 0.9))); + auto factory = std::make_unique>(); + factory->getSettings().setSolutionMethod(storm::solver::NativeLinearEquationSolverSettings::SolutionMethod::SOR); + factory->getSettings().setOmega(0.9); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::move(factory)); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); diff --git a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp index d2e3ff7d6..58977dc60 100644 --- a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp @@ -7,7 +7,7 @@ #include "src/builder/DdPrismModelBuilder.h" #include "src/storage/dd/DdType.h" -#include "src/utility/solver.h" +#include "src/solver/NativeLinearEquationSolver.h" #include "src/models/symbolic/StandardRewardModel.h" #include "src/modelchecker/csl/HybridCtmcCslModelChecker.h" #include "src/modelchecker/results/HybridQuantitativeCheckResult.h" @@ -42,7 +42,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Cudd) { std::shared_ptr> ctmc = model->as>(); // Create model checker. - storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::make_unique>()); // Start checking properties. formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=100 !\"minimum\"]"); @@ -139,7 +139,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Sylvan) { std::shared_ptr> ctmc = model->as>(); // Create model checker. - storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::make_unique>()); // Start checking properties. formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=100 !\"minimum\"]"); @@ -236,7 +236,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Cudd) { std::shared_ptr> ctmc = model->as>(); // Create model checker. - storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::make_unique>()); // Start checking properties. formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10000 \"down\"]"); @@ -315,7 +315,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Sylvan) { std::shared_ptr> ctmc = model->as>(); // Create model checker. - storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::make_unique>()); // Start checking properties. formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10000 \"down\"]"); @@ -387,7 +387,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Cudd) { std::shared_ptr> ctmc = model->as>(); // Create model checker. - storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::make_unique>()); // Start checking properties. formula = formulaParser.parseSingleFormulaFromString("P=?[ F<=10 \"target\"]"); @@ -423,7 +423,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Sylvan) { std::shared_ptr> ctmc = model->as>(); // Create model checker. - storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::make_unique>()); // Start checking properties. formula = formulaParser.parseSingleFormulaFromString("P=?[ F<=10 \"target\"]"); @@ -473,7 +473,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Cudd) { std::shared_ptr> ctmc = model->as>(); // Create model checker. - storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::make_unique>()); // Start checking properties. formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"network_full\" ]"); @@ -563,7 +563,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Sylvan) { std::shared_ptr> ctmc = model->as>(); // Create model checker. - storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::make_unique>()); // Start checking properties. formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"network_full\" ]"); diff --git a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp index 072745694..bac3f8aa3 100644 --- a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp @@ -3,7 +3,7 @@ #include "src/parser/FormulaParser.h" #include "src/logic/Formulas.h" -#include "src/utility/solver.h" +#include "src/solver/NativeLinearEquationSolver.h" #include "src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h" #include "src/modelchecker/results/HybridQuantitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" @@ -41,7 +41,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_Cudd) { std::shared_ptr> dtmc = model->as>(); - storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::make_unique>()); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); @@ -102,7 +102,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_Sylvan) { std::shared_ptr> dtmc = model->as>(); - storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::make_unique>()); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); @@ -155,7 +155,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_Cudd) { std::shared_ptr> dtmc = model->as>(); - storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::make_unique>()); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); @@ -199,7 +199,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) { std::shared_ptr> dtmc = model->as>(); - storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::make_unique>()); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); @@ -251,7 +251,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) { std::shared_ptr> dtmc = model->as>(); - storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::make_unique>()); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); @@ -303,7 +303,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) { std::shared_ptr> dtmc = model->as>(); - storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::make_unique>()); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); diff --git a/test/functional/solver/EigenLinearEquationSolverTest.cpp b/test/functional/solver/EigenLinearEquationSolverTest.cpp index 65710ca1b..2bf575c2a 100644 --- a/test/functional/solver/EigenLinearEquationSolverTest.cpp +++ b/test/functional/solver/EigenLinearEquationSolverTest.cpp @@ -54,9 +54,10 @@ TEST(EigenLinearEquationSolver, SparseLU) { std::vector x(3); std::vector b = {16, -4, -7}; - ASSERT_NO_THROW(storm::solver::EigenLinearEquationSolver solver(A, storm::solver::EigenLinearEquationSolver::SolutionMethod::SparseLU, 1e-6, 10000, storm::solver::EigenLinearEquationSolver::Preconditioner::None)); - - storm::solver::EigenLinearEquationSolver solver(A, storm::solver::EigenLinearEquationSolver::SolutionMethod::SparseLU, 1e-6, 10000, storm::solver::EigenLinearEquationSolver::Preconditioner::None); + storm::solver::EigenLinearEquationSolver solver(A); + solver.getSettings().setSolutionMethod(storm::solver::EigenLinearEquationSolverSettings::SolutionMethod::SparseLU); + solver.getSettings().setMaximalNumberOfIterations(10000); + solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings::Preconditioner::None); ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); @@ -82,9 +83,7 @@ TEST(EigenLinearEquationSolver, SparseLU_RationalNumber) { std::vector x(3); std::vector b = {16, -4, -7}; - ASSERT_NO_THROW(storm::solver::EigenLinearEquationSolver solver(A, storm::solver::EigenLinearEquationSolver::SolutionMethod::SparseLU)); - - storm::solver::EigenLinearEquationSolver solver(A, storm::solver::EigenLinearEquationSolver::SolutionMethod::SparseLU); + storm::solver::EigenLinearEquationSolver solver(A); ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); ASSERT_TRUE(storm::utility::isOne(x[0])); ASSERT_TRUE(x[1] == 3); @@ -110,9 +109,7 @@ TEST(EigenLinearEquationSolver, SparseLU_RationalFunction) { std::vector x(3); std::vector b = {storm::RationalFunction(16), storm::RationalFunction(-4), storm::RationalFunction(-7)}; - ASSERT_NO_THROW(storm::solver::EigenLinearEquationSolver solver(A, storm::solver::EigenLinearEquationSolver::SolutionMethod::SparseLU)); - - storm::solver::EigenLinearEquationSolver solver(A, storm::solver::EigenLinearEquationSolver::SolutionMethod::SparseLU); + storm::solver::EigenLinearEquationSolver solver(A); ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); ASSERT_TRUE(storm::utility::isOne(x[0])); ASSERT_TRUE(x[1] == storm::RationalFunction(3)); @@ -138,9 +135,12 @@ TEST(DISABLED_EigenLinearEquationSolver, BiCGSTAB) { std::vector x(3); std::vector b = {16, -4, -7}; - ASSERT_NO_THROW(storm::solver::EigenLinearEquationSolver solver(A, storm::solver::EigenLinearEquationSolver::SolutionMethod::Bicgstab, 1e-6, 10000, storm::solver::EigenLinearEquationSolver::Preconditioner::None)); - - storm::solver::EigenLinearEquationSolver solver(A, storm::solver::EigenLinearEquationSolver::SolutionMethod::Bicgstab, 1e-6, 10000, storm::solver::EigenLinearEquationSolver::Preconditioner::None); + storm::solver::EigenLinearEquationSolver solver(A); + solver.getSettings().setSolutionMethod(storm::solver::EigenLinearEquationSolverSettings::SolutionMethod::Bicgstab); + solver.getSettings().setPrecision(1e-6); + solver.getSettings().setMaximalNumberOfIterations(10000); + solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings::Preconditioner::None); + ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); @@ -166,9 +166,11 @@ TEST(DISABLED_EigenLinearEquationSolver, BiCGSTAB_Ilu) { std::vector x(3); std::vector b = {16, -4, -7}; - ASSERT_NO_THROW(storm::solver::EigenLinearEquationSolver solver(A, storm::solver::EigenLinearEquationSolver::SolutionMethod::Bicgstab, 1e-6, 10000, storm::solver::EigenLinearEquationSolver::Preconditioner::Ilu)); - - storm::solver::EigenLinearEquationSolver solver(A, storm::solver::EigenLinearEquationSolver::SolutionMethod::Bicgstab, 1e-6, 10000, storm::solver::EigenLinearEquationSolver::Preconditioner::Ilu); + storm::solver::EigenLinearEquationSolver solver(A); + solver.getSettings().setSolutionMethod(storm::solver::EigenLinearEquationSolverSettings::SolutionMethod::Bicgstab); + solver.getSettings().setPrecision(1e-6); + solver.getSettings().setMaximalNumberOfIterations(10000); + solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings::Preconditioner::Ilu); ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); @@ -194,9 +196,11 @@ TEST(DISABLED_EigenLinearEquationSolver, BiCGSTAB_Diagonal) { std::vector x(3); std::vector b = {16, -4, -7}; - ASSERT_NO_THROW(storm::solver::EigenLinearEquationSolver solver(A, storm::solver::EigenLinearEquationSolver::SolutionMethod::Bicgstab, 1e-6, 10000, storm::solver::EigenLinearEquationSolver::Preconditioner::Diagonal)); - - storm::solver::EigenLinearEquationSolver solver(A, storm::solver::EigenLinearEquationSolver::SolutionMethod::Bicgstab, 1e-6, 10000, storm::solver::EigenLinearEquationSolver::Preconditioner::Diagonal); + storm::solver::EigenLinearEquationSolver solver(A); + solver.getSettings().setSolutionMethod(storm::solver::EigenLinearEquationSolverSettings::SolutionMethod::Bicgstab); + solver.getSettings().setPrecision(1e-6); + solver.getSettings().setMaximalNumberOfIterations(10000); + solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings::Preconditioner::Diagonal); ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); diff --git a/test/functional/solver/GmmxxLinearEquationSolverTest.cpp b/test/functional/solver/GmmxxLinearEquationSolverTest.cpp index 2820678d2..181d3429a 100644 --- a/test/functional/solver/GmmxxLinearEquationSolverTest.cpp +++ b/test/functional/solver/GmmxxLinearEquationSolverTest.cpp @@ -53,9 +53,13 @@ TEST(GmmxxLinearEquationSolver, gmres) { std::vector x(3); std::vector b = {16, -4, -7}; - ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver solver(A, storm::solver::GmmxxLinearEquationSolver::SolutionMethod::Gmres, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver::Preconditioner::None, true, 50)); + storm::solver::GmmxxLinearEquationSolver solver(A); + solver.getSettings().setSolutionMethod(storm::solver::GmmxxLinearEquationSolverSettings::SolutionMethod::Gmres); + solver.getSettings().setPrecision(1e-6); + solver.getSettings().setMaximalNumberOfIterations(10000); + solver.getSettings().setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings::Preconditioner::None); + solver.getSettings().setNumberOfIterationsUntilRestart(50); - storm::solver::GmmxxLinearEquationSolver solver(A, storm::solver::GmmxxLinearEquationSolver::SolutionMethod::Gmres, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver::Preconditioner::None, true, 50); ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); @@ -81,10 +85,19 @@ TEST(GmmxxLinearEquationSolver, qmr) { std::vector x(3); std::vector b = {16, -4, -7}; - ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver solver(A, storm::solver::GmmxxLinearEquationSolver::SolutionMethod::Qmr, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver::Preconditioner::None)); - - storm::solver::GmmxxLinearEquationSolver solver(A, storm::solver::GmmxxLinearEquationSolver::SolutionMethod::Qmr, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver::Preconditioner::None, true, 50); - ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); + storm::solver::GmmxxLinearEquationSolver solver(A); + solver.getSettings().setSolutionMethod(storm::solver::GmmxxLinearEquationSolverSettings::SolutionMethod::Qmr); + solver.getSettings().setPrecision(1e-6); + solver.getSettings().setMaximalNumberOfIterations(10000); + solver.getSettings().setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings::Preconditioner::None); + + storm::solver::GmmxxLinearEquationSolver solver2(A); + solver2.getSettings().setSolutionMethod(storm::solver::GmmxxLinearEquationSolverSettings::SolutionMethod::Qmr); + solver2.getSettings().setPrecision(1e-6); + solver2.getSettings().setMaximalNumberOfIterations(10000); + solver2.getSettings().setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings::Preconditioner::None); + + ASSERT_NO_THROW(solver2.solveEquationSystem(x, b)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision()); @@ -109,9 +122,12 @@ TEST(GmmxxLinearEquationSolver, bicgstab) { std::vector x(3); std::vector b = {16, -4, -7}; - ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver solver(A, storm::solver::GmmxxLinearEquationSolver::SolutionMethod::Bicgstab, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver::Preconditioner::None)); + storm::solver::GmmxxLinearEquationSolver solver(A); + solver.getSettings().setSolutionMethod(storm::solver::GmmxxLinearEquationSolverSettings::SolutionMethod::Bicgstab); + solver.getSettings().setPrecision(1e-6); + solver.getSettings().setMaximalNumberOfIterations(10000); + solver.getSettings().setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings::Preconditioner::None); - storm::solver::GmmxxLinearEquationSolver solver(A, storm::solver::GmmxxLinearEquationSolver::SolutionMethod::Bicgstab, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver::Preconditioner::None); ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); @@ -137,9 +153,11 @@ TEST(GmmxxLinearEquationSolver, jacobi) { std::vector x(3); std::vector b = {11, -16, 1}; - ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver solver(A, storm::solver::GmmxxLinearEquationSolver::SolutionMethod::Jacobi, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver::Preconditioner::None)); - - storm::solver::GmmxxLinearEquationSolver solver(A, storm::solver::GmmxxLinearEquationSolver::SolutionMethod::Jacobi, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver::Preconditioner::None); + storm::solver::GmmxxLinearEquationSolver solver(A); + solver.getSettings().setSolutionMethod(storm::solver::GmmxxLinearEquationSolverSettings::SolutionMethod::Jacobi); + solver.getSettings().setPrecision(1e-6); + solver.getSettings().setMaximalNumberOfIterations(10000); + solver.getSettings().setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings::Preconditioner::None); ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); @@ -165,9 +183,12 @@ TEST(GmmxxLinearEquationSolver, gmresilu) { std::vector x(3); std::vector b = {16, -4, -7}; - ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver solver(A, storm::solver::GmmxxLinearEquationSolver::SolutionMethod::Gmres, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver::Preconditioner::Ilu, true, 50)); - - storm::solver::GmmxxLinearEquationSolver solver(A, storm::solver::GmmxxLinearEquationSolver::SolutionMethod::Gmres, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver::Preconditioner::Ilu, true, 50); + storm::solver::GmmxxLinearEquationSolver solver(A); + solver.getSettings().setSolutionMethod(storm::solver::GmmxxLinearEquationSolverSettings::SolutionMethod::Gmres); + solver.getSettings().setPrecision(1e-6); + solver.getSettings().setMaximalNumberOfIterations(10000); + solver.getSettings().setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings::Preconditioner::Ilu); + solver.getSettings().setNumberOfIterationsUntilRestart(50); ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); @@ -193,9 +214,13 @@ TEST(GmmxxLinearEquationSolver, gmresdiag) { std::vector x(3); std::vector b = {16, -4, -7}; - ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver solver(A, storm::solver::GmmxxLinearEquationSolver::SolutionMethod::Gmres, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver::Preconditioner::Diagonal, true, 50)); - - storm::solver::GmmxxLinearEquationSolver solver(A, storm::solver::GmmxxLinearEquationSolver::SolutionMethod::Gmres, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver::Preconditioner::Diagonal, true, 50); + storm::solver::GmmxxLinearEquationSolver solver(A); + solver.getSettings().setSolutionMethod(storm::solver::GmmxxLinearEquationSolverSettings::SolutionMethod::Gmres); + solver.getSettings().setPrecision(1e-6); + solver.getSettings().setMaximalNumberOfIterations(10000); + solver.getSettings().setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings::Preconditioner::Diagonal); + solver.getSettings().setNumberOfIterationsUntilRestart(50); + ASSERT_NO_THROW(solver.solveEquationSystem(x, b)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp index 8f3f9607f..18d0f24bd 100644 --- a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp @@ -21,7 +21,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { ASSERT_EQ(2036647ull, dtmc->getNumberOfStates()); ASSERT_EQ(7362293ull, dtmc->getNumberOfTransitions()); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -59,7 +59,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { ASSERT_EQ(1312334ull, dtmc->getNumberOfStates()); ASSERT_EQ(1574477ull, dtmc->getNumberOfTransitions()); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; diff --git a/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp b/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp index 94635ee95..95a112a56 100644 --- a/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp @@ -21,7 +21,7 @@ TEST(NativeDtmcPrctlModelCheckerTest, Crowds) { ASSERT_EQ(2036647ull, dtmc->getNumberOfStates()); ASSERT_EQ(7362293ull, dtmc->getNumberOfTransitions()); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -59,7 +59,7 @@ TEST(NativeDtmcPrctlModelCheckerTest, SynchronousLeader) { ASSERT_EQ(1312334ull, dtmc->getNumberOfStates()); ASSERT_EQ(1574477ull, dtmc->getNumberOfTransitions()); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser;