diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 0597644e0..8b3a2d9c5 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -15,6 +15,7 @@ #include "src/exceptions/InvalidPropertyException.h" #include "src/exceptions/NotImplementedException.h" + namespace storm { namespace modelchecker { template diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 9fa3bac81..dc237b7e5 100644 --- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -5,17 +5,19 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" +#include "src/solver/LinearEquationSolver.h" + #include "src/storage/StronglyConnectedComponentDecomposition.h" #include "src/utility/macros.h" #include "src/utility/vector.h" #include "src/utility/graph.h" - #include "src/utility/numerical.h" #include "src/exceptions/InvalidStateException.h" #include "src/exceptions/InvalidPropertyException.h" + namespace storm { namespace modelchecker { namespace helper { diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.h b/src/modelchecker/csl/helper/SparseCtmcCslHelper.h index 55a143c8a..19ada5804 100644 --- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.h +++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.h @@ -7,6 +7,7 @@ #include "src/utility/solver.h" + namespace storm { namespace modelchecker { namespace helper { diff --git a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h index 03838e6c0..0b80f7f97 100644 --- a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h @@ -6,6 +6,7 @@ #include "src/utility/solver.h" #include "src/storage/dd/DdType.h" + namespace storm { namespace models { namespace symbolic { diff --git a/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp index d62ca4dcc..f3e9eeaf9 100644 --- a/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp @@ -1,5 +1,8 @@ #include "src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.h" + +#include "src/solver/LinearEquationSolver.h" + #include "src/storage/dd/CuddDdManager.h" #include "src/storage/dd/CuddAdd.h" #include "src/storage/dd/CuddBdd.h" diff --git a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index c4f488581..4169f9d0f 100644 --- a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -6,6 +6,9 @@ #include "src/utility/vector.h" #include "src/utility/graph.h" + +#include "src/solver/LinearEquationSolver.h" + #include "src/exceptions/InvalidStateException.h" #include "src/exceptions/InvalidPropertyException.h" diff --git a/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp index 4ef62691a..986b8cd35 100644 --- a/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp @@ -6,6 +6,8 @@ #include "src/storage/dd/CuddBdd.h" #include "src/storage/dd/CuddOdd.h" +#include "src/solver/SymbolicLinearEquationSolver.h" + #include "src/models/symbolic/StandardRewardModel.h" #include "src/utility/graph.h" diff --git a/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp index 6588e6f02..a0086e465 100644 --- a/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp @@ -1,5 +1,7 @@ #include "src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h" +#include "src/solver/SymbolicMinMaxLinearEquationSolver.h" + #include "src/storage/dd/CuddDdManager.h" #include "src/storage/dd/CuddAdd.h" #include "src/storage/dd/CuddBdd.h" diff --git a/src/solver/NativeLinearEquationSolver.cpp b/src/solver/NativeLinearEquationSolver.cpp index 312eaecf5..09a24972c 100644 --- a/src/solver/NativeLinearEquationSolver.cpp +++ b/src/solver/NativeLinearEquationSolver.cpp @@ -12,12 +12,12 @@ namespace storm { namespace solver { template - NativeLinearEquationSolver::NativeLinearEquationSolver(storm::storage::SparseMatrix const& A, SolutionMethod method, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : A(A), method(method), precision(precision), relative(relative), maximalNumberOfIterations(maximalNumberOfIterations) { + 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, SolutionMethod method) : A(A), method(method) { + NativeLinearEquationSolver::NativeLinearEquationSolver(storm::storage::SparseMatrix const& A, NativeLinearEquationSolverSolutionMethod method) : A(A), method(method) { // Get the settings object to customize linear solving. storm::settings::modules::NativeEquationSolverSettings const& settings = storm::settings::nativeEquationSolverSettings(); @@ -29,9 +29,9 @@ namespace storm { template void NativeLinearEquationSolver::solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult) const { - if (method == SolutionMethod::SOR || method == SolutionMethod::GaussSeidel) { + if (method == NativeLinearEquationSolverSolutionMethod::SOR || method == NativeLinearEquationSolverSolutionMethod::GaussSeidel) { // Define the omega used for SOR. - ValueType omega = method == SolutionMethod::SOR ? storm::settings::nativeEquationSolverSettings().getOmega() : storm::utility::one(); + ValueType omega = method == NativeLinearEquationSolverSolutionMethod::SOR ? storm::settings::nativeEquationSolverSettings().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; @@ -157,9 +157,9 @@ namespace storm { template std::string NativeLinearEquationSolver::methodToString() const { switch (method) { - case SolutionMethod::Jacobi: return "jacobi"; - case SolutionMethod::GaussSeidel: return "gauss-seidel"; - case SolutionMethod::SOR: return "sor"; + case NativeLinearEquationSolverSolutionMethod::Jacobi: return "jacobi"; + case NativeLinearEquationSolverSolutionMethod::GaussSeidel: return "gauss-seidel"; + case NativeLinearEquationSolverSolutionMethod::SOR: return "sor"; default: return "invalid"; } } diff --git a/src/solver/NativeLinearEquationSolver.h b/src/solver/NativeLinearEquationSolver.h index aa20b1e71..6fa972f05 100644 --- a/src/solver/NativeLinearEquationSolver.h +++ b/src/solver/NativeLinearEquationSolver.h @@ -6,16 +6,17 @@ namespace storm { namespace solver { + // An enumeration specifying the available solution methods. + enum class NativeLinearEquationSolverSolutionMethod { + Jacobi, GaussSeidel, SOR + }; /*! * A class that uses StoRM's native matrix operations to implement the LinearEquationSolver interface. */ template class NativeLinearEquationSolver : public LinearEquationSolver { public: - // An enumeration specifying the available solution methods. - enum class SolutionMethod { - Jacobi, GaussSeidel, SOR - }; + /*! * Constructs a linear equation solver with parameters being set according to the settings object. @@ -23,7 +24,7 @@ namespace storm { * @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, SolutionMethod method = SolutionMethod::Jacobi); + NativeLinearEquationSolver(storm::storage::SparseMatrix const& A, NativeLinearEquationSolverSolutionMethod method = NativeLinearEquationSolverSolutionMethod::Jacobi); /*! * Constructs a linear equation solver with the given parameters. @@ -35,7 +36,7 @@ namespace storm { * @param relative If set, the relative error rather than the absolute error is considered for convergence * detection. */ - NativeLinearEquationSolver(storm::storage::SparseMatrix const& A, SolutionMethod method, double precision, uint_fast64_t maximalNumberOfIterations, bool relative = true); + 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; @@ -53,7 +54,7 @@ namespace storm { storm::storage::SparseMatrix const& A; // The method to use for solving linear equation systems. - SolutionMethod method; + NativeLinearEquationSolverSolutionMethod method; // The required precision for the iterative methods. double precision; diff --git a/src/utility/solver.cpp b/src/utility/solver.cpp index 05d5bf479..0bad79f66 100644 --- a/src/utility/solver.cpp +++ b/src/utility/solver.cpp @@ -2,8 +2,10 @@ #include "src/solver/SymbolicGameSolver.h" +#include #include "src/solver/SymbolicLinearEquationSolver.h" +#include "src/solver/SymbolicMinMaxLinearEquationSolver.h" #include "src/solver/NativeLinearEquationSolver.h" #include "src/solver/GmmxxLinearEquationSolver.h" @@ -60,18 +62,18 @@ namespace storm { NativeLinearEquationSolverFactory::NativeLinearEquationSolverFactory() { switch (storm::settings::nativeEquationSolverSettings().getLinearEquationSystemMethod()) { case settings::modules::NativeEquationSolverSettings::LinearEquationMethod::Jacobi: - this->method = storm::solver::NativeLinearEquationSolver::SolutionMethod::Jacobi; + this->method = storm::solver::NativeLinearEquationSolverSolutionMethod::Jacobi; break; case settings::modules::NativeEquationSolverSettings::LinearEquationMethod::GaussSeidel: - this->method = storm::solver::NativeLinearEquationSolver::SolutionMethod::GaussSeidel; + this->method = storm::solver::NativeLinearEquationSolverSolutionMethod::GaussSeidel; case settings::modules::NativeEquationSolverSettings::LinearEquationMethod::SOR: - this->method = storm::solver::NativeLinearEquationSolver::SolutionMethod::SOR; + this->method = storm::solver::NativeLinearEquationSolverSolutionMethod::SOR; } omega = storm::settings::nativeEquationSolverSettings().getOmega(); } template - NativeLinearEquationSolverFactory::NativeLinearEquationSolverFactory(typename storm::solver::NativeLinearEquationSolver::SolutionMethod method, ValueType omega) : method(method), omega(omega) { + NativeLinearEquationSolverFactory::NativeLinearEquationSolverFactory(typename storm::solver::NativeLinearEquationSolverSolutionMethod method, ValueType omega) : method(method), omega(omega) { // Intentionally left empty. } @@ -83,8 +85,8 @@ namespace storm { template MinMaxLinearEquationSolverFactory::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection solver) { - setSolverType(solver); prefTech = storm::solver::MinMaxTechniqueSelection::FROMSETTINGS; + setSolverType(solver); } template diff --git a/src/utility/solver.h b/src/utility/solver.h index bcece2fb5..f112f9a99 100644 --- a/src/utility/solver.h +++ b/src/utility/solver.h @@ -1,11 +1,9 @@ #ifndef STORM_UTILITY_SOLVER_H_ #define STORM_UTILITY_SOLVER_H_ -#include "src/solver/SymbolicGameSolver.h" -#include "src/solver/SymbolicMinMaxLinearEquationSolver.h" -#include "src/solver/SymbolicLinearEquationSolver.h" -#include "src/solver/LinearEquationSolver.h" -#include "src/solver/NativeLinearEquationSolver.h" +#include +#include + #include "src/storage/dd/DdType.h" #include "src/solver/SolverSelectionOptions.h" @@ -13,10 +11,18 @@ namespace storm { namespace solver { template class SymbolicGameSolver; template class SymbolicLinearEquationSolver; + template class SymbolicMinMaxLinearEquationSolver; template class LinearEquationSolver; template class MinMaxLinearEquationSolver; class LpSolver; + + template class NativeLinearEquationSolver; + enum class NativeLinearEquationSolverSolutionMethod; + } + namespace storage { + template class SparseMatrix; } + namespace dd { template class Add; template class Bdd; @@ -62,12 +68,12 @@ namespace storm { class NativeLinearEquationSolverFactory : public LinearEquationSolverFactory { public: NativeLinearEquationSolverFactory(); - NativeLinearEquationSolverFactory(typename storm::solver::NativeLinearEquationSolver::SolutionMethod method, ValueType omega); + NativeLinearEquationSolverFactory(typename storm::solver::NativeLinearEquationSolverSolutionMethod method, ValueType omega); virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const override; private: - typename storm::solver::NativeLinearEquationSolver::SolutionMethod method; + typename storm::solver::NativeLinearEquationSolverSolutionMethod method; ValueType omega; }; diff --git a/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp index a2ec1d365..d5cb425af 100644 --- a/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp @@ -9,7 +9,7 @@ #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/settings/SettingsManager.h" - +#include "src/solver/NativeLinearEquationSolver.h" #include "src/settings/modules/GeneralSettings.h" #include "src/settings/modules/NativeEquationSolverSettings.h" @@ -153,7 +153,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, 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::NativeLinearEquationSolver::SolutionMethod::SOR, 0.9))); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory(storm::solver::NativeLinearEquationSolverSolutionMethod::SOR, 0.9))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); @@ -177,7 +177,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, 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::NativeLinearEquationSolver::SolutionMethod::SOR, 0.9))); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory(storm::solver::NativeLinearEquationSolverSolutionMethod::SOR, 0.9))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); @@ -201,7 +201,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, 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::NativeLinearEquationSolver::SolutionMethod::SOR, 0.9))); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory(storm::solver::NativeLinearEquationSolverSolutionMethod::SOR, 0.9))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); @@ -264,7 +264,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRA) { mdp.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap)); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory(storm::solver::NativeLinearEquationSolver::SolutionMethod::SOR, 0.9))); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory(storm::solver::NativeLinearEquationSolverSolutionMethod::SOR, 0.9))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");