Made model checker tests also build the model via conversion to Jani and with the Jit Builder.

7 years ago · 467abd72e9
5 changed files with 344 additions and 76 deletions
--- 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)
--- 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<ValueType> 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<storm::RationalNumber>(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<ValueType> 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<storm::RationalNumber>(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<ValueType> 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<ValueType> 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<ValueType> 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<ValueType> 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<ddType, ValueType> 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<storm::RationalNumber>(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<ddType, ValueType> 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<ddType, ValueType> ModelType;
@ -140,7 +193,7 @@ namespace {
        ValueType precision() const { return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");}
        bool isSparseModel() const { return std::is_same<typename TestType::ModelType, SparseModelType>::value; }
        bool isSymbolicModel() const { return std::is_same<typename TestType::ModelType, SymbolicModelType>::value; }
-        storm::settings::modules::CoreSettings::Engine getEngine() const { return TestType::engine; }
+        CtmcEngine getEngine() const { return TestType::engine; }
        
        template <typename MT = typename TestType::ModelType>
        typename std::enable_if<std::is_same<MT, SparseModelType>::value, std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>>>::type
@ -148,8 +201,18 @@ namespace {
            std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> 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<ValueType>(program, result.second)->template as<MT>();
+            if (TestType::engine == CtmcEngine::PrismSparse) {
+                result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
+                result.first = storm::api::buildSparseModel<ValueType>(program, result.second)->template as<MT>();
+            } 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<ValueType>(janiData.first, result.second, TestType::engine == CtmcEngine::JitSparse)->template as<MT>();
+            }
            return result;
        }
        
@ -159,8 +222,18 @@ namespace {
            std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> 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<TestType::ddType, ValueType>(program, result.second)->template as<MT>();
+            if (TestType::engine == CtmcEngine::PrismHybrid) {
+                result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
+                result.first = storm::api::buildSymbolicModel<TestType::ddType, ValueType>(program, result.second)->template as<MT>();
+            } 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<TestType::ddType, ValueType>(janiData.first, result.second)->template as<MT>();
+            }
            return result;
        }
        
@ -175,7 +248,7 @@ namespace {
        template <typename MT = typename TestType::ModelType>
        typename std::enable_if<std::is_same<MT, SparseModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type
        createModelChecker(std::shared_ptr<MT> 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<storm::modelchecker::SparseCtmcCslModelChecker<SparseModelType>>(*model);
            }
        }
@ -183,7 +256,7 @@ namespace {
        template <typename MT = typename TestType::ModelType>
        typename std::enable_if<std::is_same<MT, SymbolicModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type
        createModelChecker(std::shared_ptr<MT> 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<storm::modelchecker::HybridCtmcCslModelChecker<SymbolicModelType>>(*model);
            }
        }
@ -214,10 +287,13 @@ namespace {
  
    typedef ::testing::Types<
            SparseGmmxxGmresIluEnvironment,
+            JaniSparseGmmxxGmresIluEnvironment,
+            JitSparseGmmxxGmresIluEnvironment,
            SparseEigenDGmresEnvironment,
            SparseEigenDoubleLUEnvironment,
            SparseNativeSorEnvironment,
            HybridCuddGmmxxGmresEnvironment,
+            JaniHybridCuddGmmxxGmresEnvironment,
            HybridSylvanGmmxxGmresEnvironment
        > TestingTypes;
    
--- 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<ValueType> 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<storm::RationalNumber>(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<ValueType> 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<storm::RationalNumber>(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<ValueType> 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<ValueType> 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<ValueType> 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<ValueType> 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<ValueType> 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<ValueType> 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<ValueType> 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<ValueType> 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<ValueType> 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<ValueType> 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<ValueType> 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<ValueType> 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<ValueType> 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<ValueType> 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<ValueType> 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<ddType, ValueType> 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<ddType, ValueType> 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<ddType, ValueType> 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<ddType, ValueType> 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<ddType, ValueType> 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<storm::RationalNumber>(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<ddType, ValueType> 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<ddType, ValueType> 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<ddType, ValueType> ModelType;
@ -404,8 +457,18 @@ namespace {
            std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> 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<ValueType>(program, result.second)->template as<MT>();
+            if (TestType::engine == DtmcEngine::PrismSparse) {
+                result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
+                result.first = storm::api::buildSparseModel<ValueType>(program, result.second)->template as<MT>();
+            } 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<ValueType>(janiData.first, result.second, TestType::engine == DtmcEngine::JitSparse)->template as<MT>();
+            }
            return result;
        }
        
@ -415,8 +478,18 @@ namespace {
            std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> 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<TestType::ddType, ValueType>(program, result.second)->template as<MT>();
+            if (TestType::engine == DtmcEngine::Hybrid || TestType::engine == DtmcEngine::PrismDd) {
+                result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
+                result.first = storm::api::buildSymbolicModel<TestType::ddType, ValueType>(program, result.second)->template as<MT>();
+            } 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<TestType::ddType, ValueType>(janiData.first, result.second)->template as<MT>();
+            }
            return result;
        }
        
@ -431,7 +504,7 @@ namespace {
        template <typename MT = typename TestType::ModelType>
        typename std::enable_if<std::is_same<MT, SparseModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type
        createModelChecker(std::shared_ptr<MT> 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<storm::modelchecker::SparseDtmcPrctlModelChecker<SparseModelType>>(*model);
            }
        }
@ -439,9 +512,9 @@ namespace {
        template <typename MT = typename TestType::ModelType>
        typename std::enable_if<std::is_same<MT, SymbolicModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type
        createModelChecker(std::shared_ptr<MT> const& model) const {
-            if (TestType::engine == storm::settings::modules::CoreSettings::Engine::Hybrid) {
+            if (TestType::engine == DtmcEngine::Hybrid) {
                return std::make_shared<storm::modelchecker::HybridDtmcPrctlModelChecker<SymbolicModelType>>(*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<storm::modelchecker::SymbolicDtmcPrctlModelChecker<SymbolicModelType>>(*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;
--- 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<ValueType> ModelType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
+            env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(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<ValueType> ModelType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
+            env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(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<ValueType> 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<ValueType> 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<ValueType> 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<ValueType> ModelType;
@ -100,8 +133,18 @@ namespace {
            std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> 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<ValueType>(program, result.second)->template as<MT>();
+            if (TestType::engine == MaEngine::PrismSparse) {
+                result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
+                result.first = storm::api::buildSparseModel<ValueType>(program, result.second)->template as<MT>();
+            } 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<ValueType>(janiData.first, result.second, TestType::engine == MaEngine::JitSparse)->template as<MT>();
+            }
            return result;
        }
        
@ -127,7 +170,7 @@ namespace {
        template <typename MT = typename TestType::ModelType>
        typename std::enable_if<std::is_same<MT, SparseModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type
        createModelChecker(std::shared_ptr<MT> 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<storm::modelchecker::SparseMarkovAutomatonCslModelChecker<SparseModelType>>(*model);
            }
        }
@ -135,12 +178,11 @@ namespace {
        template <typename MT = typename TestType::ModelType>
        typename std::enable_if<std::is_same<MT, SymbolicModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type
        createModelChecker(std::shared_ptr<MT> const& model) const {
-//            if (TestType::engine == storm::settings::modules::CoreSettings::Engine::Hybrid) {
+//            if (TestType::engine == MaEngine::Hybrid) {
 //              return std::make_shared<storm::modelchecker::HybridMarkovAutomatonCslModelChecker<SymbolicModelType>>(*model);
-//            } else if (TestType::engine == storm::settings::modules::CoreSettings::Engine::Dd) {
+//            } else if (TestType::engine == MaEngine::Dd) {
 //                return std::make_shared<storm::modelchecker::SymbolicMarkovAutomatonCslModelChecker<SymbolicModelType>>(*model);
 //            }
-            return nullptr;
        }
        
        bool getQualitativeResultAtInitialState(std::shared_ptr<storm::models::Model<ValueType>> const& model, std::unique_ptr<storm::modelchecker::CheckResult>& result) {
@ -170,6 +212,8 @@ namespace {
  
    typedef ::testing::Types<
            SparseDoubleValueIterationEnvironment,
+            JaniSparseDoubleValueIterationEnvironment,
+            JitSparseDoubleValueIterationEnvironment,
            SparseDoubleIntervalIterationEnvironment,
            SparseRationalPolicyIterationEnvironment,
            SparseRationalRationalSearchEnvironment
--- 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<ValueType> ModelType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
+            env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(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<ValueType> 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<ValueType> ModelType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
+            env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(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<ValueType> 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<ValueType> 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<ValueType> 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<ValueType> 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<ValueType> 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<ValueType> 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<ddType, ValueType> 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<ddType, ValueType> 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<ddType, ValueType> 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<ddType, ValueType> 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<ddType, ValueType> ModelType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
+            env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(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<ddType, ValueType> 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<ddType, ValueType> 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<ddType, ValueType> 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<ddType, ValueType> ModelType;
@ -268,8 +317,18 @@ namespace {
            std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> 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<ValueType>(program, result.second)->template as<MT>();
+            if (TestType::engine == MdpEngine::PrismSparse) {
+                result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
+                result.first = storm::api::buildSparseModel<ValueType>(program, result.second)->template as<MT>();
+            } 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<ValueType>(janiData.first, result.second, TestType::engine == MdpEngine::JitSparse)->template as<MT>();
+            }
            return result;
        }
        
@ -279,8 +338,18 @@ namespace {
            std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> 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<TestType::ddType, ValueType>(program, result.second)->template as<MT>();
+            if (TestType::engine == MdpEngine::Hybrid || TestType::engine == MdpEngine::PrismDd) {
+                result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
+                result.first = storm::api::buildSymbolicModel<TestType::ddType, ValueType>(program, result.second)->template as<MT>();
+            } 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<TestType::ddType, ValueType>(janiData.first, result.second)->template as<MT>();
+            }
            return result;
        }
        
@ -295,7 +364,7 @@ namespace {
        template <typename MT = typename TestType::ModelType>
        typename std::enable_if<std::is_same<MT, SparseModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type
        createModelChecker(std::shared_ptr<MT> 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<storm::modelchecker::SparseMdpPrctlModelChecker<SparseModelType>>(*model);
            }
        }
@ -303,9 +372,9 @@ namespace {
        template <typename MT = typename TestType::ModelType>
        typename std::enable_if<std::is_same<MT, SymbolicModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type
        createModelChecker(std::shared_ptr<MT> const& model) const {
-            if (TestType::engine == storm::settings::modules::CoreSettings::Engine::Hybrid) {
+            if (TestType::engine == MdpEngine::Hybrid) {
                return std::make_shared<storm::modelchecker::HybridMdpPrctlModelChecker<SymbolicModelType>>(*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<storm::modelchecker::SymbolicMdpPrctlModelChecker<SymbolicModelType>>(*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]);