diff --git a/src/solver/GmmxxLinearEquationSolver.cpp b/src/solver/GmmxxLinearEquationSolver.cpp index faf13f0de..7a0dfdc33 100644 --- a/src/solver/GmmxxLinearEquationSolver.cpp +++ b/src/solver/GmmxxLinearEquationSolver.cpp @@ -10,6 +10,8 @@ #include "src/exceptions/InvalidStateException.h" #include "src/settings/modules/GmmxxEquationSolverSettings.h" +#include "src/solver/NativeLinearEquationSolver.h" + #include "src/utility/gmm.h" namespace storm { diff --git a/src/solver/NativeLinearEquationSolver.cpp b/src/solver/NativeLinearEquationSolver.cpp index 1d36cc5e5..9c402255b 100644 --- a/src/solver/NativeLinearEquationSolver.cpp +++ b/src/solver/NativeLinearEquationSolver.cpp @@ -80,7 +80,7 @@ namespace storm { std::vector const* copyX = nextX; std::vector* currentX = &x; - // Target vector for precision calculation. + // Target vector for multiplication. std::vector tmpX(x.size()); // Set up additional environment variables. diff --git a/src/solver/NativeLinearEquationSolver.h b/src/solver/NativeLinearEquationSolver.h index 42dbbd3d9..187bc8b5c 100644 --- a/src/solver/NativeLinearEquationSolver.h +++ b/src/solver/NativeLinearEquationSolver.h @@ -1,6 +1,8 @@ #ifndef STORM_SOLVER_NATIVELINEAREQUATIONSOLVER_H_ #define STORM_SOLVER_NATIVELINEAREQUATIONSOLVER_H_ +#include + #include "LinearEquationSolver.h" namespace storm { @@ -11,6 +13,8 @@ namespace storm { Jacobi, GaussSeidel, SOR }; + std::ostream& operator<<(std::ostream& out, NativeLinearEquationSolverSolutionMethod const& method); + /*! * A class that uses StoRM's native matrix operations to implement the LinearEquationSolver interface. */ @@ -24,7 +28,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, NativeLinearEquationSolverSolutionMethod method = NativeLinearEquationSolverSolutionMethod::Jacobi); + NativeLinearEquationSolver(storm::storage::SparseMatrix const& A, NativeLinearEquationSolverSolutionMethod method = NativeLinearEquationSolverSolutionMethod::GaussSeidel); /*! * Constructs a linear equation solver with the given parameters. diff --git a/src/utility/solver.cpp b/src/utility/solver.cpp index 77f644949..060fef4c9 100644 --- a/src/utility/solver.cpp +++ b/src/utility/solver.cpp @@ -63,12 +63,14 @@ namespace storm { NativeLinearEquationSolverFactory::NativeLinearEquationSolverFactory() { switch (storm::settings::getModule().getLinearEquationSystemMethod()) { case settings::modules::NativeEquationSolverSettings::LinearEquationMethod::Jacobi: - this->method = storm::solver::NativeLinearEquationSolverSolutionMethod::Jacobi; - break; + this->method = storm::solver::NativeLinearEquationSolverSolutionMethod::Jacobi; + break; case settings::modules::NativeEquationSolverSettings::LinearEquationMethod::GaussSeidel: - this->method = storm::solver::NativeLinearEquationSolverSolutionMethod::GaussSeidel; + this->method = storm::solver::NativeLinearEquationSolverSolutionMethod::GaussSeidel; + break; case settings::modules::NativeEquationSolverSettings::LinearEquationMethod::SOR: - this->method = storm::solver::NativeLinearEquationSolverSolutionMethod::SOR; + this->method = storm::solver::NativeLinearEquationSolverSolutionMethod::SOR; + break; } omega = storm::settings::getModule().getOmega(); } @@ -116,7 +118,7 @@ namespace storm { p1.reset(new storm::solver::GmmxxMinMaxLinearEquationSolver(matrix, this->prefTech)); break; } - case storm::solver::EquationSolverType::Native: + case storm::solver::EquationSolverType::Native: { p1.reset(new storm::solver::NativeMinMaxLinearEquationSolver(matrix, this->prefTech)); break; @@ -131,12 +133,12 @@ namespace storm { p1->setTrackScheduler(trackScheduler); return p1; } - + template std::unique_ptr> GameSolverFactory::create(storm::storage::SparseMatrix const& player1Matrix, storm::storage::SparseMatrix const& player2Matrix) const { return std::unique_ptr>(new storm::solver::GameSolver(player1Matrix, player2Matrix)); } - + std::unique_ptr LpSolverFactory::create(std::string const& name, storm::solver::LpSolverTypeSelection solvT) const { storm::solver::LpSolverType t; if(solvT == storm::solver::LpSolverTypeSelection::FROMSETTINGS) { @@ -157,7 +159,7 @@ namespace storm { std::unique_ptr GlpkLpSolverFactory::create(std::string const& name) const { return LpSolverFactory::create(name, storm::solver::LpSolverTypeSelection::Glpk); } - + std::unique_ptr GurobiLpSolverFactory::create(std::string const& name) const { return LpSolverFactory::create(name, storm::solver::LpSolverTypeSelection::Gurobi); } @@ -187,7 +189,7 @@ namespace storm { std::unique_ptr factory(new MathsatSmtSolverFactory()); return factory->create(manager); } - + template class SymbolicLinearEquationSolverFactory; template class SymbolicLinearEquationSolverFactory; template class SymbolicMinMaxLinearEquationSolverFactory; diff --git a/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp index 28e164a09..b53c080e2 100644 --- a/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp @@ -16,7 +16,7 @@ #include "src/settings/SettingMemento.h" #include "src/parser/AutoParser.h" -TEST(SparseDtmcPrctlModelCheckerTest, Die) { +TEST(NativeDtmcPrctlModelCheckerTest, Die) { std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.coin_flips.trans.rew"); // A parser that we use for conveniently constructing the formulas. @@ -60,7 +60,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, Die) { EXPECT_NEAR(3.6666650772094727, quantitativeResult4[0], storm::settings::getModule().getPrecision()); } -TEST(SparseDtmcPrctlModelCheckerTest, Crowds) { +TEST(NativeDtmcPrctlModelCheckerTest, Crowds) { std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.lab", "", ""); ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); @@ -97,7 +97,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, Crowds) { EXPECT_NEAR(0.32153900158185761, quantitativeResult3[0], storm::settings::getModule().getPrecision()); } -TEST(SparseDtmcPrctlModelCheckerTest, SynchronousLeader) { +TEST(NativeDtmcPrctlModelCheckerTest, SynchronousLeader) { std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.pick.trans.rew"); ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); @@ -134,7 +134,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, SynchronousLeader) { EXPECT_NEAR(1.0448979589010925, quantitativeResult3[0], storm::settings::getModule().getPrecision()); } -TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) { +TEST(NativeDtmcPrctlModelCheckerTest, LRASingleBscc) { storm::storage::SparseMatrixBuilder matrixBuilder; std::shared_ptr> dtmc; @@ -214,7 +214,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) { } } -TEST(SparseDtmcPrctlModelCheckerTest, LRA) { +TEST(NativeDtmcPrctlModelCheckerTest, LRA) { storm::storage::SparseMatrixBuilder matrixBuilder; std::shared_ptr> mdp;