Browse Source

Enabled OVI for linear equation systems in test cases.

tempestpy_adaptions
Tim Quatmann 5 years ago
parent
commit
a8c0cfbcdd
  1. 18
      src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp
  2. 16
      src/test/storm/solver/LinearEquationSolverTest.cpp

18
src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp

@ -262,6 +262,23 @@ namespace {
} }
}; };
class SparseNativeOptimisticValueIterationEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
static const DtmcEngine engine = DtmcEngine::PrismSparse;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::sparse::Dtmc<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setForceSoundness(true);
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::OptimisticValueIteration);
env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
return env;
}
};
class SparseNativeIntervalIterationEnvironment { class SparseNativeIntervalIterationEnvironment {
public: public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
@ -553,6 +570,7 @@ namespace {
SparseNativeSorEnvironment, SparseNativeSorEnvironment,
SparseNativePowerEnvironment, SparseNativePowerEnvironment,
SparseNativeSoundValueIterationEnvironment, SparseNativeSoundValueIterationEnvironment,
SparseNativeOptimisticValueIterationEnvironment,
SparseNativeIntervalIterationEnvironment, SparseNativeIntervalIterationEnvironment,
SparseNativeRationalSearchEnvironment, SparseNativeRationalSearchEnvironment,
SparseTopologicalEigenLUEnvironment, SparseTopologicalEigenLUEnvironment,

16
src/test/storm/solver/LinearEquationSolverTest.cpp

@ -39,6 +39,21 @@ namespace {
} }
}; };
class NativeDoubleOptimisticValueIterationEnvironment {
public:
typedef double ValueType;
static const bool isExact = false;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setForceSoundness(true);
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::OptimisticValueIteration);
env.solver().native().setRelativeTerminationCriterion(false);
env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-6"));
return env;
}
};
class NativeDoubleIntervalIterationEnvironment { class NativeDoubleIntervalIterationEnvironment {
public: public:
typedef double ValueType; typedef double ValueType;
@ -294,6 +309,7 @@ namespace {
typedef ::testing::Types< typedef ::testing::Types<
NativeDoublePowerEnvironment, NativeDoublePowerEnvironment,
NativeDoubleSoundValueIterationEnvironment, NativeDoubleSoundValueIterationEnvironment,
NativeDoubleOptimisticValueIterationEnvironment,
NativeDoubleIntervalIterationEnvironment, NativeDoubleIntervalIterationEnvironment,
NativeDoubleJacobiEnvironment, NativeDoubleJacobiEnvironment,
NativeDoubleGaussSeidelEnvironment, NativeDoubleGaussSeidelEnvironment,

Loading…
Cancel
Save