storm-pars library

src/CMakeLists.txt

@@ -9,6 +9,9 @@ add_subdirectory(storm-gspn)
 add_subdirectory(storm-gspn-cli)
 add_subdirectory(storm-dft)
 add_subdirectory(storm-dft-cli)
+add_subdirectory(storm-pars)
+add_subdirectory(storm-pars-cli)
+
 add_subdirectory(test)
 
-set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE)
+set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE)

src/storm-pars/CMakeLists.txt

@@ -0,0 +1,40 @@
+file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-pars/*.h ${PROJECT_SOURCE_DIR}/src/storm-pars/*.cpp)
+
+register_source_groups_from_filestructure("${ALL_FILES}" storm-pars)
+
+
+
+file(GLOB_RECURSE STORM_PARS_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-pars/*/*.cpp)
+file(GLOB_RECURSE STORM_PARS_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-pars/*/*.h)
+
+
+# Create storm-pars.
+add_library(storm-pars SHARED ${STORM_PARS_SOURCES} ${STORM_PARS_HEADERS})
+
+# Remove define symbol for shared libstorm.
+set_target_properties(storm-pars PROPERTIES DEFINE_SYMBOL "")
+#add_dependencies(storm resources)
+list(APPEND STORM_TARGETS storm-pars)
+set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE)
+
+target_link_libraries(storm-pars PUBLIC storm ${STORM_PARS_LINK_LIBRARIES})
+
+# Install storm headers to include directory.
+foreach(HEADER ${STORM_PARS_HEADERS})
+	string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER})
+	string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH})
+	string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH})
+	add_custom_command(
+		OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}
+		COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}
+		COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}
+		DEPENDS ${HEADER}
+	)
+	list(APPEND STORM_PARS_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}")
+endforeach()
+add_custom_target(copy_storm_pars_headers DEPENDS ${STORM_PARS_OUTPUT_HEADERS} ${STORM_PARS_HEADERS})
+add_dependencies(storm-pars copy_storm_pars_headers)
+
+# installation
+install(TARGETS storm-pars RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
+

src/storm-pars/api/parametric.h

@@ -0,0 +1,45 @@
+#pragma once
+
+#include <memory>
+
+#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h"
+#include "storm-pars/transformer/SparseParametricMdpSimplifier.h"
+
+#include "storm/models/sparse/Model.h"
+#include "storm/logic/Formula.h"
+#include "storm/utility/macros.h"
+
+namespace storm {
+    namespace api {
+        
+        template <typename ValueType>
+        bool simplifyParametricModel(std::shared_ptr<storm::models::sparse::Model<ValueType> const& inputModel, std::shared_ptr<storm::logic::Formula const> const& inputFormula, std::shared_ptr<storm::models::sparse::Model<ValueType>& outputModel, std::shared_ptr<storm::logic::Formula const>& outputFormula) {
+            
+            if (inputModel->isOfType(storm::models::ModelType::Dtmc)) {
+                auto const& dtmc = *inputModel->template as<storm::models::sparse::Dtmc<ValueType>>();
+                auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<ValueType>>(dtmc);
+                if (simplifier.simplify(*inputFormula)) {
+                    outputModel = simplifier.getSimplifiedModel();
+                    outputFormula = simplifier.getSimplifiedFormula();
+                    return true;
+                }
+            } else if (inputModel->isOfType(storm::models::ModelType::Mdp)) {
+                auto const& mdp = *inputModel->template as<storm::models::sparse::Mdp<ValueType>>();
+                auto simplifier = storm::transformer::SparseParametricMdpSimplifier<storm::models::sparse::Mdp<ValueType>>(mdp);
+                if (simplifier.simplify(*inputFormula)) {
+                    outputModel = simplifier.getSimplifiedModel();
+                    outputFormula = simplifier.getSimplifiedFormula();
+                    return true;
+                }
+            } else {
+                STORM_LOG_ERROR("Unable to simplify model with the given type.");
+            }
+
+            // Reaching this point means that simplification was not successful.
+            outputModel = nullptr;
+            outputFormula = nullptr;
+            return false;
+            
+        }
+    }
+}

src/storm-pars/api/region.h

@@ -0,0 +1,126 @@
+#pragma once
+
+#include <string>
+#include <set>
+#include <vector>
+#include <memory>
+#include <boost/optional.hpp>
+
+#include "storm-pars/storage/ParameterRegion.h"
+
+#include "storm-pars/modelchecker/results/RegionCheckResult.h"
+#include "storm-pars/modelchecker/results/RegionRefinementCheckResult.h"
+#include "storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h"
+#include "storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h"
+#include "storm-pars/parser/ParameterRegionParser.h"
+
+#include "storm/api/transformation.h"
+#include "storm/models/sparse/Model.h"
+#include "storm/exceptions/UnexpectedException.h"
+#include "storm/exceptions/InvalidOperationException.h"
+
+namespace storm {
+    
+    namespace api {
+        
+        
+        enum class RegionModelCheckerType {
+            ParameterLifting,
+            ExactParameterLifting,
+            ValidatingParameterLifting
+        };
+
+        template <typename ValueType>
+        std::vector<storm::storage::ParameterRegion<ValueType>> parseRegions(std::string const& inputString, std::set<typename storm::storage::ParameterRegion<ValueType>::VariableType> const& consideredVariables) {
+            // If the given input string looks like a file (containing a dot and there exists a file with that name),
+            // we try to parse it as a file, otherwise we assume it's a region string.
+            if (inputString.find(".") != std::string::npos && std::ifstream(inputString).good()) {
+                return storm::parser::ParameterRegionParser<ValueType>().parseMultipleRegionsFromFile(inputString, consideredVariables);
+            } else {
+                return storm::parser::ParameterRegionParser<ValueType>().parseMultipleRegions(inputString, consideredVariables);
+            }
+        }
+        
+        template <typename ValueType>
+        std::vector<storm::storage::ParameterRegion<ValueType>> parseRegions(std::string const& inputString, storm::models::sparse::Model<ValueType> const& model) {
+            auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
+            auto rewParameters = storm::models::sparse::getRewardParameters(*model);
+            modelParameters.insert(rewParameters.begin(), rewParameters.end());
+            return parseRegions(inputString, modelParameters);
+        }
+        
+        template <typename ParametricType, typename ConstantType>
+        std::unique_ptr<storm::modelchecker::RegionModelChecker<ParametricType>> initializeParameterLiftingRegionModelChecker(std::shared_ptr<storm::models::sparse::Model<ParametricType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ParametricType> const& task) {
+            // Treat continuous time models
+            if (model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::MarkovAutomaton)) {
+                    STORM_LOG_WARN("Parameter lifting not supported for continuous time models. Transforming continuous model to discrete model...");
+                    std::vector<std::shared_ptr<storm::logic::Formula const>> taskFormulaAsVector { task.getFormula().asSharedPointer() };
+                    auto discreteTimeModel = storm::api::transformContinuousToDiscreteTimeSparseModel(model, taskFormulaAsVector);
+                    STORM_LOG_THROW(discreteTimeModel->isOfType(storm::models::ModelType::Dtmc) || discreteTimeModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::UnexpectedException, "Transformation to discrete time model has failed.");
+                    return initializeParameterLiftingRegionModelChecker(discreteTimeModel, task);
+            }
+            
+            // Obtain the region model checker
+            std::unique_ptr<storm::modelchecker::RegionModelChecker<ParametricType>> result;
+            if (model->isOfType(storm::models::ModelType::Dtmc)) {
+                auto const& dtmc = *model->template as<storm::models::sparse::Dtmc<ParametricType>>();
+                result = std::make_unique<storm::modelchecker::SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<ValueType>, ConstantType>>(dtmc);
+            } else if (model->isOfType(storm::models::ModelType::Mdp)) {
+                auto const& mdp = *model->template as<storm::models::sparse::Mdp<ParametricType>>();
+                result = std::make_unique<storm::modelchecker::SparseMdpParameterLiftingModelChecker<storm::models::sparse::Mdp<ValueType>, ConstantType>>(mdp);
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform parameterLifting on the provided model type.");
+            }
+                
+            result->specifyFormula(task);
+        
+            return result;
+        }
+        
+        template <typename ParametricType, typename ImpreciseType, typename PreciseType>
+        std::unique_ptr<storm::modelchecker::RegionModelChecker<ValueType>> initializeValidatingRegionModelChecker(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ParametricType> const& task) {
+            // todo
+            return nullptr;
+        }
+        
+        template <typename ValueType>
+        std::unique_ptr<storm::modelchecker::RegionModelChecker<ValueType>> initializeRegionModelChecker(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task, RegionModelCheckerType checkerType) {
+            switch (checkerType) {
+                    case RegionModelCheckerType::ParameterLifting:
+                            return initializeParameterLiftingRegionModelChecker<ValueType, double>(model, task);
+                    case RegionModelCheckerType::ExactParameterLifting:
+                            return initializeParameterLiftingRegionModelChecker<ValueType, storm::RationalNumber>(model, task);
+                    case RegionModelCheckerType::ValidatingParameterLifting:
+                            return initializeValidatingRegionModelChecker<ValueType, double, storm::RationalNumber>(model, task);
+                    default:
+                            STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected region model checker type.");
+            }
+            return nullptr;
+        }
+        
+        template <typename ValueType>
+        std::unique_ptr<storm::modelchecker::RegionCheckResult<ValueType>> checkRegionsWithSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task, std::vector<storm::storage::ParameterRegion<ValueType>> const& regions, RegionModelCheckerType checkerType) {
+            auto regionChecker = initializeRegionModelChecker(model, task, checkerType);
+            return regionChecker->analyzeRegions(regions, true);
+        }
+    
+        
+        template <typename ValueType>
+        td::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ValueType>> checkAndRefineRegionWithSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task, storm::storage::ParameterRegion<ValueType> const& region, ValueType const& refinementThreshold) {
+            auto regionChecker = initializeRegionModelChecker(model, task, checkerType);
+            return regionChecker->performRegionRefinement(region, refinementThreshold);
+        }
+        
+
+        template <typename ValueType>
+        void exportRegionCheckResultToFile(std::unique_ptr<storm::modelchecker::RegionCheckResult<ValueType>> const& checkResult, std::string const& filename) {
+
+            std::ofstream filestream;
+            storm::utility::openFile(path, filestream);
+            for (auto const& res : checkResult->getRegionResults()) {
+                    filestream << res.second << ": " << res.first << std::endl;
+            }
+        }
+    
+    }
+}

src/storm-pars/api/storm-pars.h

@@ -0,0 +1,4 @@
+#pragma once
+
+#include "storm-pars/api/region.h"
+#include "storm-pars/api/parametric.h"

src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp

@@ -1,4 +1,4 @@
-#include "SparseDtmcInstantiationModelChecker.h"
+#include "storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.h"
 
 #include "storm/logic/FragmentSpecification.h"
 #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
@@ -10,43 +10,112 @@
 #include "storm/exceptions/InvalidStateException.h"
 namespace storm {
     namespace modelchecker {
-        namespace parametric {
+        
+        template <typename SparseModelType, typename ConstantType>
+        SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>::SparseDtmcInstantiationModelChecker(SparseModelType const& parametricModel) : SparseInstantiationModelChecker<SparseModelType, ConstantType>(parametricModel), modelInstantiator(parametricModel) {
+            //Intentionally left empty
+        }
+
+        template <typename SparseModelType, typename ConstantType>
+        std::unique_ptr<CheckResult> SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>::check(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) {
+            STORM_LOG_THROW(this->currentCheckTask, storm::exceptions::InvalidStateException, "Checking has been invoked but no property has been specified before.");
+            auto const& instantiatedModel = modelInstantiator.instantiate(valuation);
+            STORM_LOG_ASSERT(instantiatedModel.getTransitionMatrix().isProbabilistic(), "Instantiated matrix is not probabilistic!");
+            storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>> modelChecker(instantiatedModel);
+
+            // Check if there are some optimizations implemented for the specified property
+            if(this->currentCheckTask->getFormula().isInFragment(storm::logic::reachability())) {
+                return checkReachabilityProbabilityFormula(modelChecker);
+            } else if (this->currentCheckTask->getFormula().isInFragment(storm::logic::propositional().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setOperatorAtTopLevelRequired(true).setNestedOperatorsAllowed(false))) {
+                return checkReachabilityRewardFormula(modelChecker);
+            } else if (this->currentCheckTask->getFormula().isInFragment(storm::logic::propositional().setProbabilityOperatorsAllowed(true).setBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setOperatorAtTopLevelRequired(true).setNestedOperatorsAllowed(false))) {
+                return checkBoundedUntilFormula(modelChecker);
+            } else {
+                return modelChecker.check(*this->currentCheckTask);
+            }
+        }
+        
+        template <typename SparseModelType, typename ConstantType>
+        std::unique_ptr<CheckResult> SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>::checkReachabilityProbabilityFormula(storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>>& modelChecker) {
             
-            template <typename SparseModelType, typename ConstantType>
-            SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>::SparseDtmcInstantiationModelChecker(SparseModelType const& parametricModel) : SparseInstantiationModelChecker<SparseModelType, ConstantType>(parametricModel), modelInstantiator(parametricModel) {
-                //Intentionally left empty
+            if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) {
+                this->currentCheckTask->setHint(std::make_shared<ExplicitModelCheckerHint<ConstantType>>());
             }
-    
-            template <typename SparseModelType, typename ConstantType>
-            std::unique_ptr<CheckResult> SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>::check(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) {
-                STORM_LOG_THROW(this->currentCheckTask, storm::exceptions::InvalidStateException, "Checking has been invoked but no property has been specified before.");
-                auto const& instantiatedModel = modelInstantiator.instantiate(valuation);
-                STORM_LOG_ASSERT(instantiatedModel.getTransitionMatrix().isProbabilistic(), "Instantiated matrix is not probabilistic!");
-                storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>> modelChecker(instantiatedModel);
-
-                // Check if there are some optimizations implemented for the specified property
-                if(this->currentCheckTask->getFormula().isInFragment(storm::logic::reachability())) {
-                    return checkReachabilityProbabilityFormula(modelChecker);
-                } else if (this->currentCheckTask->getFormula().isInFragment(storm::logic::propositional().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setOperatorAtTopLevelRequired(true).setNestedOperatorsAllowed(false))) {
-                    return checkReachabilityRewardFormula(modelChecker);
-                } else if (this->currentCheckTask->getFormula().isInFragment(storm::logic::propositional().setProbabilityOperatorsAllowed(true).setBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setOperatorAtTopLevelRequired(true).setNestedOperatorsAllowed(false))) {
-                    return checkBoundedUntilFormula(modelChecker);
-                } else {
-                    return modelChecker.check(*this->currentCheckTask);
-                }
+            ExplicitModelCheckerHint<ConstantType>& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>();
+            std::unique_ptr<CheckResult> result;
+            
+            // Check the formula and store the result as a hint for the next call.
+            // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula
+            if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
+                result = modelChecker.check(*this->currentCheckTask);
+                hint.setResultHint(result->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector());
+            } else {
+                auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false);
+                std::unique_ptr<CheckResult> quantitativeResult = modelChecker.computeProbabilities(newCheckTask);
+                result = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
+                hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()));
             }
-                
-            template <typename SparseModelType, typename ConstantType>
-            std::unique_ptr<CheckResult> SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>::checkReachabilityProbabilityFormula(storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>>& modelChecker) {
-                
-                if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) {
-                    this->currentCheckTask->setHint(std::make_shared<ExplicitModelCheckerHint<ConstantType>>());
-                }
-                ExplicitModelCheckerHint<ConstantType>& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>();
-                std::unique_ptr<CheckResult> result;
-                
-                // Check the formula and store the result as a hint for the next call.
-                // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula
+            
+            if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) {
+                // Extract the maybe states from the current result.
+                assert(hint.hasResultHint());
+                storm::storage::BitVector maybeStates = ~storm::utility::vector::filter<ConstantType>(hint.getResultHint(),
+                                [] (ConstantType const& value) -> bool { return storm::utility::isZero<ConstantType>(value) || storm::utility::isOne<ConstantType>(value); });
+                hint.setMaybeStates(std::move(maybeStates));
+                hint.setComputeOnlyMaybeStates(true);
+            }
+            
+            return result;
+        }
+        
+        template <typename SparseModelType, typename ConstantType>
+        std::unique_ptr<CheckResult> SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>::checkReachabilityRewardFormula(storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>>& modelChecker) {
+            
+            if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) {
+                this->currentCheckTask->setHint(std::make_shared<ExplicitModelCheckerHint<ConstantType>>());
+            }
+            ExplicitModelCheckerHint<ConstantType>& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>();
+            std::unique_ptr<CheckResult> result;
+            
+            // Check the formula and store the result as a hint for the next call.
+            // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula
+            if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
+                result = modelChecker.check(*this->currentCheckTask);
+                this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>().setResultHint(result->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector());
+            } else {
+                auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false);
+                std::unique_ptr<CheckResult> quantitativeResult = modelChecker.computeRewards(this->currentCheckTask->getFormula().asRewardOperatorFormula().getMeasureType(), newCheckTask);
+                result = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
+                this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>().setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()));
+            }
+            
+            if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) {
+                // Extract the maybe states from the current result.
+                assert(hint.hasResultHint());
+                storm::storage::BitVector maybeStates = ~storm::utility::vector::filterInfinity(hint.getResultHint());
+                // We need to exclude the target states from the maybe states.
+                // Note that we can not consider the states with reward zero since a valuation might set a reward to zero
+                std::unique_ptr<CheckResult> subFormulaResult = modelChecker.check(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asEventuallyFormula().getSubformula());
+                maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector());
+                hint.setMaybeStates(std::move(maybeStates));
+                hint.setComputeOnlyMaybeStates(true);
+            }
+            
+            return result;
+        }
+        
+        template <typename SparseModelType, typename ConstantType>
+        std::unique_ptr<CheckResult> SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>::checkBoundedUntilFormula(storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>>& modelChecker) {
+            
+            if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) {
+                this->currentCheckTask->setHint(std::make_shared<ExplicitModelCheckerHint<ConstantType>>());
+            }
+            std::unique_ptr<CheckResult> result;
+            ExplicitModelCheckerHint<ConstantType>& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>();
+            
+            if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) {
+                // We extract the maybestates from the quantitative result
+                // For qualitative properties, we still need a quantitative result. Hence we perform the check on the subformula
                 if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
                     result = modelChecker.check(*this->currentCheckTask);
                     hint.setResultHint(result->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector());
@@ -57,93 +126,22 @@ namespace storm {
                     hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()));
                 }
                 
-                if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) {
-                    // Extract the maybe states from the current result.
-                    assert(hint.hasResultHint());
-                    storm::storage::BitVector maybeStates = ~storm::utility::vector::filter<ConstantType>(hint.getResultHint(),
-                                    [] (ConstantType const& value) -> bool { return storm::utility::isZero<ConstantType>(value) || storm::utility::isOne<ConstantType>(value); });
-                    hint.setMaybeStates(std::move(maybeStates));
-                    hint.setComputeOnlyMaybeStates(true);
-                }
-                
-                return result;
+                storm::storage::BitVector maybeStates = storm::utility::vector::filterGreaterZero(hint.getResultHint());
+                // We need to exclude the target states from the maybe states.
+                // Note that we can not consider the states with probability one since a state might reach a target state with prob 1 within >0 steps
+                std::unique_ptr<CheckResult> subFormulaResult = modelChecker.check(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asBoundedUntilFormula().getRightSubformula());
+                maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector());
+                hint.setMaybeStates(std::move(maybeStates));
+                hint.setComputeOnlyMaybeStates(true);
+            } else {
+                result = modelChecker.check(*this->currentCheckTask);
             }
             
-            template <typename SparseModelType, typename ConstantType>
-            std::unique_ptr<CheckResult> SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>::checkReachabilityRewardFormula(storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>>& modelChecker) {
-                
-                if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) {
-                    this->currentCheckTask->setHint(std::make_shared<ExplicitModelCheckerHint<ConstantType>>());
-                }
-                ExplicitModelCheckerHint<ConstantType>& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>();
-                std::unique_ptr<CheckResult> result;
-                
-                // Check the formula and store the result as a hint for the next call.
-                // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula
-                if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
-                    result = modelChecker.check(*this->currentCheckTask);
-                    this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>().setResultHint(result->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector());
-                } else {
-                    auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false);
-                    std::unique_ptr<CheckResult> quantitativeResult = modelChecker.computeRewards(this->currentCheckTask->getFormula().asRewardOperatorFormula().getMeasureType(), newCheckTask);
-                    result = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
-                    this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>().setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()));
-                }
-                                
-                if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) {
-                    // Extract the maybe states from the current result.
-                    assert(hint.hasResultHint());
-                    storm::storage::BitVector maybeStates = ~storm::utility::vector::filterInfinity(hint.getResultHint());
-                    // We need to exclude the target states from the maybe states.
-                    // Note that we can not consider the states with reward zero since a valuation might set a reward to zero
-                    std::unique_ptr<CheckResult> subFormulaResult = modelChecker.check(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asEventuallyFormula().getSubformula());
-                    maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector());
-                    hint.setMaybeStates(std::move(maybeStates));
-                    hint.setComputeOnlyMaybeStates(true);
-                }
-                
-                return result;
-            }
-            
-            template <typename SparseModelType, typename ConstantType>
-            std::unique_ptr<CheckResult> SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>::checkBoundedUntilFormula(storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>>& modelChecker) {
-                
-                if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) {
-                    this->currentCheckTask->setHint(std::make_shared<ExplicitModelCheckerHint<ConstantType>>());
-                }
-                std::unique_ptr<CheckResult> result;
-                ExplicitModelCheckerHint<ConstantType>& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>();
-                
-                if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) {
-                    // We extract the maybestates from the quantitative result
-                    // For qualitative properties, we still need a quantitative result. Hence we perform the check on the subformula
-                    if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
-                        result = modelChecker.check(*this->currentCheckTask);
-                        hint.setResultHint(result->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector());
-                    } else {
-                        auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false);
-                        std::unique_ptr<CheckResult> quantitativeResult = modelChecker.computeProbabilities(newCheckTask);
-                        result = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
-                        hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()));
-                    }
-                    
-                    storm::storage::BitVector maybeStates = storm::utility::vector::filterGreaterZero(hint.getResultHint());
-                    // We need to exclude the target states from the maybe states.
-                    // Note that we can not consider the states with probability one since a state might reach a target state with prob 1 within >0 steps
-                    std::unique_ptr<CheckResult> subFormulaResult = modelChecker.check(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asBoundedUntilFormula().getRightSubformula());
-                    maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector());
-                    hint.setMaybeStates(std::move(maybeStates));
-                    hint.setComputeOnlyMaybeStates(true);
-                } else {
-                    result = modelChecker.check(*this->currentCheckTask);
-                }
-                
-                return result;
-            }
-            
-            template class SparseDtmcInstantiationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
-            template class SparseDtmcInstantiationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber>;
-
+            return result;
         }
+        
+        template class SparseDtmcInstantiationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
+        template class SparseDtmcInstantiationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber>;
+
     }
 }

src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.h

@@ -3,35 +3,33 @@
 #include <memory>
 #include <boost/optional.hpp>
 
+#include "storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.h"
+#include "storm-pars/utility/ModelInstantiator.h"
 #include "storm/models/sparse/Dtmc.h"
 #include "storm/models/sparse/StandardRewardModel.h"
-#include "storm/modelchecker/parametric/SparseInstantiationModelChecker.h"
 #include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
-#include "storm/utility/ModelInstantiator.h"
 
 namespace storm {
     namespace modelchecker {
-        namespace parametric {
+        
+        /*!
+         * Class to efficiently check a formula on a parametric model with different parameter instantiations
+         */
+        template <typename SparseModelType, typename ConstantType>
+        class SparseDtmcInstantiationModelChecker : public SparseInstantiationModelChecker<SparseModelType, ConstantType> {
+        public:
+            SparseDtmcInstantiationModelChecker(SparseModelType const& parametricModel);
             
-            /*!
-             * Class to efficiently check a formula on a parametric model with different parameter instantiations
-             */
-            template <typename SparseModelType, typename ConstantType>
-            class SparseDtmcInstantiationModelChecker : public SparseInstantiationModelChecker<SparseModelType, ConstantType> {
-            public:
-                SparseDtmcInstantiationModelChecker(SparseModelType const& parametricModel);
-                
-                virtual std::unique_ptr<CheckResult> check(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) override;
+            virtual std::unique_ptr<CheckResult> check(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) override;
 
-            protected:
-                
-                // Optimizations for the different formula types
-                std::unique_ptr<CheckResult> checkReachabilityProbabilityFormula(storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>>& modelChecker);
-                std::unique_ptr<CheckResult> checkReachabilityRewardFormula(storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>>& modelChecker);
-                std::unique_ptr<CheckResult> checkBoundedUntilFormula(storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>>& modelChecker);
-                
-                storm::utility::ModelInstantiator<SparseModelType, storm::models::sparse::Dtmc<ConstantType>> modelInstantiator;
-            };
-        }
+        protected:
+            
+            // Optimizations for the different formula types
+            std::unique_ptr<CheckResult> checkReachabilityProbabilityFormula(storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>>& modelChecker);
+            std::unique_ptr<CheckResult> checkReachabilityRewardFormula(storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>>& modelChecker);
+            std::unique_ptr<CheckResult> checkBoundedUntilFormula(storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>>& modelChecker);
+            
+            storm::utility::ModelInstantiator<SparseModelType, storm::models::sparse::Dtmc<ConstantType>> modelInstantiator;
+        };
     }
 }

src/storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.cpp

@@ -1,4 +1,4 @@
-#include "SparseInstantiationModelChecker.h"
+#include "storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.h"
 
 #include "storm/adapters/RationalFunctionAdapter.h"
 #include "storm/models/sparse/Dtmc.h"
@@ -9,36 +9,34 @@
 
 namespace storm {
     namespace modelchecker {
-        namespace parametric {
-            
-            template <typename SparseModelType, typename ConstantType>
-            SparseInstantiationModelChecker<SparseModelType, ConstantType>::SparseInstantiationModelChecker(SparseModelType const& parametricModel) : parametricModel(parametricModel), instantiationsAreGraphPreserving(false) {
-                //Intentionally left empty
-            }
-            
-                
-            template <typename SparseModelType, typename ConstantType>
-            void SparseInstantiationModelChecker<SparseModelType, ConstantType>::specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
-                currentFormula = checkTask.getFormula().asSharedPointer();
-                currentCheckTask = std::make_unique<storm::modelchecker::CheckTask<storm::logic::Formula, ConstantType>>(checkTask.substituteFormula(*currentFormula).template convertValueType<ConstantType>());
-            }
-            
-            template <typename SparseModelType, typename ConstantType>
-            void SparseInstantiationModelChecker<SparseModelType, ConstantType>::setInstantiationsAreGraphPreserving(bool value) {
-                instantiationsAreGraphPreserving = value;
-            }
-            
-            template <typename SparseModelType, typename ConstantType>
-            bool SparseInstantiationModelChecker<SparseModelType, ConstantType>::getInstantiationsAreGraphPreserving() const {
-                return instantiationsAreGraphPreserving;
-            }
-            
-            template class SparseInstantiationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
-            template class SparseInstantiationModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
-            
-            template class SparseInstantiationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber>;
-            template class SparseInstantiationModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, storm::RationalNumber>;
-
+        
+        template <typename SparseModelType, typename ConstantType>
+        SparseInstantiationModelChecker<SparseModelType, ConstantType>::SparseInstantiationModelChecker(SparseModelType const& parametricModel) : parametricModel(parametricModel), instantiationsAreGraphPreserving(false) {
+            //Intentionally left empty
+        }
+        
+        
+        template <typename SparseModelType, typename ConstantType>
+        void SparseInstantiationModelChecker<SparseModelType, ConstantType>::specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
+            currentFormula = checkTask.getFormula().asSharedPointer();
+            currentCheckTask = std::make_unique<storm::modelchecker::CheckTask<storm::logic::Formula, ConstantType>>(checkTask.substituteFormula(*currentFormula).template convertValueType<ConstantType>());
+        }
+        
+        template <typename SparseModelType, typename ConstantType>
+        void SparseInstantiationModelChecker<SparseModelType, ConstantType>::setInstantiationsAreGraphPreserving(bool value) {
+            instantiationsAreGraphPreserving = value;
         }
+        
+        template <typename SparseModelType, typename ConstantType>
+        bool SparseInstantiationModelChecker<SparseModelType, ConstantType>::getInstantiationsAreGraphPreserving() const {
+            return instantiationsAreGraphPreserving;
+        }
+        
+        template class SparseInstantiationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
+        template class SparseInstantiationModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
+        
+        template class SparseInstantiationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber>;
+        template class SparseInstantiationModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, storm::RationalNumber>;
+
     }
 }

src/storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.h

@@ -1,44 +1,42 @@
 #pragma once
 
+#include "storm-pars/utility/parametric.h"
 #include "storm/logic/Formulas.h"
 #include "storm/modelchecker/CheckTask.h"
 #include "storm/modelchecker/results/CheckResult.h"
 #include "storm/modelchecker/hints/ModelCheckerHint.h"
-#include "storm/utility/parametric.h"
 
 namespace storm {
     namespace modelchecker {
-        namespace parametric {
+        
+        /*!
+         * Class to efficiently check a formula on a parametric model with different parameter instantiations
+         */
+        template <typename SparseModelType, typename ConstantType>
+        class SparseInstantiationModelChecker {
+        public:
+            SparseInstantiationModelChecker(SparseModelType const& parametricModel);
+            virtual ~SparseInstantiationModelChecker() = default;
             
-            /*!
-             * Class to efficiently check a formula on a parametric model with different parameter instantiations
-             */
-            template <typename SparseModelType, typename ConstantType>
-            class SparseInstantiationModelChecker {
-            public:
-                SparseInstantiationModelChecker(SparseModelType const& parametricModel);
-                virtual ~SparseInstantiationModelChecker() = default;
-                
-                void specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask);
-                
-                virtual std::unique_ptr<CheckResult> check(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) = 0;
-                
-                // If set, it is assumed that all considered model instantiations have the same underlying graph structure.
-                // This bypasses the graph analysis for the different instantiations.
-                void setInstantiationsAreGraphPreserving(bool value);
-                bool getInstantiationsAreGraphPreserving() const;
-                
-            protected:
-                
-                SparseModelType const& parametricModel;
-                std::unique_ptr<CheckTask<storm::logic::Formula, ConstantType>> currentCheckTask;
-                
-            private:
-                // store the current formula. Note that currentCheckTask only stores a reference to the formula.
-                std::shared_ptr<storm::logic::Formula const> currentFormula;
+            void specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask);
+            
+            virtual std::unique_ptr<CheckResult> check(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) = 0;
+            
+            // If set, it is assumed that all considered model instantiations have the same underlying graph structure.
+            // This bypasses the graph analysis for the different instantiations.
+            void setInstantiationsAreGraphPreserving(bool value);
+            bool getInstantiationsAreGraphPreserving() const;
+            
+        protected:
+            
+            SparseModelType const& parametricModel;
+            std::unique_ptr<CheckTask<storm::logic::Formula, ConstantType>> currentCheckTask;
+            
+        private:
+            // store the current formula. Note that currentCheckTask only stores a reference to the formula.
+            std::shared_ptr<storm::logic::Formula const> currentFormula;
 
-                bool instantiationsAreGraphPreserving;
-            };
-        }
+            bool instantiationsAreGraphPreserving;
+        };
     }
 }

src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp

@@ -1,4 +1,4 @@
-#include "SparseMdpInstantiationModelChecker.h"
+#include "storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.h"
 
 #include "storm/logic/FragmentSpecification.h"
 #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
@@ -13,161 +13,159 @@
 
 namespace storm {
     namespace modelchecker {
-        namespace parametric {
+        
+        template <typename SparseModelType, typename ConstantType>
+        SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>::SparseMdpInstantiationModelChecker(SparseModelType const& parametricModel) : SparseInstantiationModelChecker<SparseModelType, ConstantType>(parametricModel), modelInstantiator(parametricModel) {
+            //Intentionally left empty
+        }
+
+       template <typename SparseModelType, typename ConstantType>
+        std::unique_ptr<CheckResult> SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>::check(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) {
+            STORM_LOG_THROW(this->currentCheckTask, storm::exceptions::InvalidStateException, "Checking has been invoked but no property has been specified before.");
+            auto const& instantiatedModel = modelInstantiator.instantiate(valuation);
+            STORM_LOG_ASSERT(instantiatedModel.getTransitionMatrix().isProbabilistic(), "Instantiated matrix is not probabilistic!");
+            storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>> modelChecker(instantiatedModel);
+
+            // Check if there are some optimizations implemented for the specified property
+            if(this->currentCheckTask->getFormula().isInFragment(storm::logic::reachability())) {
+                return checkReachabilityProbabilityFormula(modelChecker, instantiatedModel);
+            } else if (this->currentCheckTask->getFormula().isInFragment(storm::logic::propositional().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setOperatorAtTopLevelRequired(true).setNestedOperatorsAllowed(false))) {
+                return checkReachabilityRewardFormula(modelChecker, instantiatedModel);
+            } else if (this->currentCheckTask->getFormula().isInFragment(storm::logic::propositional().setProbabilityOperatorsAllowed(true).setBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setOperatorAtTopLevelRequired(true).setNestedOperatorsAllowed(false))) {
+                return checkBoundedUntilFormula(modelChecker);
+            } else {
+                return modelChecker.check(*this->currentCheckTask);
+            }
+        }
+        
+        template <typename SparseModelType, typename ConstantType>
+        std::unique_ptr<CheckResult> SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>::checkReachabilityProbabilityFormula(storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>>& modelChecker, storm::models::sparse::Mdp<ConstantType> const& instantiatedModel) {
+            
+            this->currentCheckTask->setProduceSchedulers(true);
             
-            template <typename SparseModelType, typename ConstantType>
-            SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>::SparseMdpInstantiationModelChecker(SparseModelType const& parametricModel) : SparseInstantiationModelChecker<SparseModelType, ConstantType>(parametricModel), modelInstantiator(parametricModel) {
-                //Intentionally left empty
+            if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) {
+                this->currentCheckTask->setHint(std::make_shared<ExplicitModelCheckerHint<ConstantType>>());
             }
-    
-           template <typename SparseModelType, typename ConstantType>
-            std::unique_ptr<CheckResult> SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>::check(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) {
-                STORM_LOG_THROW(this->currentCheckTask, storm::exceptions::InvalidStateException, "Checking has been invoked but no property has been specified before.");
-                auto const& instantiatedModel = modelInstantiator.instantiate(valuation);
-                STORM_LOG_ASSERT(instantiatedModel.getTransitionMatrix().isProbabilistic(), "Instantiated matrix is not probabilistic!");
-                storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>> modelChecker(instantiatedModel);
-
-                // Check if there are some optimizations implemented for the specified property
-                if(this->currentCheckTask->getFormula().isInFragment(storm::logic::reachability())) {
-                    return checkReachabilityProbabilityFormula(modelChecker, instantiatedModel);
-                } else if (this->currentCheckTask->getFormula().isInFragment(storm::logic::propositional().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setOperatorAtTopLevelRequired(true).setNestedOperatorsAllowed(false))) {
-                    return checkReachabilityRewardFormula(modelChecker, instantiatedModel);
-                } else if (this->currentCheckTask->getFormula().isInFragment(storm::logic::propositional().setProbabilityOperatorsAllowed(true).setBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setOperatorAtTopLevelRequired(true).setNestedOperatorsAllowed(false))) {
-                    return checkBoundedUntilFormula(modelChecker);
-                } else {
-                    return modelChecker.check(*this->currentCheckTask);
-                }
+            ExplicitModelCheckerHint<ConstantType>& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>();
+            std::unique_ptr<CheckResult> result;
+            
+            // Check the formula and store the result as a hint for the next call.
+            // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula
+            if(this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
+                result = modelChecker.check(*this->currentCheckTask);
+                storm::storage::Scheduler<ConstantType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ConstantType>().getScheduler();
+                hint.setResultHint(result->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector());
+                hint.setSchedulerHint(dynamic_cast<storm::storage::Scheduler<ConstantType> const&>(scheduler));
+            } else {
+                auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false);
+                std::unique_ptr<storm::modelchecker::CheckResult> quantitativeResult = modelChecker.computeProbabilities(newCheckTask);
+                result = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
+                storm::storage::Scheduler<ConstantType>& scheduler = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getScheduler();
+                hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()));
+                hint.setSchedulerHint(std::move(dynamic_cast<storm::storage::Scheduler<ConstantType>&>(scheduler)));
             }
             
-            template <typename SparseModelType, typename ConstantType>
-            std::unique_ptr<CheckResult> SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>::checkReachabilityProbabilityFormula(storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>>& modelChecker, storm::models::sparse::Mdp<ConstantType> const& instantiatedModel) {
+            if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) {
+                // Extract the maybe states from the current result.
+                assert(hint.hasResultHint());
+                storm::storage::BitVector maybeStates = ~storm::utility::vector::filter<ConstantType>(hint.getResultHint(),
+                                [] (ConstantType const& value) -> bool { return storm::utility::isZero<ConstantType>(value) || storm::utility::isOne<ConstantType>(value); });
+                hint.setMaybeStates(std::move(maybeStates));
+                hint.setComputeOnlyMaybeStates(true);
                 
-                this->currentCheckTask->setProduceSchedulers(true);
-                
-                if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) {
-                    this->currentCheckTask->setHint(std::make_shared<ExplicitModelCheckerHint<ConstantType>>());
+                // Check if there can be end components within the maybestates
+                if (storm::solver::minimize(this->currentCheckTask->getOptimizationDirection()) ||
+                storm::utility::graph::performProb1A(instantiatedModel.getTransitionMatrix(), instantiatedModel.getTransitionMatrix().getRowGroupIndices(), instantiatedModel.getBackwardTransitions(), hint.getMaybeStates(), ~hint.getMaybeStates()).full()) {
+                    hint.setNoEndComponentsInMaybeStates(true);
                 }
-                ExplicitModelCheckerHint<ConstantType>& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>();
-                std::unique_ptr<CheckResult> result;
-                
-                // Check the formula and store the result as a hint for the next call.
-                // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula
-                if(this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
-                    result = modelChecker.check(*this->currentCheckTask);
-                    storm::storage::Scheduler<ConstantType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ConstantType>().getScheduler();
-                    hint.setResultHint(result->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector());
-                    hint.setSchedulerHint(dynamic_cast<storm::storage::Scheduler<ConstantType> const&>(scheduler));
-                } else {
-                    auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false);
-                    std::unique_ptr<storm::modelchecker::CheckResult> quantitativeResult = modelChecker.computeProbabilities(newCheckTask);
-                    result = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
-                    storm::storage::Scheduler<ConstantType>& scheduler = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getScheduler();
-                    hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()));
-                    hint.setSchedulerHint(std::move(dynamic_cast<storm::storage::Scheduler<ConstantType>&>(scheduler)));
-                }
-                
-                if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) {
-                    // Extract the maybe states from the current result.
-                    assert(hint.hasResultHint());
-                    storm::storage::BitVector maybeStates = ~storm::utility::vector::filter<ConstantType>(hint.getResultHint(),
-                                    [] (ConstantType const& value) -> bool { return storm::utility::isZero<ConstantType>(value) || storm::utility::isOne<ConstantType>(value); });
-                    hint.setMaybeStates(std::move(maybeStates));
-                    hint.setComputeOnlyMaybeStates(true);
-                    
-                    // Check if there can be end components within the maybestates
-                    if (storm::solver::minimize(this->currentCheckTask->getOptimizationDirection()) ||
-                    storm::utility::graph::performProb1A(instantiatedModel.getTransitionMatrix(), instantiatedModel.getTransitionMatrix().getRowGroupIndices(), instantiatedModel.getBackwardTransitions(), hint.getMaybeStates(), ~hint.getMaybeStates()).full()) {
-                        hint.setNoEndComponentsInMaybeStates(true);
-                    }
-                }
-                
-                return result;
             }
             
-            template <typename SparseModelType, typename ConstantType>
-            std::unique_ptr<CheckResult> SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>::checkReachabilityRewardFormula(storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>>& modelChecker, storm::models::sparse::Mdp<ConstantType> const& instantiatedModel) {
-                
-                this->currentCheckTask->setProduceSchedulers(true);
+            return result;
+        }
+        
+        template <typename SparseModelType, typename ConstantType>
+        std::unique_ptr<CheckResult> SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>::checkReachabilityRewardFormula(storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>>& modelChecker, storm::models::sparse::Mdp<ConstantType> const& instantiatedModel) {
+            
+            this->currentCheckTask->setProduceSchedulers(true);
+            
+            if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) {
+                this->currentCheckTask->setHint(std::make_shared<ExplicitModelCheckerHint<ConstantType>>());
+            }
+            ExplicitModelCheckerHint<ConstantType>& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>();
+            std::unique_ptr<CheckResult> result;
+            
+            // Check the formula and store the result as a hint for the next call.
+            // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula
+            if(this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
+                std::unique_ptr<storm::modelchecker::CheckResult> result = modelChecker.check(*this->currentCheckTask);
+                storm::storage::Scheduler<ConstantType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ConstantType>().getScheduler();
+                hint.setResultHint(result->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector());
+                hint.setSchedulerHint(dynamic_cast<storm::storage::Scheduler<ConstantType> const&>(scheduler));
+            } else {
+                auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false);
+                std::unique_ptr<storm::modelchecker::CheckResult> quantitativeResult = modelChecker.computeRewards(this->currentCheckTask->getFormula().asRewardOperatorFormula().getMeasureType(), newCheckTask);
+                result = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
+                storm::storage::Scheduler<ConstantType>& scheduler = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getScheduler();
+                hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()));
+                hint.setSchedulerHint(std::move(dynamic_cast<storm::storage::Scheduler<ConstantType>&>(scheduler)));
+            }
+            
+            if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) {
+                // Extract the maybe states from the current result.
+                assert(hint.hasResultHint());
+                storm::storage::BitVector maybeStates = ~storm::utility::vector::filterInfinity(hint.getResultHint());
+                // We need to exclude the target states from the maybe states.
+                // Note that we can not consider the states with reward zero since a valuation might set a reward to zero
+                std::unique_ptr<CheckResult> subFormulaResult = modelChecker.check(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asEventuallyFormula().getSubformula());
+                maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector());
+                hint.setMaybeStates(std::move(maybeStates));
+                hint.setComputeOnlyMaybeStates(true);
                 
-                if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) {
-                    this->currentCheckTask->setHint(std::make_shared<ExplicitModelCheckerHint<ConstantType>>());
+                // Check if there can be end components within the maybestates
+                if (storm::solver::maximize(this->currentCheckTask->getOptimizationDirection()) ||
+                storm::utility::graph::performProb1A(instantiatedModel.getTransitionMatrix(), instantiatedModel.getTransitionMatrix().getRowGroupIndices(), instantiatedModel.getBackwardTransitions(), hint.getMaybeStates(), ~hint.getMaybeStates()).full()) {
+                    hint.setNoEndComponentsInMaybeStates(true);
                 }
-                ExplicitModelCheckerHint<ConstantType>& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>();
-                std::unique_ptr<CheckResult> result;
-                
-                // Check the formula and store the result as a hint for the next call.
-                // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula
-                if(this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
-                    std::unique_ptr<storm::modelchecker::CheckResult> result = modelChecker.check(*this->currentCheckTask);
-                    storm::storage::Scheduler<ConstantType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ConstantType>().getScheduler();
+            }
+            return result;
+        }
+        
+        template <typename SparseModelType, typename ConstantType>
+        std::unique_ptr<CheckResult> SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>::checkBoundedUntilFormula(storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>>& modelChecker) {
+            
+            if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) {
+                this->currentCheckTask->setHint(std::make_shared<ExplicitModelCheckerHint<ConstantType>>());
+            }
+            std::unique_ptr<CheckResult> result;
+            ExplicitModelCheckerHint<ConstantType>& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>();
+            
+            if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) {
+                // We extract the maybestates from the quantitative result
+                // For qualitative properties, we still need a quantitative result. Hence we perform the check on the subformula
+                if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
+                    result = modelChecker.check(*this->currentCheckTask);
                     hint.setResultHint(result->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector());
-                    hint.setSchedulerHint(dynamic_cast<storm::storage::Scheduler<ConstantType> const&>(scheduler));
                 } else {
                     auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false);
-                    std::unique_ptr<storm::modelchecker::CheckResult> quantitativeResult = modelChecker.computeRewards(this->currentCheckTask->getFormula().asRewardOperatorFormula().getMeasureType(), newCheckTask);
+                    std::unique_ptr<CheckResult> quantitativeResult = modelChecker.computeProbabilities(newCheckTask);
                     result = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
-                    storm::storage::Scheduler<ConstantType>& scheduler = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getScheduler();
                     hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()));
-                    hint.setSchedulerHint(std::move(dynamic_cast<storm::storage::Scheduler<ConstantType>&>(scheduler)));
                 }
-                
-                if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) {
-                    // Extract the maybe states from the current result.
-                    assert(hint.hasResultHint());
-                    storm::storage::BitVector maybeStates = ~storm::utility::vector::filterInfinity(hint.getResultHint());
-                    // We need to exclude the target states from the maybe states.
-                    // Note that we can not consider the states with reward zero since a valuation might set a reward to zero
-                    std::unique_ptr<CheckResult> subFormulaResult = modelChecker.check(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asEventuallyFormula().getSubformula());
-                    maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector());
-                    hint.setMaybeStates(std::move(maybeStates));
-                    hint.setComputeOnlyMaybeStates(true);
-                    
-                    // Check if there can be end components within the maybestates
-                    if (storm::solver::maximize(this->currentCheckTask->getOptimizationDirection()) ||
-                    storm::utility::graph::performProb1A(instantiatedModel.getTransitionMatrix(), instantiatedModel.getTransitionMatrix().getRowGroupIndices(), instantiatedModel.getBackwardTransitions(), hint.getMaybeStates(), ~hint.getMaybeStates()).full()) {
-                        hint.setNoEndComponentsInMaybeStates(true);
-                    }
-                }
-                return result;
-            }
-            
-            template <typename SparseModelType, typename ConstantType>
-            std::unique_ptr<CheckResult> SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>::checkBoundedUntilFormula(storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>>& modelChecker) {
-                 
-                if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) {
-                    this->currentCheckTask->setHint(std::make_shared<ExplicitModelCheckerHint<ConstantType>>());
-                }
-                std::unique_ptr<CheckResult> result;
-                ExplicitModelCheckerHint<ConstantType>& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>();
-                
-                if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) {
-                    // We extract the maybestates from the quantitative result
-                    // For qualitative properties, we still need a quantitative result. Hence we perform the check on the subformula
-                    if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
-                        result = modelChecker.check(*this->currentCheckTask);
-                        hint.setResultHint(result->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector());
-                    } else {
-                        auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false);
-                        std::unique_ptr<CheckResult> quantitativeResult = modelChecker.computeProbabilities(newCheckTask);
-                        result = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
-                        hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()));
-                    }
-                    storm::storage::BitVector maybeStates = storm::utility::vector::filterGreaterZero(hint.getResultHint());
-                    // We need to exclude the target states from the maybe states.
-                    // Note that we can not consider the states with probability one since a state might reach a target state with prob 1 within >0 steps
-                    std::unique_ptr<CheckResult> subFormulaResult = modelChecker.check(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asBoundedUntilFormula().getRightSubformula());
-                    maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector());
-                    hint.setMaybeStates(std::move(maybeStates));
-                    hint.setComputeOnlyMaybeStates(true);
-                } else {
-                    result = modelChecker.check(*this->currentCheckTask);
-                }
-                return result;
+                storm::storage::BitVector maybeStates = storm::utility::vector::filterGreaterZero(hint.getResultHint());
+                // We need to exclude the target states from the maybe states.
+                // Note that we can not consider the states with probability one since a state might reach a target state with prob 1 within >0 steps
+                std::unique_ptr<CheckResult> subFormulaResult = modelChecker.check(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asBoundedUntilFormula().getRightSubformula());
+                maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector());
+                hint.setMaybeStates(std::move(maybeStates));
+                hint.setComputeOnlyMaybeStates(true);
+            } else {
+                result = modelChecker.check(*this->currentCheckTask);
             }
-            
-            template class SparseMdpInstantiationModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
-            template class SparseMdpInstantiationModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, storm::RationalNumber>;
-
+            return result;
         }
+        
+        template class SparseMdpInstantiationModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
+        template class SparseMdpInstantiationModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, storm::RationalNumber>;
+
     }
 }

src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.h

@@ -2,35 +2,33 @@
 
 #include <memory>
 
+#include "storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.h"
+#include "storm-pars/utility/ModelInstantiator.h"
 #include "storm/models/sparse/Mdp.h"
 #include "storm/models/sparse/Dtmc.h"
 #include "storm/models/sparse/StandardRewardModel.h"
-#include "storm/modelchecker/parametric/SparseInstantiationModelChecker.h"
 #include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
-#include "storm/utility/ModelInstantiator.h"
 
 namespace storm {
     namespace modelchecker {
-        namespace parametric {
+        
+        /*!
+         * Class to efficiently check a formula on a parametric model with different parameter instantiations
+         */
+        template <typename SparseModelType, typename ConstantType>
+        class SparseMdpInstantiationModelChecker : public SparseInstantiationModelChecker<SparseModelType, ConstantType> {
+        public:
+            SparseMdpInstantiationModelChecker(SparseModelType const& parametricModel);
             
-            /*!
-             * Class to efficiently check a formula on a parametric model with different parameter instantiations
-             */
-            template <typename SparseModelType, typename ConstantType>
-            class SparseMdpInstantiationModelChecker : public SparseInstantiationModelChecker<SparseModelType, ConstantType> {
-            public:
-                SparseMdpInstantiationModelChecker(SparseModelType const& parametricModel);
-                
-                virtual std::unique_ptr<CheckResult> check(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) override;
+            virtual std::unique_ptr<CheckResult> check(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) override;
 
-            protected:
-                // Optimizations for the different formula types
-                std::unique_ptr<CheckResult> checkReachabilityProbabilityFormula(storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>>& modelChecker, storm::models::sparse::Mdp<ConstantType> const& instantiatedModel);
-                std::unique_ptr<CheckResult> checkReachabilityRewardFormula(storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>>& modelChecker, storm::models::sparse::Mdp<ConstantType> const& instantiatedModel);
-                std::unique_ptr<CheckResult> checkBoundedUntilFormula(storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>>& modelChecker);
-                
-                storm::utility::ModelInstantiator<SparseModelType, storm::models::sparse::Mdp<ConstantType>> modelInstantiator;
-            };
-        }
+        protected:
+            // Optimizations for the different formula types
+            std::unique_ptr<CheckResult> checkReachabilityProbabilityFormula(storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>>& modelChecker, storm::models::sparse::Mdp<ConstantType> const& instantiatedModel);
+            std::unique_ptr<CheckResult> checkReachabilityRewardFormula(storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>>& modelChecker, storm::models::sparse::Mdp<ConstantType> const& instantiatedModel);
+            std::unique_ptr<CheckResult> checkBoundedUntilFormula(storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>>& modelChecker);
+            
+            storm::utility::ModelInstantiator<SparseModelType, storm::models::sparse::Mdp<ConstantType>> modelInstantiator;
+        };
     }
 }

src/storm-pars/modelchecker/region/RegionCheckEngine.cpp

@@ -0,0 +1,25 @@
+#include "storm-pars/modelchecker/region/RegionCheckEngine.h"
+
+#include "storm/utility/macros.h"
+#include "storm/exceptions/NotImplementedException.h"
+
+namespace storm {
+    namespace modelchecker {
+        std::ostream& operator<<(std::ostream& os, RegionCheckEngine const& e) {
+            switch (e) {
+                case RegionCheckEngine::ParameterLifting:
+                    os << "Parameter Lifting";
+                    break;
+                case RegionCheckEngine::ExactParameterLifting:
+                    os << "Exact Parameter Lifting";
+                    break;
+                case RegionCheckEngine::ValidatingParameterLifting:
+                    os << "Validating Parameter Lifting";
+                    break;
+                default:
+                    STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Could not get a string from the region check engine. The case has not been implemented");
+            }
+            return os;
+        }
+    }
+}

src/storm-pars/modelchecker/region/RegionCheckEngine.h

@@ -0,0 +1,19 @@
+#pragma once
+
+#include <ostream>
+
+namespace storm {
+    namespace modelchecker {
+        /*!
+         * The considered engine for region checking
+         */
+        enum class RegionCheckEngine {
+            ParameterLifting, /*!< Parameter lifting approach */
+            ExactParameterLifting, /*!< Parameter lifting approach with exact arithmethics*/
+            ValidatingParameterLifting, /*!< Parameter lifting approach with a) inexact (and fast) computation first and b) exact validation of obtained results second */
+        };
+        
+        std::ostream& operator<<(std::ostream& os, RegionCheckEngine const& regionCheckResult);
+    }
+}
+

src/storm-pars/modelchecker/region/RegionModelChecker.cpp

@@ -1,11 +1,10 @@
 #include <sstream>
 #include <queue>
 
-#include "storm/modelchecker/parametric/RegionChecker.h"
+#include "storm-pars/modelchecker/region/RegionModelChecker.h"
 
 #include "storm/adapters/RationalFunctionAdapter.h"
 
-#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
 
 #include "storm/utility/vector.h"
 #include "storm/models/sparse/StandardRewardModel.h"
@@ -18,164 +17,88 @@
 
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/CoreSettings.h"
-#include "storm/settings/modules/ParametricSettings.h"
 
 
 namespace storm {
     namespace modelchecker {
-        namespace parametric {
 
-            RegionCheckerSettings::RegionCheckerSettings() {
-                this->applyExactValidation = storm::settings::getModule<storm::settings::modules::ParametricSettings>().isExactValidationSet();
-            }
-            
-            template <typename SparseModelType, typename ConstantType, typename ExactConstantType>
-            RegionChecker<SparseModelType, ConstantType, ExactConstantType>::RegionChecker(SparseModelType const& parametricModel) : parametricModel(parametricModel), numOfCorrectedRegions(0) {
-                initializationStopwatch.start();
-                STORM_LOG_THROW(parametricModel.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "Parameter lifting requires models with only one initial state");
-                initializationStopwatch.stop();
+            template <typename ParametricType>
+            RegionModelChecker<ParametricType>::RegionModelChecker() {
+                // Intentionally left empty
             }
         
-            template <typename SparseModelType, typename ConstantType, typename ExactConstantType>
-            RegionCheckerSettings const& RegionChecker<SparseModelType, ConstantType, ExactConstantType>::getSettings() const {
-                return settings;
-            }
-            
-            template <typename SparseModelType, typename ConstantType, typename ExactConstantType>
-            void RegionChecker<SparseModelType, ConstantType, ExactConstantType>::setSettings(RegionCheckerSettings const& newSettings) {
-                settings = newSettings;
-            }
-            
-            template <typename SparseModelType, typename ConstantType, typename ExactConstantType>
-            void RegionChecker<SparseModelType, ConstantType, ExactConstantType>::specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
-                initializationStopwatch.start();
-                STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::NotSupportedException, "Parameter lifting requires a property where only the value in the initial states is relevant.");
-                STORM_LOG_THROW(checkTask.isBoundSet(), storm::exceptions::NotSupportedException, "Parameter lifting requires a bounded property.");
+            template <typename ParametricType>
+            std::unique_ptr<storm::modelchecker::RegionCheckResult<ParametricType>> RegionModelChecker<ParametricType>::analyzeRegions(std::vector<storm::storage::ParameterRegion<ParametricType>> const& regions, bool sampleVerticesOfRegion) {
                 
-                simplifyParametricModel(checkTask);
-                initializeUnderlyingCheckers();
-                currentCheckTask = std::make_unique<storm::modelchecker::CheckTask<storm::logic::Formula, typename SparseModelType::ValueType>>(checkTask.substituteFormula(*currentFormula));
-
-                STORM_LOG_THROW(parameterLiftingChecker->canHandle(*currentCheckTask) &&
-                                (!exactParameterLiftingChecker || exactParameterLiftingChecker->canHandle(*currentCheckTask)),
-                                storm::exceptions::NotSupportedException, "Parameter lifting is not supported for this property.");
-                if (exactParameterLiftingChecker) {
-                    exactParameterLiftingChecker->specifyFormula(*currentCheckTask);
-                }
-                parameterLiftingChecker->specifyFormula(*currentCheckTask);
-                instantiationChecker->specifyFormula(*currentCheckTask);
-                initializationStopwatch.stop();
-            }
-    
-            template <typename SparseModelType, typename ConstantType, typename ExactConstantType>
-            RegionResult RegionChecker<SparseModelType, ConstantType, ExactConstantType>::analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResult const& initialResult, bool sampleVerticesOfRegion) {
-                      RegionResult result = initialResult;
-
-                // Check if we need to check the formula on one point to decide whether to show AllSat or AllViolated
-                instantiationCheckerStopwatch.start();
-                if (result == RegionCheckResult::Unknown) {
-                     result = instantiationChecker->check(region.getCenterPoint())->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()] ? RegionCheckResult::CenterSat : RegionCheckResult::CenterViolated;
-                }
-                instantiationCheckerStopwatch.stop();
+                std::vector<std::pair<storm::storage::ParameterRegion<ParametricType>, storm::modelchecker::RegionResult>> result;
                 
-                // try to prove AllSat or AllViolated, depending on the obtained result
-                parameterLiftingCheckerStopwatch.start();
-                if(result == RegionCheckResult::ExistsSat || result == RegionCheckResult::CenterSat) {
-                    // show AllSat:
-                    storm::solver::OptimizationDirection parameterOptimizationDirection = isLowerBound(this->currentCheckTask->getBound().comparisonType) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize;
-                    if(parameterLiftingChecker->check(region, parameterOptimizationDirection)->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
-                        result = RegionCheckResult::AllSat;
-                    } else if (sampleVerticesOfRegion) {
-                        parameterLiftingCheckerStopwatch.stop(); instantiationCheckerStopwatch.start();
-                        // Check if there is a point in the region for which the property is violated
-                        auto vertices = region.getVerticesOfRegion(region.getVariables());
-                        for (auto const& v : vertices) {
-                            if (!instantiationChecker->check(v)->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
-                                result = RegionCheckResult::ExistsBoth;
-                            }
-                        }
-                        instantiationCheckerStopwatch.stop(); parameterLiftingCheckerStopwatch.start();
-                    }
-                } else if (result == RegionCheckResult::ExistsViolated || result == RegionCheckResult::CenterViolated) {
-                    // show AllViolated:
-                    storm::solver::OptimizationDirection parameterOptimizationDirection = isLowerBound(this->currentCheckTask->getBound().comparisonType) ? storm::solver::OptimizationDirection::Maximize : storm::solver::OptimizationDirection::Minimize;
-                    if(!parameterLiftingChecker->check(region, parameterOptimizationDirection)->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
-                        result = RegionCheckResult::AllViolated;
-                    } else if (sampleVerticesOfRegion) {
-                        parameterLiftingCheckerStopwatch.stop(); instantiationCheckerStopwatch.start();
-                        // Check if there is a point in the region for which the property is satisfied
-                        auto vertices = region.getVerticesOfRegion(region.getVariables());
-                        for (auto const& v : vertices) {
-                            if (instantiationChecker->check(v)->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
-                                result = RegionCheckResult::ExistsBoth;
-                            }
-                        }
-                        instantiationCheckerStopwatch.stop(); parameterLiftingCheckerStopwatch.start();
-                    }
-                } else {
-                    STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "When analyzing a region, an invalid initial result was given: " << initialResult);
+                for (auto const& region : regions) {
+                    storm::modelchecker::RegionResult regionRes = analyzeRegion(region, storm::modelchecker::RegionResult::Unknown, sampleVerticesOfRegion);
+                    result.emplace_back(region, regionRes);
                 }
-                parameterLiftingCheckerStopwatch.stop();
-                return result;
+                
+                return std::make_unique<storm::modelchecker::RegionCheckResult<ParametricType>>(std::move(result));
             }
-            
-            template <typename SparseModelType, typename ConstantType, typename ExactConstantType>
-            RegionResult RegionChecker<SparseModelType, ConstantType, ExactConstantType>::analyzeRegionExactValidation(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResult const& initialResult) {
+
+            /*
+#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
+            template <typename ParametricType, typename ConstantType, typename ExactConstantType>
+            RegionResult RegionModelChecker<ParametricType, ConstantType, ExactConstantType>::analyzeRegionExactValidation(storm::storage::ParameterRegion<typename ParametricType::ValueType> const& region, RegionResult const& initialResult) {
                 RegionResult numericResult = analyzeRegion(region, initialResult, false);
                 parameterLiftingCheckerStopwatch.start();
-                if (numericResult == RegionCheckResult::AllSat || numericResult == RegionCheckResult::AllViolated) {
+                if (numericResult == RegionResult::AllSat || numericResult == RegionResult::AllViolated) {
                     applyHintsToExactChecker();
                 }
-                if (numericResult == RegionCheckResult::AllSat) {
+                if (numericResult == RegionResult::AllSat) {
                     if(!exactParameterLiftingChecker->check(region, this->currentCheckTask->getOptimizationDirection())->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
                         // Numerical result is wrong; Check whether the region is AllViolated!
                         STORM_LOG_INFO("Numerical result was wrong for one region... Applying exact methods to obtain the actual result...");
                         ++numOfCorrectedRegions;
                         if(!exactParameterLiftingChecker->check(region, storm::solver::invert(this->currentCheckTask->getOptimizationDirection()))->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
                             parameterLiftingCheckerStopwatch.stop();
-                            return RegionCheckResult::AllViolated;
+                            return RegionResult::AllViolated;
                         } else {
                             parameterLiftingCheckerStopwatch.stop();
-                            return RegionCheckResult::Unknown;
+                            return RegionResult::Unknown;
                         }
                     }
-                } else if (numericResult == RegionCheckResult::AllViolated) {
+                } else if (numericResult == RegionResult::AllViolated) {
                     if(exactParameterLiftingChecker->check(region, storm::solver::invert(this->currentCheckTask->getOptimizationDirection()))->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
                         // Numerical result is wrong; Check whether the region is AllSat!
                         STORM_LOG_INFO("Numerical result was wrong for one region... Applying exact methods to obtain the actual result...");
                         ++numOfCorrectedRegions;
                         if(exactParameterLiftingChecker->check(region, this->currentCheckTask->getOptimizationDirection())->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
                             parameterLiftingCheckerStopwatch.stop();
-                            return RegionCheckResult::AllSat;
+                            return RegionResult::AllSat;
                         } else {
                             parameterLiftingCheckerStopwatch.stop();
-                            return RegionCheckResult::Unknown;
+                            return RegionResult::Unknown;
                         }
                     }
                 }
                 parameterLiftingCheckerStopwatch.stop();
                 return numericResult;
             }
-
+*/
     
-            template <typename SparseModelType, typename ConstantType, typename ExactConstantType>
-            std::vector<std::pair<storm::storage::ParameterRegion<typename SparseModelType::ValueType>, RegionResult>> RegionChecker<SparseModelType, ConstantType, ExactConstantType>::performRegionRefinement(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, CoefficientType const& threshold) {
+            template <typename ParametricType>
+            std::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ParametricType>> RegionModelChecker<ParametricType>::performRegionRefinement(storm::storage::ParameterRegion<ParametricType> const& region, ParametricType const& threshold) {
                 STORM_LOG_INFO("Applying refinement on region: " << region.toString(true) << " .");
                 
+                auto thresholdAsCoefficient = storm::utility::convertNumber<CoefficientType>(threshold);
                 auto areaOfParameterSpace = region.area();
                 auto fractionOfUndiscoveredArea = storm::utility::one<CoefficientType>();
                 auto fractionOfAllSatArea = storm::utility::zero<CoefficientType>();
                 auto fractionOfAllViolatedArea = storm::utility::zero<CoefficientType>();
                 
-                std::queue<std::pair<storm::storage::ParameterRegion<typename SparseModelType::ValueType>, RegionResult>> unprocessedRegions;
-                std::vector<std::pair<storm::storage::ParameterRegion<typename SparseModelType::ValueType>, RegionResult>> result;
-                unprocessedRegions.emplace(region, RegionCheckResult::Unknown);
+                std::queue<std::pair<storm::storage::ParameterRegion<ParametricType>, RegionResult>> unprocessedRegions;
+                std::vector<std::pair<storm::storage::ParameterRegion<ParametricType>, RegionResult>> result;
+                unprocessedRegions.emplace(region, RegionResult::Unknown);
                 uint_fast64_t numOfAnalyzedRegions = 0;
-                numOfCorrectedRegions = 0;
                 CoefficientType displayedProgress = storm::utility::zero<CoefficientType>();
                 if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {
                     STORM_PRINT_AND_LOG("Progress (solved fraction) :" << std::endl <<  "0% [");
-                    while (displayedProgress < storm::utility::one<CoefficientType>() - threshold) {
+                    while (displayedProgress < storm::utility::one<CoefficientType>() - thresholdAsCoefficient) {
                         STORM_PRINT_AND_LOG(" ");
                         displayedProgress += storm::utility::convertNumber<CoefficientType>(0.01);
                     }
@@ -187,33 +110,29 @@ namespace storm {
                     displayedProgress = storm::utility::zero<CoefficientType>();
                 }
 
-                while (fractionOfUndiscoveredArea > threshold) {
+                while (fractionOfUndiscoveredArea > thresholdAsCoefficient) {
                     STORM_LOG_THROW(!unprocessedRegions.empty(), storm::exceptions::InvalidStateException, "Threshold for undiscovered area not reached but no unprocessed regions left.");
                     STORM_LOG_INFO("Analyzing region #" << numOfAnalyzedRegions << " (" << storm::utility::convertNumber<double>(fractionOfUndiscoveredArea) * 100 << "% still unknown)");
                     auto& currentRegion = unprocessedRegions.front().first;
                     auto& res = unprocessedRegions.front().second;
-                    if (settings.applyExactValidation) {
-                        res = analyzeRegionExactValidation(currentRegion, res);
-                    } else {
-                        res = analyzeRegion(currentRegion, res, false);
-                    }
+                    res = analyzeRegion(currentRegion, res, false);
                     switch (res) {
-                        case RegionCheckResult::AllSat:
+                        case RegionResult::AllSat:
                             fractionOfUndiscoveredArea -= currentRegion.area() / areaOfParameterSpace;
                             fractionOfAllSatArea += currentRegion.area() / areaOfParameterSpace;
                             result.push_back(std::move(unprocessedRegions.front()));
                             break;
-                        case RegionCheckResult::AllViolated:
+                        case RegionResult::AllViolated:
                             fractionOfUndiscoveredArea -= currentRegion.area() / areaOfParameterSpace;
                             fractionOfAllViolatedArea += currentRegion.area() / areaOfParameterSpace;
                             result.push_back(std::move(unprocessedRegions.front()));
                             break;
                         default:
-                            std::vector<storm::storage::ParameterRegion<typename SparseModelType::ValueType>> newRegions;
+                            std::vector<storm::storage::ParameterRegion<ParametricType>> newRegions;
                             currentRegion.split(currentRegion.getCenterPoint(), newRegions);
-                            RegionResult initResForNewRegions = (res == RegionCheckResult::CenterSat) ? RegionCheckResult::ExistsSat :
-                                                                     ((res == RegionCheckResult::CenterViolated) ? RegionCheckResult::ExistsViolated :
-                                                                      RegionCheckResult::Unknown);
+                            RegionResult initResForNewRegions = (res == RegionResult::CenterSat) ? RegionResult::ExistsSat :
+                                                                     ((res == RegionResult::CenterViolated) ? RegionResult::ExistsViolated :
+                                                                      RegionResult::Unknown);
                             for(auto& newRegion : newRegions) {
                                 unprocessedRegions.emplace(std::move(newRegion), initResForNewRegions);
                             }
@@ -236,91 +155,17 @@ namespace storm {
                     }
                     STORM_PRINT_AND_LOG("]" << std::endl);
                     
-                    STORM_PRINT_AND_LOG("Parameter Lifting Statistics:" << std::endl);
+                    STORM_PRINT_AND_LOG("Region Refinement Statistics:" << std::endl);
                     STORM_PRINT_AND_LOG("    Analyzed a total of " << numOfAnalyzedRegions << " regions." << std::endl);
-                    if (settings.applyExactValidation) {
-                        STORM_PRINT_AND_LOG("    Exact validation corrected " << numOfCorrectedRegions << " regions." << std::endl);
-                    }
-                    STORM_PRINT_AND_LOG("    Initialization took " << initializationStopwatch << " seconds." << std::endl);
-                    STORM_PRINT_AND_LOG("    Checking sampled models took " << instantiationCheckerStopwatch << " seconds." << std::endl);
-                    STORM_PRINT_AND_LOG("    Checking lifted models took " << parameterLiftingCheckerStopwatch << " seconds." << std::endl);
-                }
-                return result;
-            }
-    
-            template <typename SparseModelType, typename ConstantType, typename ExactConstantType>
-            SparseModelType const& RegionChecker<SparseModelType, ConstantType, ExactConstantType>::getConsideredParametricModel() const {
-                if (simplifiedModel) {
-                    return *simplifiedModel;
-                } else {
-                    return parametricModel;
                 }
-            }
-    
-            template <typename SparseModelType, typename ConstantType, typename ExactConstantType>
-            std::string RegionChecker<SparseModelType, ConstantType, ExactConstantType>::visualizeResult(std::vector<std::pair<storm::storage::ParameterRegion<typename SparseModelType::ValueType>, RegionResult>> const& result, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& parameterSpace, typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::VariableType const& x, typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::VariableType const& y) {
-                
-                std::stringstream stream;
                 
-                uint_fast64_t const sizeX = 128;
-                uint_fast64_t const sizeY = 64;
-                
-                stream << "Parameter lifting result (visualization):" << std::endl;
-                stream << " \t x-axis: " << x << "  \t y-axis: " << y << "  \t S=safe, [ ]=unsafe, -=ambiguous " << std::endl;
-                for (uint_fast64_t i = 0; i < sizeX+2; ++i) stream << "#"; stream << std::endl;
-                
-                CoefficientType deltaX = (parameterSpace.getUpperBoundary(x) - parameterSpace.getLowerBoundary(x)) / storm::utility::convertNumber<CoefficientType>(sizeX);
-                CoefficientType deltaY = (parameterSpace.getUpperBoundary(y) - parameterSpace.getLowerBoundary(y)) / storm::utility::convertNumber<CoefficientType>(sizeY);
-                CoefficientType printedRegionArea = deltaX * deltaY;
-                for (CoefficientType yUpper = parameterSpace.getUpperBoundary(y); yUpper != parameterSpace.getLowerBoundary(y); yUpper -= deltaY) {
-                    CoefficientType yLower = yUpper - deltaY;
-                    stream << "#";
-                    for (CoefficientType xLower = parameterSpace.getLowerBoundary(x); xLower != parameterSpace.getUpperBoundary(x); xLower += deltaX) {
-                        CoefficientType xUpper = xLower + deltaX;
-                        bool currRegionSafe = false;
-                        bool currRegionUnSafe = false;
-                        bool currRegionComplete = false;
-                        CoefficientType coveredArea = storm::utility::zero<CoefficientType>();
-                        for (auto const& r : result) {
-                            CoefficientType interesctionSizeY = std::min(yUpper, r.first.getUpperBoundary(y)) - std::max(yLower, r.first.getLowerBoundary(y));
-                            interesctionSizeY = std::max(interesctionSizeY, storm::utility::zero<CoefficientType>());
-                            CoefficientType interesctionSizeX = std::min(xUpper, r.first.getUpperBoundary(x)) - std::max(xLower, r.first.getLowerBoundary(x));
-                            interesctionSizeX = std::max(interesctionSizeX, storm::utility::zero<CoefficientType>());
-                            CoefficientType instersectionArea =  interesctionSizeY * interesctionSizeX;
-                            if(!storm::utility::isZero(instersectionArea)) {
-                                currRegionSafe = currRegionSafe || r.second == RegionCheckResult::AllSat;
-                                currRegionUnSafe = currRegionUnSafe || r.second == RegionCheckResult::AllViolated;
-                                coveredArea += instersectionArea;
-                                if(currRegionSafe && currRegionUnSafe) {
-                                    break;
-                                }
-                                if(coveredArea == printedRegionArea) {
-                                    currRegionComplete = true;
-                                    break;
-                                }
-                            }
-                        }
-                        if (currRegionComplete && currRegionSafe && !currRegionUnSafe) {
-                            stream << "S";
-                        } else if (currRegionComplete && currRegionUnSafe && !currRegionSafe) {
-                            stream << " ";
-                        } else {
-                            stream << "-";
-                        }
-                    }
-                    stream << "#" << std::endl;
-                }
-                for (uint_fast64_t i = 0; i < sizeX+2; ++i) stream << "#"; stream << std::endl;
-                return stream.str();
+                auto regionCopyForResult = region;
+                return std::make_unique<storm::modelchecker::RegionRefinementCheckResult<ParametricType>>(std::move(result), std::move(regionCopyForResult));
             }
-        
+    
 #ifdef STORM_HAVE_CARL
-            template class RegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double, storm::RationalNumber>;
-            template class RegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double, storm::RationalNumber>;
-            template class RegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber>;
-            template class RegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, storm::RationalNumber>;
+            template class RegionModelChecker<storm::RationalFunction>;
 #endif
-        } // namespace parametric
     } //namespace modelchecker
 } //namespace storm
 

src/storm-pars/modelchecker/region/RegionModelChecker.h

@@ -2,84 +2,49 @@
 
 #include <memory>
 
-#include "storm/modelchecker/parametric/RegionCheckResult.h"
-#include "storm/modelchecker/parametric/SparseInstantiationModelChecker.h"
-#include "storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h"
+#include "storm-pars/modelchecker/results/RegionCheckResult.h"
+#include "storm-pars/modelchecker/results/RegionRefinementCheckResult.h"
+#include "storm-pars/modelchecker/region/RegionResult.h"
+#include "storm-pars/storage/ParameterRegion.h"
+
 #include "storm/modelchecker/CheckTask.h"
-#include "storm/storage/ParameterRegion.h"
-#include "storm/utility/Stopwatch.h"
-#include "storm/utility/NumberTraits.h"
 
 namespace storm {
     namespace modelchecker{
-        namespace parametric{
+        
+        template<typename ParametricType>
+        class RegionModelChecker {
+        public:
             
-            struct RegionCheckerSettings {
-                RegionCheckerSettings();
-                
-                bool applyExactValidation;
-            };
-
-            template<typename SparseModelType, typename ConstantType, typename ExactConstantType = ConstantType>
-            class RegionChecker {
-                static_assert(storm::NumberTraits<ExactConstantType>::IsExact, "Specified type for exact computations is not exact.");
+            typedef typename storm::storage::ParameterRegion<ParametricType>::CoefficientType CoefficientType;
 
-            public:
-                
-                typedef typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::CoefficientType CoefficientType;
+            RegionModelChecker();
+            virtual ~RegionModelChecker() = default;
+            
+            virtual bool canHandle(CheckTask<storm::logic::Formula, ParametricType> const& checkTask) const = 0;
 
-                RegionChecker(SparseModelType const& parametricModel);
-                virtual ~RegionChecker() = default;
-                
-                RegionCheckerSettings const& getSettings() const;
-                void setSettings(RegionCheckerSettings const& newSettings);
-                
-                void specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask);
-                
-                /*!
-                 * Analyzes the given region by means of parameter lifting.
-                 * We first check whether there is one point in the region for which the property is satisfied/violated.
-                 * If the given initialResults already indicates that there is such a point, this step is skipped.
-                 * Then, we check whether ALL points in the region violate/satisfy the property
-                 *
-                 */
-                RegionResult analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResult const& initialResult = RegionCheckResult::Unknown, bool sampleVerticesOfRegion = false);
-                /*!
-                 * Similar to analyze region but additionaly invokes exact parameter lifting to validate results AllSat or AllViolated
-                 */
-                RegionResult analyzeRegionExactValidation(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResult const& initialResult = RegionCheckResult::Unknown);
-                
-                /*!
-                 * Iteratively refines the region until parameter lifting yields a conclusive result (AllSat or AllViolated).
-                 * The refinement stops as soon as the fraction of the area of the subregions with inconclusive result is less then the given threshold
-                 */
-                std::vector<std::pair<storm::storage::ParameterRegion<typename SparseModelType::ValueType>, RegionResult>> performRegionRefinement(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, CoefficientType const& threshold);
-                
-                static std::string visualizeResult(std::vector<std::pair<storm::storage::ParameterRegion<typename SparseModelType::ValueType>, RegionResult>> const& result, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& parameterSpace, typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::VariableType const& x, typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::VariableType const& y);
-                
-            protected:
-                SparseModelType const& getConsideredParametricModel() const;
-                
-                virtual void initializeUnderlyingCheckers() = 0;
-                virtual void simplifyParametricModel(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) = 0;
-                virtual void applyHintsToExactChecker() = 0;
-                
-                SparseModelType const& parametricModel;
-                RegionCheckerSettings settings;
-                std::unique_ptr<CheckTask<storm::logic::Formula, typename SparseModelType::ValueType>> currentCheckTask;
-                std::shared_ptr<storm::logic::Formula const> currentFormula;
-                std::shared_ptr<SparseModelType> simplifiedModel;
-                
+            virtual void specifyFormula(CheckTask<storm::logic::Formula, ParametricType> const& checkTask) = 0;
+            
+            /*!
+             * Analyzes the given region.
+             * An initial region result can be given to simplify the analysis (e.g. if the initial result is ExistsSat, we do not check for AllViolated).
+             * If supported by this model checker, it is possible to sample the vertices of the region whenever AllSat/AllViolated could not be shown.
+             */
+            virtual RegionResult analyzeRegion(storm::storage::ParameterRegion<ParametricType> const& region, RegionResult const& initialResult = RegionResult::Unknown, bool sampleVerticesOfRegion = false) = 0;
+            
+             /*!
+             * Analyzes the given regions.
+             * If supported by this model checker, it is possible to sample the vertices of the regions whenever AllSat/AllViolated could not be shown.
+             */
+            std::unique_ptr<storm::modelchecker::RegionCheckResult<ParametricType>> analyzeRegions(std::vector<storm::storage::ParameterRegion<ParametricType>> const& regions, bool sampleVerticesOfRegion = false) ;
+            
+            /*!
+             * Iteratively refines the region until the region analysis yields a conclusive result (AllSat or AllViolated).
+             * The refinement stops as soon as the fraction of the area of the subregions with inconclusive result is less then the given threshold
+             */
+            std::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ParametricType>> performRegionRefinement(storm::storage::ParameterRegion<ParametricType> const& region, ParametricType const& threshold);
+            
+        };
 
-                std::unique_ptr<SparseParameterLiftingModelChecker<SparseModelType, ConstantType>> parameterLiftingChecker;
-                std::unique_ptr<SparseParameterLiftingModelChecker<SparseModelType, ExactConstantType>> exactParameterLiftingChecker;
-                std::unique_ptr<SparseInstantiationModelChecker<SparseModelType, ConstantType>> instantiationChecker;
-                
-                // Information for statistics
-                mutable storm::utility::Stopwatch initializationStopwatch, instantiationCheckerStopwatch, parameterLiftingCheckerStopwatch;
-                mutable uint_fast64_t numOfCorrectedRegions;
-            };
-    
-        } //namespace parametric
     } //namespace modelchecker
 } //namespace storm

src/storm-pars/modelchecker/region/RegionResult.cpp

@@ -1,42 +1,40 @@
-#include "storm/modelchecker/parametric/RegionCheckResult.h"
+#include "storm-pars/modelchecker/region/RegionResult.h"
 
 #include "storm/utility/macros.h"
 #include "storm/exceptions/NotImplementedException.h"
 
 namespace storm {
     namespace modelchecker {
-        namespace parametric {
-            std::ostream& operator<<(std::ostream& os, RegionCheckResult const& regionCheckResult) {
-                switch (regionCheckResult) {
-                    case RegionCheckResult::Unknown:
-                        os << "Unknown";
-                        break;
-                    case RegionCheckResult::ExistsSat:
-                        os << "ExistsSat";
-                        break;
-                    case RegionCheckResult::ExistsViolated:
-                        os << "ExistsViolated";
-                        break;
-                    case RegionCheckResult::CenterSat:
-                        os << "CenterSat";
-                        break;
-                    case RegionCheckResult::CenterViolated:
-                        os << "CenterViolated";
-                        break;
-                    case RegionCheckResult::ExistsBoth:
-                        os << "ExistsBoth";
-                        break;
-                    case RegionCheckResult::AllSat:
-                        os << "AllSat";
-                        break;
-                    case RegionCheckResult::AllViolated:
-                        os << "AllViolated";
-                        break;
-                    default:
-                        STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Could not get a string from the region check result. The case has not been implemented");
-                }
-                return os;
+        std::ostream& operator<<(std::ostream& os, RegionResult const& regionResult) {
+            switch (regionResult) {
+                case RegionResult::Unknown:
+                    os << "Unknown";
+                    break;
+                case RegionResult::ExistsSat:
+                    os << "ExistsSat";
+                    break;
+                case RegionResult::ExistsViolated:
+                    os << "ExistsViolated";
+                    break;
+                case RegionResult::CenterSat:
+                    os << "CenterSat";
+                    break;
+                case RegionResult::CenterViolated:
+                    os << "CenterViolated";
+                    break;
+                case RegionResult::ExistsBoth:
+                    os << "ExistsBoth";
+                    break;
+                case RegionResult::AllSat:
+                    os << "AllSat";
+                    break;
+                case RegionResult::AllViolated:
+                    os << "AllViolated";
+                    break;
+                default:
+                    STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Could not get a string from the region check result. The case has not been implemented");
             }
+            return os;
         }
     }
 }

src/storm-pars/modelchecker/region/RegionResult.h

@@ -4,23 +4,21 @@
 
 namespace storm {
     namespace modelchecker {
-        namespace parametric {
-            /*!
-             * The results for a single Parameter region
-             */
-            enum class RegionCheckResult { 
-                Unknown, /*!< the result is unknown */
-                ExistsSat, /*!< the formula is satisfied for at least one parameter evaluation that lies in the given region */
-                ExistsViolated, /*!< the formula is violated for at least one parameter evaluation that lies in the given region */
-                CenterSat, /*!< the formula is satisfied for the parameter Valuation that corresponds to the center point of the region */
-                CenterViolated, /*!< the formula is violated for the parameter Valuation that corresponds to the center point of the region */
-                ExistsBoth, /*!< the formula is satisfied for some parameters but also violated for others */
-                AllSat, /*!< the formula is satisfied for all parameters in the given region */
-                AllViolated /*!< the formula is violated for all parameters in the given region */
-            };
-            
-            std::ostream& operator<<(std::ostream& os, RegionCheckResult const& regionCheckResult);
-        }
+        /*!
+         * The results for a single Parameter Region
+         */
+        enum class RegionResult {
+            Unknown, /*!< the result is unknown */
+            ExistsSat, /*!< the formula is satisfied for at least one parameter evaluation that lies in the given region */
+            ExistsViolated, /*!< the formula is violated for at least one parameter evaluation that lies in the given region */
+            CenterSat, /*!< the formula is satisfied for the parameter Valuation that corresponds to the center point of the region */
+            CenterViolated, /*!< the formula is violated for the parameter Valuation that corresponds to the center point of the region */
+            ExistsBoth, /*!< the formula is satisfied for some parameters but also violated for others */
+            AllSat, /*!< the formula is satisfied for all parameters in the given region */
+            AllViolated /*!< the formula is violated for all parameters in the given region */
+        };
+        
+        std::ostream& operator<<(std::ostream& os, RegionResult const& regionCheckResult);
     }
 }
 

src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp

@@ -1,4 +1,5 @@
-#include "storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h"
+#include "storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h"
+#include "storm-pars/utility/parameterlifting.h"
 
 #include "storm/adapters/RationalFunctionAdapter.h"
 #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
@@ -17,265 +18,278 @@
 
 namespace storm {
     namespace modelchecker {
-        namespace parametric {
-            
-            template <typename SparseModelType, typename ConstantType>
-            SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseDtmcParameterLiftingModelChecker(SparseModelType const& parametricModel) : SparseParameterLiftingModelChecker<SparseModelType, ConstantType>(parametricModel), solverFactory(std::make_unique<storm::solver::GeneralMinMaxLinearEquationSolverFactory<ConstantType>>()) {
+        
+        template <typename SparseModelType, typename ConstantType>
+        SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseDtmcParameterLiftingModelChecker(SparseModelType const& parametricModel) : SparseParameterLiftingModelChecker<SparseModelType, ConstantType>(parametricModel), solverFactory(std::make_unique<storm::solver::GeneralMinMaxLinearEquationSolverFactory<ConstantType>>()) {
+        }
+        
+        template <typename SparseModelType, typename ConstantType>
+        SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseDtmcParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>>&& solverFactory) : SparseParameterLiftingModelChecker<SparseModelType, ConstantType>(parametricModel), solverFactory(std::move(solverFactory)) {
+        }
+        
+        template <typename SparseModelType, typename ConstantType>
+        bool SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const {
+            bool result = checkTask.getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(true).setCumulativeRewardFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true));
+            if (result) {
+                storm::utility::parameterlifting::validateParameterLiftingSound(this->parametricModel, checkTask.getFormula());
+                STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(this->parametricModel, checkTask.getFormula()), "Could not validate whether parameter lifting is applicable. Please validate manually...");
             }
+            return result;
+        }
+        
+        template <typename SparseModelType, typename ConstantType>
+        void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyBoundedUntilFormula(CheckTask<storm::logic::BoundedUntilFormula, ConstantType> const& checkTask) {
             
-            template <typename SparseModelType, typename ConstantType>
-            SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseDtmcParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>>&& solverFactory) : SparseParameterLiftingModelChecker<SparseModelType, ConstantType>(parametricModel), solverFactory(std::move(solverFactory)) {
+            // get the step bound
+            STORM_LOG_THROW(!checkTask.getFormula().hasLowerBound(), storm::exceptions::NotSupportedException, "Lower step bounds are not supported.");
+            STORM_LOG_THROW(checkTask.getFormula().hasUpperBound(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with an upper bound.");
+            STORM_LOG_THROW(checkTask.getFormula().isStepBounded(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with step bounds.");
+            stepBound = checkTask.getFormula().getUpperBound().evaluateAsInt();
+            STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive.");
+            if (checkTask.getFormula().isUpperBoundStrict()) {
+                STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Expected a strict upper step bound that is greater than zero.");
+                --(*stepBound);
             }
+            STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive.");
+
+            // get the results for the subformulas
+            storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(this->parametricModel);
+            STORM_LOG_THROW(propositionalChecker.canHandle(checkTask.getFormula().getLeftSubformula()) && propositionalChecker.canHandle(checkTask.getFormula().getRightSubformula()), storm::exceptions::NotSupportedException, "Parameter lifting with non-propositional subformulas is not supported");
+            storm::storage::BitVector phiStates = std::move(propositionalChecker.check(checkTask.getFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
+            storm::storage::BitVector psiStates = std::move(propositionalChecker.check(checkTask.getFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
             
-            template <typename SparseModelType, typename ConstantType>
-            bool SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const {
-                return checkTask.getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(true).setCumulativeRewardFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true));
-            }
+            // get the maybeStates
+            maybeStates = storm::utility::graph::performProbGreater0(this->parametricModel.getBackwardTransitions(), phiStates, psiStates, true, *stepBound);
+            maybeStates &= ~psiStates;
             
-            template <typename SparseModelType, typename ConstantType>
-            void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyBoundedUntilFormula(CheckTask<storm::logic::BoundedUntilFormula, ConstantType> const& checkTask) {
-                
-                // get the step bound
-                STORM_LOG_THROW(!checkTask.getFormula().hasLowerBound(), storm::exceptions::NotSupportedException, "Lower step bounds are not supported.");
-                STORM_LOG_THROW(checkTask.getFormula().hasUpperBound(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with an upper bound.");
-                STORM_LOG_THROW(checkTask.getFormula().isStepBounded(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with step bounds.");
-                stepBound = checkTask.getFormula().getUpperBound().evaluateAsInt();
-                STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive.");
-                if (checkTask.getFormula().isUpperBoundStrict()) {
-                    STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Expected a strict upper step bound that is greater than zero.");
-                    --(*stepBound);
-                }
-                STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive.");
-
-                // get the results for the subformulas
-                storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(this->parametricModel);
-                STORM_LOG_THROW(propositionalChecker.canHandle(checkTask.getFormula().getLeftSubformula()) && propositionalChecker.canHandle(checkTask.getFormula().getRightSubformula()), storm::exceptions::NotSupportedException, "Parameter lifting with non-propositional subformulas is not supported");
-                storm::storage::BitVector phiStates = std::move(propositionalChecker.check(checkTask.getFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
-                storm::storage::BitVector psiStates = std::move(propositionalChecker.check(checkTask.getFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
-                
-                // get the maybeStates
-                maybeStates = storm::utility::graph::performProbGreater0(this->parametricModel.getBackwardTransitions(), phiStates, psiStates, true, *stepBound);
-                maybeStates &= ~psiStates;
-                
-                // set the result for all non-maybe states
-                resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel.getNumberOfStates(), storm::utility::zero<ConstantType>());
-                storm::utility::vector::setVectorValues(resultsForNonMaybeStates, psiStates, storm::utility::one<ConstantType>());
-                
-                // if there are maybestates, create the parameterLifter
-                if (!maybeStates.empty()) {
-                    // Create the vector of one-step probabilities to go to target states.
-                    std::vector<typename SparseModelType::ValueType> b = this->parametricModel.getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), psiStates);
-                    
-                    parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel.getTransitionMatrix(), b, maybeStates, maybeStates);
-                }
-                
-                // We know some bounds for the results so set them
-                lowerResultBound = storm::utility::zero<ConstantType>();
-                upperResultBound = storm::utility::one<ConstantType>();
-            }
-    
-            template <typename SparseModelType, typename ConstantType>
-            void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyUntilFormula(CheckTask<storm::logic::UntilFormula, ConstantType> const& checkTask) {
-                
-                // get the results for the subformulas
-                storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(this->parametricModel);
-                STORM_LOG_THROW(propositionalChecker.canHandle(checkTask.getFormula().getLeftSubformula()) && propositionalChecker.canHandle(checkTask.getFormula().getRightSubformula()), storm::exceptions::NotSupportedException, "Parameter lifting with non-propositional subformulas is not supported");
-                storm::storage::BitVector phiStates = std::move(propositionalChecker.check(checkTask.getFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
-                storm::storage::BitVector psiStates = std::move(propositionalChecker.check(checkTask.getFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
-                
-                // get the maybeStates
-                std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(this->parametricModel.getBackwardTransitions(), phiStates, psiStates);
-                maybeStates = ~(statesWithProbability01.first | statesWithProbability01.second);
-                
-                // set the result for all non-maybe states
-                resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel.getNumberOfStates(), storm::utility::zero<ConstantType>());
-                storm::utility::vector::setVectorValues(resultsForNonMaybeStates, statesWithProbability01.second, storm::utility::one<ConstantType>());
+            // set the result for all non-maybe states
+            resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel.getNumberOfStates(), storm::utility::zero<ConstantType>());
+            storm::utility::vector::setVectorValues(resultsForNonMaybeStates, psiStates, storm::utility::one<ConstantType>());
+            
+            // if there are maybestates, create the parameterLifter
+            if (!maybeStates.empty()) {
+                // Create the vector of one-step probabilities to go to target states.
+                std::vector<typename SparseModelType::ValueType> b = this->parametricModel.getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), psiStates);
                 
-                // if there are maybestates, create the parameterLifter
-                if (!maybeStates.empty()) {
-                    // Create the vector of one-step probabilities to go to target states.
-                    std::vector<typename SparseModelType::ValueType> b = this->parametricModel.getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), psiStates);
-                    
-                    parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel.getTransitionMatrix(), b, maybeStates, maybeStates);
-                }
-                                
-                // We know some bounds for the results so set them
-                lowerResultBound = storm::utility::zero<ConstantType>();
-                upperResultBound = storm::utility::one<ConstantType>();
+                parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel.getTransitionMatrix(), b, maybeStates, maybeStates);
             }
-    
-            template <typename SparseModelType, typename ConstantType>
-            void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyReachabilityRewardFormula(CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask) {
-                
-                // get the results for the subformula
-                storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(this->parametricModel);
-                STORM_LOG_THROW(propositionalChecker.canHandle(checkTask.getFormula().getSubformula()), storm::exceptions::NotSupportedException, "Parameter lifting with non-propositional subformulas is not supported");
-                storm::storage::BitVector targetStates = std::move(propositionalChecker.check(checkTask.getFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
-                
-                // get the maybeStates
-                storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(this->parametricModel.getBackwardTransitions(), storm::storage::BitVector(this->parametricModel.getNumberOfStates(), true), targetStates);
-                infinityStates.complement();
-                maybeStates = ~(targetStates | infinityStates);
-                
-                // set the result for all the non-maybe states
-                resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel.getNumberOfStates(), storm::utility::zero<ConstantType>());
-                storm::utility::vector::setVectorValues(resultsForNonMaybeStates, infinityStates, storm::utility::infinity<ConstantType>());
-                
-                // if there are maybestates, create the parameterLifter
-                if (!maybeStates.empty()) {
-                    // Create the reward vector
-                    STORM_LOG_THROW((checkTask.isRewardModelSet() && this->parametricModel.hasRewardModel(checkTask.getRewardModel())) || (!checkTask.isRewardModelSet() && this->parametricModel.hasUniqueRewardModel()), storm::exceptions::InvalidPropertyException, "The reward model specified by the CheckTask is not available in the given model.");
-
-                    typename SparseModelType::RewardModelType const& rewardModel = checkTask.isRewardModelSet() ? this->parametricModel.getRewardModel(checkTask.getRewardModel()) : this->parametricModel.getUniqueRewardModel();
+            
+            // We know some bounds for the results so set them
+            lowerResultBound = storm::utility::zero<ConstantType>();
+            upperResultBound = storm::utility::one<ConstantType>();
+        }
 
-                    std::vector<typename SparseModelType::ValueType> b = rewardModel.getTotalRewardVector(this->parametricModel.getTransitionMatrix());
-                    
-                    parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel.getTransitionMatrix(), b, maybeStates, maybeStates);
-                }
+        template <typename SparseModelType, typename ConstantType>
+        void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyUntilFormula(CheckTask<storm::logic::UntilFormula, ConstantType> const& checkTask) {
+            
+            // get the results for the subformulas
+            storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(this->parametricModel);
+            STORM_LOG_THROW(propositionalChecker.canHandle(checkTask.getFormula().getLeftSubformula()) && propositionalChecker.canHandle(checkTask.getFormula().getRightSubformula()), storm::exceptions::NotSupportedException, "Parameter lifting with non-propositional subformulas is not supported");
+            storm::storage::BitVector phiStates = std::move(propositionalChecker.check(checkTask.getFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
+            storm::storage::BitVector psiStates = std::move(propositionalChecker.check(checkTask.getFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
+            
+            // get the maybeStates
+            std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(this->parametricModel.getBackwardTransitions(), phiStates, psiStates);
+            maybeStates = ~(statesWithProbability01.first | statesWithProbability01.second);
+            
+            // set the result for all non-maybe states
+            resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel.getNumberOfStates(), storm::utility::zero<ConstantType>());
+            storm::utility::vector::setVectorValues(resultsForNonMaybeStates, statesWithProbability01.second, storm::utility::one<ConstantType>());
+            
+            // if there are maybestates, create the parameterLifter
+            if (!maybeStates.empty()) {
+                // Create the vector of one-step probabilities to go to target states.
+                std::vector<typename SparseModelType::ValueType> b = this->parametricModel.getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), psiStates);
                 
-                // We only know a lower bound for the result
-                lowerResultBound = storm::utility::zero<ConstantType>();
-
+                parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel.getTransitionMatrix(), b, maybeStates, maybeStates);
             }
-    
-            template <typename SparseModelType, typename ConstantType>
-            void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyCumulativeRewardFormula(CheckTask<storm::logic::CumulativeRewardFormula, ConstantType> const& checkTask) {
-                
-                // Obtain the stepBound
-                stepBound = checkTask.getFormula().getBound().evaluateAsInt();
-                if (checkTask.getFormula().isBoundStrict()) {
-                    STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Expected a strict upper step bound that is greater than zero.");
-                    --(*stepBound);
-                }
-                STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive.");
-                
-                //Every state is a maybeState
-                maybeStates = storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getColumnCount(), true);
-                resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel.getNumberOfStates());
-                
+            
+            // We know some bounds for the results so set them
+            lowerResultBound = storm::utility::zero<ConstantType>();
+            upperResultBound = storm::utility::one<ConstantType>();
+        }
+
+        template <typename SparseModelType, typename ConstantType>
+        void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyReachabilityRewardFormula(CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask) {
+            
+            // get the results for the subformula
+            storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(this->parametricModel);
+            STORM_LOG_THROW(propositionalChecker.canHandle(checkTask.getFormula().getSubformula()), storm::exceptions::NotSupportedException, "Parameter lifting with non-propositional subformulas is not supported");
+            storm::storage::BitVector targetStates = std::move(propositionalChecker.check(checkTask.getFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
+            
+            // get the maybeStates
+            storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(this->parametricModel.getBackwardTransitions(), storm::storage::BitVector(this->parametricModel.getNumberOfStates(), true), targetStates);
+            infinityStates.complement();
+            maybeStates = ~(targetStates | infinityStates);
+            
+            // set the result for all the non-maybe states
+            resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel.getNumberOfStates(), storm::utility::zero<ConstantType>());
+            storm::utility::vector::setVectorValues(resultsForNonMaybeStates, infinityStates, storm::utility::infinity<ConstantType>());
+            
+            // if there are maybestates, create the parameterLifter
+            if (!maybeStates.empty()) {
                 // Create the reward vector
                 STORM_LOG_THROW((checkTask.isRewardModelSet() && this->parametricModel.hasRewardModel(checkTask.getRewardModel())) || (!checkTask.isRewardModelSet() && this->parametricModel.hasUniqueRewardModel()), storm::exceptions::InvalidPropertyException, "The reward model specified by the CheckTask is not available in the given model.");
+
                 typename SparseModelType::RewardModelType const& rewardModel = checkTask.isRewardModelSet() ? this->parametricModel.getRewardModel(checkTask.getRewardModel()) : this->parametricModel.getUniqueRewardModel();
+
                 std::vector<typename SparseModelType::ValueType> b = rewardModel.getTotalRewardVector(this->parametricModel.getTransitionMatrix());
-                    
-                parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel.getTransitionMatrix(), b, maybeStates, maybeStates);
                 
-                                
-                // We only know a lower bound for the result
-                lowerResultBound = storm::utility::zero<ConstantType>();
+                parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel.getTransitionMatrix(), b, maybeStates, maybeStates);
             }
             
-            template <typename SparseModelType, typename ConstantType>
-            std::unique_ptr<CheckResult> SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::computeQuantitativeValues(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
-                
-                if(maybeStates.empty()) {
-                    return std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ConstantType>>(resultsForNonMaybeStates);
-                }
-                
-                parameterLifter->specifyRegion(region, dirForParameters);
-                
-                // Set up the solver
-                auto solver = solverFactory->create(parameterLifter->getMatrix());
-                if (storm::NumberTraits<ConstantType>::IsExact && dynamic_cast<storm::solver::StandardMinMaxLinearEquationSolver<ConstantType>*>(solver.get())) {
-                    STORM_LOG_INFO("Parameter Lifting: Setting solution method for exact MinMaxSolver to policy iteration");
-                    auto* standardSolver = dynamic_cast<storm::solver::StandardMinMaxLinearEquationSolver<ConstantType>*>(solver.get());
-                    auto settings = standardSolver->getSettings();
-                    settings.setSolutionMethod(storm::solver::StandardMinMaxLinearEquationSolverSettings<ConstantType>::SolutionMethod::PolicyIteration);
-                    standardSolver->setSettings(settings);
-                }
-                if (lowerResultBound) solver->setLowerBound(lowerResultBound.get());
-                if (upperResultBound) solver->setUpperBound(upperResultBound.get());
-                if (!stepBound) solver->setTrackScheduler(true);
-                if (storm::solver::minimize(dirForParameters) && minSchedChoices && !stepBound) solver->setSchedulerHint(std::move(minSchedChoices.get()));
-                if (storm::solver::maximize(dirForParameters) && maxSchedChoices && !stepBound) solver->setSchedulerHint(std::move(maxSchedChoices.get()));
-                if (this->currentCheckTask->isBoundSet() && solver->hasSchedulerHint()) {
-                    // If we reach this point, we know that after applying the hint, the x-values can only become larger (if we maximize) or smaller (if we minimize).
-                    std::unique_ptr<storm::solver::TerminationCondition<ConstantType>> termCond;
-                    storm::storage::BitVector relevantStatesInSubsystem = this->currentCheckTask->isOnlyInitialStatesRelevantSet() ? this->parametricModel.getInitialStates() % maybeStates : storm::storage::BitVector(maybeStates.getNumberOfSetBits(), true);
-                    if (storm::solver::minimize(dirForParameters)) {
-                        // Terminate if the value for ALL relevant states is already below the threshold
-                        termCond = std::make_unique<storm::solver::TerminateIfFilteredExtremumBelowThreshold<ConstantType>> (relevantStatesInSubsystem, this->currentCheckTask->getBoundThreshold(), true, false);
-                    } else {
-                        // Terminate if the value for ALL relevant states is already above the threshold
-                        termCond = std::make_unique<storm::solver::TerminateIfFilteredExtremumExceedsThreshold<ConstantType>> (relevantStatesInSubsystem, true, this->currentCheckTask->getBoundThreshold(), true);
-                    }
-                    solver->setTerminationCondition(std::move(termCond));
-                }
-                
-                // Invoke the solver
-                if(stepBound) {
-                    assert(*stepBound > 0);
-                    x = std::vector<ConstantType>(maybeStates.getNumberOfSetBits(), storm::utility::zero<ConstantType>());
-                    solver->repeatedMultiply(dirForParameters, x, &parameterLifter->getVector(), *stepBound);
+            // We only know a lower bound for the result
+            lowerResultBound = storm::utility::zero<ConstantType>();
+
+        }
+
+        template <typename SparseModelType, typename ConstantType>
+        void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyCumulativeRewardFormula(CheckTask<storm::logic::CumulativeRewardFormula, ConstantType> const& checkTask) {
+            
+            // Obtain the stepBound
+            stepBound = checkTask.getFormula().getBound().evaluateAsInt();
+            if (checkTask.getFormula().isBoundStrict()) {
+                STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Expected a strict upper step bound that is greater than zero.");
+                --(*stepBound);
+            }
+            STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive.");
+            
+            //Every state is a maybeState
+            maybeStates = storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getColumnCount(), true);
+            resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel.getNumberOfStates());
+            
+            // Create the reward vector
+            STORM_LOG_THROW((checkTask.isRewardModelSet() && this->parametricModel.hasRewardModel(checkTask.getRewardModel())) || (!checkTask.isRewardModelSet() && this->parametricModel.hasUniqueRewardModel()), storm::exceptions::InvalidPropertyException, "The reward model specified by the CheckTask is not available in the given model.");
+            typename SparseModelType::RewardModelType const& rewardModel = checkTask.isRewardModelSet() ? this->parametricModel.getRewardModel(checkTask.getRewardModel()) : this->parametricModel.getUniqueRewardModel();
+            std::vector<typename SparseModelType::ValueType> b = rewardModel.getTotalRewardVector(this->parametricModel.getTransitionMatrix());
+            
+            parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel.getTransitionMatrix(), b, maybeStates, maybeStates);
+            
+            
+            // We only know a lower bound for the result
+            lowerResultBound = storm::utility::zero<ConstantType>();
+        }
+        
+        template <typename SparseModelType, typename ConstantType>
+        storm::modelchecker::SparseInstantiationModelChecker<SparseModelType, ConstantType>& SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::getInstantiationChecker() {
+            if (!instantiationChecker) {
+                instantiationChecker = std::make_unique<storm::modelchecker::SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>>(this->parametricModel);
+                instantiationChecker->specifyFormula(this->currentCheckTask->template convertValueType<typename SparseModelType::ValueType>());
+            }
+            return *instantiationChecker;
+        }
+        
+        template <typename SparseModelType, typename ConstantType>
+        std::unique_ptr<CheckResult> SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::computeQuantitativeValues(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
+            
+            if(maybeStates.empty()) {
+                return std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ConstantType>>(resultsForNonMaybeStates);
+            }
+            
+            parameterLifter->specifyRegion(region, dirForParameters);
+            
+            // Set up the solver
+            auto solver = solverFactory->create(parameterLifter->getMatrix());
+            if (storm::NumberTraits<ConstantType>::IsExact && dynamic_cast<storm::solver::StandardMinMaxLinearEquationSolver<ConstantType>*>(solver.get())) {
+                STORM_LOG_INFO("Parameter Lifting: Setting solution method for exact MinMaxSolver to policy iteration");
+                auto* standardSolver = dynamic_cast<storm::solver::StandardMinMaxLinearEquationSolver<ConstantType>*>(solver.get());
+                auto settings = standardSolver->getSettings();
+                settings.setSolutionMethod(storm::solver::StandardMinMaxLinearEquationSolverSettings<ConstantType>::SolutionMethod::PolicyIteration);
+                standardSolver->setSettings(settings);
+            }
+            if (lowerResultBound) solver->setLowerBound(lowerResultBound.get());
+            if (upperResultBound) solver->setUpperBound(upperResultBound.get());
+            if (!stepBound) solver->setTrackScheduler(true);
+            if (storm::solver::minimize(dirForParameters) && minSchedChoices && !stepBound) solver->setSchedulerHint(std::move(minSchedChoices.get()));
+            if (storm::solver::maximize(dirForParameters) && maxSchedChoices && !stepBound) solver->setSchedulerHint(std::move(maxSchedChoices.get()));
+            if (this->currentCheckTask->isBoundSet() && solver->hasSchedulerHint()) {
+                // If we reach this point, we know that after applying the hint, the x-values can only become larger (if we maximize) or smaller (if we minimize).
+                std::unique_ptr<storm::solver::TerminationCondition<ConstantType>> termCond;
+                storm::storage::BitVector relevantStatesInSubsystem = this->currentCheckTask->isOnlyInitialStatesRelevantSet() ? this->parametricModel.getInitialStates() % maybeStates : storm::storage::BitVector(maybeStates.getNumberOfSetBits(), true);
+                if (storm::solver::minimize(dirForParameters)) {
+                    // Terminate if the value for ALL relevant states is already below the threshold
+                    termCond = std::make_unique<storm::solver::TerminateIfFilteredExtremumBelowThreshold<ConstantType>> (relevantStatesInSubsystem, this->currentCheckTask->getBoundThreshold(), true, false);
                 } else {
-                    x.resize(maybeStates.getNumberOfSetBits(), storm::utility::zero<ConstantType>());
-                    solver->solveEquations(dirForParameters, x, parameterLifter->getVector());
-                    if(storm::solver::minimize(dirForParameters)) {
-                        minSchedChoices = solver->getSchedulerChoices();
-                    } else {
-                        maxSchedChoices = solver->getSchedulerChoices();
-                    }
+                    // Terminate if the value for ALL relevant states is already above the threshold
+                    termCond = std::make_unique<storm::solver::TerminateIfFilteredExtremumExceedsThreshold<ConstantType>> (relevantStatesInSubsystem, true, this->currentCheckTask->getBoundThreshold(), true);
                 }
-                
-                // Get the result for the complete model (including maybestates)
-                std::vector<ConstantType> result = resultsForNonMaybeStates;
-                auto maybeStateResIt = x.begin();
-                for(auto const& maybeState : maybeStates) {
-                    result[maybeState] = *maybeStateResIt;
-                    ++maybeStateResIt;
+                solver->setTerminationCondition(std::move(termCond));
+            }
+            
+            // Invoke the solver
+            if(stepBound) {
+                assert(*stepBound > 0);
+                x = std::vector<ConstantType>(maybeStates.getNumberOfSetBits(), storm::utility::zero<ConstantType>());
+                solver->repeatedMultiply(dirForParameters, x, &parameterLifter->getVector(), *stepBound);
+            } else {
+                x.resize(maybeStates.getNumberOfSetBits(), storm::utility::zero<ConstantType>());
+                solver->solveEquations(dirForParameters, x, parameterLifter->getVector());
+                if(storm::solver::minimize(dirForParameters)) {
+                    minSchedChoices = solver->getSchedulerChoices();
+                } else {
+                    maxSchedChoices = solver->getSchedulerChoices();
                 }
-                return std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ConstantType>>(std::move(result));
             }
             
-                
-            template <typename SparseModelType, typename ConstantType>
-            void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::reset() {
-                maybeStates.resize(0);
-                resultsForNonMaybeStates.clear();
-                stepBound = boost::none;
-                parameterLifter = nullptr;
-                minSchedChoices = boost::none;
-                maxSchedChoices = boost::none;
-                x.clear();
-                lowerResultBound = boost::none;
-                upperResultBound = boost::none;
+            // Get the result for the complete model (including maybestates)
+            std::vector<ConstantType> result = resultsForNonMaybeStates;
+            auto maybeStateResIt = x.begin();
+            for(auto const& maybeState : maybeStates) {
+                result[maybeState] = *maybeStateResIt;
+                ++maybeStateResIt;
+            }
+            return std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ConstantType>>(std::move(result));
+        }
+        
+        
+        template <typename SparseModelType, typename ConstantType>
+        void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::reset() {
+            maybeStates.resize(0);
+            resultsForNonMaybeStates.clear();
+            stepBound = boost::none;
+            instantiationChecker = nullptr;
+            parameterLifter = nullptr;
+            minSchedChoices = boost::none;
+            maxSchedChoices = boost::none;
+            x.clear();
+            lowerResultBound = boost::none;
+            upperResultBound = boost::none;
+        }
+        
+        template <typename SparseModelType, typename ConstantType>
+        boost::optional<storm::storage::Scheduler<ConstantType>> SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::getCurrentMinScheduler() {
+            if (!minSchedChoices) {
+                return boost::none;
             }
             
-            template <typename SparseModelType, typename ConstantType>
-            boost::optional<storm::storage::Scheduler<ConstantType>> SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::getCurrentMinScheduler() {
-                if (!minSchedChoices) {
-                    return boost::none;
-                }
-                
-                storm::storage::Scheduler<ConstantType> result(minSchedChoices->size());
-                uint_fast64_t state = 0;
-                for (auto const& schedulerChoice : minSchedChoices.get()) {
-                    result.setChoice(schedulerChoice, state);
-                    ++state;
-                }
-                
-                return result;
+            storm::storage::Scheduler<ConstantType> result(minSchedChoices->size());
+            uint_fast64_t state = 0;
+            for (auto const& schedulerChoice : minSchedChoices.get()) {
+                result.setChoice(schedulerChoice, state);
+                ++state;
             }
-                    
-            template <typename SparseModelType, typename ConstantType>
-            boost::optional<storm::storage::Scheduler<ConstantType>> SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::getCurrentMaxScheduler() {
-                if (!maxSchedChoices) {
-                    return boost::none;
-                }
-                
-                storm::storage::Scheduler<ConstantType> result(maxSchedChoices->size());
-                uint_fast64_t state = 0;
-                for (auto const& schedulerChoice : maxSchedChoices.get()) {
-                    result.setChoice(schedulerChoice, state);
-                    ++state;
-                }
-                
-                return result;
+            
+            return result;
+        }
+        
+        template <typename SparseModelType, typename ConstantType>
+        boost::optional<storm::storage::Scheduler<ConstantType>> SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::getCurrentMaxScheduler() {
+            if (!maxSchedChoices) {
+                return boost::none;
             }
             
-            template class SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
-            template class SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber>;
-
+            storm::storage::Scheduler<ConstantType> result(maxSchedChoices->size());
+            uint_fast64_t state = 0;
+            for (auto const& schedulerChoice : maxSchedChoices.get()) {
+                result.setChoice(schedulerChoice, state);
+                ++state;
+            }
+            
+            return result;
         }
+        
+        template class SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
+        template class SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber>;
+
     }
 }

src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h

@@ -4,53 +4,58 @@
 #include <memory>
 #include <boost/optional.hpp>
 
-#include "storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h"
+#include "storm-pars/transformer/ParameterLifter.h"
+#include "storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h"
+#include "storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.h"
 #include "storm/storage/BitVector.h"
 #include "storm/storage/Scheduler.h"
 #include "storm/solver/MinMaxLinearEquationSolver.h"
-#include "storm/transformer/ParameterLifter.h"
 #include "storm/logic/FragmentSpecification.h"
 
 
 namespace storm {
     namespace modelchecker {
-        namespace parametric {
             
-            template <typename SparseModelType, typename ConstantType>
-            class SparseDtmcParameterLiftingModelChecker : public SparseParameterLiftingModelChecker<SparseModelType, ConstantType> {
-            public:
-                SparseDtmcParameterLiftingModelChecker(SparseModelType const& parametricModel);
-                SparseDtmcParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>>&& solverFactory);
+        template <typename SparseModelType, typename ConstantType>
+        class SparseDtmcParameterLiftingModelChecker : public SparseParameterLiftingModelChecker<SparseModelType, ConstantType> {
+        public:
+            SparseDtmcParameterLiftingModelChecker(SparseModelType const& parametricModel);
+            SparseDtmcParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>>&& solverFactory);
                 
-                virtual bool canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const override;
+            virtual bool canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const override;
                 
-                boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMinScheduler();
-                boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMaxScheduler();
+            boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMinScheduler();
+            boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMaxScheduler();
 
-            protected:
+        protected:
                 
-                virtual void specifyBoundedUntilFormula(CheckTask<storm::logic::BoundedUntilFormula, ConstantType> const& checkTask) override;
-                virtual void specifyUntilFormula(CheckTask<storm::logic::UntilFormula, ConstantType> const& checkTask) override;
-                virtual void specifyReachabilityRewardFormula(CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask) override;
-                virtual void specifyCumulativeRewardFormula(CheckTask<storm::logic::CumulativeRewardFormula, ConstantType> const& checkTask) override;
+            virtual void specifyBoundedUntilFormula(CheckTask<storm::logic::BoundedUntilFormula, ConstantType> const& checkTask) override;
+            virtual void specifyUntilFormula(CheckTask<storm::logic::UntilFormula, ConstantType> const& checkTask) override;
+            virtual void specifyReachabilityRewardFormula(CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask) override;
+            virtual void specifyCumulativeRewardFormula(CheckTask<storm::logic::CumulativeRewardFormula, ConstantType> const& checkTask) override;
+
+            virtual storm::modelchecker::SparseInstantiationModelChecker<SparseModelType, ConstantType>& getInstantiationChecker() override;
+                
+            virtual std::unique_ptr<CheckResult> computeQuantitativeValues(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) override;
                 
-                virtual std::unique_ptr<CheckResult> computeQuantitativeValues(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) override;
+            virtual void reset() override;
                 
-                virtual void reset() override;
+        private:
+
+            
+            storm::storage::BitVector maybeStates;
+            std::vector<ConstantType> resultsForNonMaybeStates;
+            boost::optional<uint_fast64_t> stepBound;
                 
-            private:
-                storm::storage::BitVector maybeStates;
-                std::vector<ConstantType> resultsForNonMaybeStates;
-                boost::optional<uint_fast64_t> stepBound;
+            std::unique_ptr<storm::modelchecker::SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>> instantiationChecker;
                 
-                std::unique_ptr<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>> parameterLifter;
-                std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>> solverFactory;
+            std::unique_ptr<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>> parameterLifter;
+            std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>> solverFactory;
                 
-                // Results from the most recent solver call.
-                boost::optional<std::vector<uint_fast64_t>> minSchedChoices, maxSchedChoices;
-                std::vector<ConstantType> x;
-                boost::optional<ConstantType> lowerResultBound, upperResultBound;
-            };
-        }
+            // Results from the most recent solver call.
+            boost::optional<std::vector<uint_fast64_t>> minSchedChoices, maxSchedChoices;
+            std::vector<ConstantType> x;
+            boost::optional<ConstantType> lowerResultBound, upperResultBound;
+        };
     }
 }

src/storm-pars/modelchecker/region/SparseDtmcRegionChecker.cpp

@@ -1,65 +0,0 @@
-#include "storm/modelchecker/parametric/SparseDtmcRegionChecker.h"
-
-#include "storm/adapters/RationalFunctionAdapter.h"
-
-#include "storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h"
-#include "storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.h"
-#include "storm/transformer/SparseParametricDtmcSimplifier.h"
-#include "storm/models/sparse/StandardRewardModel.h"
-#include "storm/models/sparse/Dtmc.h"
-#include "storm/utility/NumberTraits.h"
-
-namespace storm {
-    namespace modelchecker {
-        namespace parametric {
-
-            template <typename SparseModelType, typename ConstantType, typename ExactConstantType>
-            SparseDtmcRegionChecker<SparseModelType, ConstantType, ExactConstantType>::SparseDtmcRegionChecker(SparseModelType const& parametricModel) : RegionChecker<SparseModelType, ConstantType, ExactConstantType>(parametricModel) {
-                // Intentionally left empty
-            }
-    
-            template <typename SparseModelType, typename ConstantType, typename ExactConstantType>
-            void SparseDtmcRegionChecker<SparseModelType, ConstantType, ExactConstantType>::simplifyParametricModel(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
-                storm::transformer::SparseParametricDtmcSimplifier<SparseModelType> simplifier(this->parametricModel);
-                if(simplifier.simplify(checkTask.getFormula())) {
-                    this->simplifiedModel = simplifier.getSimplifiedModel();
-                    this->currentFormula = simplifier.getSimplifiedFormula();
-                } else {
-                    this->simplifiedModel = nullptr;
-                    this->currentFormula = checkTask.getFormula().asSharedPointer();
-                }
-            }
-            
-            template <typename SparseModelType, typename ConstantType, typename ExactConstantType>
-            void SparseDtmcRegionChecker<SparseModelType, ConstantType, ExactConstantType>::initializeUnderlyingCheckers() {
-                if (this->settings.applyExactValidation) {
-                    STORM_LOG_WARN_COND(!storm::NumberTraits<ConstantType>::IsExact, "Exact validation is not necessarry if the original computation is already exact");
-                    this->exactParameterLiftingChecker = std::make_unique<SparseDtmcParameterLiftingModelChecker<SparseModelType, ExactConstantType>>(this->getConsideredParametricModel());
-                }
-                this->parameterLiftingChecker = std::make_unique<SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>>(this->getConsideredParametricModel());
-                this->instantiationChecker = std::make_unique<SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>>(this->getConsideredParametricModel());
-                this->instantiationChecker->setInstantiationsAreGraphPreserving(true);
-            }
-    
-            template <typename SparseModelType, typename ConstantType, typename ExactConstantType>
-            void SparseDtmcRegionChecker<SparseModelType, ConstantType, ExactConstantType>::applyHintsToExactChecker() {
-                auto dtmcPLChecker = dynamic_cast<storm::modelchecker::parametric::SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>*>(this->parameterLiftingChecker.get());
-                STORM_LOG_ASSERT(dtmcPLChecker, "Underlying Parameter lifting checker has unexpected type");
-                auto exactDtmcPLChecker = dynamic_cast<storm::modelchecker::parametric::SparseDtmcParameterLiftingModelChecker<SparseModelType, ExactConstantType>*>(this->exactParameterLiftingChecker.get());
-                STORM_LOG_ASSERT(exactDtmcPLChecker, "Underlying exact parameter lifting checker has unexpected type");
-                if (dtmcPLChecker->getCurrentMaxScheduler()) {
-                    exactDtmcPLChecker->getCurrentMaxScheduler() = dtmcPLChecker->getCurrentMaxScheduler()->template toValueType<ExactConstantType>();
-                }
-                if (dtmcPLChecker->getCurrentMinScheduler()) {
-                    exactDtmcPLChecker->getCurrentMinScheduler() = dtmcPLChecker->getCurrentMinScheduler()->template toValueType<ExactConstantType>();
-                }
-            }
-       
-#ifdef STORM_HAVE_CARL
-            template class SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double, storm::RationalNumber>;
-            template class SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber>;
-#endif
-        } // namespace parametric
-    } //namespace modelchecker
-} //namespace storm
-

src/storm-pars/modelchecker/region/SparseDtmcRegionChecker.h

@@ -1,27 +0,0 @@
-#pragma once
-
-#include <memory>
-
-#include "storm/modelchecker/parametric/RegionChecker.h"
-
-namespace storm {
-    namespace modelchecker{
-        namespace parametric{
-            
-
-            template <typename SparseModelType, typename ConstantType, typename ExactConstantType = ConstantType>
-            class SparseDtmcRegionChecker : public RegionChecker<SparseModelType, ConstantType, ExactConstantType> {
-
-            public:
-                SparseDtmcRegionChecker(SparseModelType const& parametricModel);
-                
-            protected:
-                virtual void simplifyParametricModel(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) override;
-                virtual void initializeUnderlyingCheckers() override;
-                virtual void applyHintsToExactChecker() override;
-                
-            };
-    
-        } //namespace parametric
-    } //namespace modelchecker
-} //namespace storm

src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp

@@ -1,4 +1,5 @@
-#include "storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h"
+#include "storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h"
+#include "storm-pars/utility/parameterlifting.h"
 
 #include "storm/adapters/RationalFunctionAdapter.h"
 #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
@@ -18,331 +19,343 @@
 
 namespace storm {
     namespace modelchecker {
-        namespace parametric {
-            
-            template <typename SparseModelType, typename ConstantType>
-            SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel) : SparseParameterLiftingModelChecker<SparseModelType, ConstantType>(parametricModel), solverFactory(std::make_unique<storm::solver::GameSolverFactory<ConstantType>>()) {
+        template <typename SparseModelType, typename ConstantType>
+        SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel) : SparseParameterLiftingModelChecker<SparseModelType, ConstantType>(parametricModel), solverFactory(std::make_unique<storm::solver::GameSolverFactory<ConstantType>>()) {
+        }
+        
+        template <typename SparseModelType, typename ConstantType>
+        SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr<storm::solver::GameSolverFactory<ConstantType>>&& solverFactory) : SparseParameterLiftingModelChecker<SparseModelType, ConstantType>(parametricModel), solverFactory(std::move(solverFactory)) {
+        }
+
+        template <typename SparseModelType, typename ConstantType>
+        bool SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const {
+            bool result = checkTask.getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setCumulativeRewardFormulasAllowed(true));
+            if (result) {
+                STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(this->parametricModel, checkTask.getFormula()), "Could not validate whether parameter lifting is applicable. Please validate manually...");
             }
+            return result;
+
+        }
+        
+        template <typename SparseModelType, typename ConstantType>
+        void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyBoundedUntilFormula(CheckTask<storm::logic::BoundedUntilFormula, ConstantType> const& checkTask) {
             
-            template <typename SparseModelType, typename ConstantType>
-            SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr<storm::solver::GameSolverFactory<ConstantType>>&& solverFactory) : SparseParameterLiftingModelChecker<SparseModelType, ConstantType>(parametricModel), solverFactory(std::move(solverFactory)) {
+            // get the step bound
+            STORM_LOG_THROW(!checkTask.getFormula().hasLowerBound(), storm::exceptions::NotSupportedException, "Lower step bounds are not supported.");
+            STORM_LOG_THROW(checkTask.getFormula().hasUpperBound(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with an upper bound.");
+            STORM_LOG_THROW(checkTask.getFormula().isStepBounded(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with step bounds.");
+            stepBound = checkTask.getFormula().getUpperBound().evaluateAsInt();
+            STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive.");
+            if (checkTask.getFormula().isUpperBoundStrict()) {
+                STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Expected a strict upper step bound that is greater than zero.");
+                --(*stepBound);
             }
-    
-            template <typename SparseModelType, typename ConstantType>
-            bool SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const {
-                return checkTask.getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setCumulativeRewardFormulasAllowed(true));
-            }
-            
-            template <typename SparseModelType, typename ConstantType>
-            void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyBoundedUntilFormula(CheckTask<storm::logic::BoundedUntilFormula, ConstantType> const& checkTask) {
-                
-                // get the step bound
-                STORM_LOG_THROW(!checkTask.getFormula().hasLowerBound(), storm::exceptions::NotSupportedException, "Lower step bounds are not supported.");
-                STORM_LOG_THROW(checkTask.getFormula().hasUpperBound(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with an upper bound.");
-                STORM_LOG_THROW(checkTask.getFormula().isStepBounded(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with step bounds.");
-                stepBound = checkTask.getFormula().getUpperBound().evaluateAsInt();
-                STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive.");
-                if (checkTask.getFormula().isUpperBoundStrict()) {
-                    STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Expected a strict upper step bound that is greater than zero.");
-                    --(*stepBound);
-                }
-                STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive.");
+            STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive.");
 
-                // get the results for the subformulas
-                storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(this->parametricModel);
-                STORM_LOG_THROW(propositionalChecker.canHandle(checkTask.getFormula().getLeftSubformula()) && propositionalChecker.canHandle(checkTask.getFormula().getRightSubformula()), storm::exceptions::NotSupportedException, "Parameter lifting with non-propositional subformulas is not supported");
-                storm::storage::BitVector phiStates = std::move(propositionalChecker.check(checkTask.getFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
-                storm::storage::BitVector psiStates = std::move(propositionalChecker.check(checkTask.getFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
-                
-                // get the maybeStates
-                maybeStates = storm::solver::minimize(checkTask.getOptimizationDirection()) ?
-                              storm::utility::graph::performProbGreater0A(this->parametricModel.getTransitionMatrix(), this->parametricModel.getTransitionMatrix().getRowGroupIndices(), this->parametricModel.getBackwardTransitions(), phiStates, psiStates, true, *stepBound) :
-                              storm::utility::graph::performProbGreater0E(this->parametricModel.getBackwardTransitions(), phiStates, psiStates, true, *stepBound);
-                maybeStates &= ~psiStates;
-                
-                // set the result for all non-maybe states
-                resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel.getNumberOfStates(), storm::utility::zero<ConstantType>());
-                storm::utility::vector::setVectorValues(resultsForNonMaybeStates, psiStates, storm::utility::one<ConstantType>());
+            // get the results for the subformulas
+            storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(this->parametricModel);
+            STORM_LOG_THROW(propositionalChecker.canHandle(checkTask.getFormula().getLeftSubformula()) && propositionalChecker.canHandle(checkTask.getFormula().getRightSubformula()), storm::exceptions::NotSupportedException, "Parameter lifting with non-propositional subformulas is not supported");
+            storm::storage::BitVector phiStates = std::move(propositionalChecker.check(checkTask.getFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
+            storm::storage::BitVector psiStates = std::move(propositionalChecker.check(checkTask.getFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
+            
+            // get the maybeStates
+            maybeStates = storm::solver::minimize(checkTask.getOptimizationDirection()) ?
+                          storm::utility::graph::performProbGreater0A(this->parametricModel.getTransitionMatrix(), this->parametricModel.getTransitionMatrix().getRowGroupIndices(), this->parametricModel.getBackwardTransitions(), phiStates, psiStates, true, *stepBound) :
+                          storm::utility::graph::performProbGreater0E(this->parametricModel.getBackwardTransitions(), phiStates, psiStates, true, *stepBound);
+            maybeStates &= ~psiStates;
+            
+            // set the result for all non-maybe states
+            resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel.getNumberOfStates(), storm::utility::zero<ConstantType>());
+            storm::utility::vector::setVectorValues(resultsForNonMaybeStates, psiStates, storm::utility::one<ConstantType>());
+            
+            // if there are maybestates, create the parameterLifter
+            if (!maybeStates.empty()) {
+                // Create the vector of one-step probabilities to go to target states.
+                std::vector<typename SparseModelType::ValueType> b = this->parametricModel.getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), psiStates);
                 
-                // if there are maybestates, create the parameterLifter
-                if (!maybeStates.empty()) {
-                    // Create the vector of one-step probabilities to go to target states.
-                    std::vector<typename SparseModelType::ValueType> b = this->parametricModel.getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), psiStates);
-                    
-                    parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel.getTransitionMatrix(), b, this->parametricModel.getTransitionMatrix().getRowFilter(maybeStates), maybeStates);
-                    computePlayer1Matrix();
-                    
-                    applyPreviousResultAsHint = false;
-                }
+                parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel.getTransitionMatrix(), b, this->parametricModel.getTransitionMatrix().getRowFilter(maybeStates), maybeStates);
+                computePlayer1Matrix();
                 
-                // We know some bounds for the results
-                lowerResultBound = storm::utility::zero<ConstantType>();
-                upperResultBound = storm::utility::one<ConstantType>();
+                applyPreviousResultAsHint = false;
             }
-    
-            template <typename SparseModelType, typename ConstantType>
-            void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyUntilFormula(CheckTask<storm::logic::UntilFormula, ConstantType> const& checkTask) {
-                
-                // get the results for the subformulas
-                storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(this->parametricModel);
-                STORM_LOG_THROW(propositionalChecker.canHandle(checkTask.getFormula().getLeftSubformula()) && propositionalChecker.canHandle(checkTask.getFormula().getRightSubformula()), storm::exceptions::NotSupportedException, "Parameter lifting with non-propositional subformulas is not supported");
-                storm::storage::BitVector phiStates = std::move(propositionalChecker.check(checkTask.getFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
-                storm::storage::BitVector psiStates = std::move(propositionalChecker.check(checkTask.getFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
-                
-                // get the maybeStates
-                std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::solver::minimize(checkTask.getOptimizationDirection()) ?
-                                                                                                          storm::utility::graph::performProb01Min(this->parametricModel.getTransitionMatrix(), this->parametricModel.getTransitionMatrix().getRowGroupIndices(), this->parametricModel.getBackwardTransitions(), phiStates, psiStates) :
-                                                                                                          storm::utility::graph::performProb01Max(this->parametricModel.getTransitionMatrix(), this->parametricModel.getTransitionMatrix().getRowGroupIndices(), this->parametricModel.getBackwardTransitions(), phiStates, psiStates);
-                maybeStates = ~(statesWithProbability01.first | statesWithProbability01.second);
+            
+            // We know some bounds for the results
+            lowerResultBound = storm::utility::zero<ConstantType>();
+            upperResultBound = storm::utility::one<ConstantType>();
+        }
+
+        template <typename SparseModelType, typename ConstantType>
+        void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyUntilFormula(CheckTask<storm::logic::UntilFormula, ConstantType> const& checkTask) {
+            
+            // get the results for the subformulas
+            storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(this->parametricModel);
+            STORM_LOG_THROW(propositionalChecker.canHandle(checkTask.getFormula().getLeftSubformula()) && propositionalChecker.canHandle(checkTask.getFormula().getRightSubformula()), storm::exceptions::NotSupportedException, "Parameter lifting with non-propositional subformulas is not supported");
+            storm::storage::BitVector phiStates = std::move(propositionalChecker.check(checkTask.getFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
+            storm::storage::BitVector psiStates = std::move(propositionalChecker.check(checkTask.getFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
+            
+            // get the maybeStates
+            std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::solver::minimize(checkTask.getOptimizationDirection()) ?
+                                                                                                      storm::utility::graph::performProb01Min(this->parametricModel.getTransitionMatrix(), this->parametricModel.getTransitionMatrix().getRowGroupIndices(), this->parametricModel.getBackwardTransitions(), phiStates, psiStates) :
+                                                                                                      storm::utility::graph::performProb01Max(this->parametricModel.getTransitionMatrix(), this->parametricModel.getTransitionMatrix().getRowGroupIndices(), this->parametricModel.getBackwardTransitions(), phiStates, psiStates);
+            maybeStates = ~(statesWithProbability01.first | statesWithProbability01.second);
+            
+            // set the result for all non-maybe states
+            resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel.getNumberOfStates(), storm::utility::zero<ConstantType>());
+            storm::utility::vector::setVectorValues(resultsForNonMaybeStates, statesWithProbability01.second, storm::utility::one<ConstantType>());
+            
+            // if there are maybestates, create the parameterLifter
+            if (!maybeStates.empty()) {
+                // Create the vector of one-step probabilities to go to target states.
+                std::vector<typename SparseModelType::ValueType> b = this->parametricModel.getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), statesWithProbability01.second);
                 
-                // set the result for all non-maybe states
-                resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel.getNumberOfStates(), storm::utility::zero<ConstantType>());
-                storm::utility::vector::setVectorValues(resultsForNonMaybeStates, statesWithProbability01.second, storm::utility::one<ConstantType>());
+                parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel.getTransitionMatrix(), b, this->parametricModel.getTransitionMatrix().getRowFilter(maybeStates), maybeStates);
+                computePlayer1Matrix();
                 
-                // if there are maybestates, create the parameterLifter
-                if (!maybeStates.empty()) {
-                    // Create the vector of one-step probabilities to go to target states.
-                    std::vector<typename SparseModelType::ValueType> b = this->parametricModel.getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), statesWithProbability01.second);
-                    
-                    parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel.getTransitionMatrix(), b, this->parametricModel.getTransitionMatrix().getRowFilter(maybeStates), maybeStates);
-                    computePlayer1Matrix();
-                    
-                    // Check whether there is an EC consisting of maybestates
-                    applyPreviousResultAsHint = storm::solver::minimize(checkTask.getOptimizationDirection()) || // when minimizing, there can not be an EC within the maybestates
-                                                storm::utility::graph::performProb1A(this->parametricModel.getTransitionMatrix(), this->parametricModel.getTransitionMatrix().getRowGroupIndices(), this->parametricModel.getBackwardTransitions(), maybeStates, ~maybeStates).full();
-                }
-                                
-                // We know some bounds for the results
-                lowerResultBound = storm::utility::zero<ConstantType>();
-                upperResultBound = storm::utility::one<ConstantType>();
+                // Check whether there is an EC consisting of maybestates
+                applyPreviousResultAsHint = storm::solver::minimize(checkTask.getOptimizationDirection()) || // when minimizing, there can not be an EC within the maybestates
+                                            storm::utility::graph::performProb1A(this->parametricModel.getTransitionMatrix(), this->parametricModel.getTransitionMatrix().getRowGroupIndices(), this->parametricModel.getBackwardTransitions(), maybeStates, ~maybeStates).full();
             }
-    
-            template <typename SparseModelType, typename ConstantType>
-            void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyReachabilityRewardFormula(CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask) {
-                
-                // get the results for the subformula
-                storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(this->parametricModel);
-                STORM_LOG_THROW(propositionalChecker.canHandle(checkTask.getFormula().getSubformula()), storm::exceptions::NotSupportedException, "Parameter lifting with non-propositional subformulas is not supported");
-                storm::storage::BitVector targetStates = std::move(propositionalChecker.check(checkTask.getFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
+            
+            // We know some bounds for the results
+            lowerResultBound = storm::utility::zero<ConstantType>();
+            upperResultBound = storm::utility::one<ConstantType>();
+        }
+
+        template <typename SparseModelType, typename ConstantType>
+        void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyReachabilityRewardFormula(CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask) {
+            
+            // get the results for the subformula
+            storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(this->parametricModel);
+            STORM_LOG_THROW(propositionalChecker.canHandle(checkTask.getFormula().getSubformula()), storm::exceptions::NotSupportedException, "Parameter lifting with non-propositional subformulas is not supported");
+            storm::storage::BitVector targetStates = std::move(propositionalChecker.check(checkTask.getFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
+            
+            // get the maybeStates
+            storm::storage::BitVector infinityStates = storm::solver::minimize(checkTask.getOptimizationDirection()) ?
+                                                       storm::utility::graph::performProb1E(this->parametricModel.getTransitionMatrix(), this->parametricModel.getTransitionMatrix().getRowGroupIndices(), this->parametricModel.getBackwardTransitions(), storm::storage::BitVector(this->parametricModel.getNumberOfStates(), true), targetStates) :
+                                                       storm::utility::graph::performProb1A(this->parametricModel.getTransitionMatrix(), this->parametricModel.getTransitionMatrix().getRowGroupIndices(), this->parametricModel.getBackwardTransitions(), storm::storage::BitVector(this->parametricModel.getNumberOfStates(), true), targetStates);
+            infinityStates.complement();
+            maybeStates = ~(targetStates | infinityStates);
+            
+            // set the result for all the non-maybe states
+            resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel.getNumberOfStates(), storm::utility::zero<ConstantType>());
+            storm::utility::vector::setVectorValues(resultsForNonMaybeStates, infinityStates, storm::utility::infinity<ConstantType>());
+            
+            // if there are maybestates, create the parameterLifter
+            if (!maybeStates.empty()) {
+                // Create the reward vector
+                STORM_LOG_THROW((checkTask.isRewardModelSet() && this->parametricModel.hasRewardModel(checkTask.getRewardModel())) || (!checkTask.isRewardModelSet() && this->parametricModel.hasUniqueRewardModel()), storm::exceptions::InvalidPropertyException, "The reward model specified by the CheckTask is not available in the given model.");
+
+                typename SparseModelType::RewardModelType const& rewardModel = checkTask.isRewardModelSet() ? this->parametricModel.getRewardModel(checkTask.getRewardModel()) : this->parametricModel.getUniqueRewardModel();
+
+                std::vector<typename SparseModelType::ValueType> b = rewardModel.getTotalRewardVector(this->parametricModel.getTransitionMatrix());
                 
-                // get the maybeStates
-                storm::storage::BitVector infinityStates = storm::solver::minimize(checkTask.getOptimizationDirection()) ?
-                                                           storm::utility::graph::performProb1E(this->parametricModel.getTransitionMatrix(), this->parametricModel.getTransitionMatrix().getRowGroupIndices(), this->parametricModel.getBackwardTransitions(), storm::storage::BitVector(this->parametricModel.getNumberOfStates(), true), targetStates) :
-                                                           storm::utility::graph::performProb1A(this->parametricModel.getTransitionMatrix(), this->parametricModel.getTransitionMatrix().getRowGroupIndices(), this->parametricModel.getBackwardTransitions(), storm::storage::BitVector(this->parametricModel.getNumberOfStates(), true), targetStates);
-                infinityStates.complement();
-                maybeStates = ~(targetStates | infinityStates);
+                // We need to handle choices that lead to an infinity state.
+                // As a maybeState does not have reward infinity, a choice leading to an infinity state will never be picked. Hence, we can unselect the corresponding rows
+                storm::storage::BitVector selectedRows = this->parametricModel.getTransitionMatrix().getRowFilter(maybeStates, ~infinityStates);
                 
-                // set the result for all the non-maybe states
-                resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel.getNumberOfStates(), storm::utility::zero<ConstantType>());
-                storm::utility::vector::setVectorValues(resultsForNonMaybeStates, infinityStates, storm::utility::infinity<ConstantType>());
+                parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel.getTransitionMatrix(), b, selectedRows, maybeStates);
+                computePlayer1Matrix();
                 
-                // if there are maybestates, create the parameterLifter
-                if (!maybeStates.empty()) {
-                    // Create the reward vector
-                    STORM_LOG_THROW((checkTask.isRewardModelSet() && this->parametricModel.hasRewardModel(checkTask.getRewardModel())) || (!checkTask.isRewardModelSet() && this->parametricModel.hasUniqueRewardModel()), storm::exceptions::InvalidPropertyException, "The reward model specified by the CheckTask is not available in the given model.");
-
-                    typename SparseModelType::RewardModelType const& rewardModel = checkTask.isRewardModelSet() ? this->parametricModel.getRewardModel(checkTask.getRewardModel()) : this->parametricModel.getUniqueRewardModel();
+                // Check whether there is an EC consisting of maybestates
+                applyPreviousResultAsHint = !storm::solver::minimize(checkTask.getOptimizationDirection()) || // when maximizing, there can not be an EC within the maybestates
+                                            storm::utility::graph::performProb1A(this->parametricModel.getTransitionMatrix(), this->parametricModel.getTransitionMatrix().getRowGroupIndices(), this->parametricModel.getBackwardTransitions(), maybeStates, ~maybeStates).full();
+            }
+            
+            // We only know a lower bound for the result
+            lowerResultBound = storm::utility::zero<ConstantType>();
 
-                    std::vector<typename SparseModelType::ValueType> b = rewardModel.getTotalRewardVector(this->parametricModel.getTransitionMatrix());
-                    
-                    // We need to handle choices that lead to an infinity state.
-                    // As a maybeState does not have reward infinity, a choice leading to an infinity state will never be picked. Hence, we can unselect the corresponding rows
-                    storm::storage::BitVector selectedRows = this->parametricModel.getTransitionMatrix().getRowFilter(maybeStates, ~infinityStates);
-                    
-                    parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel.getTransitionMatrix(), b, selectedRows, maybeStates);
-                    computePlayer1Matrix();
-                    
-                    // Check whether there is an EC consisting of maybestates
-                    applyPreviousResultAsHint = !storm::solver::minimize(checkTask.getOptimizationDirection()) || // when maximizing, there can not be an EC within the maybestates
-                                                storm::utility::graph::performProb1A(this->parametricModel.getTransitionMatrix(), this->parametricModel.getTransitionMatrix().getRowGroupIndices(), this->parametricModel.getBackwardTransitions(), maybeStates, ~maybeStates).full();
-                }
-                
-                // We only know a lower bound for the result
-                lowerResultBound = storm::utility::zero<ConstantType>();
+        }
 
+        template <typename SparseModelType, typename ConstantType>
+        void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyCumulativeRewardFormula(CheckTask<storm::logic::CumulativeRewardFormula, ConstantType> const& checkTask) {
+            
+            // Obtain the stepBound
+            stepBound = checkTask.getFormula().getBound().evaluateAsInt();
+            if (checkTask.getFormula().isBoundStrict()) {
+                STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Expected a strict upper step bound that is greater than zero.");
+                --(*stepBound);
             }
-    
-            template <typename SparseModelType, typename ConstantType>
-            void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyCumulativeRewardFormula(CheckTask<storm::logic::CumulativeRewardFormula, ConstantType> const& checkTask) {
-                
-                // Obtain the stepBound
-                stepBound = checkTask.getFormula().getBound().evaluateAsInt();
-                if (checkTask.getFormula().isBoundStrict()) {
-                    STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Expected a strict upper step bound that is greater than zero.");
-                    --(*stepBound);
-                }
-                STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive.");
-                
-                //Every state is a maybeState
-                maybeStates = storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getColumnCount(), true);
-                resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel.getNumberOfStates());
+            STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive.");
+            
+            //Every state is a maybeState
+            maybeStates = storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getColumnCount(), true);
+            resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel.getNumberOfStates());
 
-                // Create the reward vector
-                STORM_LOG_THROW((checkTask.isRewardModelSet() && this->parametricModel.hasRewardModel(checkTask.getRewardModel())) || (!checkTask.isRewardModelSet() && this->parametricModel.hasUniqueRewardModel()), storm::exceptions::InvalidPropertyException, "The reward model specified by the CheckTask is not available in the given model.");
-                typename SparseModelType::RewardModelType const& rewardModel = checkTask.isRewardModelSet() ? this->parametricModel.getRewardModel(checkTask.getRewardModel()) : this->parametricModel.getUniqueRewardModel();
-                std::vector<typename SparseModelType::ValueType> b = rewardModel.getTotalRewardVector(this->parametricModel.getTransitionMatrix());
-                    
-                parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel.getTransitionMatrix(), b, storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), maybeStates);
-                computePlayer1Matrix();
+            // Create the reward vector
+            STORM_LOG_THROW((checkTask.isRewardModelSet() && this->parametricModel.hasRewardModel(checkTask.getRewardModel())) || (!checkTask.isRewardModelSet() && this->parametricModel.hasUniqueRewardModel()), storm::exceptions::InvalidPropertyException, "The reward model specified by the CheckTask is not available in the given model.");
+            typename SparseModelType::RewardModelType const& rewardModel = checkTask.isRewardModelSet() ? this->parametricModel.getRewardModel(checkTask.getRewardModel()) : this->parametricModel.getUniqueRewardModel();
+            std::vector<typename SparseModelType::ValueType> b = rewardModel.getTotalRewardVector(this->parametricModel.getTransitionMatrix());
+            
+            parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel.getTransitionMatrix(), b, storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), maybeStates);
+            computePlayer1Matrix();
 
-                applyPreviousResultAsHint = false;
-                
-                // We only know a lower bound for the result
-                lowerResultBound = storm::utility::zero<ConstantType>();
+            applyPreviousResultAsHint = false;
+            
+            // We only know a lower bound for the result
+            lowerResultBound = storm::utility::zero<ConstantType>();
+        }
+        
+        template <typename SparseModelType, typename ConstantType>
+        storm::modelchecker::SparseInstantiationModelChecker<SparseModelType, ConstantType>& SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::getInstantiationChecker() {
+            if (!instantiationChecker) {
+                instantiationChecker = std::make_unique<storm::modelchecker::SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>>(this->parametricModel);
+                instantiationChecker->specifyFormula(this->currentCheckTask->template convertValueType<typename SparseModelType::ValueType>());
             }
+            return *instantiationChecker;
+        }
+
+        template <typename SparseModelType, typename ConstantType>
+        std::unique_ptr<CheckResult> SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::computeQuantitativeValues(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
             
-            template <typename SparseModelType, typename ConstantType>
-            std::unique_ptr<CheckResult> SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::computeQuantitativeValues(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
-                
-                if(maybeStates.empty()) {
-                    return std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ConstantType>>(resultsForNonMaybeStates);
-                }
-                
-                parameterLifter->specifyRegion(region, dirForParameters);
-                
-                // Set up the solver
-                auto solver = solverFactory->create(player1Matrix, parameterLifter->getMatrix());
-                if (storm::NumberTraits<ConstantType>::IsExact && dynamic_cast<storm::solver::StandardGameSolver<ConstantType>*>(solver.get())) {
-                    STORM_LOG_INFO("Parameter Lifting: Setting solution method for exact Game Solver to policy iteration");
-                    auto* standardSolver = dynamic_cast<storm::solver::StandardGameSolver<ConstantType>*>(solver.get());
-                    auto settings = standardSolver->getSettings();
-                    settings.setSolutionMethod(storm::solver::StandardGameSolverSettings<ConstantType>::SolutionMethod::PolicyIteration);
-                    standardSolver->setSettings(settings);
-                }
-                if (lowerResultBound) solver->setLowerBound(lowerResultBound.get());
-                if (upperResultBound) solver->setUpperBound(upperResultBound.get());
-                if (applyPreviousResultAsHint) {
-                    solver->setTrackSchedulers(true);
-                    x.resize(maybeStates.getNumberOfSetBits(), storm::utility::zero<ConstantType>());
-                    if(storm::solver::minimize(dirForParameters) && minSchedChoices && player1SchedChoices) solver->setSchedulerHints(std::move(player1SchedChoices.get()), std::move(minSchedChoices.get()));
-                    if(storm::solver::maximize(dirForParameters) && maxSchedChoices && player1SchedChoices) solver->setSchedulerHints(std::move(player1SchedChoices.get()), std::move(maxSchedChoices.get()));
+            if(maybeStates.empty()) {
+                return std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ConstantType>>(resultsForNonMaybeStates);
+            }
+            
+            parameterLifter->specifyRegion(region, dirForParameters);
+            
+            // Set up the solver
+            auto solver = solverFactory->create(player1Matrix, parameterLifter->getMatrix());
+            if (storm::NumberTraits<ConstantType>::IsExact && dynamic_cast<storm::solver::StandardGameSolver<ConstantType>*>(solver.get())) {
+                STORM_LOG_INFO("Parameter Lifting: Setting solution method for exact Game Solver to policy iteration");
+                auto* standardSolver = dynamic_cast<storm::solver::StandardGameSolver<ConstantType>*>(solver.get());
+                auto settings = standardSolver->getSettings();
+                settings.setSolutionMethod(storm::solver::StandardGameSolverSettings<ConstantType>::SolutionMethod::PolicyIteration);
+                standardSolver->setSettings(settings);
+            }
+            if (lowerResultBound) solver->setLowerBound(lowerResultBound.get());
+            if (upperResultBound) solver->setUpperBound(upperResultBound.get());
+            if (applyPreviousResultAsHint) {
+                solver->setTrackSchedulers(true);
+                x.resize(maybeStates.getNumberOfSetBits(), storm::utility::zero<ConstantType>());
+                if(storm::solver::minimize(dirForParameters) && minSchedChoices && player1SchedChoices) solver->setSchedulerHints(std::move(player1SchedChoices.get()), std::move(minSchedChoices.get()));
+                if(storm::solver::maximize(dirForParameters) && maxSchedChoices && player1SchedChoices) solver->setSchedulerHints(std::move(player1SchedChoices.get()), std::move(maxSchedChoices.get()));
+            } else {
+                x.assign(maybeStates.getNumberOfSetBits(), storm::utility::zero<ConstantType>());
+            }
+            if (this->currentCheckTask->isBoundSet() && this->currentCheckTask->getOptimizationDirection() == dirForParameters && solver->hasSchedulerHints()) {
+                // If we reach this point, we know that after applying the hints, the x-values can only become larger (if we maximize) or smaller (if we minimize).
+                std::unique_ptr<storm::solver::TerminationCondition<ConstantType>> termCond;
+                storm::storage::BitVector relevantStatesInSubsystem = this->currentCheckTask->isOnlyInitialStatesRelevantSet() ? this->parametricModel.getInitialStates() % maybeStates : storm::storage::BitVector(maybeStates.getNumberOfSetBits(), true);
+                if (storm::solver::minimize(dirForParameters)) {
+                    // Terminate if the value for ALL relevant states is already below the threshold
+                    termCond = std::make_unique<storm::solver::TerminateIfFilteredExtremumBelowThreshold<ConstantType>> (relevantStatesInSubsystem, this->currentCheckTask->getBoundThreshold(), true, false);
                 } else {
-                    x.assign(maybeStates.getNumberOfSetBits(), storm::utility::zero<ConstantType>());
+                    // Terminate if the value for ALL relevant states is already above the threshold
+                    termCond = std::make_unique<storm::solver::TerminateIfFilteredExtremumExceedsThreshold<ConstantType>> (relevantStatesInSubsystem, true, this->currentCheckTask->getBoundThreshold(), true);
                 }
-                if (this->currentCheckTask->isBoundSet() && this->currentCheckTask->getOptimizationDirection() == dirForParameters && solver->hasSchedulerHints()) {
-                    // If we reach this point, we know that after applying the hints, the x-values can only become larger (if we maximize) or smaller (if we minimize).
-                    std::unique_ptr<storm::solver::TerminationCondition<ConstantType>> termCond;
-                    storm::storage::BitVector relevantStatesInSubsystem = this->currentCheckTask->isOnlyInitialStatesRelevantSet() ? this->parametricModel.getInitialStates() % maybeStates : storm::storage::BitVector(maybeStates.getNumberOfSetBits(), true);
-                    if (storm::solver::minimize(dirForParameters)) {
-                        // Terminate if the value for ALL relevant states is already below the threshold
-                        termCond = std::make_unique<storm::solver::TerminateIfFilteredExtremumBelowThreshold<ConstantType>> (relevantStatesInSubsystem, this->currentCheckTask->getBoundThreshold(), true, false);
+                solver->setTerminationCondition(std::move(termCond));
+            }
+            
+            // Invoke the solver
+            if(stepBound) {
+                assert(*stepBound > 0);
+                solver->repeatedMultiply(this->currentCheckTask->getOptimizationDirection(), dirForParameters, x, &parameterLifter->getVector(), *stepBound);
+            } else {
+                solver->solveGame(this->currentCheckTask->getOptimizationDirection(), dirForParameters, x, parameterLifter->getVector());
+                if(applyPreviousResultAsHint) {
+                    if(storm::solver::minimize(dirForParameters)) {
+                        minSchedChoices = solver->getPlayer2SchedulerChoices();
                     } else {
-                        // Terminate if the value for ALL relevant states is already above the threshold
-                        termCond = std::make_unique<storm::solver::TerminateIfFilteredExtremumExceedsThreshold<ConstantType>> (relevantStatesInSubsystem, true, this->currentCheckTask->getBoundThreshold(), true);
-                    }
-                    solver->setTerminationCondition(std::move(termCond));
-                }
-                
-                // Invoke the solver
-                if(stepBound) {
-                    assert(*stepBound > 0);
-                    solver->repeatedMultiply(this->currentCheckTask->getOptimizationDirection(), dirForParameters, x, &parameterLifter->getVector(), *stepBound);
-                } else {
-                    solver->solveGame(this->currentCheckTask->getOptimizationDirection(), dirForParameters, x, parameterLifter->getVector());
-                    if(applyPreviousResultAsHint) {
-                        if(storm::solver::minimize(dirForParameters)) {
-                            minSchedChoices = solver->getPlayer2SchedulerChoices();
-                        } else {
-                            maxSchedChoices = solver->getPlayer2SchedulerChoices();
-                        }
-                        player1SchedChoices = solver->getPlayer1SchedulerChoices();
+                        maxSchedChoices = solver->getPlayer2SchedulerChoices();
                     }
+                    player1SchedChoices = solver->getPlayer1SchedulerChoices();
                 }
-                
-                // Get the result for the complete model (including maybestates)
-                std::vector<ConstantType> result = resultsForNonMaybeStates;
-                auto maybeStateResIt = x.begin();
-                for(auto const& maybeState : maybeStates) {
-                    result[maybeState] = *maybeStateResIt;
-                    ++maybeStateResIt;
-                }
-                return std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ConstantType>>(std::move(result));
             }
             
-            template <typename SparseModelType, typename ConstantType>
-            void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::computePlayer1Matrix() {
-                uint_fast64_t n = 0;
-                for(auto const& maybeState : maybeStates) {
-                    n += this->parametricModel.getTransitionMatrix().getRowGroupSize(maybeState);
-                }
-                // The player 1 matrix is the identity matrix of size n with the row groups as given by the original matrix
-                storm::storage::SparseMatrixBuilder<storm::storage::sparse::state_type> matrixBuilder(n, n, n, true, true, maybeStates.getNumberOfSetBits());
-                uint_fast64_t p1MatrixRow = 0;
-                for (auto maybeState : maybeStates){
-                    matrixBuilder.newRowGroup(p1MatrixRow);
-                    for (uint_fast64_t row = this->parametricModel.getTransitionMatrix().getRowGroupIndices()[maybeState]; row < this->parametricModel.getTransitionMatrix().getRowGroupIndices()[maybeState + 1]; ++row){
-                        matrixBuilder.addNextValue(p1MatrixRow, p1MatrixRow, storm::utility::one<storm::storage::sparse::state_type>());
-                        ++p1MatrixRow;
-                    }
+            // Get the result for the complete model (including maybestates)
+            std::vector<ConstantType> result = resultsForNonMaybeStates;
+            auto maybeStateResIt = x.begin();
+            for(auto const& maybeState : maybeStates) {
+                result[maybeState] = *maybeStateResIt;
+                ++maybeStateResIt;
+            }
+            return std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ConstantType>>(std::move(result));
+        }
+        
+        template <typename SparseModelType, typename ConstantType>
+        void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::computePlayer1Matrix() {
+            uint_fast64_t n = 0;
+            for(auto const& maybeState : maybeStates) {
+                n += this->parametricModel.getTransitionMatrix().getRowGroupSize(maybeState);
+            }
+            // The player 1 matrix is the identity matrix of size n with the row groups as given by the original matrix
+            storm::storage::SparseMatrixBuilder<storm::storage::sparse::state_type> matrixBuilder(n, n, n, true, true, maybeStates.getNumberOfSetBits());
+            uint_fast64_t p1MatrixRow = 0;
+            for (auto maybeState : maybeStates){
+                matrixBuilder.newRowGroup(p1MatrixRow);
+                for (uint_fast64_t row = this->parametricModel.getTransitionMatrix().getRowGroupIndices()[maybeState]; row < this->parametricModel.getTransitionMatrix().getRowGroupIndices()[maybeState + 1]; ++row){
+                    matrixBuilder.addNextValue(p1MatrixRow, p1MatrixRow, storm::utility::one<storm::storage::sparse::state_type>());
+                    ++p1MatrixRow;
                 }
-                player1Matrix = matrixBuilder.build();
             }
-    
-            template <typename SparseModelType, typename ConstantType>
-            void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::reset() {
-                maybeStates.resize(0);
-                resultsForNonMaybeStates.clear();
-                stepBound = boost::none;
-                player1Matrix = storm::storage::SparseMatrix<storm::storage::sparse::state_type>();
-                parameterLifter = nullptr;
-                minSchedChoices = boost::none;
-                maxSchedChoices = boost::none;
-                x.clear();
-                lowerResultBound = boost::none;
-                upperResultBound = boost::none;
-                applyPreviousResultAsHint = false;
+            player1Matrix = matrixBuilder.build();
+        }
+
+        template <typename SparseModelType, typename ConstantType>
+        void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::reset() {
+            maybeStates.resize(0);
+            resultsForNonMaybeStates.clear();
+            stepBound = boost::none;
+            instantiationChecker = nullptr;
+            player1Matrix = storm::storage::SparseMatrix<storm::storage::sparse::state_type>();
+            parameterLifter = nullptr;
+            minSchedChoices = boost::none;
+            maxSchedChoices = boost::none;
+            x.clear();
+            lowerResultBound = boost::none;
+            upperResultBound = boost::none;
+            applyPreviousResultAsHint = false;
+        }
+        
+        template <typename SparseModelType, typename ConstantType>
+        boost::optional<storm::storage::Scheduler<ConstantType>> SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::getCurrentMinScheduler() {
+            if (!minSchedChoices) {
+                return boost::none;
             }
             
-            template <typename SparseModelType, typename ConstantType>
-            boost::optional<storm::storage::Scheduler<ConstantType>> SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::getCurrentMinScheduler() {
-                if (!minSchedChoices) {
-                    return boost::none;
-                }
-                
-                storm::storage::Scheduler<ConstantType> result(minSchedChoices->size());
-                uint_fast64_t state = 0;
-                for (auto const& schedulerChoice : minSchedChoices.get()) {
-                    result.setChoice(schedulerChoice, state);
-                    ++state;
-                }
-                
-                return result;
+            storm::storage::Scheduler<ConstantType> result(minSchedChoices->size());
+            uint_fast64_t state = 0;
+            for (auto const& schedulerChoice : minSchedChoices.get()) {
+                result.setChoice(schedulerChoice, state);
+                ++state;
             }
-                    
-            template <typename SparseModelType, typename ConstantType>
-            boost::optional<storm::storage::Scheduler<ConstantType>> SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::getCurrentMaxScheduler() {
-                if (!maxSchedChoices) {
-                    return boost::none;
-                }
-                
-                storm::storage::Scheduler<ConstantType> result(maxSchedChoices->size());
-                uint_fast64_t state = 0;
-                for (auto const& schedulerChoice : maxSchedChoices.get()) {
-                    result.setChoice(schedulerChoice, state);
-                    ++state;
-                }
-                
-                return result;
+            
+            return result;
+        }
+        
+        template <typename SparseModelType, typename ConstantType>
+        boost::optional<storm::storage::Scheduler<ConstantType>> SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::getCurrentMaxScheduler() {
+            if (!maxSchedChoices) {
+                return boost::none;
             }
             
-            template <typename SparseModelType, typename ConstantType>
-            boost::optional<storm::storage::Scheduler<ConstantType>> SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::getCurrentPlayer1Scheduler() {
-                if (!player1SchedChoices) {
-                    return boost::none;
-                }
-                
-                storm::storage::Scheduler<ConstantType> result(player1SchedChoices->size());
-                uint_fast64_t state = 0;
-                for (auto const& schedulerChoice : player1SchedChoices.get()) {
-                    result.setChoice(schedulerChoice, state);
-                    ++state;
-                }
-                
-                return result;
+            storm::storage::Scheduler<ConstantType> result(maxSchedChoices->size());
+            uint_fast64_t state = 0;
+            for (auto const& schedulerChoice : maxSchedChoices.get()) {
+                result.setChoice(schedulerChoice, state);
+                ++state;
             }
-    
-            template class SparseMdpParameterLiftingModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
-            template class SparseMdpParameterLiftingModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, storm::RationalNumber>;
+            
+            return result;
         }
+        
+        template <typename SparseModelType, typename ConstantType>
+        boost::optional<storm::storage::Scheduler<ConstantType>> SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::getCurrentPlayer1Scheduler() {
+            if (!player1SchedChoices) {
+                return boost::none;
+            }
+            
+            storm::storage::Scheduler<ConstantType> result(player1SchedChoices->size());
+            uint_fast64_t state = 0;
+            for (auto const& schedulerChoice : player1SchedChoices.get()) {
+                result.setChoice(schedulerChoice, state);
+                ++state;
+            }
+            
+            return result;
+        }
+
+        template class SparseMdpParameterLiftingModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
+        template class SparseMdpParameterLiftingModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, storm::RationalNumber>;
     }
 }

src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h

@@ -4,60 +4,64 @@
 #include <memory>
 #include <boost/optional.hpp>
 
-#include "storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h"
+#include "storm-pars/transformer/ParameterLifter.h"
+#include "storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h"
+#include "storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.h"
+
 #include "storm/storage/BitVector.h"
 #include "storm/storage/SparseMatrix.h"
 #include "storm/storage/sparse/StateType.h"
 #include "storm/solver/GameSolver.h"
-#include "storm/transformer/ParameterLifter.h"
 #include "storm/storage/Scheduler.h"
 
 namespace storm {
     namespace modelchecker {
-        namespace parametric {
-            
-            template <typename SparseModelType, typename ConstantType>
-            class SparseMdpParameterLiftingModelChecker : public SparseParameterLiftingModelChecker<SparseModelType, ConstantType> {
-            public:
-                SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel);
-                SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr<storm::solver::GameSolverFactory<ConstantType>>&& solverFactory);
+        
+        template <typename SparseModelType, typename ConstantType>
+        class SparseMdpParameterLiftingModelChecker : public SparseParameterLiftingModelChecker<SparseModelType, ConstantType> {
+        public:
+            SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel);
+            SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr<storm::solver::GameSolverFactory<ConstantType>>&& solverFactory);
                 
-                virtual bool canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const override;
+            virtual bool canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const override;
                 
-                boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMinScheduler();
-                boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMaxScheduler();
-                boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentPlayer1Scheduler();
+            boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMinScheduler();
+            boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMaxScheduler();
+            boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentPlayer1Scheduler();
                 
-            protected:
+        protected:
                 
-                virtual void specifyBoundedUntilFormula(CheckTask<storm::logic::BoundedUntilFormula, ConstantType> const& checkTask) override;
-                virtual void specifyUntilFormula(CheckTask<storm::logic::UntilFormula, ConstantType> const& checkTask) override;
-                virtual void specifyReachabilityRewardFormula(CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask) override;
-                virtual void specifyCumulativeRewardFormula(CheckTask<storm::logic::CumulativeRewardFormula, ConstantType> const& checkTask) override;
+            virtual void specifyBoundedUntilFormula(CheckTask<storm::logic::BoundedUntilFormula, ConstantType> const& checkTask) override;
+            virtual void specifyUntilFormula(CheckTask<storm::logic::UntilFormula, ConstantType> const& checkTask) override;
+            virtual void specifyReachabilityRewardFormula(CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask) override;
+            virtual void specifyCumulativeRewardFormula(CheckTask<storm::logic::CumulativeRewardFormula, ConstantType> const& checkTask) override;
                 
-                virtual std::unique_ptr<CheckResult> computeQuantitativeValues(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) override;
+            virtual storm::modelchecker::SparseInstantiationModelChecker<SparseModelType, ConstantType>& getInstantiationChecker() override;
+
+            virtual std::unique_ptr<CheckResult> computeQuantitativeValues(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) override;
                 
-                virtual void reset() override;
+            virtual void reset() override;
                 
 
-            private:
-                void computePlayer1Matrix();
-                
-                storm::storage::BitVector maybeStates;
-                std::vector<ConstantType> resultsForNonMaybeStates;
-                boost::optional<uint_fast64_t> stepBound;
-                
-                storm::storage::SparseMatrix<storm::storage::sparse::state_type> player1Matrix;
-                std::unique_ptr<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>> parameterLifter;
-                std::unique_ptr<storm::solver::GameSolverFactory<ConstantType>> solverFactory;
-                
-                // Results from the most recent solver call.
-                boost::optional<std::vector<uint_fast64_t>> minSchedChoices, maxSchedChoices;
-                boost::optional<std::vector<uint_fast64_t>> player1SchedChoices;
-                std::vector<ConstantType> x;
-                boost::optional<ConstantType> lowerResultBound, upperResultBound;
-                bool applyPreviousResultAsHint;
-            };
-        }
+        private:
+            void computePlayer1Matrix();
+            
+            storm::storage::BitVector maybeStates;
+            std::vector<ConstantType> resultsForNonMaybeStates;
+            boost::optional<uint_fast64_t> stepBound;
+                
+            std::unique_ptr<storm::modelchecker::SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>> instantiationChecker;
+                
+            storm::storage::SparseMatrix<storm::storage::sparse::state_type> player1Matrix;
+            std::unique_ptr<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>> parameterLifter;
+            std::unique_ptr<storm::solver::GameSolverFactory<ConstantType>> solverFactory;
+                
+            // Results from the most recent solver call.
+            boost::optional<std::vector<uint_fast64_t>> minSchedChoices, maxSchedChoices;
+            boost::optional<std::vector<uint_fast64_t>> player1SchedChoices;
+            std::vector<ConstantType> x;
+            boost::optional<ConstantType> lowerResultBound, upperResultBound;
+            bool applyPreviousResultAsHint;
+        };
     }
 }

src/storm-pars/modelchecker/region/SparseMdpRegionChecker.cpp

@@ -1,70 +0,0 @@
-#include "storm/modelchecker/parametric/SparseMdpRegionChecker.h"
-
-#include "storm/adapters/RationalFunctionAdapter.h"
-
-#include "storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h"
-#include "storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.h"
-#include "storm/transformer/SparseParametricMdpSimplifier.h"
-#include "storm/models/sparse/StandardRewardModel.h"
-#include "storm/models/sparse/Mdp.h"
-#include "storm/utility/NumberTraits.h"
-
-
-namespace storm {
-    namespace modelchecker {
-        namespace parametric {
-
-            template <typename SparseModelType, typename ConstantType, typename ExactConstantType>
-            SparseMdpRegionChecker<SparseModelType, ConstantType, ExactConstantType>::SparseMdpRegionChecker(SparseModelType const& parametricModel) : RegionChecker<SparseModelType, ConstantType, ExactConstantType>(parametricModel) {
-                // Intentionally left empty
-            }
-    
-            template <typename SparseModelType, typename ConstantType, typename ExactConstantType>
-            void SparseMdpRegionChecker<SparseModelType, ConstantType, ExactConstantType>::simplifyParametricModel(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
-                storm::transformer::SparseParametricMdpSimplifier<SparseModelType> simplifier(this->parametricModel);
-                if(simplifier.simplify(checkTask.getFormula())) {
-                    this->simplifiedModel = simplifier.getSimplifiedModel();
-                    this->currentFormula = simplifier.getSimplifiedFormula();
-                } else {
-                    this->simplifiedModel = nullptr;
-                    this->currentFormula = checkTask.getFormula().asSharedPointer();
-                }
-            }
-            
-            template <typename SparseModelType, typename ConstantType, typename ExactConstantType>
-            void SparseMdpRegionChecker<SparseModelType, ConstantType, ExactConstantType>::initializeUnderlyingCheckers() {
-                if (this->settings.applyExactValidation) {
-                    STORM_LOG_WARN_COND(!storm::NumberTraits<ConstantType>::IsExact, "Exact validation is not necessarry if the original computation is already exact");
-                    this->exactParameterLiftingChecker = std::make_unique<SparseMdpParameterLiftingModelChecker<SparseModelType, ExactConstantType>>(this->getConsideredParametricModel());
-                }
-                this->parameterLiftingChecker = std::make_unique<SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>>(this->getConsideredParametricModel());
-                this->instantiationChecker = std::make_unique<SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>>(this->getConsideredParametricModel());
-                this->instantiationChecker->setInstantiationsAreGraphPreserving(true);
-            }
-    
-            template <typename SparseModelType, typename ConstantType, typename ExactConstantType>
-            void SparseMdpRegionChecker<SparseModelType, ConstantType, ExactConstantType>::applyHintsToExactChecker() {
-                auto MdpPLChecker = dynamic_cast<storm::modelchecker::parametric::SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>*>(this->parameterLiftingChecker.get());
-                STORM_LOG_ASSERT(MdpPLChecker, "Underlying Parameter lifting checker has unexpected type");
-                auto exactMdpPLChecker = dynamic_cast<storm::modelchecker::parametric::SparseMdpParameterLiftingModelChecker<SparseModelType, ExactConstantType>*>(this->exactParameterLiftingChecker.get());
-                STORM_LOG_ASSERT(exactMdpPLChecker, "Underlying exact parameter lifting checker has unexpected type");
-                if (MdpPLChecker->getCurrentMaxScheduler()) {
-                    exactMdpPLChecker->getCurrentMaxScheduler() = MdpPLChecker->getCurrentMaxScheduler()->template toValueType<ExactConstantType>();
-                }
-                if (MdpPLChecker->getCurrentMinScheduler()) {
-                    exactMdpPLChecker->getCurrentMinScheduler() = MdpPLChecker->getCurrentMinScheduler()->template toValueType<ExactConstantType>();
-                }
-                if (MdpPLChecker->getCurrentPlayer1Scheduler()) {
-                    exactMdpPLChecker->getCurrentPlayer1Scheduler() = MdpPLChecker->getCurrentPlayer1Scheduler()->template toValueType<ExactConstantType>();
-                }
-            }
-            
-       
-#ifdef STORM_HAVE_CARL
-            template class SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double, storm::RationalNumber>;
-            template class SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, storm::RationalNumber>;
-#endif
-        } // namespace parametric
-    } //namespace modelchecker
-} //namespace storm
-

src/storm-pars/modelchecker/region/SparseMdpRegionChecker.h

@@ -1,28 +0,0 @@
-#pragma once
-
-#include <memory>
-
-#include "storm/modelchecker/parametric/RegionChecker.h"
-
-namespace storm {
-    namespace modelchecker{
-        namespace parametric{
-            
-
-            template <typename SparseModelType, typename ConstantType, typename ExactConstantType = ConstantType>
-            class SparseMdpRegionChecker : public RegionChecker<SparseModelType, ConstantType, ExactConstantType> {
-                
-            public:
-                SparseMdpRegionChecker(SparseModelType const& parametricModel);
-                
-            protected:
-
-                virtual void initializeUnderlyingCheckers() override;
-                virtual void simplifyParametricModel(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) override;
-                virtual void applyHintsToExactChecker() override;
-                
-            };
-    
-        } //namespace parametric
-    } //namespace modelchecker
-} //namespace storm

src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp

@@ -13,82 +13,130 @@
 
 namespace storm {
     namespace modelchecker {
-        namespace parametric {
+        
+        template <typename SparseModelType, typename ConstantType>
+        SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseParameterLiftingModelChecker(SparseModelType const& parametricModel) : parametricModel(parametricModel) {
+            //Intentionally left empty
+        }
+        
+        template <typename SparseModelType, typename ConstantType>
+        void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
+            STORM_LOG_ASSERT(this->canHandle(checkTask), "specified formula can not be handled by this.");
+            reset();
+            currentFormula = checkTask.getFormula().asSharedPointer();
+            currentCheckTask = std::make_unique<storm::modelchecker::CheckTask<storm::logic::Formula, ConstantType>>(checkTask.substituteFormula(*currentFormula).template convertValueType<ConstantType>());
             
-            template <typename SparseModelType, typename ConstantType>
-            SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseParameterLiftingModelChecker(SparseModelType const& parametricModel) : parametricModel(parametricModel) {
-                //Intentionally left empty
+            if(currentCheckTask->getFormula().isProbabilityOperatorFormula()) {
+                auto const& probOpFormula = currentCheckTask->getFormula().asProbabilityOperatorFormula();
+                if(probOpFormula.getSubformula().isBoundedUntilFormula()) {
+                    specifyBoundedUntilFormula(currentCheckTask->substituteFormula(probOpFormula.getSubformula().asBoundedUntilFormula()));
+                } else if(probOpFormula.getSubformula().isUntilFormula()) {
+                    specifyUntilFormula(currentCheckTask->substituteFormula(probOpFormula.getSubformula().asUntilFormula()));
+                } else if (probOpFormula.getSubformula().isEventuallyFormula()) {
+                    specifyReachabilityProbabilityFormula(currentCheckTask->substituteFormula(probOpFormula.getSubformula().asEventuallyFormula()));
+                } else {
+                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property.");
+                }
+            } else if (currentCheckTask->getFormula().isRewardOperatorFormula()) {
+                auto const& rewOpFormula = currentCheckTask->getFormula().asRewardOperatorFormula();
+                if(rewOpFormula.getSubformula().isEventuallyFormula()) {
+                    specifyReachabilityRewardFormula(currentCheckTask->substituteFormula(rewOpFormula.getSubformula().asEventuallyFormula()));
+                } else if (rewOpFormula.getSubformula().isCumulativeRewardFormula()) {
+                    specifyCumulativeRewardFormula(currentCheckTask->substituteFormula(rewOpFormula.getSubformula().asCumulativeRewardFormula()));
+                }
             }
+        }
+        
+        template <typename SparseModelType, typename ConstantType>
+        RegionResult SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResult const& initialResult, bool sampleVerticesOfRegion) {
+        
+            STORM_LOG_THROW(this->currentCheckTask->isOnlyInitialStatesRelevantSet(), storm::exceptions::NotSupportedException, "Analyzing regions with parameter lifting requires a property where only the value in the initial states is relevant.");
+            STORM_LOG_THROW(this->currentCheckTask->isBoundSet(), storm::exceptions::NotSupportedException, "Analyzing regions with parameter lifting requires a bounded property.");
+            STORM_LOG_THROW(this->parametricModel.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "Analyzing regions with parameter lifting requires a model with a single initial state.");
             
-            template <typename SparseModelType, typename ConstantType>
-            void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
-                reset();
-                currentFormula = checkTask.getFormula().asSharedPointer();
-                currentCheckTask = std::make_unique<storm::modelchecker::CheckTask<storm::logic::Formula, ConstantType>>(checkTask.substituteFormula(*currentFormula).template convertValueType<ConstantType>());
-                
-                if(currentCheckTask->getFormula().isProbabilityOperatorFormula()) {
-                    auto const& probOpFormula = currentCheckTask->getFormula().asProbabilityOperatorFormula();
-                    if(probOpFormula.getSubformula().isBoundedUntilFormula()) {
-                        specifyBoundedUntilFormula(currentCheckTask->substituteFormula(probOpFormula.getSubformula().asBoundedUntilFormula()));
-                    } else if(probOpFormula.getSubformula().isUntilFormula()) {
-                        specifyUntilFormula(currentCheckTask->substituteFormula(probOpFormula.getSubformula().asUntilFormula()));
-                    } else if (probOpFormula.getSubformula().isEventuallyFormula()) {
-                        specifyReachabilityProbabilityFormula(currentCheckTask->substituteFormula(probOpFormula.getSubformula().asEventuallyFormula()));
-                    } else {
-                        STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property.");
-                    }
-                } else if (currentCheckTask->getFormula().isRewardOperatorFormula()) {
-                    auto const& rewOpFormula = currentCheckTask->getFormula().asRewardOperatorFormula();
-                    if(rewOpFormula.getSubformula().isEventuallyFormula()) {
-                        specifyReachabilityRewardFormula(currentCheckTask->substituteFormula(rewOpFormula.getSubformula().asEventuallyFormula()));
-                    } else if (rewOpFormula.getSubformula().isCumulativeRewardFormula()) {
-                        specifyCumulativeRewardFormula(currentCheckTask->substituteFormula(rewOpFormula.getSubformula().asCumulativeRewardFormula()));
-                    }
-                }
+            RegionResult result = initialResult;
+
+            // Check if we need to check the formula on one point to decide whether to show AllSat or AllViolated
+            if (result == RegionResult::Unknown) {
+                 result = getInstantiationChecker().check(region.getCenterPoint())->asExplicitQualitativeCheckResult()[*this->parametricModel.getInitialStates().begin()] ? RegionResult::CenterSat : RegionResult::CenterViolated;
             }
             
-            template <typename SparseModelType, typename ConstantType>
-            std::unique_ptr<CheckResult> SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::check(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
-                auto quantitativeResult = computeQuantitativeValues(region, dirForParameters);
-                if(currentCheckTask->getFormula().hasQuantitativeResult()) {
-                    return quantitativeResult;
-                } else {
-                    return quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
+            // try to prove AllSat or AllViolated, depending on the obtained result
+            if (result == RegionResult::ExistsSat || result == RegionResult::CenterSat) {
+                // show AllSat:
+                storm::solver::OptimizationDirection parameterOptimizationDirection = isLowerBound(this->currentCheckTask->getBound().comparisonType) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize;
+                if (this->check(region, parameterOptimizationDirection)->asExplicitQualitativeCheckResult()[*this->parametricModel.getInitialStates().begin()]) {
+                    result = RegionResult::AllSat;
+                } else if (sampleVerticesOfRegion) {
+                    // Check if there is a point in the region for which the property is violated
+                    auto vertices = region.getVerticesOfRegion(region.getVariables());
+                    for (auto const& v : vertices) {
+                        if (!getInstantiationChecker().check(v)->asExplicitQualitativeCheckResult()[*this->parametricModel.getInitialStates().begin()]) {
+                            result = RegionResult::ExistsBoth;
+                        }
+                    }
                 }
+            } else if (result == RegionResult::ExistsViolated || result == RegionResult::CenterViolated) {
+                // show AllViolated:
+                storm::solver::OptimizationDirection parameterOptimizationDirection = isLowerBound(this->currentCheckTask->getBound().comparisonType) ? storm::solver::OptimizationDirection::Maximize : storm::solver::OptimizationDirection::Minimize;
+                if (!this->check(region, parameterOptimizationDirection)->asExplicitQualitativeCheckResult()[*this->parametricModel.getInitialStates().begin()]) {
+                    result = RegionResult::AllViolated;
+                } else if (sampleVerticesOfRegion) {
+                    // Check if there is a point in the region for which the property is satisfied
+                    auto vertices = region.getVerticesOfRegion(region.getVariables());
+                    for (auto const& v : vertices) {
+                        if (getInstantiationChecker().check(v)->asExplicitQualitativeCheckResult()[*this->parametricModel.getInitialStates().begin()]) {
+                            result = RegionResult::ExistsBoth;
+                        }
+                    }
+                }
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "When analyzing a region, an invalid initial result was given: " << initialResult);
             }
-    
-            template <typename SparseModelType, typename ConstantType>
-            void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyBoundedUntilFormula(CheckTask<logic::BoundedUntilFormula, ConstantType> const& checkTask) {
-                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property.");
-            }
-    
-            template <typename SparseModelType, typename ConstantType>
-            void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyUntilFormula(CheckTask<logic::UntilFormula, ConstantType> const& checkTask) {
-                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property.");
-            }
-    
-            template <typename SparseModelType, typename ConstantType>
-            void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyReachabilityProbabilityFormula(CheckTask<logic::EventuallyFormula, ConstantType> const& checkTask) {
-                // transform to until formula
-                auto untilFormula = std::make_shared<storm::logic::UntilFormula const>(storm::logic::Formula::getTrueFormula(), checkTask.getFormula().getSubformula().asSharedPointer());
-                specifyUntilFormula(currentCheckTask->substituteFormula(*untilFormula));
-            }
-    
-            template <typename SparseModelType, typename ConstantType>
-            void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyReachabilityRewardFormula(CheckTask<logic::EventuallyFormula, ConstantType> const& checkTask) {
-                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property.");
-            }
-    
-            template <typename SparseModelType, typename ConstantType>
-            void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyCumulativeRewardFormula(CheckTask<logic::CumulativeRewardFormula, ConstantType> const& checkTask) {
-                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property.");
+            return result;
+        }
+
+        template <typename SparseModelType, typename ConstantType>
+        std::unique_ptr<CheckResult> SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::check(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
+            auto quantitativeResult = computeQuantitativeValues(region, dirForParameters);
+            if(currentCheckTask->getFormula().hasQuantitativeResult()) {
+                return quantitativeResult;
+            } else {
+                return quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
             }
-    
-            template class SparseParameterLiftingModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
-            template class SparseParameterLiftingModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
-            template class SparseParameterLiftingModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber>;
-            template class SparseParameterLiftingModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, storm::RationalNumber>;
+        }
+
+        template <typename SparseModelType, typename ConstantType>
+        void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyBoundedUntilFormula(CheckTask<logic::BoundedUntilFormula, ConstantType> const& checkTask) {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property.");
+        }
 
+        template <typename SparseModelType, typename ConstantType>
+        void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyUntilFormula(CheckTask<logic::UntilFormula, ConstantType> const& checkTask) {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property.");
         }
+
+        template <typename SparseModelType, typename ConstantType>
+        void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyReachabilityProbabilityFormula(CheckTask<logic::EventuallyFormula, ConstantType> const& checkTask) {
+            // transform to until formula
+            auto untilFormula = std::make_shared<storm::logic::UntilFormula const>(storm::logic::Formula::getTrueFormula(), checkTask.getFormula().getSubformula().asSharedPointer());
+            specifyUntilFormula(currentCheckTask->substituteFormula(*untilFormula));
+        }
+
+        template <typename SparseModelType, typename ConstantType>
+        void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyReachabilityRewardFormula(CheckTask<logic::EventuallyFormula, ConstantType> const& checkTask) {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property.");
+        }
+
+        template <typename SparseModelType, typename ConstantType>
+        void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyCumulativeRewardFormula(CheckTask<logic::CumulativeRewardFormula, ConstantType> const& checkTask) {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property.");
+        }
+
+        template class SparseParameterLiftingModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
+        template class SparseParameterLiftingModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
+        template class SparseParameterLiftingModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber>;
+        template class SparseParameterLiftingModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, storm::RationalNumber>;
+
     }
 }

src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h

@@ -1,60 +1,74 @@
 #pragma once
 
+#include "storm-pars/modelchecker/region/RegionModelChecker.h"
+#include "storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.h"
+#include "storm-pars/storage/ParameterRegion.h"
+#include "storm-pars/utility/parametric.h"
+
 #include "storm/logic/Formulas.h"
 #include "storm/modelchecker/CheckTask.h"
 #include "storm/modelchecker/results/CheckResult.h"
-#include "storm/storage/ParameterRegion.h"
 #include "storm/solver/OptimizationDirection.h"
-#include "storm/utility/parametric.h"
 
 namespace storm {
     namespace modelchecker {
-        namespace parametric {
             
+        /*!
+         * Class to approximatively check a formula on a parametric model for all parameter valuations within a region
+         * It is assumed that all considered valuations are graph-preserving and well defined, i.e.,
+         * * all non-const transition probabilities evaluate to some non-zero value
+         * * the sum of all outgoing transitions is one
+         */
+        template <typename SparseModelType, typename ConstantType>
+        class SparseParameterLiftingModelChecker : public RegionModelChecker<typename SparseModelType::ValueType> {
+        public:
+            SparseParameterLiftingModelChecker(SparseModelType const& parametricModel);
+            virtual ~SparseParameterLiftingModelChecker() = default;
+            
+            virtual void specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) override;
+
             /*!
-             * Class to approximatively check a formula on a parametric model for all parameter valuations within a region
-             * It is assumed that all considered valuations are graph-preserving and well defined, i.e.,
-             * * all non-const transition probabilities evaluate to some non-zero value
-             * * the sum of all outgoing transitions is one
+             * Analyzes the given region by means of parameter lifting.
+             * We first check whether there is one point in the region for which the property is satisfied/violated.
+             * If the given initialResults already indicates that there is such a point, this step is skipped.
+             * Then, we check whether ALL points in the region violate/satisfy the property
+             *
              */
-            template <typename SparseModelType, typename ConstantType>
-            class SparseParameterLiftingModelChecker {
-            public:
-                SparseParameterLiftingModelChecker(SparseModelType const& parametricModel);
-                virtual ~SparseParameterLiftingModelChecker() = default;
-                
-                virtual bool canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const = 0;
-                
-                void specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask);
-    
-                /*!
-                 * Checks the specified formula on the given region by applying parameter lifting (Parameter choices are lifted to nondeterministic choices)
-                 * This yields a (sound) approximative model checking result.
-
-                 * @param region the region on which parameter lifting is applied
-                 * @param dirForParameters  The optimization direction for the parameter choices. If this is, e.g., minimize, then the returned result will be a lower bound for all results induced by the parameter evaluations inside the region.
-                 */
-                std::unique_ptr<CheckResult> check(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters);
-                
-            protected:
-                
-                virtual void specifyBoundedUntilFormula(CheckTask<storm::logic::BoundedUntilFormula, ConstantType> const& checkTask);
-                virtual void specifyUntilFormula(CheckTask<storm::logic::UntilFormula, ConstantType> const& checkTask);
-                virtual void specifyReachabilityProbabilityFormula(CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask);
-                virtual void specifyReachabilityRewardFormula(CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask);
-                virtual void specifyCumulativeRewardFormula(CheckTask<storm::logic::CumulativeRewardFormula, ConstantType> const& checkTask);
-                
-                virtual std::unique_ptr<CheckResult> computeQuantitativeValues(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) = 0;
-                
-                virtual void reset() = 0;
-                
-                SparseModelType const& parametricModel;
-                std::unique_ptr<CheckTask<storm::logic::Formula, ConstantType>> currentCheckTask;
-              
-            private:
-                // store the current formula. Note that currentCheckTask only stores a reference to the formula.
-                std::shared_ptr<storm::logic::Formula const> currentFormula;
-            };
-        }
+            virtual RegionResult analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResult const& initialResult = RegionResult::Unknown, bool sampleVerticesOfRegion = false) override;
+
+            /*!
+             * Checks the specified formula on the given region by applying parameter lifting (Parameter choices are lifted to nondeterministic choices)
+             * This yields a (sound) approximative model checking result.
+
+             * @param region the region on which parameter lifting is applied
+             * @param dirForParameters  The optimization direction for the parameter choices. If this is, e.g., minimize, then the returned result will be a lower bound for all results induced by the parameter evaluations inside the region.
+             */
+            std::unique_ptr<CheckResult> check(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters);
+            
+        protected:
+            
+            // Resets all data that correspond to the currently defined property.
+            virtual void reset() = 0;
+
+            virtual void specifyBoundedUntilFormula(CheckTask<storm::logic::BoundedUntilFormula, ConstantType> const& checkTask);
+            virtual void specifyUntilFormula(CheckTask<storm::logic::UntilFormula, ConstantType> const& checkTask);
+            virtual void specifyReachabilityProbabilityFormula(CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask);
+            virtual void specifyReachabilityRewardFormula(CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask);
+            virtual void specifyCumulativeRewardFormula(CheckTask<storm::logic::CumulativeRewardFormula, ConstantType> const& checkTask);
+
+            
+            virtual storm::modelchecker::SparseInstantiationModelChecker<SparseModelType, ConstantType>& getInstantiationChecker() = 0;
+            
+            virtual std::unique_ptr<CheckResult> computeQuantitativeValues(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) = 0;
+            
+            
+            SparseModelType const& parametricModel;
+            std::unique_ptr<CheckTask<storm::logic::Formula, ConstantType>> currentCheckTask;
+
+        private:
+            // store the current formula. Note that currentCheckTask only stores a reference to the formula.
+            std::shared_ptr<storm::logic::Formula const> currentFormula;
+            
+        };
     }
 }

src/storm-pars/modelchecker/results/RegionCheckResult.cpp

@@ -0,0 +1,112 @@
+#include "storm-pars/modelchecker/results/RegionCheckResult.h"
+
+#include <map>
+
+#include "storm/adapters/RationalFunctionAdapter.h"
+#include "storm/utility/constants.h"
+#include "storm/utility/macros.h"
+
+namespace storm {
+    namespace modelchecker {
+
+        template<typename ValueType>
+        RegionCheckResult<ValueType>::RegionCheckResult(std::vector<std::pair<storm::storage::ParameterRegion<ValueType>, storm::modelchecker::RegionResult>> const& regionResults) : regionResults(regionResults) {
+            auto overallArea = storm::utility::zero<typename storm::storage::ParameterRegion<ValueType>::CoefficientType>();
+            for (auto const& res : this->regionResults) {
+                overallArea += res.first.area();
+            }
+            initFractions(overallArea);
+        }
+        
+        template<typename ValueType>
+        RegionCheckResult<ValueType>::RegionCheckResult(std::vector<std::pair<storm::storage::ParameterRegion<ValueType>, storm::modelchecker::RegionResult>>&& regionResults) : regionResults(std::move(regionResults)) {
+            auto overallArea = storm::utility::zero<typename storm::storage::ParameterRegion<ValueType>::CoefficientType>();
+            for (auto const& res : this->regionResults) {
+                overallArea += res.first.area();
+            }
+            initFractions(overallArea);
+        }
+
+        template<typename ValueType>
+        bool RegionCheckResult<ValueType>::isRegionCheckResult() const {
+            return true;
+        }
+        
+        template<typename ValueType>
+        bool RegionCheckResult<ValueType>::isRegionRefinementCheckResult() const {
+            return false;
+        }
+            
+        template<typename ValueType>
+        std::vector<std::pair<storm::storage::ParameterRegion<ValueType>, storm::modelchecker::RegionResult>> const& RegionCheckResult<ValueType>::getRegionResults() const {
+            return regionResults;
+        }
+        
+        template<typename ValueType>
+        typename storm::storage::ParameterRegion<ValueType>::CoefficientType const& RegionCheckResult<ValueType>::getSatFraction() const {
+            return satFraction;
+        }
+        
+        template<typename ValueType>
+        typename storm::storage::ParameterRegion<ValueType>::CoefficientType const& RegionCheckResult<ValueType>::getUnsatFraction() const {
+            return unsatFraction;
+        }
+
+        template<typename ValueType>
+        std::ostream& RegionCheckResult<ValueType>::writeToStream(std::ostream& out) const {
+            writeCondensedToStream(out);
+            out << std::endl << "Region results: " << std::endl;
+            for (auto const& res : this->regionResults) {
+                out << res.first.toString() << ": \t" << res.second << std::endl;
+            }
+        }
+        
+        template<typename ValueType>
+        std::ostream& RegionCheckResult<ValueType>::writeCondensedToStream(std::ostream& out) const {
+            auto oneHundred = storm::utility::convertNumber<typename storm::storage::ParameterRegion<ValueType>::CoefficientType>(100.0);
+            auto one = storm::utility::convertNumber<typename storm::storage::ParameterRegion<ValueType>::CoefficientType>(1.0);
+            out << "Fraction of satisfied area:   " << (satFraction * oneHundred) << std::endl;
+            out << "Fraction of unsatisfied area: " << (unsatFraction * oneHundred) << std::endl;
+            out << "Unknown fraction:             " << ((one - satFraction - unsatFraction) * oneHundred) << std::endl;
+            out << "Total Number of regions:      " << regionResults.size() << std::endl;
+            std::map<storm::modelchecker::RegionResult, uint_fast64_t> counters;
+            for (auto const& res : this->regionResults) {
+                ++counters[res.second];
+            }
+            for (auto const& counter : counters) {
+                out << std::setw(28) << counter.first << ": " << counter.second << std::endl;
+            }
+        }
+
+        template<typename ValueType>
+        std::ostream& RegionCheckResult<ValueType>::writeIllustrationToStream(std::ostream& out) const {
+            STORM_LOG_WARN("Writing illustration of region check result to a stream is not implemented.");
+        }
+  
+        template<typename ValueType>
+        void RegionCheckResult<ValueType>::initFractions(typename storm::storage::ParameterRegion<ValueType>::CoefficientType const& overallArea) {
+            auto satArea = storm::utility::zero<typename storm::storage::ParameterRegion<ValueType>::CoefficientType>();
+            auto unsatArea = storm::utility::zero<typename storm::storage::ParameterRegion<ValueType>::CoefficientType>();
+            for (auto const& res : this->regionResults) {
+                if (res.second == storm::modelchecker::RegionResult::AllSat) {
+                    satArea += res.first.area();
+                } else if (res.second == storm::modelchecker::RegionResult::AllViolated) {
+                    unsatArea += res.first.area();
+                }
+            }
+            satFraction = satArea / overallArea;
+            unsatFraction = unsatArea / overallArea;
+        }
+        
+        template<typename ValueType>
+        void RegionCheckResult<ValueType>::filter(QualitativeCheckResult const& filter) {
+            // Filtering has no effect as we only store the result w.r.t. a single state anyway.
+            // Hence, this is intentionally left empty.
+        }
+
+        
+#ifdef STORM_HAVE_CARL
+        template class RegionCheckResult<storm::RationalFunction>;
+#endif
+    }
+}

src/storm-pars/modelchecker/results/RegionCheckResult.h

@@ -0,0 +1,40 @@
+#pragma once
+
+#include <vector>
+
+#include "storm/modelchecker/results/CheckResult.h"
+#include "storm-pars/modelchecker/region/RegionResult.h"
+#include "storm-pars/storage/ParameterRegion.h"
+
+namespace storm {
+    namespace modelchecker {
+        template<typename ValueType>
+        class RegionCheckResult : public CheckResult {
+        public:
+
+            RegionCheckResult(std::vector<std::pair<storm::storage::ParameterRegion<ValueType>, storm::modelchecker::RegionResult>> const& regionResults);
+            RegionCheckResult(std::vector<std::pair<storm::storage::ParameterRegion<ValueType>, storm::modelchecker::RegionResult>>&& regionResults);
+            virtual ~RegionCheckResult() = default;
+
+            virtual bool isRegionCheckResult() const;
+            virtual bool isRegionRefinementCheckResult() const;
+            
+            std::vector<std::pair<storm::storage::ParameterRegion<ValueType>, storm::modelchecker::RegionResult>> const& getRegionResults() const;
+            typename storm::storage::ParameterRegion<ValueType>::CoefficientType const& getSatFraction() const;
+            typename storm::storage::ParameterRegion<ValueType>::CoefficientType const& getUnsatFraction() const;
+            
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            virtual std::ostream& writeCondensedToStream(std::ostream& out) const;
+            virtual std::ostream& writeIllustrationToStream(std::ostream& out) const;
+
+            virtual void filter(QualitativeCheckResult const& filter) override;
+            
+        protected:
+            virtual void initFractions(typename storm::storage::ParameterRegion<ValueType>::CoefficientType const& overallArea);
+            
+            std::vector<std::pair<storm::storage::ParameterRegion<ValueType>, storm::modelchecker::RegionResult>> regionResults;
+            typename storm::storage::ParameterRegion<ValueType>::CoefficientType satFraction, unsatFraction;
+
+        };
+    }
+}

src/storm-pars/modelchecker/results/RegionRefinementCheckResult.cpp

@@ -0,0 +1,100 @@
+#include "storm-pars/modelchecker/results/RegionRefinementCheckResult.h"
+
+#include <map>
+
+#include "storm/adapters/RationalFunctionAdapter.h"
+#include "storm/utility/constants.h"
+#include "storm/utility/macros.h"
+
+namespace storm {
+    namespace modelchecker {
+
+        template<typename ValueType>
+        RegionRefinementCheckResult<ValueType>::RegionRefinementCheckResult(std::vector<std::pair<storm::storage::ParameterRegion<ValueType>, storm::modelchecker::RegionResult>> const& regionResults, storm::storage::ParameterRegion<ValueType> const& parameterSpace) : RegionCheckResult<ValueType>(regionResults), parameterSpace(parameterSpace) {
+            this->initFractions(this->parameterSpace.area());
+        }
+        
+        
+        template<typename ValueType>
+        RegionRefinementCheckResult<ValueType>::RegionRefinementCheckResult(std::vector<std::pair<storm::storage::ParameterRegion<ValueType>, storm::modelchecker::RegionResult>>&& regionResults, storm::storage::ParameterRegion<ValueType>&& parameterSpace) : RegionCheckResult<ValueType>(std::move(regionResults)), parameterSpace(std::move(parameterSpace)) {
+            this->initFractions(this->parameterSpace.area());
+        }
+        
+        template<typename ValueType>
+        bool RegionRefinementCheckResult<ValueType>::isRegionRefinementCheckResult() const {
+            return true;
+        }
+        
+        template<typename ValueType>
+        storm::storage::ParameterRegion<ValueType> const& RegionRefinementCheckResult<ValueType>::getParameterSpace() const {
+            return parameterSpace;
+        }
+
+        template<typename ValueType>
+        std::ostream& RegionRefinementCheckResult<ValueType>::writeIllustrationToStream(std::ostream& out) const {
+            if (this->getParameterSpace().getVariables().size() == 2) {
+                
+                typedef typename storm::storage::ParameterRegion<ValueType>::CoefficientType CoefficientType;
+                auto x = *this->getParameterSpace().getVariables().begin();
+                auto y = *(this->getParameterSpace().getVariables().rbegin());
+            
+                uint_fast64_t const sizeX = 128;
+                uint_fast64_t const sizeY = 64;
+                
+                out << "Region refinement Check result (visualization):" << std::endl;
+                out << " \t x-axis: " << x << "  \t y-axis: " << y << "  \t S=safe, [ ]=unsafe, -=ambiguous " << std::endl;
+                for (uint_fast64_t i = 0; i < sizeX+2; ++i) out << "#"; out << std::endl;
+                
+                CoefficientType deltaX = (getParameterSpace().getUpperBoundary(x) - getParameterSpace().getLowerBoundary(x)) / storm::utility::convertNumber<CoefficientType>(sizeX);
+                CoefficientType deltaY = (getParameterSpace().getUpperBoundary(y) - getParameterSpace().getLowerBoundary(y)) / storm::utility::convertNumber<CoefficientType>(sizeY);
+                CoefficientType printedRegionArea = deltaX * deltaY;
+                for (CoefficientType yUpper = getParameterSpace().getUpperBoundary(y); yUpper != getParameterSpace().getLowerBoundary(y); yUpper -= deltaY) {
+                    CoefficientType yLower = yUpper - deltaY;
+                    out << "#";
+                    for (CoefficientType xLower = getParameterSpace().getLowerBoundary(x); xLower != getParameterSpace().getUpperBoundary(x); xLower += deltaX) {
+                        CoefficientType xUpper = xLower + deltaX;
+                        bool currRegionSafe = false;
+                        bool currRegionUnSafe = false;
+                        bool currRegionComplete = false;
+                        CoefficientType coveredArea = storm::utility::zero<CoefficientType>();
+                        for (auto const& r : this->getRegionResults()) {
+                            CoefficientType interesctionSizeY = std::min(yUpper, r.first.getUpperBoundary(y)) - std::max(yLower, r.first.getLowerBoundary(y));
+                            interesctionSizeY = std::max(interesctionSizeY, storm::utility::zero<CoefficientType>());
+                            CoefficientType interesctionSizeX = std::min(xUpper, r.first.getUpperBoundary(x)) - std::max(xLower, r.first.getLowerBoundary(x));
+                            interesctionSizeX = std::max(interesctionSizeX, storm::utility::zero<CoefficientType>());
+                            CoefficientType instersectionArea =  interesctionSizeY * interesctionSizeX;
+                            if(!storm::utility::isZero(instersectionArea)) {
+                                currRegionSafe = currRegionSafe || r.second == storm::modelchecker::RegionResult::AllSat;
+                                currRegionUnSafe = currRegionUnSafe || r.second == storm::modelchecker::RegionResult::AllViolated;
+                                coveredArea += instersectionArea;
+                                if(currRegionSafe && currRegionUnSafe) {
+                                    break;
+                                }
+                                if(coveredArea == printedRegionArea) {
+                                    currRegionComplete = true;
+                                    break;
+                                }
+                            }
+                        }
+                        if (currRegionComplete && currRegionSafe && !currRegionUnSafe) {
+                            out << "S";
+                        } else if (currRegionComplete && currRegionUnSafe && !currRegionSafe) {
+                            out << " ";
+                        } else {
+                            out << "-";
+                        }
+                    }
+                    out << "#" << std::endl;
+                }
+                for (uint_fast64_t i = 0; i < sizeX+2; ++i) out << "#"; out << std::endl;
+            } else {
+                STORM_LOG_WARN("Writing illustration of region check result to a stream is only implemented for two parameters.");
+            }
+            return out;
+        }
+        
+#ifdef STORM_HAVE_CARL
+        template class RegionRefinementCheckResult<storm::RationalFunction>;
+#endif
+    }
+}

src/storm-pars/modelchecker/results/RegionRefinementCheckResult.h

@@ -0,0 +1,30 @@
+#pragma once
+
+#include <vector>
+
+#include "storm-pars/modelchecker/results/RegionCheckResult.h"
+#include "storm-pars/modelchecker/region/RegionResult.h"
+#include "storm-pars/storage/ParameterRegion.h"
+
+namespace storm {
+    namespace modelchecker {
+        template<typename ValueType>
+        class RegionRefinementCheckResult : public RegionCheckResult<ValueType> {
+        public:
+
+            RegionRefinementCheckResult(std::vector<std::pair<storm::storage::ParameterRegion<ValueType>, storm::modelchecker::RegionResult>> const& regionResults, storm::storage::ParameterRegion<ValueType> const& parameterSpace);
+            RegionRefinementCheckResult(std::vector<std::pair<storm::storage::ParameterRegion<ValueType>, storm::modelchecker::RegionResult>>&& regionResults, storm::storage::ParameterRegion<ValueType>&& parameterSpace);
+            virtual ~RegionRefinementCheckResult() = default;
+
+            virtual bool isRegionRefinementCheckResult() const override;
+            
+            storm::storage::ParameterRegion<ValueType> const& getParameterSpace() const;
+
+            virtual std::ostream& writeIllustrationToStream(std::ostream& out) const override;
+            
+
+        protected:
+            storm::storage::ParameterRegion<ValueType> parameterSpace;
+        };
+    }
+}

src/storm-pars/parser/ParameterRegionParser.cpp

@@ -0,0 +1,97 @@
+#include "storm-pars/parser/ParameterRegionParser.h"
+
+#include "storm/utility/macros.h"
+#include "storm/exceptions/InvalidArgumentException.h"
+#include "storm/utility/constants.h"
+#include "storm/utility/file.h"
+
+namespace storm {
+    namespace parser {
+
+        template<typename ParametricType>
+        void ParameterRegionParser<ParametricType>::parseParameterBoundaries(Valuation& lowerBoundaries, Valuation& upperBoundaries, std::string const& parameterBoundariesString, std::set<VariableType> const& consideredVariables) {
+            
+            std::string::size_type positionOfFirstRelation = parameterBoundariesString.find("<=");
+            STORM_LOG_THROW(positionOfFirstRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find  a '<=' after the first number");
+            std::string::size_type positionOfSecondRelation = parameterBoundariesString.find("<=", positionOfFirstRelation+2);
+            STORM_LOG_THROW(positionOfSecondRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find  a '<=' after the parameter");
+
+            std::string parameter = parameterBoundariesString.substr(positionOfFirstRelation+2,positionOfSecondRelation-(positionOfFirstRelation+2));
+            //removes all whitespaces from the parameter string:
+            parameter.erase(std::remove_if (parameter.begin(), parameter.end(), ::isspace), parameter.end());
+            STORM_LOG_THROW(parameter.length()>0, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a parameter");
+
+            std::unique_ptr<VariableType> var;
+            for (auto const& v : consideredVariables) {
+                std::stringstream stream;
+                stream << v;
+                std::string vAsString = stream.str();
+                if (parameter == stream.str()) {
+                    var = std::make_unique<VariableType>(v);
+                }
+            }
+            STORM_LOG_ASSERT(var, "Could not find parameter " << parameter << " in the set of considered variables");
+            
+            CoefficientType lb = storm::utility::convertNumber<CoefficientType>(parameterBoundariesString.substr(0,positionOfFirstRelation));
+            CoefficientType ub = storm::utility::convertNumber<CoefficientType>(parameterBoundariesString.substr(positionOfSecondRelation+2));
+            lowerBoundaries.emplace(std::make_pair(*var, lb));
+            upperBoundaries.emplace(std::make_pair(*var, ub));
+        }
+
+        template<typename ParametricType>
+        storm::storage::ParameterRegion<ParametricType> ParameterRegionParser<ParametricType>::parseRegion(std::string const& regionString, std::set<VariableType> const& consideredVariables) {
+            Valuation lowerBoundaries;
+            Valuation upperBoundaries;
+            std::vector<std::string> parameterBoundaries;
+            boost::split(parameterBoundaries, regionString, boost::is_any_of(","));
+            for (auto const& parameterBoundary : parameterBoundaries){
+                if (!std::all_of(parameterBoundary.begin(),parameterBoundary.end(), ::isspace)){ //skip this string if it only consists of space
+                    parseParameterBoundaries(lowerBoundaries, upperBoundaries, parameterBoundary, consideredVariables);
+                }
+            }
+            return storm::storage::ParameterRegion<ParametricType>(std::move(lowerBoundaries), std::move(upperBoundaries));
+        }
+
+        template<typename ParametricType>
+        std::vector<storm::storage::ParameterRegion<ParametricType>> ParameterRegionParser<ParametricType>::parseMultipleRegions(std::string const& regionsString, std::set<VariableType> const& consideredVariables) {
+            std::vector<storm::storage::ParameterRegion<ParametricType>> result;
+            std::vector<std::string> regionsStrVec;
+            boost::split(regionsStrVec, regionsString, boost::is_any_of(";"));
+            for (auto const& regionStr : regionsStrVec){
+                if (!std::all_of(regionStr.begin(),regionStr.end(), ::isspace)){ //skip this string if it only consists of space
+                    result.emplace_back(parseRegion(regionStr, consideredVariables));
+                }
+            }
+            return result;
+        }
+
+        template<typename ParametricType>
+        std::vector<storm::storage::ParameterRegion<ParametricType>> ParameterRegionParser<ParametricType>::parseMultipleRegionsFromFile(std::string const& fileName, std::set<VariableType> const& consideredVariables) {
+     
+            // Open file and initialize result.
+            std::ifstream inputFileStream;
+            storm::utility::openFile(fileName, inputFileStream);
+            
+            std::vector<storm::storage::ParameterRegion<ParametricType>> result;
+            
+            // Now try to parse the contents of the file.
+            try {
+                std::string fileContent((std::istreambuf_iterator<char>(inputFileStream)), (std::istreambuf_iterator<char>()));
+                result = parseMultipleRegions(fileContent, consideredVariables);
+            } catch(std::exception& e) {
+                // In case of an exception properly close the file before passing exception.
+                storm::utility::closeFile(inputFileStream);
+                throw e;
+            }
+            
+            // Close the stream in case everything went smoothly and return result.
+            storm::utility::closeFile(inputFileStream);
+            return result;
+        }
+        
+#ifdef STORM_HAVE_CARL
+            template class ParameterRegionParser<storm::RationalFunction>;
+#endif
+    }
+}
+

src/storm-pars/parser/ParameterRegionParser.h

@@ -0,0 +1,47 @@
+#pragma once
+
+#include <map>
+
+#include "storm-pars/storage/ParameterRegion.h"
+
+namespace storm {
+    namespace parser {
+        template<typename ParametricType>
+        class ParameterRegionParser{
+        public:
+
+            typedef typename storm::storage::ParameterRegion<ParametricType>::VariableType VariableType;
+            typedef typename storm::storage::ParameterRegion<ParametricType>::CoefficientType CoefficientType;
+            typedef typename storm::storage::ParameterRegion<ParametricType>::Valuation Valuation;
+            
+            /*
+             * Parse a single parameter with its boundaries from a string of the form "0.3<=p<=0.5".
+             * The results will be inserted in the given maps
+             *
+             */
+            static void parseParameterBoundaries( Valuation& lowerBoundaries, Valuation& upperBoundaries, std::string const& parameterBoundariesString, std::set<VariableType> const& consideredVariables);
+
+            /*
+             * Parse a single region from a string of the form "0.3<=p<=0.5,0.4<=q<=0.7".
+             *
+             */
+            static storm::storage::ParameterRegion<ParametricType> parseRegion(std::string const& regionString, std::set<VariableType> const& consideredVariables);
+
+            /*
+             * Parse a vector of region from a string of the form "0.3<=p<=0.5,0.4<=q<=0.7;0.1<=p<=0.3,0.2<=q<=0.4".
+             *
+             */
+            static std::vector<storm::storage::ParameterRegion<ParametricType>> parseMultipleRegions(std::string const& regionsString, std::set<VariableType> const& consideredVariables);
+            
+
+            /*
+             * Parse multiple regions from a file
+             *
+             */
+            static std::vector<storm::storage::ParameterRegion<ParametricType>> parseMultipleRegionsFromFile(std::string const& fileName, std::set<VariableType> const& consideredVariables);
+            
+        };
+    }
+}
+
+

src/storm-pars/settings/modules/ParametricSettings.cpp

@@ -1,4 +1,4 @@
-#include "storm/settings/modules/ParametricSettings.h"
+#include "storm-pars/settings/modules/ParametricSettings.h"
 
 #include "storm/settings/Option.h"
 #include "storm/settings/OptionBuilder.h"
@@ -13,71 +13,27 @@ namespace storm {
         namespace modules {
             
             const std::string ParametricSettings::moduleName = "parametric";
-            const std::string ParametricSettings::encodeSmt2StrategyOptionName = "smt2strategy";
-            const std::string ParametricSettings::exportSmt2DestinationPathOptionName = "smt2path";
-            const std::string ParametricSettings::exportResultDestinationPathOptionName = "resultfile";
-            const std::string ParametricSettings::parameterSpaceOptionName = "parameterspace";
-            const std::string ParametricSettings::refinementThresholdOptionName = "refinementthreshold";
-            const std::string ParametricSettings::exactValidationOptionName = "exactvalidation";
+            const std::string ParametricSettings::exportResultOptionName = "resultfile";
+            const std::string ParametricSettings::simplifyOptionName = "simplify";
             const std::string ParametricSettings::derivativesOptionName = "derivatives";
             
             ParametricSettings::ParametricSettings() : ModuleSettings(moduleName) {
-                this->addOption(storm::settings::OptionBuilder(moduleName, encodeSmt2StrategyOptionName, true, "Set the smt2 encoding strategy.")
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("strategy", "the used strategy").build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, exportSmt2DestinationPathOptionName, true, "A path to a file where the result should be saved.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, exportResultOptionName, true, "A path to a file where the parametric result should be saved.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "the location.").addValidatorString(ArgumentValidatorFactory::createWritableFileValidator()).build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, exportResultDestinationPathOptionName, true, "A path to a file where the smt2 encoding should be saved.")
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "the location.").addValidatorString(ArgumentValidatorFactory::createWritableFileValidator()).build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, parameterSpaceOptionName, true, "Sets the considered parameter-space (i.e., the initial region) for parameter lifting.")
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("region", "The parameter-space (given in format a<=x<=b,c<=y<=d).").build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, refinementThresholdOptionName, true, "Parameter space refinement converges if the fraction of unknown area falls below this threshold.")
-                                .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("threshold", "The threshold").setDefaultValueDouble(0.05).addValidatorDouble(storm::settings::ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0,1.0)).build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, exactValidationOptionName, true, "Sets whether numerical results from Parameter lifting should be validated with exact techniques.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, simplifyOptionName, true, "Sets whether to perform simplification steps before model analysis.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, derivativesOptionName, true, "Sets whether to generate the derivatives of the resulting rational function.").build());
             }
             
             bool ParametricSettings::exportResultToFile() const {
-                return this->getOption(exportResultDestinationPathOptionName).getHasOptionBeenSet();
+                return this->getOption(exportResultOptionName).getHasOptionBeenSet();
             }
             
             std::string ParametricSettings::exportResultPath() const {
-                return this->getOption(exportResultDestinationPathOptionName).getArgumentByName("path").getValueAsString();
-            }
-            
-            bool ParametricSettings::isParameterSpaceSet() const {
-                return this->getOption(parameterSpaceOptionName).getHasOptionBeenSet();
-            }
-            
-            std::string ParametricSettings::getParameterSpace() const {
-                return this->getOption(parameterSpaceOptionName).getArgumentByName("region").getValueAsString();
-            }
-            
-            double ParametricSettings::getRefinementThreshold() const {
-                return this->getOption(refinementThresholdOptionName).getArgumentByName("threshold").getValueAsDouble();
-            }
-            
-            bool ParametricSettings::isExactValidationSet() const {
-                return this->getOption(exactValidationOptionName).getHasOptionBeenSet();
-            }
-            
-            bool ParametricSettings::exportToSmt2File() const {
-                return this->getOption(exportSmt2DestinationPathOptionName).getHasOptionBeenSet();
-            }
-            
-            std::string ParametricSettings::exportSmt2Path() const {
-                return this->getOption(exportSmt2DestinationPathOptionName).getArgumentByName("path").getValueAsString();
+                return this->getOption(exportResultOptionName).getArgumentByName("path").getValueAsString();
             }
             
-            ParametricSettings::Smt2EncodingStrategy ParametricSettings::smt2EncodingStrategy() const {
-                std::string strategy = this->getOption(encodeSmt2StrategyOptionName).getArgumentByName("strategy").getValueAsString();
-                
-                if(strategy == "fts") {
-                    return Smt2EncodingStrategy::FULL_TRANSITION_SYSTEM;
-                } else if(strategy == "rf") {
-                    return Smt2EncodingStrategy::RATIONAL_FUNCTION;
-                } else {
-                    STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown smt2encoding strategy '" << strategy << "'.");
-                }
+            bool ParametricSettings::isSimplifySet() const {
+                return this->getOption(simplifyOptionName).getHasOptionBeenSet();
             }
             
             bool ParametricSettings::isDerivativesSet() const {

src/storm-pars/settings/modules/ParametricSettings.h

@@ -30,28 +30,12 @@ namespace storm {
                  */
 				std::string exportResultPath() const;
 				
-				/*!
-				 * Retrieves whether the parameter space was declared
-				 */
-				bool isRegionSet() const;
-				
-				/*!
-				 * Retrieves the given parameter spcae
-				 */
-				std::string getRegionString() const;
-				
-				/*!
-				 * Retrieves the threshold considered for iterative region refinement.
-				 * The refinement converges as soon as the fraction of unknown area falls below this threshold
-				 */
-				double getRefinementThreshold() const;
-				
-				/*!
-				 * Retrieves whether exact validation should be performed
-				 */
-				bool isExactValidationSet() const;
-				
                 /*!
+                 * Retrieves whether or not the input model should be simplified before its analysis.
+                 */
+                bool isSimplifySet() const;
+                
+               /*!
                  * Retrieves whether or not derivatives of the resulting rational function are to be generated.
                  *
                  * @return True if the derivatives are to be generated.
@@ -61,12 +45,8 @@ namespace storm {
                 const static std::string moduleName;
                 
             private:
-				const static std::string encodeSmt2StrategyOptionName;
-				const static std::string exportSmt2DestinationPathOptionName;
-				const static std::string exportResultDestinationPathOptionName;
-				const static std::string regionOptionName;
-				const static std::string refinementThresholdOptionName;
-				const static std::string exactValidationOptionName;
+				const static std::string exportResultOptionName;
+                const static std::string simplifyOptionName;
                 const static std::string derivativesOptionName;
             };
             

src/storm-pars/settings/modules/RegionSettings.cpp

@@ -0,0 +1,82 @@
+#include "storm-pars/settings/modules/RegionSettings.h"
+
+#include "storm/settings/Option.h"
+#include "storm/settings/OptionBuilder.h"
+#include "storm/settings/ArgumentBuilder.h"
+#include "storm/settings/Argument.h"
+
+#include "storm/utility/macros.h"
+#include "storm/exceptions/IllegalArgumentValueException.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            const std::string RegionSettings::moduleName = "region";
+            const std::string RegionSettings::regionOptionName = "region";
+            const std::string RegionSettings::refineOptionName = "refine";
+            const std::string RegionSettings::checkEngineOptionName = "engine";
+            const std::string RegionSettings::printNoIllustrationOptionName = "noillustration";
+            const std::string RegionSettings::printFullResultOptionName = "printfullresult";
+            
+            RegionSettings::RegionSettings() : ModuleSettings(moduleName) {
+                this->addOption(storm::settings::OptionBuilder(moduleName, regionOptionName, true, "Sets the region(s) considered for analysis.")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("regioninput", "The region(s) given in format a<=x<=b,c<=y<=d seperated by ';'. Can also be point to a file.").build()).build());
+                
+                this->addOption(storm::settings::OptionBuilder(moduleName, refineOptionName, true, "Enables region refinement.")
+                                .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("threshold", "Refinement converges if the fraction of unknown area falls below this threshold.").setDefaultValueDouble(0.05).addValidatorDouble(storm::settings::ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0,1.0)).build()).build());
+                
+                std::vector<std::string> engines = {"pl", "exactpl", "validatingpl"};
+                this->addOption(storm::settings::OptionBuilder(moduleName, checkEngineOptionName, false, "Sets which engine is used for analyzing regions.")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(engines)).setDefaultValueString("pl").build()).build());
+
+                this->addOption(storm::settings::OptionBuilder(moduleName, printNoIllustrationOptionName, true, "If set, no illustration of the result is printed.").build());
+                
+                this->addOption(storm::settings::OptionBuilder(moduleName, printFullResultOptionName, true, "If set, the full result for every region is printed.").build());
+            }
+            
+            bool RegionSettings::isRegionSet() const {
+                return this->getOption(regionOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string RegionSettings::getRegionString() const {
+                return this->getOption(regionOptionName).getArgumentByName("regioninput").getValueAsString();
+            }
+            
+            bool RegionSettings::isRefineSet() const {
+                return this->getOption(refineOptionName).getHasOptionBeenSet();
+            }
+            
+            double RegionSettings::getRefinementThreshold() const {
+                return this->getOption(refineOptionName).getArgumentByName("threshold").getValueAsDouble();
+            }
+            
+            storm::modelchecker::RegionCheckEngine RegionSettings::getRegionCheckEngine() const {
+                std::string engineString = this->getOption(regionOptionName).getArgumentByName("regioninput").getValueAsString();
+                
+                storm::modelchecker::RegionCheckEngine result;
+                if (engineString == "pl") {
+                    result = storm::modelchecker::RegionCheckEngine::ParameterLifting;
+                } else if (engineString == "exactpl") {
+                    result = storm::modelchecker::RegionCheckEngine::ExactParameterLifting;
+                } else if (engineString == "validatingpl") {
+                    result = storm::modelchecker::RegionCheckEngine::ValidatingParameterLifting;
+                } else {
+                    STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown region check engine '" << engineString << "'.");
+                }
+                
+                return result;
+            }
+            
+            bool RegionSettings::isPrintNoIllustrationSet() const {
+                return this->getOption(printNoIllustrationOptionName).getHasOptionBeenSet();
+            }
+            
+            bool RegionSettings::isPrintFullResultSet() const {
+                return this->getOption(printFullResultOptionName).getHasOptionBeenSet();
+            }
+            
+
+        } // namespace modules
+    } // namespace settings
+} // namespace storm

src/storm-pars/settings/modules/RegionSettings.h

@@ -0,0 +1,71 @@
+#pragma once
+
+#include "storm-pars/modelchecker/region/RegionCheckEngine.h"
+
+#include "storm/settings/modules/ModuleSettings.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+
+            /*!
+             * This class represents the settings for parametric model checking.
+             */
+            class RegionSettings : public ModuleSettings {
+            public:
+                
+                /*!
+                 * Creates a new set of parametric model checking settings.
+                 */
+                RegionSettings();
+				
+				/*!
+				 * Retrieves whether region(s) were declared
+				 */
+				bool isRegionSet() const;
+				
+				/*!
+				 * Retrieves the region definition string
+				 */
+				std::string getRegionString() const;
+				
+				/*!
+				 * Retrieves whether region refinement is enabled
+				 */
+				bool isRefineSet() const;
+				
+				/*!
+				 * Retrieves the threshold considered for iterative region refinement.
+				 * The refinement converges as soon as the fraction of unknown area falls below this threshold
+				 */
+				double getRefinementThreshold() const;
+				
+				/*!
+				 * Retrieves which type of region check should be performed
+				 */
+				storm::modelchecker::RegionCheckEngine getRegionCheckEngine() const;
+				
+				/*!
+				 * Retrieves whether no illustration of the result should be printed.
+				 */
+                bool isPrintNoIllustrationSet() const;
+                
+                /*!
+                 * Retrieves whether the full result should be printed
+                 */
+                bool isPrintFullResultSet() const;
+                
+                const static std::string moduleName;
+                
+            private:
+				const static std::string regionOptionName;
+				const static std::string refineOptionName;
+				const static std::string checkEngineOptionName;
+				const static std::string printNoIllustrationOptionName;
+				const static std::string printFullResultOptionName;
+            };
+            
+        } // namespace modules
+    } // namespace settings
+} // namespace storm
+

src/storm-pars/storage/ParameterRegion.cpp

@@ -1,9 +1,8 @@
-#include "ParameterRegion.h"
+#include "storm-pars/storage/ParameterRegion.h"
 
 #include "storm/utility/macros.h"
 #include "storm/exceptions/InvalidArgumentException.h"
 #include "storm/utility/constants.h"
-#include "storm/utility/file.h"
 
 namespace storm {
     namespace storage {
@@ -164,65 +163,7 @@ namespace storm {
             regionstring = regionstring.substr(0, regionstring.length() - 1) + ";";
             return regionstring;
         }
-
-
-        template<typename ParametricType>
-        void ParameterRegion<ParametricType>::parseParameterBoundaries(Valuation& lowerBoundaries, Valuation& upperBoundaries, std::string const& parameterBoundariesString, std::set<VariableType> const& consideredVariables) {
-            
-            std::string::size_type positionOfFirstRelation = parameterBoundariesString.find("<=");
-            STORM_LOG_THROW(positionOfFirstRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find  a '<=' after the first number");
-            std::string::size_type positionOfSecondRelation = parameterBoundariesString.find("<=", positionOfFirstRelation+2);
-            STORM_LOG_THROW(positionOfSecondRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find  a '<=' after the parameter");
-
-            std::string parameter = parameterBoundariesString.substr(positionOfFirstRelation+2,positionOfSecondRelation-(positionOfFirstRelation+2));
-            //removes all whitespaces from the parameter string:
-            parameter.erase(std::remove_if(parameter.begin(), parameter.end(), ::isspace), parameter.end());
-            STORM_LOG_THROW(parameter.length()>0, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a parameter");
-
-            std::unique_ptr<VariableType> var;
-            for (auto const& v : consideredVariables) {
-                std::stringstream stream;
-                stream << v;
-                std::string vAsString = stream.str();
-                if(parameter == stream.str()) {
-                    var = std::make_unique<VariableType>(v);
-                }
-            }
-            STORM_LOG_ASSERT(var, "Could not find parameter " << parameter << " in the set of considered variables");
-            
-            CoefficientType lb = storm::utility::convertNumber<CoefficientType>(parameterBoundariesString.substr(0,positionOfFirstRelation));
-            CoefficientType ub = storm::utility::convertNumber<CoefficientType>(parameterBoundariesString.substr(positionOfSecondRelation+2));
-            lowerBoundaries.emplace(std::make_pair(*var, lb));
-            upperBoundaries.emplace(std::make_pair(*var, ub));
-        }
-
-        template<typename ParametricType>
-        ParameterRegion<ParametricType> ParameterRegion<ParametricType>::parseRegion(std::string const& regionString, std::set<VariableType> const& consideredVariables) {
-            Valuation lowerBoundaries;
-            Valuation upperBoundaries;
-            std::vector<std::string> parameterBoundaries;
-            boost::split(parameterBoundaries, regionString, boost::is_any_of(","));
-            for(auto const& parameterBoundary : parameterBoundaries){
-                if(!std::all_of(parameterBoundary.begin(),parameterBoundary.end(), ::isspace)){ //skip this string if it only consists of space
-                    parseParameterBoundaries(lowerBoundaries, upperBoundaries, parameterBoundary, consideredVariables);
-                }
-            }
-            return ParameterRegion(std::move(lowerBoundaries), std::move(upperBoundaries));
-        }
-
-        template<typename ParametricType>
-        std::vector<ParameterRegion<ParametricType>> ParameterRegion<ParametricType>::parseMultipleRegions(std::string const& regionsString, std::set<VariableType> const& consideredVariables) {
-            std::vector<ParameterRegion> result;
-            std::vector<std::string> regionsStrVec;
-            boost::split(regionsStrVec, regionsString, boost::is_any_of(";"));
-            for(auto const& regionStr : regionsStrVec){
-                if(!std::all_of(regionStr.begin(),regionStr.end(), ::isspace)){ //skip this string if it only consists of space
-                    result.emplace_back(parseRegion(regionStr, consideredVariables));
-                }
-            }
-            return result;
-        }
-            
+        
 #ifdef STORM_HAVE_CARL
             template class ParameterRegion<storm::RationalFunction>;
 #endif

src/storm-pars/storage/ParameterRegion.h

@@ -2,7 +2,7 @@
 
 #include <map>
 
-#include "storm/utility/parametric.h"
+#include "storm-pars/utility/parametric.h"
 
 namespace storm {
     namespace storage {
@@ -62,28 +62,6 @@ namespace storm {
             //returns the region as string in the format 0.3<=p<=0.4,0.2<=q<=0.5;
             std::string toString(bool boundariesAsDouble = false) const;
 
-            /*
-             * Can be used to parse a single parameter with its boundaries from a string of the form "0.3<=p<=0.5".
-             * The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::CoefficientType.
-             * The results will be inserted in the given maps
-             *
-             */
-            static void parseParameterBoundaries( Valuation& lowerBoundaries, Valuation& upperBoundaries, std::string const& parameterBoundariesString, std::set<VariableType> const& consideredVariables);
-
-            /*
-             * Can be used to parse a single region from a string of the form "0.3<=p<=0.5,0.4<=q<=0.7".
-             * The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::CoefficientType.
-             *
-             */
-            static ParameterRegion parseRegion(std::string const& regionString, std::set<VariableType> const& consideredVariables);
-
-            /*
-             * Can be used to parse a vector of region from a string of the form "0.3<=p<=0.5,0.4<=q<=0.7;0.1<=p<=0.3,0.2<=q<=0.4".
-             * The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::CoefficientType.
-             *
-             */
-            static std::vector<ParameterRegion> parseMultipleRegions(std::string const& regionsString, std::set<VariableType> const& consideredVariables);
-
         private:
 
             void init();

src/storm-pars/transformer/ParameterLifter.cpp

@@ -1,4 +1,4 @@
-#include "storm/transformer/ParameterLifter.h"
+#include "storm-pars/transformer/ParameterLifter.h"
 
 
 #include "storm/adapters/RationalFunctionAdapter.h"

src/storm-pars/transformer/ParameterLifter.h

@@ -6,10 +6,10 @@
 #include <set>
 
 
+#include "storm-pars/storage/ParameterRegion.h"
+#include "storm-pars/utility/parametric.h"
 #include "storm/storage/BitVector.h"
 #include "storm/storage/SparseMatrix.h"
-#include "storm/utility/parametric.h"
-#include "storm/storage/ParameterRegion.h"
 #include "storm/solver/OptimizationDirection.h"
 
 namespace storm {

src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp

@@ -1,4 +1,4 @@
-#include "storm/transformer/SparseParametricDtmcSimplifier.h"
+#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h"
 
 #include "storm/adapters/RationalFunctionAdapter.h"
 

src/storm-pars/transformer/SparseParametricDtmcSimplifier.h

@@ -1,7 +1,7 @@
 #pragma once
 
 
-#include "storm/transformer/SparseParametricModelSimplifier.h"
+#include "storm-pars/transformer/SparseParametricModelSimplifier.h"
 
 namespace storm {
     namespace transformer {

src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp

@@ -1,4 +1,4 @@
-#include "storm/transformer/SparseParametricMdpSimplifier.h"
+#include "storm-pars/transformer/SparseParametricMdpSimplifier.h"
 
 #include "storm/adapters/RationalFunctionAdapter.h"
 

src/storm-pars/transformer/SparseParametricMdpSimplifier.h

@@ -1,7 +1,7 @@
 #pragma once
 
 
-#include "storm/transformer/SparseParametricModelSimplifier.h"
+#include "storm-pars/transformer/SparseParametricModelSimplifier.h"
 
 namespace storm {
     namespace transformer {

src/storm-pars/transformer/SparseParametricModelSimplifier.cpp

@@ -1,4 +1,4 @@
-#include "storm/transformer/SparseParametricModelSimplifier.h"
+#include "storm-pars/transformer/SparseParametricModelSimplifier.h"
 
 #include "storm/adapters/RationalFunctionAdapter.h"
 

src/storm-pars/utility/ModelInstantiator.cpp

@@ -1,4 +1,4 @@
-#include "storm/utility/ModelInstantiator.h"
+#include "storm-pars/utility/ModelInstantiator.h"
 #include "storm/models/sparse/StandardRewardModel.h"
 
 namespace storm {

src/storm-pars/utility/ModelInstantiator.h

@@ -5,12 +5,12 @@
 #include <memory>
 #include <type_traits>
 
+#include "storm-pars/utility/parametric.h"
 #include "storm/models/sparse/Dtmc.h"
 #include "storm/models/sparse/Mdp.h"
 #include "storm/models/sparse/Ctmc.h"
 #include "storm/models/sparse/MarkovAutomaton.h"
 #include "storm/models/sparse/StochasticTwoPlayerGame.h"
-#include "storm/utility/parametric.h"
 #include "storm/utility/constants.h"
 
 namespace storm {

src/storm-pars/utility/parameterlifting.h

@@ -3,8 +3,8 @@
 
 #include <vector>
 
+#include "storm-pars/utility/parametric.h"
 #include "storm/models/sparse/Model.h"
-#include "storm/utility/parametric.h"
 #include "storm/utility/macros.h"
 #include "storm/logic/Formula.h"
 #include "storm/logic/FragmentSpecification.h"
@@ -31,37 +31,38 @@ namespace storm {
              * @return true iff it was successfully validated that parameter lifting is sound on the provided model.
              */
             template<typename ValueType>
-            static bool validateParameterLiftingSound(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::shared_ptr<storm::logic::Formula const> const& formula) {
+            static bool validateParameterLiftingSound(storm::models::sparse::Model<ValueType> const& model, storm::logic::Formula const& formula) {
                 
                 // Check whether all numbers occurring in the model are multilinear
                 
                 // Transition matrix
-                if (model->isOfType(storm::models::ModelType::Dtmc) || model->isOfType(storm::models::ModelType::Mdp) || model->isOfType(storm::models::ModelType::Ctmc)) {
-                    for (auto const& entry : model->getTransitionMatrix()) {
+                if (model.isOfType(storm::models::ModelType::Dtmc) || model.isOfType(storm::models::ModelType::Mdp) || model.isOfType(storm::models::ModelType::Ctmc)) {
+                    for (auto const& entry : model.getTransitionMatrix()) {
                         if (!storm::utility::parametric::isMultiLinearPolynomial(entry.getValue())) {
                             STORM_LOG_WARN("The input model contains a non-linear polynomial as transition: '" << entry.getValue() << "'. Can not validate that parameter lifting is sound on this model.");
                             return false;
                         }
                     }
-                } else if (model->isOfType(storm::models::ModelType::MarkovAutomaton)) {
+                } else if (model.isOfType(storm::models::ModelType::MarkovAutomaton)) {
+                    auto const& ma = dynamic_cast<storm::models::sparse::MarkovAutomaton<ValueType> const&>(model);
                     // Markov Automata store the probability matrix and the exit rate vector. However, we need to considert the rate matrix.
-                    if (!model->template as<storm::models::sparse::MarkovAutomaton<ValueType>>()->isClosed()) {
+                    if (!ma.isClosed()) {
                         STORM_LOG_ERROR("parameter lifting requires a closed Markov automaton.");
                         return false;
                     }
-                    auto const& rateVector = model->template as<storm::models::sparse::MarkovAutomaton<ValueType>>()->getExitRates();
-                    auto const& markovianStates = model->template as<storm::models::sparse::MarkovAutomaton<ValueType>>()->getMarkovianStates();
-                    for (uint_fast64_t state = 0; state < model->getNumberOfStates(); ++state) {
+                    auto const& rateVector = ma.getExitRates();
+                    auto const& markovianStates = ma.getMarkovianStates();
+                    for (uint_fast64_t state = 0; state < model.getNumberOfStates(); ++state) {
                         if (markovianStates.get(state)) {
                             auto const& exitRate = rateVector[state];
-                            for (auto const& entry : model->getTransitionMatrix().getRowGroup(state)) {
+                            for (auto const& entry : model.getTransitionMatrix().getRowGroup(state)) {
                                 if (!storm::utility::parametric::isMultiLinearPolynomial(storm::utility::simplify(entry.getValue() * exitRate))) {
                                     STORM_LOG_WARN("The input model contains a non-linear polynomial as transition rate: '" << storm::utility::simplify(entry.getValue() * exitRate) << "'. Can not validate that parameter lifting is sound on this model.");
                                     return false;
                                 }
                             }
                         } else {
-                            for (auto const& entry : model->getTransitionMatrix().getRowGroup(state)) {
+                            for (auto const& entry : model.getTransitionMatrix().getRowGroup(state)) {
                                 if (!storm::utility::parametric::isMultiLinearPolynomial(entry.getValue())) {
                                     STORM_LOG_WARN("The input model contains a non-linear polynomial as transition: '" << entry.getValue() << "'. Can not validate that parameter lifting is sound on this model.");
                                     return false;
@@ -75,10 +76,10 @@ namespace storm {
                 }
                 
                 // Rewards
-                if (formula->isRewardOperatorFormula()) {
-                    storm::models::sparse::StandardRewardModel<ValueType> const& rewardModel = formula->asRewardOperatorFormula().hasRewardModelName() ?
-                                                                                    model->getRewardModel(formula->asRewardOperatorFormula().getRewardModelName()) :
-                                                                                    model->getUniqueRewardModel();
+                if (formula.isRewardOperatorFormula()) {
+                    storm::models::sparse::StandardRewardModel<ValueType> const& rewardModel = formula.asRewardOperatorFormula().hasRewardModelName() ?
+                                                                                    model.getRewardModel(formula.asRewardOperatorFormula().getRewardModelName()) :
+                                                                                    model.getUniqueRewardModel();
                     if (rewardModel.hasStateRewards()) {
                         for (auto const& rew : rewardModel.getStateRewardVector()) {
                             if (!storm::utility::parametric::isMultiLinearPolynomial(rew)) {
@@ -91,7 +92,7 @@ namespace storm {
                     // Note: This check could also be done action-wise.
                     std::set<typename storm::utility::parametric::VariableType<ValueType>::type> collectedRewardParameters;
                     if (rewardModel.hasStateActionRewards()) {
-                        if (model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::MarkovAutomaton)) {
+                        if (model.isOfType(storm::models::ModelType::Ctmc) || model.isOfType(storm::models::ModelType::MarkovAutomaton)) {
                             for (auto const& rew : rewardModel.getStateActionRewardVector()) {
                                 if (!storm::utility::parametric::isMultiLinearPolynomial(rew)) {
                                     STORM_LOG_WARN("The input model contains a non-linear polynomial as action reward: '" << rew << "'. Can not validate that parameter lifting is sound on this model.");
@@ -120,7 +121,7 @@ namespace storm {
                     }
                     
                     if (!collectedRewardParameters.empty()) {
-                        std::set<typename storm::utility::parametric::VariableType<ValueType>::type> transitionParameters = storm::models::sparse::getProbabilityParameters(*model);
+                        std::set<typename storm::utility::parametric::VariableType<ValueType>::type> transitionParameters = storm::models::sparse::getProbabilityParameters(model);
                         auto rewParIt = collectedRewardParameters.begin();
                         auto trParIt = transitionParameters.begin();
                         while (rewParIt != collectedRewardParameters.end() && trParIt != transitionParameters.end()) {

src/storm-pars/utility/parametric.cpp

@@ -1,6 +1,6 @@
 #include <string>
 
-#include "storm/utility/parametric.h"
+#include "storm-pars/utility/parametric.h"
 #include "storm/utility/constants.h"
 #include "storm/utility/macros.h"
 #include "storm/settings/SettingsManager.h"