sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

some minor fixes 

Former-commit-id: f114c397f6
tempestpy_adaptions
dehnert 9 years ago
parent
94fd4cd9a8
commit
bb700457de
5 changed files with 24 additions and 16 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      src/solver/GmmxxLinearEquationSolver.cpp
  2. 2
      src/solver/NativeLinearEquationSolver.cpp
  3. 6
      src/solver/NativeLinearEquationSolver.h
  4. 20
      src/utility/solver.cpp
  5. 10
      test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp

2
src/solver/GmmxxLinearEquationSolver.cpp
View File

@ -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 {

2
src/solver/NativeLinearEquationSolver.cpp
View File

@ -80,7 +80,7 @@ namespace storm {
std::vector<ValueType> const* copyX = nextX;
std::vector<ValueType>* currentX = &x;
// Target vector for precision calculation.
// Target vector for multiplication.
std::vector<ValueType> tmpX(x.size());
// Set up additional environment variables.

6
src/solver/NativeLinearEquationSolver.h
View File

@ -1,6 +1,8 @@
#ifndef STORM_SOLVER_NATIVELINEAREQUATIONSOLVER_H_
#define STORM_SOLVER_NATIVELINEAREQUATIONSOLVER_H_
#include <ostream>
#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<ValueType> const& A, NativeLinearEquationSolverSolutionMethod method = NativeLinearEquationSolverSolutionMethod::Jacobi);
NativeLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, NativeLinearEquationSolverSolutionMethod method = NativeLinearEquationSolverSolutionMethod::GaussSeidel);
/*!
* Constructs a linear equation solver with the given parameters.

20
src/utility/solver.cpp
View File

@ -63,12 +63,14 @@ namespace storm {
NativeLinearEquationSolverFactory<ValueType>::NativeLinearEquationSolverFactory() {
switch (storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().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<storm::settings::modules::NativeEquationSolverSettings>().getOmega();
}
@ -116,7 +118,7 @@ namespace storm {
p1.reset(new storm::solver::GmmxxMinMaxLinearEquationSolver<ValueType>(matrix, this->prefTech));
break;
}
case storm::solver::EquationSolverType::Native:
case storm::solver::EquationSolverType::Native:
{
p1.reset(new storm::solver::NativeMinMaxLinearEquationSolver<ValueType>(matrix, this->prefTech));
break;
@ -131,12 +133,12 @@ namespace storm {
p1->setTrackScheduler(trackScheduler);
return p1;
}
template<typename ValueType>
std::unique_ptr<storm::solver::GameSolver<ValueType>> GameSolverFactory<ValueType>::create(storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix, storm::storage::SparseMatrix<ValueType> const& player2Matrix) const {
return std::unique_ptr<storm::solver::GameSolver<ValueType>>(new storm::solver::GameSolver<ValueType>(player1Matrix, player2Matrix));
}
std::unique_ptr<storm::solver::LpSolver> 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<storm::solver::LpSolver> GlpkLpSolverFactory::create(std::string const& name) const {
return LpSolverFactory::create(name, storm::solver::LpSolverTypeSelection::Glpk);
}
std::unique_ptr<storm::solver::LpSolver> GurobiLpSolverFactory::create(std::string const& name) const {
return LpSolverFactory::create(name, storm::solver::LpSolverTypeSelection::Gurobi);
}
@ -187,7 +189,7 @@ namespace storm {
std::unique_ptr<storm::utility::solver::SmtSolverFactory> factory(new MathsatSmtSolverFactory());
return factory->create(manager);
}
template class SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>;
template class SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>;
template class SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>;

10
test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
View File

@ -16,7 +16,7 @@
#include "src/settings/SettingMemento.h"
#include "src/parser/AutoParser.h"
TEST(SparseDtmcPrctlModelCheckerTest, Die) {
TEST(NativeDtmcPrctlModelCheckerTest, Die) {
std::shared_ptr<storm::models::sparse::Model<double>> 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<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
}
TEST(SparseDtmcPrctlModelCheckerTest, Crowds) {
TEST(NativeDtmcPrctlModelCheckerTest, Crowds) {
std::shared_ptr<storm::models::sparse::Model<double>> 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<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
}
TEST(SparseDtmcPrctlModelCheckerTest, SynchronousLeader) {
TEST(NativeDtmcPrctlModelCheckerTest, SynchronousLeader) {
std::shared_ptr<storm::models::sparse::Model<double>> 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<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
}
TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) {
TEST(NativeDtmcPrctlModelCheckerTest, LRASingleBscc) {
storm::storage::SparseMatrixBuilder<double> matrixBuilder;
std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc;
@ -214,7 +214,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) {
}
}
TEST(SparseDtmcPrctlModelCheckerTest, LRA) {
TEST(NativeDtmcPrctlModelCheckerTest, LRA) {
storm::storage::SparseMatrixBuilder<double> matrixBuilder;
std::shared_ptr<storm::models::sparse::Dtmc<double>> mdp;

Write Preview
Loading…
Cancel
Save