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;