Merge branch 'branch'

src/test/storm/CMakeLists.txt

@@ -9,15 +9,37 @@ register_source_groups_from_filestructure("${ALL_FILES}" test)
 # Note that the tests also need the source files, except for the main file
 include_directories(${GTEST_INCLUDE_DIR})
 
-foreach (testsuite abstraction adapter builder logic modelchecker parser permissiveschedulers solver storage transformer utility)
-
-	  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 storm-conv)
-	  target_link_libraries(test-${testsuite} ${STORM_TEST_LINK_LIBRARIES})
-
-	  add_dependencies(test-${testsuite} test-resources)
-	  add_test(NAME run-test-${testsuite} COMMAND $<TARGET_FILE:test-${testsuite}>)
-      add_dependencies(tests test-${testsuite})
-	
-endforeach ()
+# Set split and non-split test directories
+set(NON_SPLIT_TESTS abstraction adapter builder logic parser permissiveschedulers solver storage transformer utility)
+set(MODELCHECKER_TEST_SPLITS abstraction csl exploration multiobjective reachability)
+set(MODELCHECKER_PRCTL_TEST_SPLITS dtmc mdp)
+
+function(configure_testsuite_target testsuite)
+	#message(CONFIGURING TESTSUITE '${testsuite}') #DEBUG
+	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)
+	add_test(NAME run-test-${testsuite} COMMAND $<TARGET_FILE:test-${testsuite}>)
+	add_dependencies(tests test-${testsuite})
+endfunction()
+
+foreach(testsuite ${NON_SPLIT_TESTS})
+	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)
+	configure_testsuite_target(${testsuite})
+endforeach()
+
+# Modelchecker testsuite split
+foreach(modelchecker_split ${MODELCHECKER_TEST_SPLITS})
+	file(GLOB_RECURSE TEST_MODELCHECKER_${modelchecker_split}_FILES ${STORM_TESTS_BASE_PATH}/modelchecker/${modelchecker_split}/*.h ${STORM_TESTS_BASE_PATH}/modelchecker/${modelchecker_split}/*.cpp)
+	add_executable(test-modelchecker-${modelchecker_split} ${TEST_MODELCHECKER_${modelchecker_split}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp)
+	configure_testsuite_target(modelchecker-${modelchecker_split})
+endforeach()
+
+# Modelchecker-Prctl testsuite split
+foreach(prctl_split ${MODELCHECKER_PRCTL_TEST_SPLITS})
+	file(GLOB_RECURSE TEST_MODELCHECKER_PRCTL_${prctl_split}_FILES ${STORM_TESTS_BASE_PATH}/modelchecker/prctl/${prctl_split}/*.h ${STORM_TESTS_BASE_PATH}/modelchecker/prctl/${prctl_split}/*.cpp)
+	add_executable(test-modelchecker-prctl-${prctl_split} ${TEST_MODELCHECKER_PRCTL_${prctl_split}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp)
+	configure_testsuite_target(modelchecker-prctl-${prctl_split})
+endforeach()

src/test/storm/modelchecker/prctl/dtmc/ConditionalDtmcPrctlModelCheckerTest.cpp

@@ -0,0 +1,170 @@
+#include "gtest/gtest.h"
+#include "test/storm_gtest.h"
+#include "storm-config.h"
+
+#include "storm-parsers/parser/FormulaParser.h"
+#include "storm/logic/Formulas.h"
+#include "storm/models/sparse/StandardRewardModel.h"
+#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
+#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+#include "storm-parsers/parser/PrismParser.h"
+#include "storm/api/builder.h"
+#include "storm/storage/expressions/ExpressionManager.h"
+
+#include "storm/environment/solver/GmmxxSolverEnvironment.h"
+#include "storm/environment/solver/EigenSolverEnvironment.h"
+#include "storm/environment/solver/NativeSolverEnvironment.h"
+
+namespace {
+    
+    class GmmxxDoubleGmresEnvironment {
+    public:
+        typedef double ValueType;
+        static const bool isExact = false;
+        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 EigenDoubleDGmresEnvironment {
+    public:
+        typedef double ValueType;
+        static const bool isExact = false;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
+            env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::DGmres);
+            env.solver().eigen().setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner::Ilu);
+            env.solver().eigen().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
+            return env;
+        }
+    };
+    
+    class EigenRationalLUEnvironment {
+    public:
+        typedef storm::RationalNumber ValueType;
+        static const bool isExact = true;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
+            env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
+            return env;
+        }
+    };
+    
+    class NativeSorEnvironment {
+    public:
+        typedef double ValueType;
+        static const bool isExact = false;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
+            env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::SOR);
+            env.solver().native().setSorOmega(storm::utility::convertNumber<storm::RationalNumber>(0.9));
+            env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
+            return env;
+        }
+    };
+    
+    class NativePowerEnvironment {
+    public:
+        typedef double ValueType;
+        static const bool isExact = false;
+        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 NativeWalkerChaeEnvironment {
+    public:
+        typedef double ValueType;
+        static const bool isExact = false;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
+            env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::WalkerChae);
+            env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
+            env.solver().native().setMaximalNumberOfIterations(50000);
+            return env;
+        }
+    };
+    
+    template<typename TestType>
+    class ConditionalDtmcPrctlModelCheckerTest : public ::testing::Test {
+    public:
+        typedef typename TestType::ValueType ValueType;
+        ConditionalDtmcPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
+        storm::Environment const& env() const { return _environment; }
+        ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber<ValueType>(input);}
+        ValueType precision() const { return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");}
+
+    private:
+        storm::Environment _environment;
+    };
+  
+    typedef ::testing::Types<
+            GmmxxDoubleGmresEnvironment,
+            EigenDoubleDGmresEnvironment,
+            EigenRationalLUEnvironment,
+            NativeSorEnvironment,
+            NativePowerEnvironment,
+            NativeWalkerChaeEnvironment
+    > TestingTypes;
+    
+    TYPED_TEST_CASE(ConditionalDtmcPrctlModelCheckerTest, TestingTypes);
+
+ 
+    TYPED_TEST(ConditionalDtmcPrctlModelCheckerTest, Conditional) {
+        typedef typename TestFixture::ValueType ValueType;
+
+        storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/test_conditional.pm");
+    
+        storm::generator::NextStateGeneratorOptions options;
+        options.setBuildAllLabels().setBuildAllRewardModels();
+        std::shared_ptr<storm::models::sparse::Model<ValueType>> model = storm::builder::ExplicitModelBuilder<ValueType>(program, options).build();
+        ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
+        ASSERT_EQ(4ul, model->getNumberOfStates());
+        ASSERT_EQ(5ul, model->getNumberOfTransitions());
+        
+        std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc = model->template as<storm::models::sparse::Dtmc<ValueType>>();
+        
+        storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> checker(*dtmc);
+        
+        // A parser that we use for conveniently constructing the formulas.
+        
+        auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
+        storm::parser::FormulaParser formulaParser(expManager);
+        std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"target\"]");
+        
+        std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
+        storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
+        EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[0], this->precision());
+        
+        formula = formulaParser.parseSingleFormulaFromString("P=? [F \"target\" || F \"condition\"]");
+        
+        result = checker.check(this->env(), *formula);
+        storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<ValueType>();
+        EXPECT_NEAR(storm::utility::one<ValueType>(), quantitativeResult2[0], this->precision());
+        
+        formula = formulaParser.parseSingleFormulaFromString("R=? [F \"target\"]");
+        
+        result = checker.check(this->env(), *formula);
+        storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<ValueType>();
+        EXPECT_EQ(storm::utility::infinity<ValueType>(), quantitativeResult3[0]);
+        
+        formula = formulaParser.parseSingleFormulaFromString("R=? [F \"target\" || F \"condition\"]");
+        
+        result = checker.check(this->env(), *formula);
+        storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<ValueType>();
+        EXPECT_NEAR(storm::utility::one<ValueType>(), quantitativeResult4[0], this->precision());
+    }
+}

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

@@ -0,0 +1,701 @@
+#include "gtest/gtest.h"
+#include "test/storm_gtest.h"
+#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"
+#include "storm-parsers/parser/FormulaParser.h"
+#include "storm/logic/Formulas.h"
+#include "storm/solver/EigenLinearEquationSolver.h"
+#include "storm/models/sparse/StandardRewardModel.h"
+#include "storm/models/symbolic/StandardRewardModel.h"
+#include "storm/models/sparse/Dtmc.h"
+#include "storm/models/symbolic/Dtmc.h"
+#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
+#include "storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h"
+#include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h"
+#include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h"
+#include "storm/modelchecker/results/QuantitativeCheckResult.h"
+#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
+#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
+#include "storm/modelchecker/results/QualitativeCheckResult.h"
+#include "storm-parsers/parser/PrismParser.h"
+#include "storm/storage/expressions/ExpressionManager.h"
+#include "storm/settings/modules/CoreSettings.h"
+#include "storm/environment/solver/NativeSolverEnvironment.h"
+#include "storm/environment/solver/GmmxxSolverEnvironment.h"
+#include "storm/environment/solver/EigenSolverEnvironment.h"
+#include "storm/environment/solver/TopologicalSolverEnvironment.h"
+
+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 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;
+        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 SparseGmmxxGmresDiagEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
+        static const DtmcEngine engine = DtmcEngine::PrismSparse;
+        static const bool isExact = false;
+        typedef double ValueType;
+        typedef storm::models::sparse::Dtmc<ValueType> ModelType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
+            env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
+            env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Diagonal);
+            env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
+            return env;
+        }
+    };
+    
+    class SparseGmmxxBicgstabIluEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
+        static const DtmcEngine engine = DtmcEngine::PrismSparse;
+        static const bool isExact = false;
+        typedef double ValueType;
+        typedef storm::models::sparse::Dtmc<ValueType> ModelType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
+            env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Bicgstab);
+            env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
+            env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
+            return env;
+        }
+    };
+    
+    class SparseEigenDGmresEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
+        static const DtmcEngine engine = DtmcEngine::PrismSparse;
+        static const bool isExact = false;
+        typedef double ValueType;
+        typedef storm::models::sparse::Dtmc<ValueType> ModelType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
+            env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::DGmres);
+            env.solver().eigen().setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner::Ilu);
+            env.solver().eigen().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
+            return env;
+        }
+    };
+    
+    class SparseEigenDoubleLUEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
+        static const DtmcEngine engine = DtmcEngine::PrismSparse;
+        static const bool isExact = false;
+        typedef double ValueType;
+        typedef storm::models::sparse::Dtmc<ValueType> ModelType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
+            env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
+            return env;
+        }
+    };
+    
+    class SparseEigenRationalLUEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
+        static const DtmcEngine engine = DtmcEngine::PrismSparse;
+        static const bool isExact = true;
+        typedef storm::RationalNumber ValueType;
+        typedef storm::models::sparse::Dtmc<ValueType> ModelType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
+            env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
+            return env;
+        }
+    };
+    
+    class SparseRationalEliminationEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
+        static const DtmcEngine engine = DtmcEngine::PrismSparse;
+        static const bool isExact = true;
+        typedef storm::RationalNumber ValueType;
+        typedef storm::models::sparse::Dtmc<ValueType> ModelType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Elimination);
+            return env;
+        }
+    };
+    
+    class SparseNativeJacobiEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
+        static const DtmcEngine engine = DtmcEngine::PrismSparse;
+        static const bool isExact = false;
+        typedef double ValueType;
+        typedef storm::models::sparse::Dtmc<ValueType> ModelType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
+            env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Jacobi);
+            env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
+            return env;
+        }
+    };
+
+    class SparseNativeWalkerChaeEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
+        static const DtmcEngine engine = DtmcEngine::PrismSparse;
+        static const bool isExact = false;
+        typedef double ValueType;
+        typedef storm::models::sparse::Dtmc<ValueType> ModelType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
+            env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::WalkerChae);
+            env.solver().native().setMaximalNumberOfIterations(1000000);
+            env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-7));
+            return env;
+        }
+    };
+
+    class SparseNativeSorEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
+        static const DtmcEngine engine = DtmcEngine::PrismSparse;
+        static const bool isExact = false;
+        typedef double ValueType;
+        typedef storm::models::sparse::Dtmc<ValueType> ModelType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
+            env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::SOR);
+            env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
+            return env;
+        }
+    };
+
+    class SparseNativePowerEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
+        static const DtmcEngine engine = DtmcEngine::PrismSparse;
+        static const bool isExact = false;
+        typedef double ValueType;
+        typedef storm::models::sparse::Dtmc<ValueType> ModelType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().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 SparseNativeSoundValueIterationEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
+        static const DtmcEngine engine = DtmcEngine::PrismSparse;
+        static const bool isExact = false;
+        typedef double ValueType;
+        typedef storm::models::sparse::Dtmc<ValueType> ModelType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().setForceSoundness(true);
+            env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
+            env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::SoundValueIteration);
+            env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
+            return env;
+        }
+    };
+
+    class SparseNativeIntervalIterationEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
+        static const DtmcEngine engine = DtmcEngine::PrismSparse;
+        static const bool isExact = false;
+        typedef double ValueType;
+        typedef storm::models::sparse::Dtmc<ValueType> ModelType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().setForceSoundness(true);
+            env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
+            env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::IntervalIteration);
+            env.solver().native().setRelativeTerminationCriterion(false);
+            env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
+            return env;
+        }
+    };
+
+    class SparseNativeRationalSearchEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
+        static const DtmcEngine engine = DtmcEngine::PrismSparse;
+        static const bool isExact = true;
+        typedef storm::RationalNumber ValueType;
+        typedef storm::models::sparse::Dtmc<ValueType> ModelType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
+            env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::RationalSearch);
+            return env;
+        }
+    };
+
+    class SparseTopologicalEigenLUEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
+        static const DtmcEngine engine = DtmcEngine::PrismSparse;
+        static const bool isExact = true;
+        typedef storm::RationalNumber ValueType;
+        typedef storm::models::sparse::Dtmc<ValueType> ModelType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Topological);
+            env.solver().topological().setUnderlyingEquationSolverType(storm::solver::EquationSolverType::Eigen);
+            env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
+            return env;
+        }
+    };
+
+    class HybridSylvanGmmxxGmresEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
+        static const DtmcEngine engine = DtmcEngine::Hybrid;
+        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::Gmmxx);
+            env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
+            env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
+            return env;
+        }
+    };
+    
+    class HybridCuddNativeJacobiEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
+        static const DtmcEngine engine = DtmcEngine::Hybrid;
+        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::Jacobi);
+            env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
+            return env;
+        }
+    };
+    
+    class HybridCuddNativeSoundValueIterationEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
+        static const DtmcEngine engine = DtmcEngine::Hybrid;
+        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().setForceSoundness(true);
+            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-6));
+            return env;
+        }
+    };
+    
+    class HybridSylvanNativeRationalSearchEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
+        static const DtmcEngine engine = DtmcEngine::Hybrid;
+        static const bool isExact = true;
+        typedef storm::RationalNumber 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::RationalSearch);
+            return env;
+        }
+    };
+    
+    class DdSylvanNativePowerEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
+        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;
+        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 DdCuddNativeJacobiEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
+        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 DdSylvanRationalSearchEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
+        static const DtmcEngine engine = DtmcEngine::PrismDd;
+        static const bool isExact = true;
+        typedef storm::RationalNumber 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::RationalSearch);
+            return env;
+        }
+    };
+
+    template<typename TestType>
+    class DtmcPrctlModelCheckerTest : public ::testing::Test {
+    public:
+        typedef typename TestType::ValueType ValueType;
+        typedef typename storm::models::sparse::Dtmc<ValueType> SparseModelType;
+        typedef typename storm::models::symbolic::Dtmc<TestType::ddType, ValueType> SymbolicModelType;
+        
+        DtmcPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
+        storm::Environment const& env() const { return _environment; }
+        ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber<ValueType>(input);}
+        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; }
+        
+        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
+        buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
+            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);
+            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) {
+                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;
+        }
+        
+        template <typename MT = typename TestType::ModelType>
+        typename std::enable_if<std::is_same<MT, SymbolicModelType>::value, std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>>>::type
+        buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
+            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);
+            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) {
+                auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
+                janiData.first.substituteFunctions();
+                result.second = storm::api::extractFormulasFromProperties(janiData.second);
+                result.first = storm::api::buildSymbolicModel<TestType::ddType, ValueType>(janiData.first, result.second)->template as<MT>();
+            }
+            return result;
+        }
+        
+        std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> getTasks(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) const {
+            std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> result;
+            for (auto const& f : formulas) {
+                result.emplace_back(*f);
+            }
+            return result;
+        }
+        
+        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 == DtmcEngine::PrismSparse || TestType::engine == DtmcEngine::JaniSparse || TestType::engine == DtmcEngine::JitSparse) {
+                return std::make_shared<storm::modelchecker::SparseDtmcPrctlModelChecker<SparseModelType>>(*model);
+            }
+        }
+        
+        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 == DtmcEngine::Hybrid) {
+                return std::make_shared<storm::modelchecker::HybridDtmcPrctlModelChecker<SymbolicModelType>>(*model);
+            } else if (TestType::engine == DtmcEngine::PrismDd || TestType::engine == DtmcEngine::JaniDd) {
+                return std::make_shared<storm::modelchecker::SymbolicDtmcPrctlModelChecker<SymbolicModelType>>(*model);
+            }
+        }
+        
+        bool getQualitativeResultAtInitialState(std::shared_ptr<storm::models::Model<ValueType>> const& model, std::unique_ptr<storm::modelchecker::CheckResult>& result) {
+            auto filter = getInitialStateFilter(model);
+            result->filter(*filter);
+            return result->asQualitativeCheckResult().forallTrue();
+        }
+        
+        ValueType getQuantitativeResultAtInitialState(std::shared_ptr<storm::models::Model<ValueType>> const& model, std::unique_ptr<storm::modelchecker::CheckResult>& result) {
+            auto filter = getInitialStateFilter(model);
+            result->filter(*filter);
+            return result->asQuantitativeCheckResult<ValueType>().getMin();
+        }
+    
+    private:
+        storm::Environment _environment;
+        
+        std::unique_ptr<storm::modelchecker::QualitativeCheckResult> getInitialStateFilter(std::shared_ptr<storm::models::Model<ValueType>> const& model) const {
+            if (isSparseModel()) {
+                return std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult>(model->template as<SparseModelType>()->getInitialStates());
+            } else {
+                return std::make_unique<storm::modelchecker::SymbolicQualitativeCheckResult<TestType::ddType>>(model->template as<SymbolicModelType>()->getReachableStates(), model->template as<SymbolicModelType>()->getInitialStates());
+            }
+        }
+    };
+  
+    typedef ::testing::Types<
+            SparseGmmxxGmresIluEnvironment,
+            JaniSparseGmmxxGmresIluEnvironment,
+            JitSparseGmmxxGmresIluEnvironment,
+            SparseGmmxxGmresDiagEnvironment,
+            SparseGmmxxBicgstabIluEnvironment,
+            SparseEigenDGmresEnvironment,
+            SparseEigenDoubleLUEnvironment,
+            SparseEigenRationalLUEnvironment,
+            SparseRationalEliminationEnvironment,
+            SparseNativeJacobiEnvironment,
+            SparseNativeWalkerChaeEnvironment,
+            SparseNativeSorEnvironment,
+            SparseNativePowerEnvironment,
+            SparseNativeSoundValueIterationEnvironment,
+            SparseNativeIntervalIterationEnvironment,
+            SparseNativeRationalSearchEnvironment,
+            SparseTopologicalEigenLUEnvironment,
+            HybridSylvanGmmxxGmresEnvironment,
+            HybridCuddNativeJacobiEnvironment,
+            HybridCuddNativeSoundValueIterationEnvironment,
+            HybridSylvanNativeRationalSearchEnvironment,
+            DdSylvanNativePowerEnvironment,
+            JaniDdSylvanNativePowerEnvironment,
+            DdCuddNativeJacobiEnvironment,
+            DdSylvanRationalSearchEnvironment
+        > TestingTypes;
+    
+    TYPED_TEST_CASE(DtmcPrctlModelCheckerTest, TestingTypes);
+
+    TYPED_TEST(DtmcPrctlModelCheckerTest, Die) {
+        std::string formulasString = "P=? [F \"one\"]";
+        formulasString += "; P=? [F \"two\"]";
+        formulasString += "; P=? [F \"three\"]";
+        formulasString += "; R=? [F \"done\"]";
+        
+        auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm", formulasString);
+        auto model = std::move(modelFormulas.first);
+        auto tasks = this->getTasks(modelFormulas.second);
+        EXPECT_EQ(13ul, model->getNumberOfStates());
+        EXPECT_EQ(20ul, model->getNumberOfTransitions());
+        ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
+        auto checker = this->createModelChecker(model);
+        std::unique_ptr<storm::modelchecker::CheckResult> result;
+        
+        result = checker->check(this->env(), tasks[0]);
+        EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+    
+        result = checker->check(this->env(), tasks[1]);
+        EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+    
+        result = checker->check(this->env(), tasks[2]);
+        EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+    
+        result = checker->check(this->env(), tasks[3]);
+        EXPECT_NEAR(this->parseNumber("11/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+    }
+    
+    TYPED_TEST(DtmcPrctlModelCheckerTest, Crowds) {
+        std::string formulasString = "P=? [F observe0>1]";
+        formulasString += "; P=? [F \"observeIGreater1\"]";
+        formulasString += "; P=? [F observe1>1]";
+        
+        auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-4-3.pm", formulasString);
+        auto model = std::move(modelFormulas.first);
+        auto tasks = this->getTasks(modelFormulas.second);
+        EXPECT_EQ(726ul, model->getNumberOfStates());
+        EXPECT_EQ(1146ul, model->getNumberOfTransitions());
+        ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
+        auto checker = this->createModelChecker(model);
+        std::unique_ptr<storm::modelchecker::CheckResult> result;
+        
+        result = checker->check(this->env(), tasks[0]);
+        EXPECT_NEAR(this->parseNumber("78686542099694893/1268858272000000000"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+    
+        result = checker->check(this->env(), tasks[1]);
+        EXPECT_NEAR(this->parseNumber("40300855878315123/1268858272000000000"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+    
+        result = checker->check(this->env(), tasks[2]);
+        EXPECT_NEAR(this->parseNumber("13433618626105041/1268858272000000000"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+    
+    }
+    
+    TYPED_TEST(DtmcPrctlModelCheckerTest, SynchronousLeader) {
+        std::string formulasString = "P=? [F \"elected\"]";
+        formulasString += "; P=? [F<=5 \"elected\"]";
+        formulasString += "; R=? [F \"elected\"]";
+        
+        auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm", formulasString);
+        auto model = std::move(modelFormulas.first);
+        auto tasks = this->getTasks(modelFormulas.second);
+        EXPECT_EQ(273ul, model->getNumberOfStates());
+        EXPECT_EQ(397ul, model->getNumberOfTransitions());
+        ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
+        auto checker = this->createModelChecker(model);
+        std::unique_ptr<storm::modelchecker::CheckResult> result;
+        
+        result = checker->check(this->env(), tasks[0]);
+        EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+        
+        result = checker->check(this->env(), tasks[1]);
+        EXPECT_NEAR(this->parseNumber("24/25"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+        
+        result = checker->check(this->env(), tasks[2]);
+        EXPECT_NEAR(this->parseNumber("25/24"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+    }
+
+    TEST(DtmcPrctlModelCheckerTest, AllUntilProbabilities) {
+        std::string formulasString = "P=? [F \"one\"]";
+        formulasString += "; P=? [F \"two\"]";
+        formulasString += "; P=? [F \"three\"]";
+
+        storm::prism::Program program = storm::api::parseProgram(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
+        auto formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasString, program));
+        std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, double>> tasks;
+        for (auto const& f : formulas) {
+            tasks.emplace_back(*f);
+        }
+        auto model = storm::api::buildSparseModel<double>(program, formulas)->template as<storm::models::sparse::Dtmc<double>>();
+        EXPECT_EQ(13ul, model->getNumberOfStates());
+        EXPECT_EQ(20ul, model->getNumberOfTransitions());
+
+        storm::storage::SparseMatrix<double> matrix = model->getTransitionMatrix();
+        storm::storage::BitVector initialStates(13);
+        initialStates.set(0);
+        storm::storage::BitVector phiStates(13);
+        storm::storage::BitVector psiStates(13);
+        psiStates.set(7);
+        psiStates.set(8);
+        psiStates.set(9);
+        psiStates.set(10);
+        psiStates.set(11);
+        psiStates.set(12);
+        storm::Environment env;
+        storm::solver::SolveGoal<double> goal(*model, tasks[0]);
+        std::vector<double> result = storm::modelchecker::helper::SparseDtmcPrctlHelper<double>::computeAllUntilProbabilities(env, std::move(goal), matrix, initialStates, phiStates, psiStates);
+
+        EXPECT_NEAR(1.0/6, result[7], 1e-6);
+        EXPECT_NEAR(1.0/6, result[8], 1e-6);
+        EXPECT_NEAR(1.0/6, result[9], 1e-6);
+        EXPECT_NEAR(1.0/6, result[10], 1e-6);
+        EXPECT_NEAR(1.0/6, result[11], 1e-6);
+        EXPECT_NEAR(1.0/6, result[12], 1e-6);
+
+        phiStates.set(6);
+        psiStates.set(1);
+        result = storm::modelchecker::helper::SparseDtmcPrctlHelper<double>::computeAllUntilProbabilities(env, std::move(goal), matrix, initialStates, phiStates, psiStates);
+
+        EXPECT_NEAR(1, result[0], 1e-6);
+        EXPECT_NEAR(0.5, result[1], 1e-6);
+        EXPECT_NEAR(0.5, result[2], 1e-6);
+        EXPECT_NEAR(0.25, result[5], 1e-6);
+        EXPECT_NEAR(0, result[7], 1e-6);
+        EXPECT_NEAR(0, result[8], 1e-6);
+        EXPECT_NEAR(0, result[9], 1e-6);
+        EXPECT_NEAR(0.125, result[10], 1e-6);
+        EXPECT_NEAR(0.125, result[11], 1e-6);
+        EXPECT_NEAR(0, result[12], 1e-6);
+    }
+
+}

src/test/storm/modelchecker/prctl/dtmc/ExplicitDtmcPrctlModelCheckerTest.cpp

@@ -0,0 +1,158 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+
+#include "storm-parsers/parser/FormulaParser.h"
+#include "storm/logic/Formulas.h"
+#include "storm/models/sparse/StandardRewardModel.h"
+#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
+#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/GeneralSettings.h"
+#include "storm/settings/SettingMemento.h"
+#include "storm-parsers/parser/AutoParser.h"
+#include "storm-parsers/parser/PrismParser.h"
+#include "storm/builder/ExplicitModelBuilder.h"
+#include "storm/storage/expressions/ExpressionManager.h"
+
+#include "storm/environment/solver/SolverEnvironment.h"
+
+TEST(ExplicitDtmcPrctlModelCheckerTest, Die) {
+    std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/die.tra", STORM_TEST_RESOURCES_DIR "/lab/die.lab", "", STORM_TEST_RESOURCES_DIR "/rew/die.coin_flips.trans.rew");
+    
+    storm::Environment env;
+    double const precision = 1e-6;
+    // Increase precision a little to get more accurate results
+    env.solver().setLinearEquationSolverPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
+    
+    // A parser that we use for conveniently constructing the formulas.
+    
+    auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
+    storm::parser::FormulaParser formulaParser(expManager);
+    
+    ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
+    
+    std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
+    
+    ASSERT_EQ(dtmc->getNumberOfStates(), 13ull);
+    ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull);
+    
+    storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc);
+    
+    std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
+    
+    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(env, *formula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
+    
+    EXPECT_NEAR(1.0 / 6.0, quantitativeResult1[0], precision);
+    
+    formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
+    
+    result = checker.check(env, *formula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
+    
+    EXPECT_NEAR(1.0 / 6.0, quantitativeResult2[0], precision);
+    
+    formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]");
+    
+    result = checker.check(env, *formula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
+    
+    EXPECT_NEAR(1.0 / 6.0, quantitativeResult3[0], precision);
+    
+    formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]");
+    
+    result = checker.check(env, *formula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
+    
+    EXPECT_NEAR(11.0 / 3.0, quantitativeResult4[0], precision);
+}
+
+TEST(ExplicitDtmcPrctlModelCheckerTest, Crowds) {
+
+    storm::Environment env;
+    double const precision = 1e-6;
+    // Increase precision a little to get more accurate results
+    env.solver().setLinearEquationSolverPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
+    
+
+    std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/crowds5_5.tra", STORM_TEST_RESOURCES_DIR "/lab/crowds5_5.lab", "", "");
+    
+    ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
+    
+    // A parser that we use for conveniently constructing the formulas.
+    
+    auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
+    storm::parser::FormulaParser formulaParser(expManager);
+    
+    std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
+    
+    ASSERT_EQ(8607ull, dtmc->getNumberOfStates());
+    ASSERT_EQ(15113ull, dtmc->getNumberOfTransitions());
+    
+    storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc);
+    
+    std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
+    
+    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(env, *formula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
+    
+    EXPECT_NEAR(0.3328800375801578281, quantitativeResult1[0], precision);
+    
+    formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]");
+    
+    result = checker.check(env, *formula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
+    
+    EXPECT_NEAR(0.1522194965, quantitativeResult2[0], precision);
+    
+    formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]");
+    
+    result = checker.check(env, *formula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
+    
+    EXPECT_NEAR(0.32153724292835045, quantitativeResult3[0], precision);
+}
+
+TEST(ExplicitDtmcPrctlModelCheckerTest, SynchronousLeader) {
+    storm::Environment env;
+    double const precision = 1e-6;
+    // Increase precision a little to get more accurate results
+    env.solver().setLinearEquationSolverPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
+    
+    std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/leader4_8.tra", STORM_TEST_RESOURCES_DIR "/lab/leader4_8.lab", "", STORM_TEST_RESOURCES_DIR "/rew/leader4_8.pick.trans.rew");
+    
+    ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
+    
+    // A parser that we use for conveniently constructing the formulas.
+    
+    auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
+    storm::parser::FormulaParser formulaParser(expManager);
+    
+    std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
+    
+    ASSERT_EQ(12400ull, dtmc->getNumberOfStates());
+    ASSERT_EQ(16495ull, dtmc->getNumberOfTransitions());
+    
+    storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc);
+    
+    std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
+    
+    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(env, *formula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
+    
+    EXPECT_NEAR(1.0, quantitativeResult1[0], precision);
+    
+    formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]");
+    
+    result = checker.check(env, *formula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
+    
+    EXPECT_NEAR(0.9999965911265462636, quantitativeResult2[0], precision);
+    
+    formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]");
+    
+    result = checker.check(env, *formula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
+    
+    EXPECT_NEAR(1.0448979591836789, quantitativeResult3[0], precision);
+}

src/test/storm/modelchecker/prctl/dtmc/LraDtmcPrctlModelCheckerTest.cpp

@@ -0,0 +1,268 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+#include "test/storm_gtest.h"
+
+#include "storm-parsers/parser/FormulaParser.h"
+#include "storm/settings/SettingMemento.h"
+#include "storm/logic/Formulas.h"
+#include "storm/solver/NativeLinearEquationSolver.h"
+#include "storm/models/sparse/StandardRewardModel.h"
+#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
+#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+#include "storm/settings/SettingsManager.h"
+#include "storm/solver/NativeLinearEquationSolver.h"
+#include "storm/settings/modules/GeneralSettings.h"
+
+#include "storm/environment/solver/NativeSolverEnvironment.h"
+#include "storm/environment/solver/EigenSolverEnvironment.h"
+#include "storm/environment/solver/GmmxxSolverEnvironment.h"
+
+#include "storm-parsers/parser/AutoParser.h"
+#include "storm/builder/ExplicitModelBuilder.h"
+
+namespace {
+    
+    class GmmxxDoubleGmresEnvironment {
+    public:
+        typedef double ValueType;
+        static const bool isExact = false;
+        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 EigenDoubleDGmresEnvironment {
+    public:
+        typedef double ValueType;
+        static const bool isExact = false;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
+            env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::DGmres);
+            env.solver().eigen().setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner::Ilu);
+            env.solver().eigen().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
+            return env;
+        }
+    };
+    
+    class EigenRationalLUEnvironment {
+    public:
+        typedef double ValueType;
+        static const bool isExact = true;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
+            env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
+            return env;
+        }
+    };
+    
+    class NativeSorEnvironment {
+    public:
+        typedef double ValueType;
+        static const bool isExact = false;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
+            env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::SOR);
+            env.solver().native().setSorOmega(storm::utility::convertNumber<storm::RationalNumber>(0.9));
+            env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
+            return env;
+        }
+    };
+    
+    class NativeWalkerChaeEnvironment {
+    public:
+        typedef double ValueType;
+        static const bool isExact = false;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
+            env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::WalkerChae);
+            env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
+            env.solver().native().setMaximalNumberOfIterations(50000);
+            return env;
+        }
+    };
+    
+    template<typename TestType>
+    class LraDtmcPrctlModelCheckerTest : public ::testing::Test {
+    public:
+        typedef typename TestType::ValueType ValueType;
+        LraDtmcPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
+        storm::Environment const& env() const { return _environment; }
+        ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber<ValueType>(input);}
+        ValueType precision() const { return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");}
+
+    private:
+        storm::Environment _environment;
+    };
+  
+    typedef ::testing::Types<
+            GmmxxDoubleGmresEnvironment,
+            EigenDoubleDGmresEnvironment,
+            EigenRationalLUEnvironment,
+            NativeSorEnvironment,
+            NativeWalkerChaeEnvironment
+    > TestingTypes;
+    
+   TYPED_TEST_CASE(LraDtmcPrctlModelCheckerTest, TestingTypes);
+
+    
+    
+    TYPED_TEST(LraDtmcPrctlModelCheckerTest, LRASingleBscc) {
+        typedef typename TestFixture::ValueType ValueType;
+
+        storm::storage::SparseMatrixBuilder<ValueType> matrixBuilder;
+        std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc;
+    
+        // A parser that we use for conveniently constructing the formulas.
+        storm::parser::FormulaParser formulaParser;
+        
+        {
+            matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(2, 2, 2);
+            matrixBuilder.addNextValue(0, 1, this->parseNumber("1"));
+            matrixBuilder.addNextValue(1, 0, this->parseNumber("1"));
+            storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
+    
+            storm::models::sparse::StateLabeling ap(2);
+            ap.addLabel("a");
+            ap.addLabelToState("a", 1);
+    
+            dtmc.reset(new storm::models::sparse::Dtmc<ValueType>(transitionMatrix, ap));
+    
+            storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> checker(*dtmc);
+    
+            std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
+            
+            std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
+                storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
+    
+            EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[0], this->precision());
+            EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[1], this->precision());
+        }
+        {
+            matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(2, 2, 4);
+            matrixBuilder.addNextValue(0, 0, this->parseNumber("0.5"));
+            matrixBuilder.addNextValue(0, 1, this->parseNumber("0.5"));
+            matrixBuilder.addNextValue(1, 0, this->parseNumber("0.5"));
+            matrixBuilder.addNextValue(1, 1, this->parseNumber("0.5"));
+            storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
+    
+            storm::models::sparse::StateLabeling ap(2);
+            ap.addLabel("a");
+            ap.addLabelToState("a", 1);
+    
+            dtmc.reset(new storm::models::sparse::Dtmc<ValueType>(transitionMatrix, ap));
+    
+            storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> checker(*dtmc);
+    
+            std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
+            
+            std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
+            storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
+    
+            EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[0], this->precision());
+            EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[1], this->precision());
+        }
+    
+        {
+            matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(3, 3, 3);
+            matrixBuilder.addNextValue(0, 1, this->parseNumber("1"));
+            matrixBuilder.addNextValue(1, 2, this->parseNumber("1"));
+            matrixBuilder.addNextValue(2, 0, this->parseNumber("1"));
+            storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
+    
+            storm::models::sparse::StateLabeling ap(3);
+            ap.addLabel("a");
+            ap.addLabelToState("a", 2);
+    
+            dtmc.reset(new storm::models::sparse::Dtmc<ValueType>(transitionMatrix, ap));
+    
+            storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> checker(*dtmc);
+    
+            std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
+            
+            std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
+            storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
+    
+            EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[0], this->precision());
+            EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[1], this->precision());
+            EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[2], this->precision());
+        }
+    }
+    
+    TYPED_TEST(LraDtmcPrctlModelCheckerTest, LRA) {
+        typedef typename TestFixture::ValueType ValueType;
+
+        storm::storage::SparseMatrixBuilder<ValueType> matrixBuilder;
+        std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc;
+    
+        // A parser that we use for conveniently constructing the formulas.
+        storm::parser::FormulaParser formulaParser;
+        
+        {
+            matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(15, 15, 20, true);
+            matrixBuilder.addNextValue(0, 1, this->parseNumber("1"));
+            matrixBuilder.addNextValue(1, 4, this->parseNumber("0.7"));
+            matrixBuilder.addNextValue(1, 6, this->parseNumber("0.3"));
+            matrixBuilder.addNextValue(2, 0, this->parseNumber("1"));
+    
+            matrixBuilder.addNextValue(3, 5, this->parseNumber("0.8"));
+            matrixBuilder.addNextValue(3, 9, this->parseNumber("0.2"));
+            matrixBuilder.addNextValue(4, 3, this->parseNumber("1"));
+            matrixBuilder.addNextValue(5, 3, this->parseNumber("1"));
+    
+            matrixBuilder.addNextValue(6, 7, this->parseNumber("1"));
+            matrixBuilder.addNextValue(7, 8, this->parseNumber("1"));
+            matrixBuilder.addNextValue(8, 6, this->parseNumber("1"));
+    
+            matrixBuilder.addNextValue(9, 10, this->parseNumber("1"));
+            matrixBuilder.addNextValue(10, 9, this->parseNumber("1"));
+            matrixBuilder.addNextValue(11, 9, this->parseNumber("1"));
+    
+            matrixBuilder.addNextValue(12, 5, this->parseNumber("0.4"));
+            matrixBuilder.addNextValue(12, 8, this->parseNumber("0.3"));
+            matrixBuilder.addNextValue(12, 11, this->parseNumber("0.3"));
+    
+            matrixBuilder.addNextValue(13, 7, this->parseNumber("0.7"));
+            matrixBuilder.addNextValue(13, 12, this->parseNumber("0.3"));
+    
+            matrixBuilder.addNextValue(14, 12, this->parseNumber("1"));
+    
+            storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
+    
+            storm::models::sparse::StateLabeling ap(15);
+            ap.addLabel("a");
+            ap.addLabelToState("a", 1);
+            ap.addLabelToState("a", 4);
+            ap.addLabelToState("a", 5);
+            ap.addLabelToState("a", 7);
+            ap.addLabelToState("a", 11);
+            ap.addLabelToState("a", 13);
+            ap.addLabelToState("a", 14);
+    
+            dtmc.reset(new storm::models::sparse::Dtmc<ValueType>(transitionMatrix, ap));
+            
+            storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> checker(*dtmc);
+    
+            std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
+            
+            std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
+            storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
+    
+            EXPECT_NEAR(this->parseNumber("1/10"), quantitativeResult1[0], this->precision());
+            EXPECT_NEAR(this->parseNumber("0"), quantitativeResult1[3], this->precision());
+            EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[6], this->precision());
+            EXPECT_NEAR(this->parseNumber("0"), quantitativeResult1[9], this->precision());
+            EXPECT_NEAR(this->parseNumber("1/10"), quantitativeResult1[12], this->precision());
+            EXPECT_NEAR(this->parseNumber("79/300"), quantitativeResult1[13], this->precision());
+            EXPECT_NEAR(this->parseNumber("1/10"), quantitativeResult1[14], this->precision());
+        }
+    }
+}

src/test/storm/modelchecker/prctl/mdp/ExplicitMdpPrctlModelCheckerTest.cpp

@@ -0,0 +1,199 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+
+#include "storm-parsers/parser/FormulaParser.h"
+#include "storm/logic/Formulas.h"
+#include "storm/solver/StandardMinMaxLinearEquationSolver.h"
+#include "storm/models/sparse/StandardRewardModel.h"
+#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
+#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+
+#include "storm/environment/solver/MinMaxSolverEnvironment.h"
+
+#include "storm-parsers/parser/AutoParser.h"
+#include "storm-parsers/parser/PrismParser.h"
+#include "storm/builder/ExplicitModelBuilder.h"
+
+TEST(ExplicitMdpPrctlModelCheckerTest, Dice) {
+    std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", "", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew");
+    storm::Environment env;
+    double const precision = 1e-6;
+    // Increase precision a little to get more accurate results
+    env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
+    
+    // A parser that we use for conveniently constructing the formulas.
+    storm::parser::FormulaParser formulaParser;
+
+    ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp);
+
+    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
+
+    ASSERT_EQ(mdp->getNumberOfStates(), 169ull);
+    ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull);
+
+    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
+
+    std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
+
+    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(env, *formula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
+
+    EXPECT_NEAR(1.0/36.0, quantitativeResult1[0], precision);
+
+    formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]");
+
+    result = checker.check(env, *formula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
+
+    EXPECT_NEAR(1.0/36.0, quantitativeResult2[0], precision);
+
+    formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]");
+
+    result = checker.check(env, *formula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
+
+    EXPECT_NEAR(2.0/36.0, quantitativeResult3[0], precision);
+
+    formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]");
+
+    result = checker.check(env, *formula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
+
+    EXPECT_NEAR(2.0/36.0, quantitativeResult4[0], precision);
+
+    formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]");
+
+    result = checker.check(env, *formula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
+
+    EXPECT_NEAR(3.0/36.0, quantitativeResult5[0], precision);
+
+    formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]");
+
+    result = checker.check(env, *formula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
+
+    EXPECT_NEAR(3.0/36.0, quantitativeResult6[0], precision);
+
+    formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]");
+
+    result = checker.check(env, *formula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult7 = result->asExplicitQuantitativeCheckResult<double>();
+
+    EXPECT_NEAR(22.0/3.0, quantitativeResult7[0], precision);
+
+    formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
+
+    result = checker.check(env, *formula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult8 = result->asExplicitQuantitativeCheckResult<double>();
+
+    EXPECT_NEAR(22.0/3.0, quantitativeResult8[0], precision);
+
+    abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", "");
+
+    ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp);
+
+    std::shared_ptr<storm::models::sparse::Mdp<double>> stateRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
+
+    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateRewardModelChecker(*mdp);
+
+    formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]");
+
+    result = stateRewardModelChecker.check(env, *formula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult9 = result->asExplicitQuantitativeCheckResult<double>();
+
+    EXPECT_NEAR(22.0/3.0, quantitativeResult9[0], precision);
+
+    formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
+
+    result = stateRewardModelChecker.check(env, *formula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult10 = result->asExplicitQuantitativeCheckResult<double>();
+
+    EXPECT_NEAR(22.0/3.0, quantitativeResult10[0], precision);
+
+    abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew");
+
+    ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp);
+
+    std::shared_ptr<storm::models::sparse::Mdp<double>> stateAndTransitionRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
+
+    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp);
+
+    formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]");
+
+    result = stateAndTransitionRewardModelChecker.check(env, *formula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult11 = result->asExplicitQuantitativeCheckResult<double>();
+
+    EXPECT_NEAR(44.0/3.0, quantitativeResult11[0], precision);
+
+    formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
+
+    result = stateAndTransitionRewardModelChecker.check(env, *formula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult12 = result->asExplicitQuantitativeCheckResult<double>();
+
+    EXPECT_NEAR(44.0/3.0, quantitativeResult12[0], precision);
+}
+
+TEST(ExplicitMdpPrctlModelCheckerTest, AsynchronousLeader) {
+    storm::Environment env;
+    double const precision = 1e-6;
+    // Increase precision a little to get more accurate results
+    env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
+
+    std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/leader4.tra", STORM_TEST_RESOURCES_DIR "/lab/leader4.lab", "", STORM_TEST_RESOURCES_DIR "/rew/leader4.trans.rew");
+
+    // A parser that we use for conveniently constructing the formulas.
+    storm::parser::FormulaParser formulaParser;
+
+    ASSERT_EQ(storm::models::ModelType::Mdp, abstractModel->getType());
+
+    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
+
+    ASSERT_EQ(3172ull, mdp->getNumberOfStates());
+    ASSERT_EQ(7144ull, mdp->getNumberOfTransitions());
+
+    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
+
+    std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
+
+    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(env, *formula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
+
+    EXPECT_NEAR(1.0, quantitativeResult1[0], precision);
+
+    formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]");
+
+    result = checker.check(env, *formula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
+
+    EXPECT_NEAR(1.0, quantitativeResult2[0], precision);
+
+    formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]");
+
+    result = checker.check(env, *formula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
+
+    EXPECT_NEAR(1.0/16.0, quantitativeResult3[0], precision);
+
+    formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]");
+
+    result = checker.check(env, *formula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
+
+    EXPECT_NEAR(1.0/16.0, quantitativeResult4[0], precision);
+
+    formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]");
+
+    result = checker.check(env, *formula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
+
+    EXPECT_NEAR(30.0/7.0, quantitativeResult5[0], precision);
+
+    formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
+
+    result = checker.check(env, *formula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
+
+    EXPECT_NEAR(30.0/7.0, quantitativeResult6[0], precision);
+}
+

src/test/storm/modelchecker/prctl/mdp/LraMdpPrctlModelCheckerTest.cpp

@@ -0,0 +1,468 @@
+#include "gtest/gtest.h"
+
+#include "test/storm_gtest.h"
+
+#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"
+
+#include "storm-parsers/parser/FormulaParser.h"
+#include "storm/logic/Formulas.h"
+#include "storm/solver/StandardMinMaxLinearEquationSolver.h"
+#include "storm/models/sparse/StandardRewardModel.h"
+#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
+#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+#include "storm/settings/SettingsManager.h"
+
+#include "storm/settings/modules/GeneralSettings.h"
+
+#include "storm/settings/modules/NativeEquationSolverSettings.h"
+#include "storm-parsers/parser/AutoParser.h"
+#include "storm/environment/solver/MinMaxSolverEnvironment.h"
+
+namespace {
+    
+    
+    class SparseValueTypeValueIterationEnvironment {
+    public:
+        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().setLraMethod(storm::solver::LraMethod::ValueIteration);
+            env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
+            return env;
+        }
+    };
+    
+    class SparseValueTypeLinearProgrammingEnvironment {
+    public:
+        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().setLraMethod(storm::solver::LraMethod::LinearProgramming);
+            env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
+            return env;
+        }
+    };
+    
+    class SparseRationalLinearProgrammingEnvironment {
+    public:
+        static const bool isExact = true;
+        typedef storm::RationalNumber ValueType;
+        typedef storm::models::sparse::Mdp<ValueType> ModelType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().minMax().setLraMethod(storm::solver::LraMethod::LinearProgramming);
+            return env;
+        }
+    };
+    
+    template<typename TestType>
+    class LraMdpPrctlModelCheckerTest : public ::testing::Test {
+    public:
+        typedef typename TestType::ValueType ValueType;
+        typedef typename storm::models::sparse::Mdp<ValueType> SparseModelType;
+        
+        LraMdpPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
+        storm::Environment const& env() const { return _environment; }
+        ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber<ValueType>(input);}
+        ValueType precision() const { return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");}
+        bool isSparseModel() const { return std::is_same<typename TestType::ModelType, SparseModelType>::value; }
+        
+        std::pair<std::shared_ptr<SparseModelType>, std::vector<std::shared_ptr<storm::logic::Formula const>>> buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
+            std::pair<std::shared_ptr<SparseModelType>, 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<SparseModelType>();
+            return result;
+        }
+        
+        std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> getTasks(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) const {
+            std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> result;
+            for (auto const& f : formulas) {
+                result.emplace_back(*f);
+            }
+            return result;
+        }
+        
+    private:
+        storm::Environment _environment;
+    };
+  
+    typedef ::testing::Types<
+            SparseValueTypeValueIterationEnvironment,
+            SparseValueTypeLinearProgrammingEnvironment
+#ifdef STORM_HAVE_Z3_OPTIMIZE
+            , SparseRationalLinearProgrammingEnvironment
+#endif
+        > TestingTypes;
+    
+    TYPED_TEST_CASE(LraMdpPrctlModelCheckerTest, TestingTypes);
+    
+    
+    TYPED_TEST(LraMdpPrctlModelCheckerTest, LRA_SingleMec) {
+        typedef typename TestFixture::ValueType ValueType;
+
+        storm::storage::SparseMatrixBuilder<ValueType> matrixBuilder;
+        std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp;
+    
+        // A parser that we use for conveniently constructing the formulas.
+        storm::parser::FormulaParser formulaParser;
+    
+        {
+            matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(2, 2, 2);
+            matrixBuilder.addNextValue(0, 1, this->parseNumber("1"));
+            matrixBuilder.addNextValue(1, 0, this->parseNumber("1"));
+            storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
+    
+            storm::models::sparse::StateLabeling ap(2);
+            ap.addLabel("a");
+            ap.addLabelToState("a", 1);
+    
+            mdp.reset(new storm::models::sparse::Mdp<ValueType>(transitionMatrix, ap));
+    
+            storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
+    
+            std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
+    
+            std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
+            storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
+    
+            EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[0], this->precision());
+            EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[1], this->precision());
+    
+            formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
+    
+            result = checker.check(this->env(), *formula);
+            storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<ValueType>();
+    
+            EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult2[0], this->precision());
+            EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult2[1], this->precision());
+        }
+        {
+            matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(2, 2, 4);
+            matrixBuilder.addNextValue(0, 0, this->parseNumber("0.5"));
+            matrixBuilder.addNextValue(0, 1, this->parseNumber("0.5"));
+            matrixBuilder.addNextValue(1, 0, this->parseNumber("0.5"));
+            matrixBuilder.addNextValue(1, 1, this->parseNumber("0.5"));
+            storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
+    
+            storm::models::sparse::StateLabeling ap(2);
+            ap.addLabel("a");
+            ap.addLabelToState("a", 1);
+    
+            mdp.reset(new storm::models::sparse::Mdp<ValueType>(transitionMatrix, ap));
+    
+            storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
+    
+            std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
+    
+            std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
+            storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
+    
+            EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[0], this->precision());
+            EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[1], this->precision());
+    
+            formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
+    
+            result = checker.check(this->env(), *formula);
+            storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<ValueType>();
+    
+            EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult2[0], this->precision());
+            EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult2[1], this->precision());
+        }
+        {
+            matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(4, 3, 4, true, true, 3);
+            matrixBuilder.newRowGroup(0);
+            matrixBuilder.addNextValue(0, 1, this->parseNumber("1"));
+            matrixBuilder.newRowGroup(1);
+            matrixBuilder.addNextValue(1, 0, this->parseNumber("1"));
+            matrixBuilder.addNextValue(2, 2, this->parseNumber("1"));
+            matrixBuilder.newRowGroup(3);
+            matrixBuilder.addNextValue(3, 0, this->parseNumber("1"));
+            storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
+    
+            storm::models::sparse::StateLabeling ap(3);
+            ap.addLabel("a");
+            ap.addLabelToState("a", 2);
+            ap.addLabel("b");
+            ap.addLabelToState("b", 0);
+            ap.addLabel("c");
+            ap.addLabelToState("c", 0);
+            ap.addLabelToState("c", 2);
+    
+            mdp.reset(new storm::models::sparse::Mdp<ValueType>(transitionMatrix, ap));
+    
+            storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
+    
+            std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
+    
+            std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
+            storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
+    
+            EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[0], this->precision());
+            EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[1], this->precision());
+            EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[2], this->precision());
+    
+            formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
+    
+            result = checker.check(this->env(), *formula);
+            storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<ValueType>();
+    
+            EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[0], this->precision());
+            EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[1], this->precision());
+            EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[2], this->precision());
+    
+            formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"b\"]");
+    
+            result = checker.check(this->env(), *formula);
+            storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<ValueType>();
+    
+            EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult3[0], this->precision());
+            EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult3[1], this->precision());
+            EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult3[2], this->precision());
+    
+            formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"b\"]");
+    
+            result = checker.check(this->env(), *formula);
+            storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<ValueType>();
+    
+            EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult4[0], this->precision());
+            EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult4[1], this->precision());
+            EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult4[2], this->precision());
+    
+            formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"c\"]");
+    
+            result = checker.check(this->env(), *formula);
+            storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<ValueType>();
+    
+            EXPECT_NEAR(this->parseNumber("2/3"), quantitativeResult5[0], this->precision());
+            EXPECT_NEAR(this->parseNumber("2/3"), quantitativeResult5[1], this->precision());
+            EXPECT_NEAR(this->parseNumber("2/3"), quantitativeResult5[2], this->precision());
+    
+            formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"c\"]");
+    
+            result = checker.check(this->env(), *formula);
+            storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<ValueType>();
+    
+            EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult6[0], this->precision());
+            EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult6[1], this->precision());
+            EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult6[2], this->precision());
+        }
+    }
+    
+    TYPED_TEST(LraMdpPrctlModelCheckerTest, LRA) {
+        typedef typename TestFixture::ValueType ValueType;
+        
+        storm::storage::SparseMatrixBuilder<ValueType> matrixBuilder;
+        std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp;
+    
+        // A parser that we use for conveniently constructing the formulas.
+        storm::parser::FormulaParser formulaParser;
+    
+        {
+            matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(4, 3, 4, true, true, 3);
+            matrixBuilder.newRowGroup(0);
+            matrixBuilder.addNextValue(0, 1, this->parseNumber("1"));
+            matrixBuilder.newRowGroup(1);
+            matrixBuilder.addNextValue(1, 1, this->parseNumber("1"));
+            matrixBuilder.addNextValue(2, 2, this->parseNumber("1"));
+            matrixBuilder.newRowGroup(3);
+            matrixBuilder.addNextValue(3, 2, this->parseNumber("1"));
+            storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
+    
+            storm::models::sparse::StateLabeling ap(3);
+            ap.addLabel("a");
+            ap.addLabelToState("a", 0);
+            ap.addLabel("b");
+            ap.addLabelToState("b", 1);
+            ap.addLabel("c");
+            ap.addLabelToState("c", 2);
+    
+            mdp.reset(new storm::models::sparse::Mdp<ValueType>(transitionMatrix, ap));
+    
+            storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
+    
+            std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
+    
+            std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
+            storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
+    
+            EXPECT_NEAR(this->parseNumber("0"), quantitativeResult1[0], this->precision());
+            EXPECT_NEAR(this->parseNumber("0"), quantitativeResult1[1], this->precision());
+            EXPECT_NEAR(this->parseNumber("0"), quantitativeResult1[2], this->precision());
+    
+            formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
+    
+            result = checker.check(this->env(), *formula);
+            storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<ValueType>();
+    
+            EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[0], this->precision());
+            EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[1], this->precision());
+            EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[2], this->precision());
+    
+            formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"b\"]");
+    
+            result = checker.check(this->env(), *formula);
+            storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<ValueType>();
+    
+            EXPECT_NEAR(this->parseNumber("1"), quantitativeResult3[0], this->precision());
+            EXPECT_NEAR(this->parseNumber("1"), quantitativeResult3[1], this->precision());
+            EXPECT_NEAR(this->parseNumber("0"), quantitativeResult3[2], this->precision());
+    
+            formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"b\"]");
+    
+            result = checker.check(this->env(), *formula);
+            storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<ValueType>();
+    
+            EXPECT_NEAR(this->parseNumber("0"), quantitativeResult4[0], this->precision());
+            EXPECT_NEAR(this->parseNumber("0"), quantitativeResult4[1], this->precision());
+            EXPECT_NEAR(this->parseNumber("0"), quantitativeResult4[2], this->precision());
+    
+            formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"c\"]");
+    
+            result = checker.check(this->env(), *formula);
+            storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<ValueType>();
+    
+            EXPECT_NEAR(this->parseNumber("1"), quantitativeResult5[0], this->precision());
+            EXPECT_NEAR(this->parseNumber("1"), quantitativeResult5[1], this->precision());
+            EXPECT_NEAR(this->parseNumber("1"), quantitativeResult5[2], this->precision());
+    
+            formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"c\"]");
+    
+            result = checker.check(this->env(), *formula);
+            storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<ValueType>();
+    
+            EXPECT_NEAR(this->parseNumber("0"), quantitativeResult6[0], this->precision());
+            EXPECT_NEAR(this->parseNumber("0"), quantitativeResult6[1], this->precision());
+            EXPECT_NEAR(this->parseNumber("1"), quantitativeResult6[2], this->precision());
+        }
+        {
+            matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(22, 15, 28, true, true, 15);
+            matrixBuilder.newRowGroup(0);
+            matrixBuilder.addNextValue(0, 1, this->parseNumber("1"));
+            matrixBuilder.newRowGroup(1);
+            matrixBuilder.addNextValue(1, 0, this->parseNumber("1"));
+            matrixBuilder.addNextValue(2, 2, this->parseNumber("1"));
+            matrixBuilder.addNextValue(3, 4, this->parseNumber("0.7"));
+            matrixBuilder.addNextValue(3, 6, this->parseNumber("0.3"));
+            matrixBuilder.newRowGroup(4);
+            matrixBuilder.addNextValue(4, 0, this->parseNumber("1"));
+    
+            matrixBuilder.newRowGroup(5);
+            matrixBuilder.addNextValue(5, 4, this->parseNumber("1"));
+            matrixBuilder.addNextValue(6, 5, this->parseNumber("0.8"));
+            matrixBuilder.addNextValue(6, 9, this->parseNumber("0.2"));
+            matrixBuilder.newRowGroup(7);
+            matrixBuilder.addNextValue(7, 3, this->parseNumber("1"));
+            matrixBuilder.addNextValue(8, 5, this->parseNumber("1"));
+            matrixBuilder.newRowGroup(9);
+            matrixBuilder.addNextValue(9, 3, this->parseNumber("1"));
+    
+            matrixBuilder.newRowGroup(10);
+            matrixBuilder.addNextValue(10, 7, this->parseNumber("1"));
+            matrixBuilder.newRowGroup(11);
+            matrixBuilder.addNextValue(11, 6, this->parseNumber("1"));
+            matrixBuilder.addNextValue(12, 8, this->parseNumber("1"));
+            matrixBuilder.newRowGroup(13);
+            matrixBuilder.addNextValue(13, 6, this->parseNumber("1"));
+    
+            matrixBuilder.newRowGroup(14);
+            matrixBuilder.addNextValue(14, 10, this->parseNumber("1"));
+            matrixBuilder.newRowGroup(15);
+            matrixBuilder.addNextValue(15, 9, this->parseNumber("1"));
+            matrixBuilder.addNextValue(16, 11, this->parseNumber("1"));
+            matrixBuilder.newRowGroup(17);
+            matrixBuilder.addNextValue(17, 9, this->parseNumber("1"));
+    
+            matrixBuilder.newRowGroup(18);
+            matrixBuilder.addNextValue(18, 5, this->parseNumber("0.4"));
+            matrixBuilder.addNextValue(18, 8, this->parseNumber("0.3"));
+            matrixBuilder.addNextValue(18, 11, this->parseNumber("0.3"));
+    
+            matrixBuilder.newRowGroup(19);
+            matrixBuilder.addNextValue(19, 7, this->parseNumber("0.7"));
+            matrixBuilder.addNextValue(19, 12, this->parseNumber("0.3"));
+    
+            matrixBuilder.newRowGroup(20);
+            matrixBuilder.addNextValue(20, 12, this->parseNumber("0.1"));
+            matrixBuilder.addNextValue(20, 13, this->parseNumber("0.9"));
+            matrixBuilder.addNextValue(21, 12, this->parseNumber("1"));
+    
+            storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
+    
+            storm::models::sparse::StateLabeling ap(15);
+            ap.addLabel("a");
+            ap.addLabelToState("a", 1);
+            ap.addLabelToState("a", 4);
+            ap.addLabelToState("a", 5);
+            ap.addLabelToState("a", 7);
+            ap.addLabelToState("a", 11);
+            ap.addLabelToState("a", 13);
+            ap.addLabelToState("a", 14);
+    
+            mdp.reset(new storm::models::sparse::Mdp<ValueType>(transitionMatrix, ap));
+    
+            storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
+    
+            std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
+    
+            std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
+            storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
+    
+            EXPECT_NEAR(this->parseNumber("37 / 60"), quantitativeResult1[0], this->precision());
+            EXPECT_NEAR(this->parseNumber("2/3"), quantitativeResult1[3], this->precision());
+            EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[6], this->precision());
+            EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[9], this->precision());
+            EXPECT_NEAR(this->parseNumber("31 / 60"), quantitativeResult1[12], this->precision());
+            EXPECT_NEAR(this->parseNumber("101 / 200"), quantitativeResult1[13], this->precision());
+            EXPECT_NEAR(this->parseNumber("31 / 60"), quantitativeResult1[14], this->precision());
+    
+            formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
+    
+            result = checker.check(this->env(), *formula);
+            storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<ValueType>();
+    
+            EXPECT_NEAR(this->parseNumber("0.1"), quantitativeResult2[0], this->precision());
+            EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[3], this->precision());
+            EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult2[6], this->precision());
+            EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[9], this->precision());
+            EXPECT_NEAR(this->parseNumber("0.1"), quantitativeResult2[12], this->precision());
+            EXPECT_NEAR(this->parseNumber("79 / 300"), quantitativeResult2[13], this->precision());
+            EXPECT_NEAR(this->parseNumber("0.1"), quantitativeResult2[14], this->precision());
+        }
+    }
+    
+    TYPED_TEST(LraMdpPrctlModelCheckerTest, cs_nfail) {
+        typedef typename TestFixture::ValueType ValueType;
+
+        std::string formulasString = "R{\"grants\"}max=? [ MP ]";
+        
+        auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/cs_nfail3.nm", formulasString);
+        auto model = std::move(modelFormulas.first);
+        auto tasks = this->getTasks(modelFormulas.second);
+        EXPECT_EQ(184ul, model->getNumberOfStates());
+        EXPECT_EQ(541ul, model->getNumberOfTransitions());
+        ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
+        auto mdp = model->template as<storm::models::sparse::Mdp<ValueType>>();
+        storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
+        std::unique_ptr<storm::modelchecker::CheckResult> result;
+        
+        result = checker.check(this->env(), tasks[0]);
+        storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult = result->asExplicitQuantitativeCheckResult<ValueType>();
+
+        EXPECT_NEAR(this->parseNumber("333/1000"), quantitativeResult[*mdp->getInitialStates().begin()], this->precision());
+
+    }
+
+    
+}

src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp

@@ -0,0 +1,607 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+
+#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"
+
+#include "storm/models/sparse/Mdp.h"
+#include "storm/models/symbolic/Mdp.h"
+#include "storm/models/sparse/StandardRewardModel.h"
+#include "storm/models/symbolic/StandardRewardModel.h"
+#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
+#include "storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h"
+#include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h"
+#include "storm/modelchecker/results/QuantitativeCheckResult.h"
+#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
+#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
+#include "storm/modelchecker/results/QualitativeCheckResult.h"
+#include "storm/environment/solver/MinMaxSolverEnvironment.h"
+#include "storm/environment/solver/TopologicalSolverEnvironment.h"
+#include "storm/settings/modules/CoreSettings.h"
+#include "storm/logic/Formulas.h"
+#include "storm/storage/jani/Property.h"
+#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 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;
+        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 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 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().setForceSoundness(true);
+            env.solver().minMax().setMethod(storm::solver::MinMaxMethod::IntervalIteration);
+            env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
+            env.solver().minMax().setRelativeTerminationCriterion(false);
+            return env;
+        }
+    };
+    class SparseDoubleSoundValueIterationEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
+        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().setForceSoundness(true);
+            env.solver().minMax().setMethod(storm::solver::MinMaxMethod::SoundValueIteration);
+            env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
+            env.solver().minMax().setRelativeTerminationCriterion(false);
+            return env;
+        }
+    };
+    
+    class SparseDoubleTopologicalValueIterationEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
+        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::Topological);
+            env.solver().topological().setUnderlyingMinMaxMethod(storm::solver::MinMaxMethod::ValueIteration);
+            env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
+            env.solver().minMax().setRelativeTerminationCriterion(false);
+            return env;
+        }
+    };
+    
+    class SparseDoubleTopologicalSoundValueIterationEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
+        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().setForceSoundness(true);
+            env.solver().minMax().setMethod(storm::solver::MinMaxMethod::Topological);
+            env.solver().topological().setUnderlyingMinMaxMethod(storm::solver::MinMaxMethod::SoundValueIteration);
+            env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
+            env.solver().minMax().setRelativeTerminationCriterion(false);
+            return env;
+        }
+    };
+    
+    class SparseRationalPolicyIterationEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
+        static const MdpEngine engine = MdpEngine::PrismSparse;
+        static const bool isExact = true;
+        typedef storm::RationalNumber ValueType;
+        typedef storm::models::sparse::Mdp<ValueType> ModelType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration);
+            return env;
+        }
+    };
+    
+    class SparseRationalViToPiEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
+        static const MdpEngine engine = MdpEngine::PrismSparse;
+        static const bool isExact = true;
+        typedef storm::RationalNumber ValueType;
+        typedef storm::models::sparse::Mdp<ValueType> ModelType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ViToPi);
+            return env;
+        }
+    };
+    
+    class SparseRationalRationalSearchEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
+        static const MdpEngine engine = MdpEngine::PrismSparse;
+        static const bool isExact = true;
+        typedef storm::RationalNumber ValueType;
+        typedef storm::models::sparse::Mdp<ValueType> ModelType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().minMax().setMethod(storm::solver::MinMaxMethod::RationalSearch);
+            return env;
+        }
+    };
+    class HybridCuddDoubleValueIterationEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
+        static const MdpEngine engine = MdpEngine::Hybrid;
+        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 HybridSylvanDoubleValueIterationEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
+        static const MdpEngine engine = MdpEngine::Hybrid;
+        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 HybridCuddDoubleSoundValueIterationEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
+        static const MdpEngine engine = MdpEngine::Hybrid;
+        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().setForceSoundness(true);
+            env.solver().minMax().setMethod(storm::solver::MinMaxMethod::SoundValueIteration);
+            env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
+            env.solver().minMax().setRelativeTerminationCriterion(false);
+            return env;
+        }
+    };
+    class HybridSylvanRationalPolicyIterationEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
+        static const MdpEngine engine = MdpEngine::Hybrid;
+        static const bool isExact = true;
+        typedef storm::RationalNumber ValueType;
+        typedef storm::models::symbolic::Mdp<ddType, ValueType> ModelType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration);
+            return env;
+        }
+    };
+   class DdCuddDoubleValueIterationEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
+        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;
+        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 DdSylvanDoubleValueIterationEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
+        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 DdCuddDoublePolicyIterationEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
+        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::PolicyIteration);
+            env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
+            return env;
+        }
+    };
+    class DdSylvanRationalRationalSearchEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
+        static const MdpEngine engine = MdpEngine::PrismDd;
+        static const bool isExact = true;
+        typedef storm::RationalNumber ValueType;
+        typedef storm::models::symbolic::Mdp<ddType, ValueType> ModelType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().minMax().setMethod(storm::solver::MinMaxMethod::RationalSearch);
+            return env;
+        }
+    };
+
+    template<typename TestType>
+    class MdpPrctlModelCheckerTest : public ::testing::Test {
+    public:
+        typedef typename TestType::ValueType ValueType;
+        typedef typename storm::models::sparse::Mdp<ValueType> SparseModelType;
+        typedef typename storm::models::symbolic::Mdp<TestType::ddType, ValueType> SymbolicModelType;
+        
+        MdpPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
+        storm::Environment const& env() const { return _environment; }
+        ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber<ValueType>(input);}
+        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; }
+        
+        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
+        buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
+            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);
+            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) {
+                auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
+                janiData.first.substituteFunctions();
+                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;
+        }
+        
+        template <typename MT = typename TestType::ModelType>
+        typename std::enable_if<std::is_same<MT, SymbolicModelType>::value, std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>>>::type
+        buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
+            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);
+            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) {
+                auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
+                janiData.first.substituteFunctions();
+                result.second = storm::api::extractFormulasFromProperties(janiData.second);
+                result.first = storm::api::buildSymbolicModel<TestType::ddType, ValueType>(janiData.first, result.second)->template as<MT>();
+            }
+            return result;
+        }
+        
+        std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> getTasks(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) const {
+            std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> result;
+            for (auto const& f : formulas) {
+                result.emplace_back(*f);
+            }
+            return result;
+        }
+        
+        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 == MdpEngine::PrismSparse || TestType::engine == MdpEngine::JaniSparse || TestType::engine == MdpEngine::JitSparse) {
+                return std::make_shared<storm::modelchecker::SparseMdpPrctlModelChecker<SparseModelType>>(*model);
+            }
+        }
+        
+        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 == MdpEngine::Hybrid) {
+                return std::make_shared<storm::modelchecker::HybridMdpPrctlModelChecker<SymbolicModelType>>(*model);
+            } else if (TestType::engine == MdpEngine::PrismDd || TestType::engine == MdpEngine::JaniDd) {
+                return std::make_shared<storm::modelchecker::SymbolicMdpPrctlModelChecker<SymbolicModelType>>(*model);
+            }
+        }
+        
+        bool getQualitativeResultAtInitialState(std::shared_ptr<storm::models::Model<ValueType>> const& model, std::unique_ptr<storm::modelchecker::CheckResult>& result) {
+            auto filter = getInitialStateFilter(model);
+            result->filter(*filter);
+            return result->asQualitativeCheckResult().forallTrue();
+        }
+        
+        ValueType getQuantitativeResultAtInitialState(std::shared_ptr<storm::models::Model<ValueType>> const& model, std::unique_ptr<storm::modelchecker::CheckResult>& result) {
+            auto filter = getInitialStateFilter(model);
+            result->filter(*filter);
+            return result->asQuantitativeCheckResult<ValueType>().getMin();
+        }
+    
+    private:
+        storm::Environment _environment;
+        
+        std::unique_ptr<storm::modelchecker::QualitativeCheckResult> getInitialStateFilter(std::shared_ptr<storm::models::Model<ValueType>> const& model) const {
+            if (isSparseModel()) {
+                return std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult>(model->template as<SparseModelType>()->getInitialStates());
+            } else {
+                return std::make_unique<storm::modelchecker::SymbolicQualitativeCheckResult<TestType::ddType>>(model->template as<SymbolicModelType>()->getReachableStates(), model->template as<SymbolicModelType>()->getInitialStates());
+            }
+        }
+    };
+  
+    typedef ::testing::Types<
+            SparseDoubleValueIterationEnvironment,
+            JaniSparseDoubleValueIterationEnvironment,
+            JitSparseDoubleValueIterationEnvironment,
+            SparseDoubleIntervalIterationEnvironment,
+            SparseDoubleSoundValueIterationEnvironment,
+            SparseDoubleTopologicalValueIterationEnvironment,
+            SparseDoubleTopologicalSoundValueIterationEnvironment,
+            SparseRationalPolicyIterationEnvironment,
+            SparseRationalViToPiEnvironment,
+            SparseRationalRationalSearchEnvironment,
+            HybridCuddDoubleValueIterationEnvironment,
+            HybridSylvanDoubleValueIterationEnvironment,
+            HybridCuddDoubleSoundValueIterationEnvironment,
+            HybridSylvanRationalPolicyIterationEnvironment,
+            DdCuddDoubleValueIterationEnvironment,
+            JaniDdCuddDoubleValueIterationEnvironment,
+            DdSylvanDoubleValueIterationEnvironment,
+            DdCuddDoublePolicyIterationEnvironment,
+            DdSylvanRationalRationalSearchEnvironment
+        > TestingTypes;
+    
+    TYPED_TEST_CASE(MdpPrctlModelCheckerTest, TestingTypes);
+    
+
+    TYPED_TEST(MdpPrctlModelCheckerTest, Dice) {
+        std::string formulasString = "Pmin=? [F \"two\"]";
+                 formulasString += "; Pmax=? [F \"two\"]";
+                 formulasString += "; Pmin=? [F \"three\"]";
+                 formulasString += "; Pmax=? [F \"three\"]";
+                 formulasString += "; Pmin=? [F \"four\"]";
+                 formulasString += "; Pmax=? [F \"four\"]";
+                 formulasString += "; Rmin=? [F \"done\"]";
+                 formulasString += "; Rmax=? [F \"done\"]";
+        
+        auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm", formulasString);
+        auto model = std::move(modelFormulas.first);
+        auto tasks = this->getTasks(modelFormulas.second);
+        EXPECT_EQ(169ul, model->getNumberOfStates());
+        EXPECT_EQ(436ul, model->getNumberOfTransitions());
+        ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
+        auto checker = this->createModelChecker(model);
+        std::unique_ptr<storm::modelchecker::CheckResult> result;
+        
+        result = checker->check(this->env(), tasks[0]);
+        EXPECT_NEAR(this->parseNumber("1/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+        
+        result = checker->check(this->env(), tasks[1]);
+        EXPECT_NEAR(this->parseNumber("1/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+        
+        result = checker->check(this->env(), tasks[2]);
+        EXPECT_NEAR(this->parseNumber("2/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+        
+        result = checker->check(this->env(), tasks[3]);
+        EXPECT_NEAR(this->parseNumber("2/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+        
+        result = checker->check(this->env(), tasks[4]);
+        EXPECT_NEAR(this->parseNumber("3/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+        
+        result = checker->check(this->env(), tasks[5]);
+        EXPECT_NEAR(this->parseNumber("3/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+        
+        result = checker->check(this->env(), tasks[6]);
+        EXPECT_NEAR(this->parseNumber("22/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+        
+        result = checker->check(this->env(), tasks[7]);
+        EXPECT_NEAR(this->parseNumber("22/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+    }
+    
+    TYPED_TEST(MdpPrctlModelCheckerTest, AsynchronousLeader) {
+        std::string formulasString = "Pmin=? [F \"elected\"]";
+                 formulasString += "; Pmax=? [F \"elected\"]";
+                 formulasString += "; Pmin=? [F<=25 \"elected\"]";
+                 formulasString += "; Pmax=? [F<=25 \"elected\"]";
+                 formulasString += "; Rmin=? [F \"elected\"]";
+                 formulasString += "; Rmax=? [F \"elected\"]";
+
+        auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/leader4.nm", formulasString);
+        auto model = std::move(modelFormulas.first);
+        auto tasks = this->getTasks(modelFormulas.second);
+        EXPECT_EQ(3172ul, model->getNumberOfStates());
+        EXPECT_EQ(7144ul, model->getNumberOfTransitions());
+        ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
+        auto checker = this->createModelChecker(model);
+        std::unique_ptr<storm::modelchecker::CheckResult> result;
+   
+        
+        result = checker->check(this->env(), tasks[0]);
+        EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+        
+        result = checker->check(this->env(), tasks[1]);
+        EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+        
+        result = checker->check(this->env(), tasks[2]);
+        EXPECT_NEAR(this->parseNumber("1/16"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+        
+        result = checker->check(this->env(), tasks[3]);
+        EXPECT_NEAR(this->parseNumber("1/16"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+        
+        result = checker->check(this->env(), tasks[4]);
+        EXPECT_NEAR(this->parseNumber("30/7"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+        
+        result = checker->check(this->env(), tasks[5]);
+        EXPECT_NEAR(this->parseNumber("30/7"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+    }
+    
+    TYPED_TEST(MdpPrctlModelCheckerTest, consensus) {
+        std::string formulasString = "Pmax=? [F \"finished\"]";
+                    formulasString += "; Pmax=? [F \"all_coins_equal_1\"]";
+                    formulasString += "; P<0.8 [F \"all_coins_equal_1\"]";
+                    formulasString += "; P<0.9 [F \"all_coins_equal_1\"]";
+                    formulasString += "; Rmax=? [F \"all_coins_equal_1\"]";
+                    formulasString += "; Rmin=? [F \"all_coins_equal_1\"]";
+                    formulasString += "; Rmax=? [F \"finished\"]";
+                    formulasString += "; Rmin=? [F \"finished\"]";
+
+        auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm", formulasString);
+        auto model = std::move(modelFormulas.first);
+        auto tasks = this->getTasks(modelFormulas.second);
+        EXPECT_EQ(272ul, model->getNumberOfStates());
+        EXPECT_EQ(492ul, model->getNumberOfTransitions());
+        ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
+        auto checker = this->createModelChecker(model);
+        std::unique_ptr<storm::modelchecker::CheckResult> result;
+
+        result = checker->check(this->env(), tasks[0]);
+        EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+ 
+        result = checker->check(this->env(), tasks[1]);
+        EXPECT_NEAR(this->parseNumber("57/64"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+ 
+        result = checker->check(this->env(), tasks[2]);
+        EXPECT_FALSE(this->getQualitativeResultAtInitialState(model, result));
+ 
+        result = checker->check(this->env(), tasks[3]);
+        EXPECT_TRUE(this->getQualitativeResultAtInitialState(model, result));
+ 
+        result = checker->check(this->env(), tasks[4]);
+        EXPECT_TRUE(storm::utility::isInfinity(this->getQuantitativeResultAtInitialState(model, result)));
+ 
+        result = checker->check(this->env(), tasks[5]);
+        EXPECT_TRUE(storm::utility::isInfinity(this->getQuantitativeResultAtInitialState(model, result)));
+ 
+        result = checker->check(this->env(), tasks[6]);
+        EXPECT_NEAR(this->parseNumber("75"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+
+        result = checker->check(this->env(), tasks[7]);
+        EXPECT_NEAR(this->parseNumber("48"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+    }
+    
+    TYPED_TEST(MdpPrctlModelCheckerTest, TinyRewards) {
+        std::string formulasString = "Rmin=? [F \"target\"]";
+        auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/tiny_rewards.nm", formulasString);
+        auto model = std::move(modelFormulas.first);
+        auto tasks = this->getTasks(modelFormulas.second);
+        EXPECT_EQ(3ul, model->getNumberOfStates());
+        EXPECT_EQ(4ul, model->getNumberOfTransitions());
+        ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
+        auto checker = this->createModelChecker(model);
+        std::unique_ptr<storm::modelchecker::CheckResult> result;
+        
+        // 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 == 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]);
+            EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+        }
+    }
+    
+    TYPED_TEST(MdpPrctlModelCheckerTest, Team) {
+        std::string formulasString = "R{\"w_1_total\"}max=? [ C ]";
+        auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/multiobj_team3.nm", formulasString);
+        auto model = std::move(modelFormulas.first);
+        auto tasks = this->getTasks(modelFormulas.second);
+        EXPECT_EQ(12475ul, model->getNumberOfStates());
+        EXPECT_EQ(15228ul, model->getNumberOfTransitions());
+        ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
+        auto checker = this->createModelChecker(model);
+        std::unique_ptr<storm::modelchecker::CheckResult> result;
+        
+        // This example considers an expected total reward formula, which is not supported in all engines
+
+        if (TypeParam::engine == MdpEngine::PrismSparse || TypeParam::engine == MdpEngine::JaniSparse || TypeParam::engine == MdpEngine::JitSparse) {
+            result = checker->check(this->env(), tasks[0]);
+            EXPECT_NEAR(this->parseNumber("114/49"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+        } else {
+            EXPECT_FALSE(checker->canHandle(tasks[0]));
+        }
+    }
+}

src/test/storm/modelchecker/prctl/mdp/QuantileQueryTest.cpp

@@ -0,0 +1,302 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+
+#include "test/storm_gtest.h"
+
+#include "storm/api/builder.h"
+#include "storm-parsers/api/model_descriptions.h"
+#include "storm/api/properties.h"
+#include "storm-parsers/api/properties.h"
+#include "storm/parser/CSVParser.h"
+
+#include "storm/models/sparse/Mdp.h"
+#include "storm/models/sparse/StandardRewardModel.h"
+#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
+#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
+#include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h"
+#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
+#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+#include "storm/environment/solver/MinMaxSolverEnvironment.h"
+#include "storm/logic/Formulas.h"
+#include "storm/storage/jani/Property.h"
+
+namespace {
+    
+    enum class MdpEngine {PrismSparse, JaniSparse, JitSparse, Hybrid, PrismDd, JaniDd};
+
+    class UnsoundEnvironment {
+    public:
+        typedef double ValueType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
+            return env;
+        }
+    };
+
+    class SoundEnvironment {
+    public:
+        typedef double ValueType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().setForceSoundness(true);
+            return env;
+        }
+    };
+
+    class ExactEnvironment {
+    public:
+        typedef storm::RationalNumber ValueType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            return env;
+        }
+    };
+    
+    template<typename TestType>
+    class QuantileQueryTest : public ::testing::Test {
+    public:
+        typedef typename TestType::ValueType ValueType;
+        QuantileQueryTest() : _environment(TestType::createEnvironment()) {}
+        storm::Environment const& env() const { return _environment; }
+        ValueType parseNumber(std::string const& input) const {
+            if (input.find("inf") != std::string::npos) {
+                return storm::utility::infinity<ValueType>();
+            }
+            return storm::utility::convertNumber<ValueType>(input);
+        }
+        
+        template <typename MT>
+        std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
+            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>();
+            return result;
+        }
+        
+        std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> getTasks(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) const {
+            std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> result;
+            for (auto const& f : formulas) {
+                result.emplace_back(*f, true); // only initial states are relevant
+            }
+            return result;
+        }
+        
+        template <typename MT>
+        typename std::enable_if<std::is_same<MT, storm::models::sparse::Mdp<ValueType>>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type
+        createModelChecker(std::shared_ptr<MT> const& model) const {
+            return std::make_shared<storm::modelchecker::SparseMdpPrctlModelChecker<MT>>(*model);
+        }
+        template <typename MT>
+        typename std::enable_if<std::is_same<MT, storm::models::sparse::Dtmc<ValueType>>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type
+        createModelChecker(std::shared_ptr<MT> const& model) const {
+            return std::make_shared<storm::modelchecker::SparseDtmcPrctlModelChecker<MT>>(*model);
+        }
+        
+        std::pair<bool, std::string> compareResult(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::unique_ptr<storm::modelchecker::CheckResult>& result, std::vector<std::string> const& expected) {
+            bool equal = true;
+            std::string errorMessage = "";
+            auto filter = getInitialStateFilter(model);
+            result->filter(*filter);
+            std::vector<std::vector<ValueType>> resultPoints;
+            if (result->isExplicitParetoCurveCheckResult()) {
+                resultPoints = result->asExplicitParetoCurveCheckResult<ValueType>().getPoints();
+            } else {
+                if (!result->isExplicitQuantitativeCheckResult()) {
+                    return { false, "The CheckResult has unexpected type."};
+                }
+                resultPoints = {{ result->asExplicitQuantitativeCheckResult<ValueType>().getMax() }};
+            }
+            std::vector<std::vector<ValueType>> expectedPoints;
+            for (auto const& pointAsString : expected) {
+                std::vector<ValueType> point;
+                for (auto const& entry : storm::parser::parseCommaSeperatedValues(pointAsString)) {
+                    point.push_back(parseNumber(entry));
+                }
+                expectedPoints.push_back(std::move(point));
+            }
+            for (auto const& resPoint : resultPoints) {
+                bool contained = false;
+                for (auto const& expPoint : expectedPoints) {
+                    if (resPoint == expPoint) {
+                        contained = true;
+                        break;
+                    }
+                }
+                if (!contained) {
+                    equal = false;
+                    errorMessage += "The result " + storm::utility::vector::toString(resPoint) + " is not contained in the expected solution. ";
+                }
+            }
+            for (auto const& expPoint : expectedPoints) {
+                bool contained = false;
+                for (auto const& resPoint : resultPoints) {
+                    if (resPoint == expPoint) {
+                        contained = true;
+                        break;
+                    }
+                }
+                if (!contained) {
+                    equal = false;
+                    errorMessage += "The expected " + storm::utility::vector::toString(expPoint) + " is not contained in the obtained solution. ";
+                }
+            }
+            return {equal, errorMessage};
+        }
+    
+    private:
+        storm::Environment _environment;
+        
+        std::unique_ptr<storm::modelchecker::QualitativeCheckResult> getInitialStateFilter(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) const {
+            return std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult>(model->getInitialStates());
+        }
+    };
+  
+    typedef ::testing::Types<
+            UnsoundEnvironment,
+            SoundEnvironment,
+            ExactEnvironment
+        > TestingTypes;
+    
+    TYPED_TEST_CASE(QuantileQueryTest, TestingTypes);
+    
+
+    TYPED_TEST(QuantileQueryTest, simple_Dtmc) {
+        typedef storm::models::sparse::Dtmc<typename TestFixture::ValueType> ModelType;
+
+        std::string formulasString = "quantile(max A, max B, P>0.95 [F{\"first\"}<=A,{\"second\"}<=B s=3]);\n";
+        
+        auto modelFormulas = this->template buildModelFormulas<ModelType>(STORM_TEST_RESOURCES_DIR "/dtmc/quantiles_simple_dtmc.pm", formulasString);
+        auto model = std::move(modelFormulas.first);
+        auto tasks = this->getTasks(modelFormulas.second);
+        EXPECT_EQ(4ul, model->getNumberOfStates());
+        EXPECT_EQ(6ul, model->getNumberOfTransitions());
+        auto checker = this->template createModelChecker<ModelType>(model);
+        std::unique_ptr<storm::modelchecker::CheckResult> result;
+        std::vector<std::string> expectedResult;
+        std::pair<bool, std::string> compare;
+        uint64_t taskId = 0;
+        
+        expectedResult.clear();
+        expectedResult.push_back("7, 18");
+        expectedResult.push_back("8, 16");
+        expectedResult.push_back("9, 14");
+        result = checker->check(this->env(), tasks[taskId++]);
+        compare = this->compareResult(model, result, expectedResult);
+        EXPECT_TRUE(compare.first) << compare.second;
+    }
+
+    TYPED_TEST(QuantileQueryTest, simple_Mdp) {
+        typedef storm::models::sparse::Mdp<typename TestFixture::ValueType> ModelType;
+
+        std::string formulasString = "quantile(B1, B2, Pmax>0.5 [F{\"first\"}>=B1,{\"second\"}>=B2 s=1]);\n";
+        formulasString += "quantile(B1, B2, Pmax>0.5 [F{\"first\"}<=B1,{\"second\"}<=B2 s=1]);\n";
+        formulasString += "quantile(B1, B2, Pmin>0.5 [F{\"first\"}<=B1,{\"second\"}<=B2 s=1]);\n";
+        formulasString += "quantile(B1, Pmax>0.5 [F{\"second\"}>=B1 s=1]);\n";
+        formulasString += "quantile(B1, B2, B3, Pmax>0.5 [F{\"first\"}<=B1,{\"second\"}<=B2,{\"third\"}<=B3 s=1]);\n";
+        
+        auto modelFormulas = this->template buildModelFormulas<ModelType>(STORM_TEST_RESOURCES_DIR "/mdp/quantiles_simple_mdp.nm", formulasString);
+        auto model = std::move(modelFormulas.first);
+        auto tasks = this->getTasks(modelFormulas.second);
+        EXPECT_EQ(7ul, model->getNumberOfStates());
+        EXPECT_EQ(13ul, model->getNumberOfTransitions());
+        auto checker = this->template createModelChecker<ModelType>(model);
+        std::unique_ptr<storm::modelchecker::CheckResult> result;
+        std::vector<std::string> expectedResult;
+        std::pair<bool, std::string> compare;
+        uint64_t taskId = 0;
+        
+        expectedResult.clear();
+        expectedResult.push_back("  0, 6");
+        expectedResult.push_back("  1, 5");
+        expectedResult.push_back("  2, 4");
+        expectedResult.push_back("  3, 3");
+        expectedResult.push_back("inf, 2");
+        result = checker->check(this->env(), tasks[taskId++]);
+        compare = this->compareResult(model, result, expectedResult);
+        EXPECT_TRUE(compare.first) << compare.second;
+        
+        expectedResult.clear();
+        expectedResult.push_back("  0, 2");
+        expectedResult.push_back("  5, 1");
+        expectedResult.push_back("  6, 0");
+        result = checker->check(this->env(), tasks[taskId++]);
+        compare = this->compareResult(model, result, expectedResult);
+        EXPECT_TRUE(compare.first) << compare.second;
+        
+        expectedResult.clear();
+        result = checker->check(this->env(), tasks[taskId++]);
+        compare = this->compareResult(model, result, expectedResult);
+        EXPECT_TRUE(compare.first) << compare.second;
+        
+        expectedResult.clear();
+        expectedResult.push_back("  6");
+        result = checker->check(this->env(), tasks[taskId++]);
+        compare = this->compareResult(model, result, expectedResult);
+        EXPECT_TRUE(compare.first) << compare.second;
+        
+        expectedResult.clear();
+        expectedResult.push_back("  0, 2, 1.4");
+        expectedResult.push_back("  5, 1, 9.8");
+        expectedResult.push_back("  6, 0, 9.8");
+        result = checker->check(this->env(), tasks[taskId++]);
+        compare = this->compareResult(model, result, expectedResult);
+        EXPECT_TRUE(compare.first) << compare.second;
+    }
+    
+    TYPED_TEST(QuantileQueryTest, firewire) {
+        typedef storm::models::sparse::Mdp<typename TestFixture::ValueType> ModelType;
+
+        std::string formulasString = "quantile(min TIME, min ROUNDS, Pmax>0.95 [F{\"time\"}<=TIME,{\"rounds\"}<=ROUNDS \"done\"]);\n";
+        
+        auto modelFormulas = this->template buildModelFormulas<ModelType>(STORM_TEST_RESOURCES_DIR "/mdp/quantiles_firewire.nm", formulasString, "delay=36");
+        auto model = std::move(modelFormulas.first);
+        auto tasks = this->getTasks(modelFormulas.second);
+        EXPECT_EQ(776ul, model->getNumberOfStates());
+        EXPECT_EQ(1411ul, model->getNumberOfTransitions());
+        auto checker = this->template createModelChecker<ModelType>(model);
+        std::unique_ptr<storm::modelchecker::CheckResult> result;
+        std::vector<std::string> expectedResult;
+        std::pair<bool, std::string> compare;
+        uint64_t taskId = 0;
+        
+        expectedResult.clear();
+        expectedResult.push_back("123, 1");
+        result = checker->check(this->env(), tasks[taskId++]);
+        compare = this->compareResult(model, result, expectedResult);
+        EXPECT_TRUE(compare.first) << compare.second;
+    
+    }
+    
+    TYPED_TEST(QuantileQueryTest, resources) {
+        typedef storm::models::sparse::Mdp<typename TestFixture::ValueType> ModelType;
+
+        std::string formulasString = "quantile(max GOLD, max GEM, Pmax>0.95 [F{\"gold\"}>=GOLD,{\"gem\"}>=GEM,{\"steps\"}<=100 true]);\n";
+        
+        auto modelFormulas = this->template buildModelFormulas<ModelType>(STORM_TEST_RESOURCES_DIR "/mdp/quantiles_resources.nm", formulasString);
+        auto model = std::move(modelFormulas.first);
+        auto tasks = this->getTasks(modelFormulas.second);
+        EXPECT_EQ(94ul, model->getNumberOfStates());
+        EXPECT_EQ(326ul, model->getNumberOfTransitions());
+        auto checker = this->template createModelChecker<ModelType>(model);
+        std::unique_ptr<storm::modelchecker::CheckResult> result;
+        std::vector<std::string> expectedResult;
+        std::pair<bool, std::string> compare;
+        uint64_t taskId = 0;
+        
+        expectedResult.clear();
+        expectedResult.push_back("0, 10");
+        expectedResult.push_back("1, 9");
+        expectedResult.push_back("4, 8");
+        expectedResult.push_back("7, 7");
+        expectedResult.push_back("8, 4");
+        expectedResult.push_back("9, 2");
+        expectedResult.push_back("10, 0");
+        result = checker->check(this->env(), tasks[taskId++]);
+        compare = this->compareResult(model, result, expectedResult);
+        EXPECT_TRUE(compare.first) << compare.second;
+    
+    }
+}

src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp

@@ -0,0 +1,142 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+
+#include "storm-parsers/parser/FormulaParser.h"
+#include "storm/logic/Formulas.h"
+#include "storm/solver/StandardMinMaxLinearEquationSolver.h"
+#include "storm/models/sparse/StandardRewardModel.h"
+#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
+#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/GeneralSettings.h"
+
+#include "storm/environment/solver/MinMaxSolverEnvironment.h"
+
+#include "storm-parsers/parser/AutoParser.h"
+#include "storm-parsers/parser/PrismParser.h"
+#include "storm/builder/ExplicitModelBuilder.h"
+
+namespace {
+    class DoubleViEnvironment {
+    public:
+        typedef double ValueType;
+        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-8));
+            return env;
+        }
+    };
+    class DoubleSoundViEnvironment {
+    public:
+        typedef double ValueType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
+            env.solver().setForceSoundness(true);
+            env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
+            return env;
+        }
+    };
+    class DoublePIEnvironment {
+    public:
+        typedef double ValueType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration);
+            env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
+            return env;
+        }
+    };
+    class RationalPIEnvironment {
+    public:
+        typedef storm::RationalNumber ValueType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration);
+            return env;
+        }
+    };
+ //   class RationalRationalSearchEnvironment {
+ //   public:
+ //       typedef storm::RationalNumber ValueType;
+ //       static storm::Environment createEnvironment() {
+ //           storm::Environment env;
+ //           env.solver().minMax().setMethod(storm::solver::MinMaxMethod::RationalSearch);
+ //           return env;
+ //       }
+ //   };
+    
+    template<typename TestType>
+    class SchedulerGenerationMdpPrctlModelCheckerTest : public ::testing::Test {
+    public:
+        typedef typename TestType::ValueType ValueType;
+        SchedulerGenerationMdpPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
+        storm::Environment const& env() const { return _environment; }
+    private:
+        storm::Environment _environment;
+    };
+  
+    typedef ::testing::Types<
+            DoubleViEnvironment,
+            DoubleSoundViEnvironment,
+            DoublePIEnvironment,
+            RationalPIEnvironment
+            //RationalRationalSearchEnvironment
+    > TestingTypes;
+    
+   TYPED_TEST_CASE(SchedulerGenerationMdpPrctlModelCheckerTest, TestingTypes);
+
+    
+    TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, reachability) {
+        typedef typename TestFixture::ValueType ValueType;
+
+        storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/scheduler_generation.nm");
+    
+        // A parser that we use for conveniently constructing the formulas.
+        storm::parser::FormulaParser formulaParser;
+        
+        storm::generator::NextStateGeneratorOptions options;
+        options.setBuildAllLabels();
+        std::shared_ptr<storm::models::sparse::Model<ValueType>> model = storm::builder::ExplicitModelBuilder<ValueType>(program, options).build();
+        EXPECT_EQ(4ull, model->getNumberOfStates());
+        EXPECT_EQ(11ull, model->getNumberOfTransitions());
+        
+        ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
+    
+        std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp = model->template as<storm::models::sparse::Mdp<ValueType>>();
+    
+        EXPECT_EQ(7ull, mdp->getNumberOfChoices());
+    
+        storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
+        
+        std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"target\"]");
+        
+        storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> checkTask(*formula);
+        checkTask.setProduceSchedulers(true);
+        
+        std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), checkTask);
+        
+        ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+        ASSERT_TRUE(result->asExplicitQuantitativeCheckResult<ValueType>().hasScheduler());
+        storm::storage::Scheduler<ValueType> const& scheduler = result->asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
+        EXPECT_EQ(0ull, scheduler.getChoice(0).getDeterministicChoice());
+        EXPECT_EQ(1ull, scheduler.getChoice(1).getDeterministicChoice());
+        EXPECT_EQ(0ull, scheduler.getChoice(2).getDeterministicChoice());
+        EXPECT_EQ(0ull, scheduler.getChoice(3).getDeterministicChoice());
+        
+        formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"target\"]");
+        
+        checkTask = storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>(*formula);
+        checkTask.setProduceSchedulers(true);
+        result = checker.check(checkTask);
+    
+        ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+        ASSERT_TRUE(result->asExplicitQuantitativeCheckResult<ValueType>().hasScheduler());
+        storm::storage::Scheduler<ValueType> const& scheduler2 = result->asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
+        EXPECT_EQ(1ull, scheduler2.getChoice(0).getDeterministicChoice());
+        EXPECT_EQ(2ull, scheduler2.getChoice(1).getDeterministicChoice());
+        EXPECT_EQ(0ull, scheduler2.getChoice(2).getDeterministicChoice());
+        EXPECT_EQ(0ull, scheduler2.getChoice(3).getDeterministicChoice());
+    }
+}