diff --git a/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp index 2d5973cc0..0040dd81f 100644 --- a/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp @@ -25,6 +25,7 @@ #include "storm/environment/solver/NativeSolverEnvironment.h" #include "storm/environment/solver/GmmxxSolverEnvironment.h" #include "storm/environment/solver/EigenSolverEnvironment.h" +#include "storm/environment/solver/TopologicalLinearEquationSolverEnvironment.h" namespace { @@ -255,6 +256,22 @@ namespace { } }; + class SparseTopologicalEigenLUEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models + static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; + static const bool isExact = true; + typedef storm::RationalNumber ValueType; + typedef storm::models::sparse::Dtmc ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Topological); + env.solver().topological().setUnderlyingSolverType(storm::solver::EquationSolverType::Eigen); + env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU); + return env; + } + }; + class HybridSylvanGmmxxGmresEnvironment { public: static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; @@ -467,6 +484,7 @@ namespace { SparseNativeSoundPowerEnvironment, SparseNativeQuickSoundPowerEnvironment, SparseNativeRationalSearchEnvironment, + SparseTopologicalEigenLUEnvironment, HybridSylvanGmmxxGmresEnvironment, HybridCuddNativeJacobiEnvironment, HybridCuddNativeSoundPowerEnvironment, diff --git a/src/test/storm/solver/LinearEquationSolverTest.cpp b/src/test/storm/solver/LinearEquationSolverTest.cpp index b4d7501eb..0ab4c1a55 100644 --- a/src/test/storm/solver/LinearEquationSolverTest.cpp +++ b/src/test/storm/solver/LinearEquationSolverTest.cpp @@ -6,6 +6,7 @@ #include "storm/environment/solver/NativeSolverEnvironment.h" #include "storm/environment/solver/GmmxxSolverEnvironment.h" #include "storm/environment/solver/EigenSolverEnvironment.h" +#include "storm/environment/solver/TopologicalLinearEquationSolverEnvironment.h" #include "storm/utility/vector.h" namespace { @@ -265,6 +266,19 @@ namespace { } }; + class TopologicalEigenRationalLUEnvironment { + public: + typedef storm::RationalNumber ValueType; + static const bool isExact = true; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Topological); + env.solver().topological().setUnderlyingSolverType(storm::solver::EquationSolverType::Eigen); + env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU); + return env; + } + }; + template class LinearEquationSolverTest : public ::testing::Test { public: @@ -296,7 +310,8 @@ namespace { EigenGmresIluEnvironment, EigenBicgstabNoneEnvironment, EigenDoubleLUEnvironment, - EigenRationalLUEnvironment + EigenRationalLUEnvironment, + TopologicalEigenRationalLUEnvironment > TestingTypes; TYPED_TEST_CASE(LinearEquationSolverTest, TestingTypes);