diff --git a/src/test/storm/CMakeLists.txt b/src/test/storm/CMakeLists.txt index c745943b4..99bc99a12 100644 --- a/src/test/storm/CMakeLists.txt +++ b/src/test/storm/CMakeLists.txt @@ -13,7 +13,7 @@ foreach (testsuite abstraction adapter builder logic modelchecker parser permiss file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp) add_executable (test-${testsuite} ${TEST_${testsuite}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp) - target_link_libraries(test-${testsuite} storm storm-parsers) + target_link_libraries(test-${testsuite} storm storm-parsers storm-conv) target_link_libraries(test-${testsuite} ${STORM_TEST_LINK_LIBRARIES}) add_dependencies(test-${testsuite} test-resources) diff --git a/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp index bf6f8654f..9e4cac7f9 100644 --- a/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp @@ -5,6 +5,7 @@ #include "storm/api/builder.h" #include "storm-parsers/api/model_descriptions.h" #include "storm/api/properties.h" +#include "storm-conv/api/storm-conv.h" #include "storm-parsers/api/properties.h" #include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/Formulas.h" @@ -28,10 +29,46 @@ namespace { + enum class CtmcEngine {PrismSparse, JaniSparse, JitSparse, PrismHybrid, JaniHybrid}; + class SparseGmmxxGmresIluEnvironment { 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 CtmcEngine engine = CtmcEngine::PrismSparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Ctmc ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx); + env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres); + env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu); + env.solver().gmmxx().setPrecision(storm::utility::convertNumber(1e-8)); + return env; + } + }; + + class JaniSparseGmmxxGmresIluEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models + static const CtmcEngine engine = CtmcEngine::JaniSparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Ctmc ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx); + env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres); + env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu); + env.solver().gmmxx().setPrecision(storm::utility::convertNumber(1e-8)); + return env; + } + }; + + class JitSparseGmmxxGmresIluEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models + static const CtmcEngine engine = CtmcEngine::JitSparse; static const bool isExact = false; typedef double ValueType; typedef storm::models::sparse::Ctmc ModelType; @@ -48,7 +85,7 @@ namespace { class SparseEigenDGmresEnvironment { 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 CtmcEngine engine = CtmcEngine::PrismSparse; static const bool isExact = false; typedef double ValueType; typedef storm::models::sparse::Ctmc ModelType; @@ -65,7 +102,7 @@ namespace { class SparseEigenDoubleLUEnvironment { 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 CtmcEngine engine = CtmcEngine::PrismSparse; static const bool isExact = false; typedef double ValueType; typedef storm::models::sparse::Ctmc ModelType; @@ -80,7 +117,7 @@ namespace { class SparseNativeSorEnvironment { 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 CtmcEngine engine = CtmcEngine::PrismSparse; static const bool isExact = false; typedef double ValueType; typedef storm::models::sparse::Ctmc ModelType; @@ -98,7 +135,23 @@ namespace { class HybridCuddGmmxxGmresEnvironment { public: static const storm::dd::DdType ddType = storm::dd::DdType::CUDD; - static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Hybrid; + static const CtmcEngine engine = CtmcEngine::PrismHybrid; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::symbolic::Ctmc ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx); + env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres); + env.solver().gmmxx().setPrecision(storm::utility::convertNumber(1e-8)); + return env; + } + }; + + class JaniHybridCuddGmmxxGmresEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::CUDD; + static const CtmcEngine engine = CtmcEngine::JaniHybrid; static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::Ctmc ModelType; @@ -114,7 +167,7 @@ namespace { class HybridSylvanGmmxxGmresEnvironment { public: static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; - static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Hybrid; + static const CtmcEngine engine = CtmcEngine::PrismHybrid; static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::Ctmc ModelType; @@ -140,7 +193,7 @@ namespace { ValueType precision() const { return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");} bool isSparseModel() const { return std::is_same::value; } bool isSymbolicModel() const { return std::is_same::value; } - storm::settings::modules::CoreSettings::Engine getEngine() const { return TestType::engine; } + CtmcEngine getEngine() const { return TestType::engine; } template typename std::enable_if::value, std::pair, std::vector>>>::type @@ -148,8 +201,18 @@ namespace { std::pair, std::vector>> result; storm::prism::Program program = storm::api::parseProgram(pathToPrismFile, true); program = storm::utility::prism::preprocess(program, constantDefinitionString); - result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); - result.first = storm::api::buildSparseModel(program, result.second)->template as(); + if (TestType::engine == CtmcEngine::PrismSparse) { + result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + result.first = storm::api::buildSparseModel(program, result.second)->template as(); + } else if (TestType::engine == CtmcEngine::JaniSparse || TestType::engine == CtmcEngine::JitSparse) { + storm::converter::PrismToJaniConverterOptions options; + options.allVariablesGlobal = true; + options.janiOptions.standardCompliant = true; + options.janiOptions.exportFlattened = true; + auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + result.second = storm::api::extractFormulasFromProperties(janiData.second); + result.first = storm::api::buildSparseModel(janiData.first, result.second, TestType::engine == CtmcEngine::JitSparse)->template as(); + } return result; } @@ -159,8 +222,18 @@ namespace { std::pair, std::vector>> result; storm::prism::Program program = storm::api::parseProgram(pathToPrismFile, true); program = storm::utility::prism::preprocess(program, constantDefinitionString); - result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); - result.first = storm::api::buildSymbolicModel(program, result.second)->template as(); + if (TestType::engine == CtmcEngine::PrismHybrid) { + result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + result.first = storm::api::buildSymbolicModel(program, result.second)->template as(); + } else if (TestType::engine == CtmcEngine::JaniHybrid) { + storm::converter::PrismToJaniConverterOptions options; + options.allVariablesGlobal = true; + options.janiOptions.standardCompliant = true; + options.janiOptions.exportFlattened = true; + auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + result.second = storm::api::extractFormulasFromProperties(janiData.second); + result.first = storm::api::buildSymbolicModel(janiData.first, result.second)->template as(); + } return result; } @@ -175,7 +248,7 @@ namespace { template typename std::enable_if::value, std::shared_ptr>>::type createModelChecker(std::shared_ptr const& model) const { - if (TestType::engine == storm::settings::modules::CoreSettings::Engine::Sparse) { + if (TestType::engine == CtmcEngine::PrismSparse || TestType::engine == CtmcEngine::JaniSparse || TestType::engine == CtmcEngine::JitSparse) { return std::make_shared>(*model); } } @@ -183,7 +256,7 @@ namespace { template typename std::enable_if::value, std::shared_ptr>>::type createModelChecker(std::shared_ptr const& model) const { - if (TestType::engine == storm::settings::modules::CoreSettings::Engine::Hybrid) { + if (TestType::engine == CtmcEngine::PrismHybrid || TestType::engine == CtmcEngine::JaniHybrid) { return std::make_shared>(*model); } } @@ -214,10 +287,13 @@ namespace { typedef ::testing::Types< SparseGmmxxGmresIluEnvironment, + JaniSparseGmmxxGmresIluEnvironment, + JitSparseGmmxxGmresIluEnvironment, SparseEigenDGmresEnvironment, SparseEigenDoubleLUEnvironment, SparseNativeSorEnvironment, HybridCuddGmmxxGmresEnvironment, + JaniHybridCuddGmmxxGmresEnvironment, HybridSylvanGmmxxGmresEnvironment > TestingTypes; diff --git a/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp index f7f3b72a1..b5d5c801b 100644 --- a/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp @@ -3,6 +3,7 @@ #include "storm-config.h" #include "storm/api/builder.h" +#include "storm-conv/api/storm-conv.h" #include "storm-parsers/api/model_descriptions.h" #include "storm/api/properties.h" #include "storm-parsers/api/properties.h" @@ -30,10 +31,46 @@ namespace { + enum class DtmcEngine {PrismSparse, JaniSparse, JitSparse, Hybrid, PrismDd, JaniDd}; + class SparseGmmxxGmresIluEnvironment { 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 DtmcEngine engine = DtmcEngine::PrismSparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Dtmc ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx); + env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres); + env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu); + env.solver().gmmxx().setPrecision(storm::utility::convertNumber(1e-8)); + return env; + } + }; + + class JaniSparseGmmxxGmresIluEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models + static const DtmcEngine engine = DtmcEngine::JaniSparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Dtmc ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx); + env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres); + env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu); + env.solver().gmmxx().setPrecision(storm::utility::convertNumber(1e-8)); + return env; + } + }; + + class JitSparseGmmxxGmresIluEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models + static const DtmcEngine engine = DtmcEngine::JitSparse; static const bool isExact = false; typedef double ValueType; typedef storm::models::sparse::Dtmc ModelType; @@ -50,7 +87,7 @@ namespace { class SparseGmmxxGmresDiagEnvironment { 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 DtmcEngine engine = DtmcEngine::PrismSparse; static const bool isExact = false; typedef double ValueType; typedef storm::models::sparse::Dtmc ModelType; @@ -67,7 +104,7 @@ namespace { class SparseGmmxxBicgstabIluEnvironment { 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 DtmcEngine engine = DtmcEngine::PrismSparse; static const bool isExact = false; typedef double ValueType; typedef storm::models::sparse::Dtmc ModelType; @@ -84,7 +121,7 @@ namespace { class SparseEigenDGmresEnvironment { 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 DtmcEngine engine = DtmcEngine::PrismSparse; static const bool isExact = false; typedef double ValueType; typedef storm::models::sparse::Dtmc ModelType; @@ -101,7 +138,7 @@ namespace { class SparseEigenDoubleLUEnvironment { 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 DtmcEngine engine = DtmcEngine::PrismSparse; static const bool isExact = false; typedef double ValueType; typedef storm::models::sparse::Dtmc ModelType; @@ -116,7 +153,7 @@ namespace { class SparseEigenRationalLUEnvironment { 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 DtmcEngine engine = DtmcEngine::PrismSparse; static const bool isExact = true; typedef storm::RationalNumber ValueType; typedef storm::models::sparse::Dtmc ModelType; @@ -131,7 +168,7 @@ namespace { class SparseRationalEliminationEnvironment { 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 DtmcEngine engine = DtmcEngine::PrismSparse; static const bool isExact = true; typedef storm::RationalNumber ValueType; typedef storm::models::sparse::Dtmc ModelType; @@ -145,7 +182,7 @@ namespace { class SparseNativeJacobiEnvironment { 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 DtmcEngine engine = DtmcEngine::PrismSparse; static const bool isExact = false; typedef double ValueType; typedef storm::models::sparse::Dtmc ModelType; @@ -161,7 +198,7 @@ namespace { class SparseNativeWalkerChaeEnvironment { 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 DtmcEngine engine = DtmcEngine::PrismSparse; static const bool isExact = false; typedef double ValueType; typedef storm::models::sparse::Dtmc ModelType; @@ -178,7 +215,7 @@ namespace { class SparseNativeSorEnvironment { 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 DtmcEngine engine = DtmcEngine::PrismSparse; static const bool isExact = false; typedef double ValueType; typedef storm::models::sparse::Dtmc ModelType; @@ -194,7 +231,7 @@ namespace { class SparseNativePowerEnvironment { 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 DtmcEngine engine = DtmcEngine::PrismSparse; static const bool isExact = false; typedef double ValueType; typedef storm::models::sparse::Dtmc ModelType; @@ -210,7 +247,7 @@ namespace { class SparseNativeSoundValueIterationEnvironment { 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 DtmcEngine engine = DtmcEngine::PrismSparse; static const bool isExact = false; typedef double ValueType; typedef storm::models::sparse::Dtmc ModelType; @@ -227,7 +264,7 @@ namespace { class SparseNativeIntervalIterationEnvironment { 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 DtmcEngine engine = DtmcEngine::PrismSparse; static const bool isExact = false; typedef double ValueType; typedef storm::models::sparse::Dtmc ModelType; @@ -245,7 +282,7 @@ namespace { class SparseNativeRationalSearchEnvironment { 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 DtmcEngine engine = DtmcEngine::PrismSparse; static const bool isExact = true; typedef storm::RationalNumber ValueType; typedef storm::models::sparse::Dtmc ModelType; @@ -260,7 +297,7 @@ 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 DtmcEngine engine = DtmcEngine::PrismSparse; static const bool isExact = true; typedef storm::RationalNumber ValueType; typedef storm::models::sparse::Dtmc ModelType; @@ -276,7 +313,7 @@ namespace { class HybridSylvanGmmxxGmresEnvironment { public: static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; - static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Hybrid; + static const DtmcEngine engine = DtmcEngine::Hybrid; static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::Dtmc ModelType; @@ -292,7 +329,7 @@ namespace { class HybridCuddNativeJacobiEnvironment { public: static const storm::dd::DdType ddType = storm::dd::DdType::CUDD; - static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Hybrid; + static const DtmcEngine engine = DtmcEngine::Hybrid; static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::Dtmc ModelType; @@ -308,7 +345,7 @@ namespace { class HybridCuddNativeSoundValueIterationEnvironment { public: static const storm::dd::DdType ddType = storm::dd::DdType::CUDD; - static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Hybrid; + static const DtmcEngine engine = DtmcEngine::Hybrid; static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::Dtmc ModelType; @@ -325,7 +362,7 @@ namespace { class HybridSylvanNativeRationalSearchEnvironment { public: static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; - static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Hybrid; + static const DtmcEngine engine = DtmcEngine::Hybrid; static const bool isExact = true; typedef storm::RationalNumber ValueType; typedef storm::models::symbolic::Dtmc ModelType; @@ -340,7 +377,23 @@ namespace { class DdSylvanNativePowerEnvironment { public: static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; - static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Dd; + static const DtmcEngine engine = DtmcEngine::PrismDd; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::symbolic::Dtmc ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native); + env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Power); + env.solver().native().setPrecision(storm::utility::convertNumber(1e-8)); + return env; + } + }; + + class JaniDdSylvanNativePowerEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; + static const DtmcEngine engine = DtmcEngine::JaniDd; static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::Dtmc ModelType; @@ -356,7 +409,7 @@ namespace { class DdCuddNativeJacobiEnvironment { public: static const storm::dd::DdType ddType = storm::dd::DdType::CUDD; - static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Dd; + static const DtmcEngine engine = DtmcEngine::PrismDd; static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::Dtmc ModelType; @@ -372,7 +425,7 @@ namespace { class DdSylvanRationalSearchEnvironment { public: static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; - static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Dd; + static const DtmcEngine engine = DtmcEngine::PrismDd; static const bool isExact = true; typedef storm::RationalNumber ValueType; typedef storm::models::symbolic::Dtmc ModelType; @@ -404,8 +457,18 @@ namespace { std::pair, std::vector>> result; storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); program = storm::utility::prism::preprocess(program, constantDefinitionString); - result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); - result.first = storm::api::buildSparseModel(program, result.second)->template as(); + if (TestType::engine == DtmcEngine::PrismSparse) { + result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + result.first = storm::api::buildSparseModel(program, result.second)->template as(); + } else if (TestType::engine == DtmcEngine::JaniSparse || TestType::engine == DtmcEngine::JitSparse) { + storm::converter::PrismToJaniConverterOptions options; + options.allVariablesGlobal = true; + options.janiOptions.standardCompliant = true; + options.janiOptions.exportFlattened = true; + auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + result.second = storm::api::extractFormulasFromProperties(janiData.second); + result.first = storm::api::buildSparseModel(janiData.first, result.second, TestType::engine == DtmcEngine::JitSparse)->template as(); + } return result; } @@ -415,8 +478,18 @@ namespace { std::pair, std::vector>> result; storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); program = storm::utility::prism::preprocess(program, constantDefinitionString); - result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); - result.first = storm::api::buildSymbolicModel(program, result.second)->template as(); + if (TestType::engine == DtmcEngine::Hybrid || TestType::engine == DtmcEngine::PrismDd) { + result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + result.first = storm::api::buildSymbolicModel(program, result.second)->template as(); + } else if (TestType::engine == DtmcEngine::JaniDd) { + storm::converter::PrismToJaniConverterOptions options; + options.allVariablesGlobal = true; + options.janiOptions.standardCompliant = true; + options.janiOptions.exportFlattened = true; + auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + result.second = storm::api::extractFormulasFromProperties(janiData.second); + result.first = storm::api::buildSymbolicModel(janiData.first, result.second)->template as(); + } return result; } @@ -431,7 +504,7 @@ namespace { template typename std::enable_if::value, std::shared_ptr>>::type createModelChecker(std::shared_ptr const& model) const { - if (TestType::engine == storm::settings::modules::CoreSettings::Engine::Sparse) { + if (TestType::engine == DtmcEngine::PrismSparse || TestType::engine == DtmcEngine::JaniSparse || TestType::engine == DtmcEngine::JitSparse) { return std::make_shared>(*model); } } @@ -439,9 +512,9 @@ namespace { template typename std::enable_if::value, std::shared_ptr>>::type createModelChecker(std::shared_ptr const& model) const { - if (TestType::engine == storm::settings::modules::CoreSettings::Engine::Hybrid) { + if (TestType::engine == DtmcEngine::Hybrid) { return std::make_shared>(*model); - } else if (TestType::engine == storm::settings::modules::CoreSettings::Engine::Dd) { + } else if (TestType::engine == DtmcEngine::PrismDd || TestType::engine == DtmcEngine::JaniDd) { return std::make_shared>(*model); } } @@ -472,6 +545,8 @@ namespace { typedef ::testing::Types< SparseGmmxxGmresIluEnvironment, + JaniSparseGmmxxGmresIluEnvironment, + JitSparseGmmxxGmresIluEnvironment, SparseGmmxxGmresDiagEnvironment, SparseGmmxxBicgstabIluEnvironment, SparseEigenDGmresEnvironment, @@ -491,6 +566,7 @@ namespace { HybridCuddNativeSoundValueIterationEnvironment, HybridSylvanNativeRationalSearchEnvironment, DdSylvanNativePowerEnvironment, + JaniDdSylvanNativePowerEnvironment, DdCuddNativeJacobiEnvironment, DdSylvanRationalSearchEnvironment > TestingTypes; diff --git a/src/test/storm/modelchecker/MarkovAutomatonCslModelCheckerTest.cpp b/src/test/storm/modelchecker/MarkovAutomatonCslModelCheckerTest.cpp index c979c3777..11d29b6b6 100644 --- a/src/test/storm/modelchecker/MarkovAutomatonCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/MarkovAutomatonCslModelCheckerTest.cpp @@ -4,6 +4,7 @@ #include "test/storm_gtest.h" #include "storm/api/builder.h" +#include "storm-conv/api/storm-conv.h" #include "storm-parsers/api/model_descriptions.h" #include "storm/api/properties.h" #include "storm-parsers/api/properties.h" @@ -23,10 +24,42 @@ #include "storm/exceptions/UncheckedRequirementException.h" namespace { + + enum class MaEngine {PrismSparse, JaniSparse, JitSparse}; + + class SparseDoubleValueIterationEnvironment { 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 MaEngine engine = MaEngine::PrismSparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::MarkovAutomaton ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); + return env; + } + }; + class JaniSparseDoubleValueIterationEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models + static const MaEngine engine = MaEngine::JaniSparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::MarkovAutomaton ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); + return env; + } + }; + class JitSparseDoubleValueIterationEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models + static const MaEngine engine = MaEngine::JitSparse; static const bool isExact = false; typedef double ValueType; typedef storm::models::sparse::MarkovAutomaton ModelType; @@ -40,7 +73,7 @@ namespace { class SparseDoubleIntervalIterationEnvironment { 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 MaEngine engine = MaEngine::PrismSparse; static const bool isExact = false; typedef double ValueType; typedef storm::models::sparse::MarkovAutomaton ModelType; @@ -56,7 +89,7 @@ namespace { class SparseRationalPolicyIterationEnvironment { 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 MaEngine engine = MaEngine::PrismSparse; static const bool isExact = true; typedef storm::RationalNumber ValueType; typedef storm::models::sparse::MarkovAutomaton ModelType; @@ -69,7 +102,7 @@ namespace { class SparseRationalRationalSearchEnvironment { 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 MaEngine engine = MaEngine::PrismSparse; static const bool isExact = true; typedef storm::RationalNumber ValueType; typedef storm::models::sparse::MarkovAutomaton ModelType; @@ -100,8 +133,18 @@ namespace { std::pair, std::vector>> result; storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); program = storm::utility::prism::preprocess(program, constantDefinitionString); - result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); - result.first = storm::api::buildSparseModel(program, result.second)->template as(); + if (TestType::engine == MaEngine::PrismSparse) { + result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + result.first = storm::api::buildSparseModel(program, result.second)->template as(); + } else if (TestType::engine == MaEngine::JaniSparse || TestType::engine == MaEngine::JitSparse) { + storm::converter::PrismToJaniConverterOptions options; + options.allVariablesGlobal = true; + options.janiOptions.standardCompliant = true; + options.janiOptions.exportFlattened = true; + auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + result.second = storm::api::extractFormulasFromProperties(janiData.second); + result.first = storm::api::buildSparseModel(janiData.first, result.second, TestType::engine == MaEngine::JitSparse)->template as(); + } return result; } @@ -127,7 +170,7 @@ namespace { template typename std::enable_if::value, std::shared_ptr>>::type createModelChecker(std::shared_ptr const& model) const { - if (TestType::engine == storm::settings::modules::CoreSettings::Engine::Sparse) { + if (TestType::engine == MaEngine::PrismSparse || TestType::engine == MaEngine::JaniSparse || TestType::engine == MaEngine::JitSparse) { return std::make_shared>(*model); } } @@ -135,12 +178,11 @@ namespace { template typename std::enable_if::value, std::shared_ptr>>::type createModelChecker(std::shared_ptr const& model) const { -// if (TestType::engine == storm::settings::modules::CoreSettings::Engine::Hybrid) { +// if (TestType::engine == MaEngine::Hybrid) { // return std::make_shared>(*model); -// } else if (TestType::engine == storm::settings::modules::CoreSettings::Engine::Dd) { +// } else if (TestType::engine == MaEngine::Dd) { // return std::make_shared>(*model); // } - return nullptr; } bool getQualitativeResultAtInitialState(std::shared_ptr> const& model, std::unique_ptr& result) { @@ -170,6 +212,8 @@ namespace { typedef ::testing::Types< SparseDoubleValueIterationEnvironment, + JaniSparseDoubleValueIterationEnvironment, + JitSparseDoubleValueIterationEnvironment, SparseDoubleIntervalIterationEnvironment, SparseRationalPolicyIterationEnvironment, SparseRationalRationalSearchEnvironment diff --git a/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp index feb90d438..59c6614be 100644 --- a/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp @@ -4,6 +4,7 @@ #include "test/storm_gtest.h" #include "storm/api/builder.h" +#include "storm-conv/api/storm-conv.h" #include "storm-parsers/api/model_descriptions.h" #include "storm/api/properties.h" #include "storm-parsers/api/properties.h" @@ -27,10 +28,28 @@ #include "storm/exceptions/UncheckedRequirementException.h" namespace { + + enum class MdpEngine {PrismSparse, JaniSparse, JitSparse, Hybrid, PrismDd, JaniDd}; + class SparseDoubleValueIterationEnvironment { 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 MdpEngine engine = MdpEngine::PrismSparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Mdp ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); + return env; + } + }; + + class JaniSparseDoubleValueIterationEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models + static const MdpEngine engine = MdpEngine::JaniSparse; static const bool isExact = false; typedef double ValueType; typedef storm::models::sparse::Mdp ModelType; @@ -41,10 +60,26 @@ namespace { return env; } }; + + class JitSparseDoubleValueIterationEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models + static const MdpEngine engine = MdpEngine::JitSparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Mdp ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); + return env; + } + }; + class SparseDoubleIntervalIterationEnvironment { 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 MdpEngine engine = MdpEngine::PrismSparse; static const bool isExact = false; typedef double ValueType; typedef storm::models::sparse::Mdp ModelType; @@ -60,7 +95,7 @@ namespace { class SparseDoubleSoundValueIterationEnvironment { 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 MdpEngine engine = MdpEngine::PrismSparse; static const bool isExact = false; typedef double ValueType; typedef storm::models::sparse::Mdp ModelType; @@ -77,7 +112,7 @@ namespace { class SparseDoubleTopologicalValueIterationEnvironment { 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 MdpEngine engine = MdpEngine::PrismSparse; static const bool isExact = false; typedef double ValueType; typedef storm::models::sparse::Mdp ModelType; @@ -94,7 +129,7 @@ namespace { class SparseDoubleTopologicalSoundValueIterationEnvironment { 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 MdpEngine engine = MdpEngine::PrismSparse; static const bool isExact = false; typedef double ValueType; typedef storm::models::sparse::Mdp ModelType; @@ -112,7 +147,7 @@ namespace { class SparseRationalPolicyIterationEnvironment { 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 MdpEngine engine = MdpEngine::PrismSparse; static const bool isExact = true; typedef storm::RationalNumber ValueType; typedef storm::models::sparse::Mdp ModelType; @@ -125,7 +160,7 @@ namespace { class SparseRationalRationalSearchEnvironment { 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 MdpEngine engine = MdpEngine::PrismSparse; static const bool isExact = true; typedef storm::RationalNumber ValueType; typedef storm::models::sparse::Mdp ModelType; @@ -138,7 +173,7 @@ namespace { class HybridCuddDoubleValueIterationEnvironment { public: static const storm::dd::DdType ddType = storm::dd::DdType::CUDD; - static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Hybrid; + static const MdpEngine engine = MdpEngine::Hybrid; static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::Mdp ModelType; @@ -152,7 +187,7 @@ namespace { class HybridSylvanDoubleValueIterationEnvironment { public: static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; - static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Hybrid; + static const MdpEngine engine = MdpEngine::Hybrid; static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::Mdp ModelType; @@ -166,7 +201,7 @@ namespace { class HybridCuddDoubleSoundValueIterationEnvironment { public: static const storm::dd::DdType ddType = storm::dd::DdType::CUDD; - static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Hybrid; + static const MdpEngine engine = MdpEngine::Hybrid; static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::Mdp ModelType; @@ -182,7 +217,7 @@ namespace { class HybridSylvanRationalPolicyIterationEnvironment { public: static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; - static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Hybrid; + static const MdpEngine engine = MdpEngine::Hybrid; static const bool isExact = true; typedef storm::RationalNumber ValueType; typedef storm::models::symbolic::Mdp ModelType; @@ -195,7 +230,21 @@ namespace { class DdCuddDoubleValueIterationEnvironment { public: static const storm::dd::DdType ddType = storm::dd::DdType::CUDD; - static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Dd; + static const MdpEngine engine = MdpEngine::PrismDd; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::symbolic::Mdp ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); + return env; + } + }; + class JaniDdCuddDoubleValueIterationEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::CUDD; + static const MdpEngine engine = MdpEngine::JaniDd; static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::Mdp ModelType; @@ -209,7 +258,7 @@ namespace { class DdSylvanDoubleValueIterationEnvironment { public: static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; - static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Dd; + static const MdpEngine engine = MdpEngine::PrismDd; static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::Mdp ModelType; @@ -223,7 +272,7 @@ namespace { class DdCuddDoublePolicyIterationEnvironment { public: static const storm::dd::DdType ddType = storm::dd::DdType::CUDD; - static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Dd; + static const MdpEngine engine = MdpEngine::PrismDd; static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::Mdp ModelType; @@ -237,7 +286,7 @@ namespace { class DdSylvanRationalRationalSearchEnvironment { public: static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; - static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Dd; + static const MdpEngine engine = MdpEngine::PrismDd; static const bool isExact = true; typedef storm::RationalNumber ValueType; typedef storm::models::symbolic::Mdp ModelType; @@ -268,8 +317,18 @@ namespace { std::pair, std::vector>> result; storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); program = storm::utility::prism::preprocess(program, constantDefinitionString); - result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); - result.first = storm::api::buildSparseModel(program, result.second)->template as(); + if (TestType::engine == MdpEngine::PrismSparse) { + result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + result.first = storm::api::buildSparseModel(program, result.second)->template as(); + } else if (TestType::engine == MdpEngine::JaniSparse || TestType::engine == MdpEngine::JitSparse) { + storm::converter::PrismToJaniConverterOptions options; + options.allVariablesGlobal = true; + options.janiOptions.standardCompliant = true; + options.janiOptions.exportFlattened = true; + auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + result.second = storm::api::extractFormulasFromProperties(janiData.second); + result.first = storm::api::buildSparseModel(janiData.first, result.second, TestType::engine == MdpEngine::JitSparse)->template as(); + } return result; } @@ -279,8 +338,18 @@ namespace { std::pair, std::vector>> result; storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); program = storm::utility::prism::preprocess(program, constantDefinitionString); - result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); - result.first = storm::api::buildSymbolicModel(program, result.second)->template as(); + if (TestType::engine == MdpEngine::Hybrid || TestType::engine == MdpEngine::PrismDd) { + result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + result.first = storm::api::buildSymbolicModel(program, result.second)->template as(); + } else if (TestType::engine == MdpEngine::JaniDd) { + storm::converter::PrismToJaniConverterOptions options; + options.allVariablesGlobal = true; + options.janiOptions.standardCompliant = true; + options.janiOptions.exportFlattened = true; + auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + result.second = storm::api::extractFormulasFromProperties(janiData.second); + result.first = storm::api::buildSymbolicModel(janiData.first, result.second)->template as(); + } return result; } @@ -295,7 +364,7 @@ namespace { template typename std::enable_if::value, std::shared_ptr>>::type createModelChecker(std::shared_ptr const& model) const { - if (TestType::engine == storm::settings::modules::CoreSettings::Engine::Sparse) { + if (TestType::engine == MdpEngine::PrismSparse || TestType::engine == MdpEngine::JaniSparse || TestType::engine == MdpEngine::JitSparse) { return std::make_shared>(*model); } } @@ -303,9 +372,9 @@ namespace { template typename std::enable_if::value, std::shared_ptr>>::type createModelChecker(std::shared_ptr const& model) const { - if (TestType::engine == storm::settings::modules::CoreSettings::Engine::Hybrid) { + if (TestType::engine == MdpEngine::Hybrid) { return std::make_shared>(*model); - } else if (TestType::engine == storm::settings::modules::CoreSettings::Engine::Dd) { + } else if (TestType::engine == MdpEngine::PrismDd || TestType::engine == MdpEngine::JaniDd) { return std::make_shared>(*model); } } @@ -336,6 +405,8 @@ namespace { typedef ::testing::Types< SparseDoubleValueIterationEnvironment, + JaniSparseDoubleValueIterationEnvironment, + JitSparseDoubleValueIterationEnvironment, SparseDoubleIntervalIterationEnvironment, SparseDoubleSoundValueIterationEnvironment, SparseDoubleTopologicalValueIterationEnvironment, @@ -347,6 +418,7 @@ namespace { HybridCuddDoubleSoundValueIterationEnvironment, HybridSylvanRationalPolicyIterationEnvironment, DdCuddDoubleValueIterationEnvironment, + JaniDdCuddDoubleValueIterationEnvironment, DdSylvanDoubleValueIterationEnvironment, DdCuddDoublePolicyIterationEnvironment, DdSylvanRationalRationalSearchEnvironment @@ -494,7 +566,7 @@ namespace { // This example considers a zero-reward end component that does not reach the target // For some methods this requires end-component elimination which is (currently) not supported in the Dd engine - if (TypeParam::engine == storm::settings::modules::CoreSettings::Engine::Dd && this->env().solver().minMax().getMethod() == storm::solver::MinMaxMethod::RationalSearch) { + if (TypeParam::engine == MdpEngine::PrismDd && this->env().solver().minMax().getMethod() == storm::solver::MinMaxMethod::RationalSearch) { EXPECT_THROW(checker->check(this->env(), tasks[0]), storm::exceptions::UncheckedRequirementException); } else { result = checker->check(this->env(), tasks[0]);