exact pla

src/storm/modelchecker/parametric/ParameterLifting.cpp

@@ -4,12 +4,6 @@
 
 #include "storm/adapters/CarlAdapter.h"
 
-#include "storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h"
-#include "storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.h"
-#include "storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h"
-#include "storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.h"
-#include "storm/transformer/SparseParametricDtmcSimplifier.h"
-#include "storm/transformer/SparseParametricMdpSimplifier.h"
 #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
 
 #include "storm/utility/vector.h"
@@ -29,6 +23,10 @@ namespace storm {
     namespace modelchecker {
         namespace parametric {
 
+            ParameterLiftingSettings::ParameterLiftingSettings() {
+                // todo: get this form settings
+                this->applyExactValidation = false;
+            }
             
             template <typename SparseModelType, typename ConstantType>
             ParameterLifting<SparseModelType, ConstantType>::ParameterLifting(SparseModelType const& parametricModel) : parametricModel(parametricModel) {
@@ -37,6 +35,16 @@ namespace storm {
                 initializationStopwatch.stop();
             }
         
+            template <typename SparseModelType, typename ConstantType>
+            ParameterLiftingSettings const& ParameterLifting<SparseModelType, ConstantType>::getSettings() const {
+                return settings;
+            }
+            
+            template <typename SparseModelType, typename ConstantType>
+            void ParameterLifting<SparseModelType, ConstantType>::setSettings(ParameterLiftingSettings const& newSettings) {
+                settings = newSettings;
+            }
+            
             template <typename SparseModelType, typename ConstantType>
             void ParameterLifting<SparseModelType, ConstantType>::specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
                 initializationStopwatch.start();
@@ -47,14 +55,19 @@ namespace storm {
                 initializeUnderlyingCheckers();
                 currentCheckTask = std::make_unique<storm::modelchecker::CheckTask<storm::logic::Formula, typename SparseModelType::ValueType>>(checkTask.substituteFormula(*currentFormula));
 
-                STORM_LOG_THROW(parameterLiftingChecker->canHandle(*currentCheckTask), storm::exceptions::NotSupportedException, "Parameter lifting is not supported for this property.");
-                instantiationChecker->specifyFormula(*currentCheckTask);
+                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>
-            RegionCheckResult ParameterLifting<SparseModelType, ConstantType>::analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionCheckResult const& initialResult, bool sampleVerticesOfRegion) const {
+            RegionCheckResult ParameterLifting<SparseModelType, ConstantType>::analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionCheckResult const& initialResult, bool sampleVerticesOfRegion) {
                       RegionCheckResult result = initialResult;
 
                 // Check if we need to check the formula on one point to decide whether to show AllSat or AllViolated
@@ -104,13 +117,46 @@ namespace storm {
             }
             
             template <typename SparseModelType, typename ConstantType>
-            std::vector<std::pair<storm::storage::ParameterRegion<typename SparseModelType::ValueType>, RegionCheckResult>> ParameterLifting<SparseModelType, ConstantType>::performRegionRefinement(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::CoefficientType const& threshold) const {
+            RegionCheckResult ParameterLifting<SparseModelType, ConstantType>::analyzeRegionExactValidation(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionCheckResult const& initialResult) {
+                RegionCheckResult numericResult = analyzeRegion(region, initialResult, false);
+                parameterLiftingCheckerStopwatch.start();
+                if (numericResult == RegionCheckResult::AllSat || numericResult == RegionCheckResult::AllViolated) {
+                    applyHintsToExactChecker();
+                }
+                if (numericResult == RegionCheckResult::AllSat) {
+                    if(!exactParameterLiftingChecker->check(region, this->currentCheckTask->getOptimizationDirection())->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
+                        // Numerical result is wrong; Check whether the region is AllViolated!
+                        if(!exactParameterLiftingChecker->check(region, storm::solver::invert(this->currentCheckTask->getOptimizationDirection()))->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
+                            parameterLiftingCheckerStopwatch.stop();
+                            return RegionCheckResult::AllViolated;
+                        } else {
+                            return RegionCheckResult::Unknown;
+                        }
+                    }
+                } else if (numericResult == RegionCheckResult::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!
+                        if(exactParameterLiftingChecker->check(region, this->currentCheckTask->getOptimizationDirection())->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
+                            parameterLiftingCheckerStopwatch.stop();
+                            return RegionCheckResult::AllSat;
+                        } else {
+                            return RegionCheckResult::Unknown;
+                        }
+                    }
+                }
+                parameterLiftingCheckerStopwatch.stop();
+                return numericResult;
+            }
+
+    
+            template <typename SparseModelType, typename ConstantType>
+            std::vector<std::pair<storm::storage::ParameterRegion<typename SparseModelType::ValueType>, RegionCheckResult>> ParameterLifting<SparseModelType, ConstantType>::performRegionRefinement(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, CoefficientType const& threshold) {
                 STORM_LOG_INFO("Applying refinement on region: " << region.toString(true) << " .");
                 
                 auto areaOfParameterSpace = region.area();
-                auto fractionOfUndiscoveredArea = storm::utility::one<typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::CoefficientType>();
-                auto fractionOfAllSatArea = storm::utility::zero<typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::CoefficientType>();
-                auto fractionOfAllViolatedArea = storm::utility::zero<typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::CoefficientType>();
+                auto fractionOfUndiscoveredArea = storm::utility::one<CoefficientType>();
+                auto fractionOfAllSatArea = storm::utility::zero<CoefficientType>();
+                auto fractionOfAllViolatedArea = storm::utility::zero<CoefficientType>();
                 
                 std::vector<std::pair<storm::storage::ParameterRegion<typename SparseModelType::ValueType>, RegionCheckResult>> regions;
                 regions.emplace_back(region, RegionCheckResult::Unknown);
@@ -122,7 +168,11 @@ namespace storm {
                     STORM_LOG_INFO("Analyzing region #" << indexOfCurrentRegion << " (" << storm::utility::convertNumber<double>(fractionOfUndiscoveredArea) * 100 << "% still unknown)");
                     auto const& currentRegion = regions[indexOfCurrentRegion].first;
                     auto& res = regions[indexOfCurrentRegion].second;
+                    if (settings.applyExactValidation) {
+                        res = analyzeRegionExactValidation(currentRegion, res);
+                    } else {
                         res = analyzeRegion(currentRegion, res, false);
+                    }
                     switch (res) {
                         case RegionCheckResult::AllSat:
                             fractionOfUndiscoveredArea -= currentRegion.area() / areaOfParameterSpace;
@@ -160,16 +210,6 @@ namespace storm {
                 return storm::utility::vector::filterVector(regions, resultRegions);
             }
     
-            template <typename SparseModelType, typename ConstantType>
-            SparseParameterLiftingModelChecker<SparseModelType, ConstantType> const& ParameterLifting<SparseModelType, ConstantType>::getParameterLiftingChecker() const {
-                return *parameterLiftingChecker;
-            }
-    
-            template <typename SparseModelType, typename ConstantType>
-            SparseInstantiationModelChecker<SparseModelType, ConstantType> const& ParameterLifting<SparseModelType, ConstantType>::getInstantiationChecker() const {
-                return *instantiationChecker;
-            }
-    
             template <typename SparseModelType, typename ConstantType>
             SparseModelType const& ParameterLifting<SparseModelType, ConstantType>::getConsideredParametricModel() const {
                 if (simplifiedModel) {
@@ -179,47 +219,9 @@ namespace storm {
                 }
             }
     
-            template <>
-            void ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::initializeUnderlyingCheckers() {
-                parameterLiftingChecker = std::make_unique<SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>>(getConsideredParametricModel());
-                instantiationChecker = std::make_unique<SparseDtmcInstantiationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>>(getConsideredParametricModel());
-            }
-    
-            template <>
-            void ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double>::initializeUnderlyingCheckers() {
-                parameterLiftingChecker = std::make_unique<SparseMdpParameterLiftingModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>>(getConsideredParametricModel());
-                instantiationChecker = std::make_unique<SparseMdpInstantiationModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>>(getConsideredParametricModel());
-            }
-    
-            template <>
-            void ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::simplifyParametricModel(CheckTask<logic::Formula, storm::RationalFunction> const& checkTask) {
-                storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>> simplifier(parametricModel);
-                if(simplifier.simplify(checkTask.getFormula())) {
-                    simplifiedModel = simplifier.getSimplifiedModel();
-                    currentFormula = simplifier.getSimplifiedFormula();
-                } else {
-                    simplifiedModel = nullptr;
-                    currentFormula = checkTask.getFormula().asSharedPointer();
-                }
-            }
-    
-            template <>
-            void ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double>::simplifyParametricModel(CheckTask<logic::Formula, storm::RationalFunction> const& checkTask) {
-                storm::transformer::SparseParametricMdpSimplifier<storm::models::sparse::Mdp<storm::RationalFunction>> simplifier(parametricModel);
-                if(simplifier.simplify(checkTask.getFormula())) {
-                    simplifiedModel = simplifier.getSimplifiedModel();
-                    currentFormula = simplifier.getSimplifiedFormula();
-                } else {
-                    simplifiedModel = nullptr;
-                    currentFormula = checkTask.getFormula().asSharedPointer();
-                }
-            }
-    
             template <typename SparseModelType, typename ConstantType>
             std::string ParameterLifting<SparseModelType, ConstantType>::visualizeResult(std::vector<std::pair<storm::storage::ParameterRegion<typename SparseModelType::ValueType>, RegionCheckResult>> 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) {
                 
-                typedef typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::CoefficientType ValueType;
-                
                 std::stringstream stream;
                 
                 uint_fast64_t const sizeX = 128;
@@ -229,21 +231,21 @@ namespace storm {
                 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;
                 
-                ValueType deltaX = (parameterSpace.getUpperBoundary(x) - parameterSpace.getLowerBoundary(x)) / storm::utility::convertNumber<ValueType>(sizeX);
-                ValueType deltaY = (parameterSpace.getUpperBoundary(y) - parameterSpace.getLowerBoundary(y)) / storm::utility::convertNumber<ValueType>(sizeY);
-                ValueType printedRegionArea = deltaX * deltaY;
-                for (ValueType yUpper = parameterSpace.getUpperBoundary(y); yUpper != parameterSpace.getLowerBoundary(y); yUpper -= deltaY) {
-                    ValueType yLower = yUpper - deltaY;
+                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 (ValueType xLower = parameterSpace.getLowerBoundary(x); xLower != parameterSpace.getUpperBoundary(x); xLower += deltaX) {
-                        ValueType xUpper = xLower + deltaX;
+                    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;
-                        ValueType coveredArea = storm::utility::zero<ValueType>();
+                        CoefficientType coveredArea = storm::utility::zero<CoefficientType>();
                         for (auto const& r : result) {
-                            ValueType instersectionArea = std::max(storm::utility::zero<ValueType>(), std::min(yUpper, r.first.getUpperBoundary(y)) - std::max(yLower, r.first.getLowerBoundary(y)));
-                            instersectionArea *= std::max(storm::utility::zero<ValueType>(), std::min(xUpper, r.first.getUpperBoundary(x)) - std::max(xLower, r.first.getLowerBoundary(x)));
+                            CoefficientType instersectionArea = std::max(storm::utility::zero<CoefficientType>(), std::min(yUpper, r.first.getUpperBoundary(y)) - std::max(yLower, r.first.getLowerBoundary(y)));
+                            instersectionArea *= std::max(storm::utility::zero<CoefficientType>(), std::min(xUpper, r.first.getUpperBoundary(x)) - std::max(xLower, r.first.getLowerBoundary(x)));
                             if(!storm::utility::isZero(instersectionArea)) {
                                 currRegionSafe = currRegionSafe || r.second == RegionCheckResult::AllSat;
                                 currRegionUnSafe = currRegionUnSafe || r.second == RegionCheckResult::AllViolated;
@@ -274,6 +276,8 @@ namespace storm {
 #ifdef STORM_HAVE_CARL
             template class ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
             template class ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
+            template class ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber>;
+            template class ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, storm::RationalNumber>;
 #endif
         } // namespace parametric
     } //namespace modelchecker

src/storm/modelchecker/parametric/ParameterLifting.h

@@ -13,14 +13,23 @@ namespace storm {
     namespace modelchecker{
         namespace parametric{
             
+            struct ParameterLiftingSettings {
+                ParameterLiftingSettings();
+                
+                bool applyExactValidation;
+            };
+
             template<typename SparseModelType, typename ConstantType>
             class ParameterLifting {
 
             public:
                 
+                typedef typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::CoefficientType CoefficientType;
+
                 ParameterLifting(SparseModelType const& parametricModel);
 
-                ~ParameterLifting() = default;
+                ParameterLiftingSettings const& getSettings() const;
+                void setSettings(ParameterLiftingSettings const& newSettings);
                 
                 void specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask);
                 
@@ -29,36 +38,38 @@ namespace storm {
                  * 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
-                 * If this does not yield a conclusive result and if the given flag is true, we also sample the vertices of the region
                  *
                  */
-                RegionCheckResult analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionCheckResult const& initialResult = RegionCheckResult::Unknown, bool sampleVerticesOfRegion = false) const;
+                RegionCheckResult analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionCheckResult const& initialResult = RegionCheckResult::Unknown, bool sampleVerticesOfRegion = false);
+                /*!
+                 * Similar to analyze region but additionaly invokes exact parameter lifting to validate results AllSat or AllViolated
+                 */
+                RegionCheckResult analyzeRegionExactValidation(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionCheckResult 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>, RegionCheckResult>> performRegionRefinement(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::CoefficientType const& threshold) const;
-                
-                SparseParameterLiftingModelChecker<SparseModelType, ConstantType> const& getParameterLiftingChecker() const;
-                SparseInstantiationModelChecker<SparseModelType, ConstantType> const& getInstantiationChecker() const;
+                std::vector<std::pair<storm::storage::ParameterRegion<typename SparseModelType::ValueType>, RegionCheckResult>> 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>, RegionCheckResult>> 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);
                 
-            private:
+            protected:
                 SparseModelType const& getConsideredParametricModel() const;
                 
-                void initializeUnderlyingCheckers();
-                void simplifyParametricModel(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask);
-                
+                virtual void initializeUnderlyingCheckers() = 0;
+                virtual void simplifyParametricModel(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) = 0;
+                virtual void applyHintsToExactChecker() = 0;
                 
                 SparseModelType const& parametricModel;
+                ParameterLiftingSettings 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;
                 
 
                 std::unique_ptr<SparseParameterLiftingModelChecker<SparseModelType, ConstantType>> parameterLiftingChecker;
+                std::unique_ptr<SparseParameterLiftingModelChecker<SparseModelType, CoefficientType>> exactParameterLiftingChecker;
                 std::unique_ptr<SparseInstantiationModelChecker<SparseModelType, ConstantType>> instantiationChecker;
                 
                 mutable storm::utility::Stopwatch initializationStopwatch, instantiationCheckerStopwatch, parameterLiftingCheckerStopwatch;

src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp

@@ -56,6 +56,7 @@ namespace storm {
             
             
             template class SparseDtmcInstantiationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
+            template class SparseDtmcInstantiationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber>;
 
         }
     }

src/storm/modelchecker/parametric/SparseDtmcParameterLifting.cpp

@@ -0,0 +1,61 @@
+#include "storm/modelchecker/parametric/SparseDtmcParameterLifting.h"
+
+#include "storm/adapters/CarlAdapter.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 "SparseMdpParameterLifting.h"
+
+namespace storm {
+    namespace modelchecker {
+        namespace parametric {
+
+            template <typename SparseModelType, typename ConstantType>
+            SparseDtmcParameterLifting<SparseModelType, ConstantType>::SparseDtmcParameterLifting(SparseModelType const& parametricModel) : ParameterLifting<SparseModelType, ConstantType>(parametricModel) {
+                // Intentionally left empty
+            }
+    
+            template <typename SparseModelType, typename ConstantType>
+            void SparseDtmcParameterLifting<SparseModelType, ConstantType>::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>
+            void SparseDtmcParameterLifting<SparseModelType, ConstantType>::initializeUnderlyingCheckers() {
+                if (this->settings.applyExactValidation) {
+                    STORM_LOG_WARN_COND((std::is_same<ConstantType, typename ParameterLifting<SparseModelType, ConstantType>::CoefficientType>::value) , "Exact validation is not necessarry if the original computation is already exact");
+                    this->exactParameterLiftingChecker = std::make_unique<SparseDtmcParameterLiftingModelChecker<SparseModelType, typename ParameterLifting<SparseModelType, ConstantType>::CoefficientType>>(this->getConsideredParametricModel());
+                }
+                this->parameterLiftingChecker = std::make_unique<SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>>(this->getConsideredParametricModel());
+                this->instantiationChecker = std::make_unique<SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>>(this->getConsideredParametricModel());
+            }
+    
+            template <typename SparseModelType, typename ConstantType>
+            void SparseDtmcParameterLifting<SparseModelType, ConstantType>::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, typename ParameterLifting<SparseModelType, ConstantType>::CoefficientType>*>(this->exactParameterLiftingChecker.get());
+                STORM_LOG_ASSERT(exactDtmcPLChecker, "Underlying exact parameter lifting checker has unexpected type");
+                exactDtmcPLChecker->getCurrentMaxScheduler() = dtmcPLChecker->getCurrentMaxScheduler();
+                exactDtmcPLChecker->getCurrentMinScheduler() = dtmcPLChecker->getCurrentMinScheduler();
+            }
+            
+       
+#ifdef STORM_HAVE_CARL
+            template class SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
+            template class SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber>;
+#endif
+        } // namespace parametric
+    } //namespace modelchecker
+} //namespace storm
+

src/storm/modelchecker/parametric/SparseDtmcParameterLifting.h

@@ -0,0 +1,27 @@
+#pragma once
+
+#include <memory>
+
+#include "storm/modelchecker/parametric/ParameterLifting.h"
+
+namespace storm {
+    namespace modelchecker{
+        namespace parametric{
+            
+
+            template<typename SparseModelType, typename ConstantType>
+            class SparseDtmcParameterLifting : public ParameterLifting<SparseModelType, ConstantType> {
+
+            public:
+                SparseDtmcParameterLifting(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/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp

@@ -1,4 +1,4 @@
-#include "SparseDtmcParameterLiftingModelChecker.h"
+#include "storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h"
 
 #include "storm/adapters/CarlAdapter.h"
 #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
@@ -6,6 +6,7 @@
 #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 #include "storm/models/sparse/Dtmc.h"
 #include "storm/models/sparse/StandardRewardModel.h"
+#include "storm/solver/StandardMinMaxLinearEquationSolver.h"
 #include "storm/utility/vector.h"
 #include "storm/utility/graph.h"
 
@@ -175,6 +176,13 @@ namespace storm {
                 // Set up the solver
                 auto solver = solverFactory->create(parameterLifter->getMatrix());
                 solver->setTrackScheduler(true);
+                if (std::is_same<ConstantType, storm::RationalNumber>::value && 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(storm::solver::minimize(dirForParameters) && minSched && !stepBound) solver->setSchedulerHint(std::move(minSched.get()));
@@ -188,7 +196,7 @@ namespace storm {
                         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, this->currentCheckTask->getBoundThreshold(), true, true);
+                        termCond = std::make_unique<storm::solver::TerminateIfFilteredExtremumExceedsThreshold<ConstantType>> (relevantStatesInSubsystem, true, this->currentCheckTask->getBoundThreshold(), true);
                     }
                     solver->setTerminationCondition(std::move(termCond));
                 }
@@ -232,7 +240,18 @@ namespace storm {
                 upperResultBound = boost::none;
             }
             
+            template <typename SparseModelType, typename ConstantType>
+            boost::optional<storm::storage::TotalScheduler>& SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::getCurrentMinScheduler() {
+                return minSched;
+            }
+                    
+            template <typename SparseModelType, typename ConstantType>
+            boost::optional<storm::storage::TotalScheduler>& SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::getCurrentMaxScheduler() {
+                return maxSched;
+            }
+            
             template class SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
+            template class SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber>;
 
         }
     }

src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h

@@ -24,6 +24,9 @@ namespace storm {
                 
                 virtual bool canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const override;
                 
+                boost::optional<storm::storage::TotalScheduler>& getCurrentMinScheduler();
+                boost::optional<storm::storage::TotalScheduler>& getCurrentMaxScheduler();
+
             protected:
                 
                 virtual void specifyBoundedUntilFormula(CheckTask<storm::logic::BoundedUntilFormula, ConstantType> const& checkTask) override;

src/storm/modelchecker/parametric/SparseInstantiationModelChecker.cpp

@@ -37,6 +37,9 @@ namespace storm {
             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/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp

@@ -63,6 +63,7 @@ namespace storm {
             }
             
             template class SparseMdpInstantiationModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
+            template class SparseMdpInstantiationModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, storm::RationalNumber>;
 
         }
     }

src/storm/modelchecker/parametric/SparseMdpParameterLifting.cpp

@@ -0,0 +1,62 @@
+#include "storm/modelchecker/parametric/SparseMdpParameterLifting.h"
+
+#include "storm/adapters/CarlAdapter.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 "SparseMdpParameterLifting.h"
+
+namespace storm {
+    namespace modelchecker {
+        namespace parametric {
+
+            template <typename SparseModelType, typename ConstantType>
+            SparseMdpParameterLifting<SparseModelType, ConstantType>::SparseMdpParameterLifting(SparseModelType const& parametricModel) : ParameterLifting<SparseModelType, ConstantType>(parametricModel) {
+                // Intentionally left empty
+            }
+    
+            template <typename SparseModelType, typename ConstantType>
+            void SparseMdpParameterLifting<SparseModelType, ConstantType>::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>
+            void SparseMdpParameterLifting<SparseModelType, ConstantType>::initializeUnderlyingCheckers() {
+                if (this->settings.applyExactValidation) {
+                    STORM_LOG_WARN_COND((std::is_same<ConstantType, typename ParameterLifting<SparseModelType, ConstantType>::CoefficientType>::value), "Exact validation is not necessarry if the original computation is already exact");
+                    this->exactParameterLiftingChecker = std::make_unique<SparseMdpParameterLiftingModelChecker<SparseModelType, typename ParameterLifting<SparseModelType, ConstantType>::CoefficientType>>(this->getConsideredParametricModel());
+                }
+                this->parameterLiftingChecker = std::make_unique<SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>>(this->getConsideredParametricModel());
+                this->instantiationChecker = std::make_unique<SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>>(this->getConsideredParametricModel());
+            }
+    
+            template <typename SparseModelType, typename ConstantType>
+            void SparseMdpParameterLifting<SparseModelType, ConstantType>::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, typename ParameterLifting<SparseModelType, ConstantType>::CoefficientType>*>(this->exactParameterLiftingChecker.get());
+                STORM_LOG_ASSERT(exactMdpPLChecker, "Underlying exact parameter lifting checker has unexpected type");
+                exactMdpPLChecker->getCurrentMaxScheduler() = MdpPLChecker->getCurrentMaxScheduler();
+                exactMdpPLChecker->getCurrentMinScheduler() = MdpPLChecker->getCurrentMinScheduler();
+                exactMdpPLChecker->getCurrentPlayer1Scheduler() = MdpPLChecker->getCurrentPlayer1Scheduler();
+            }
+            
+       
+#ifdef STORM_HAVE_CARL
+            template class SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
+            template class SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, storm::RationalNumber>;
+#endif
+        } // namespace parametric
+    } //namespace modelchecker
+} //namespace storm
+

src/storm/modelchecker/parametric/SparseMdpParameterLifting.h

@@ -0,0 +1,28 @@
+#pragma once
+
+#include <memory>
+
+#include "storm/modelchecker/parametric/ParameterLifting.h"
+
+namespace storm {
+    namespace modelchecker{
+        namespace parametric{
+            
+
+            template<typename SparseModelType, typename ConstantType>
+            class SparseMdpParameterLifting : public ParameterLifting<SparseModelType, ConstantType> {
+                
+            public:
+                SparseMdpParameterLifting(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/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp

@@ -1,4 +1,4 @@
-#include "SparseMdpParameterLiftingModelChecker.h"
+#include "storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h"
 
 #include "storm/adapters/CarlAdapter.h"
 #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
@@ -228,7 +228,7 @@ namespace storm {
                         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, this->currentCheckTask->getBoundThreshold(), true, true);
+                        termCond = std::make_unique<storm::solver::TerminateIfFilteredExtremumExceedsThreshold<ConstantType>> (relevantStatesInSubsystem, true, this->currentCheckTask->getBoundThreshold(), true);
                     }
                     solver->setTerminationCondition(std::move(termCond));
                 }
@@ -293,7 +293,23 @@ namespace storm {
                 applyPreviousResultAsHint = false;
             }
             
+            template <typename SparseModelType, typename ConstantType>
+            boost::optional<storm::storage::TotalScheduler>& SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::getCurrentMinScheduler() {
+                return minSched;
+            }
+                    
+            template <typename SparseModelType, typename ConstantType>
+            boost::optional<storm::storage::TotalScheduler>& SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::getCurrentMaxScheduler() {
+                return maxSched;
+            }
+            
+            template <typename SparseModelType, typename ConstantType>
+            boost::optional<storm::storage::TotalScheduler>& SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::getCurrentPlayer1Scheduler() {
+                return player1Sched;
+            }
+    
             template class SparseMdpParameterLiftingModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
+            template class SparseMdpParameterLiftingModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, storm::RationalNumber>;
         }
     }
 }

src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h

@@ -24,6 +24,10 @@ namespace storm {
                 
                 virtual bool canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const override;
                 
+                boost::optional<storm::storage::TotalScheduler>& getCurrentMinScheduler();
+                boost::optional<storm::storage::TotalScheduler>& getCurrentMaxScheduler();
+                boost::optional<storm::storage::TotalScheduler>& getCurrentPlayer1Scheduler();
+                
             protected:
                 
                 virtual void specifyBoundedUntilFormula(CheckTask<storm::logic::BoundedUntilFormula, ConstantType> const& checkTask) override;

src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.cpp

@@ -86,6 +86,8 @@ namespace storm {
     
             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/models/sparse/StochasticTwoPlayerGame.cpp

@@ -66,6 +66,7 @@ namespace storm {
             
 #ifdef STORM_HAVE_CARL
             template class StochasticTwoPlayerGame<storm::RationalFunction>;
+            template class StochasticTwoPlayerGame<storm::RationalNumber>;
 #endif
             
         } // namespace sparse

src/storm/settings/modules/ParametricSettings.cpp

@@ -18,6 +18,7 @@ namespace storm {
             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::derivativesOptionName = "derivatives";
             
             ParametricSettings::ParametricSettings() : ModuleSettings(moduleName) {
@@ -31,6 +32,7 @@ namespace storm {
                                 .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, derivativesOptionName, true, "Sets whether to generate the derivatives of the resulting rational function.").build());
             }
             
@@ -54,6 +56,10 @@ namespace storm {
                 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();
             }

src/storm/settings/modules/ParametricSettings.h

@@ -55,6 +55,11 @@ namespace storm {
 				 */
 				double getRefinementThreshold() const;
 				
+				/*!
+				 * Retrieves whether exact validation should be performed
+				 */
+				bool isExactValidationSet() const;
+				
 				/**
 				 * Retrieves whether the encoding of the transition system should be exported to a file. 
 				 * @return True iff the smt file should be encoded.
@@ -88,6 +93,7 @@ namespace storm {
 				const static std::string exportResultDestinationPathOptionName;
 				const static std::string parameterSpaceOptionName;
 				const static std::string refinementThresholdOptionName;
+				const static std::string exactValidationOptionName;
                 const static std::string derivativesOptionName;
             };
             

src/storm/solver/GameSolver.cpp

@@ -51,7 +51,6 @@ namespace storm {
                 storm::utility::vector::selectVectorValues<ValueType>(tmpResult, selectedRows, b);
                 
                 // Solve the resulting equation system.
-                // Note that the linEqSolver might consider a slightly different interpretation of "equalModuloPrecision". Hence, we iteratively increase its precision.
                 auto submatrixSolver = storm::solver::GeneralLinearEquationSolverFactory<ValueType>().create(std::move(inducedMatrix));
                 submatrixSolver->setCachingEnabled(true);
                 if (this->lowerBound) { submatrixSolver->setLowerBound(this->lowerBound.get()); }

src/storm/transformer/ParameterLifter.cpp

@@ -275,5 +275,6 @@ namespace storm {
         }
         
         template class ParameterLifter<storm::RationalFunction, double>;
+        template class ParameterLifter<storm::RationalFunction, storm::RationalNumber>;
     }
 }

src/storm/utility/ModelInstantiator.cpp

@@ -154,6 +154,12 @@ namespace storm {
             template class ModelInstantiator<storm::models::sparse::Ctmc<storm::RationalFunction>, storm::models::sparse::Ctmc<double>>;
             template class ModelInstantiator<storm::models::sparse::MarkovAutomaton<storm::RationalFunction>, storm::models::sparse::MarkovAutomaton<double>>;
             template class ModelInstantiator<storm::models::sparse::StochasticTwoPlayerGame<storm::RationalFunction>, storm::models::sparse::StochasticTwoPlayerGame<double>>;
+        
+            template class ModelInstantiator<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::models::sparse::Dtmc<storm::RationalNumber>>;
+            template class ModelInstantiator<storm::models::sparse::Mdp<storm::RationalFunction>, storm::models::sparse::Mdp<storm::RationalNumber>>;
+            template class ModelInstantiator<storm::models::sparse::Ctmc<storm::RationalFunction>, storm::models::sparse::Ctmc<storm::RationalNumber>>;
+            template class ModelInstantiator<storm::models::sparse::MarkovAutomaton<storm::RationalFunction>, storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>;
+            template class ModelInstantiator<storm::models::sparse::StochasticTwoPlayerGame<storm::RationalFunction>, storm::models::sparse::StochasticTwoPlayerGame<storm::RationalNumber>>;
 #endif
     } //namespace utility
 } //namespace storm

src/storm/utility/constants.cpp

@@ -415,6 +415,12 @@ namespace storm {
             return RationalFunction(number);
         }
         
+        template<>
+        RationalNumber convertNumber(RationalFunction const& number) {
+            STORM_LOG_ASSERT(isConstant(number), "Tried to convert a non-constant number to a constant type.");
+            return number.constantPart();
+        }
+
         template<>
         uint_fast64_t convertNumber(RationalFunction const& func) {
             return carl::toInt<unsigned long>(func.nominatorAsNumber());

src/storm/utility/storm.h

@@ -67,7 +67,8 @@
 #include "storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h"
 #include "storm/modelchecker/abstraction/GameBasedMdpModelChecker.h"
 #include "storm/modelchecker/exploration/SparseExplorationModelChecker.h"
-#include "storm/modelchecker/parametric/ParameterLifting.h"
+#include "storm/modelchecker/parametric/SparseDtmcParameterLifting.h"
+#include "storm/modelchecker/parametric/SparseMdpParameterLifting.h"
 
 #include "storm/modelchecker/csl/SparseCtmcCslModelChecker.h"
 #include "storm/modelchecker/csl/helper/SparseCtmcCslHelper.h"
@@ -333,21 +334,41 @@ namespace storm {
         std::string resultVisualization;
         
         if (markovModel->isOfType(storm::models::ModelType::Dtmc)) {
-            storm::modelchecker::parametric::ParameterLifting <storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*markovModel->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>());
+            if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isExactSet()) {
+                storm::modelchecker::parametric::SparseDtmcParameterLifting <storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber> parameterLiftingContext(*markovModel->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>());
                 parameterLiftingContext.specifyFormula(task);
                 result = parameterLiftingContext.performRegionRefinement(parameterSpace, refinementThreshold);
                 parameterLiftingStopWatch.stop();
                 if (modelParameters.size() == 2) {
                     resultVisualization = parameterLiftingContext.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin()));
                 }
+            } else {
+                storm::modelchecker::parametric::SparseDtmcParameterLifting <storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*markovModel->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>());
+                parameterLiftingContext.specifyFormula(task);
+                result = parameterLiftingContext.performRegionRefinement(parameterSpace, refinementThreshold);
+                parameterLiftingStopWatch.stop();
+                if (modelParameters.size() == 2) {
+                    resultVisualization = parameterLiftingContext.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin()));
+                }
+            }
         } else if (markovModel->isOfType(storm::models::ModelType::Mdp)) {
-            storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*markovModel->template as<storm::models::sparse::Mdp<storm::RationalFunction>>());
+            if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isExactSet()) {
+                storm::modelchecker::parametric::SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, storm::RationalNumber> parameterLiftingContext(*markovModel->template as<storm::models::sparse::Mdp<storm::RationalFunction>>());
                 parameterLiftingContext.specifyFormula(task);
                 result = parameterLiftingContext.performRegionRefinement(parameterSpace, refinementThreshold);
                 parameterLiftingStopWatch.stop();
                 if (modelParameters.size() == 2) {
                     resultVisualization = parameterLiftingContext.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin()));
                 }
+            } else {
+                storm::modelchecker::parametric::SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*markovModel->template as<storm::models::sparse::Mdp<storm::RationalFunction>>());
+                parameterLiftingContext.specifyFormula(task);
+                result = parameterLiftingContext.performRegionRefinement(parameterSpace, refinementThreshold);
+                parameterLiftingStopWatch.stop();
+                if (modelParameters.size() == 2) {
+                    resultVisualization = parameterLiftingContext.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin()));
+                }
+            }
         } else {
             STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to perform parameterLifting on the provided model type.");
         }

src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp

@@ -7,7 +7,7 @@
 
 #include "utility/storm.h"
 #include "storm/models/sparse/Model.h"
-#include "modelchecker/parametric/ParameterLifting.h"
+#include "modelchecker/parametric/SparseDtmcParameterLifting.h"
 
 TEST(SparseDtmcParameterLiftingTest, Brp_Prob) {
     
@@ -25,7 +25,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Prob) {
     auto rewParameters = storm::models::sparse::getRewardParameters(*model);
     modelParameters.insert(rewParameters.begin(), rewParameters.end());
     
-    storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
+    storm::modelchecker::parametric::SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
     parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
 
     //start testing
@@ -55,7 +55,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew) {
     auto rewParameters = storm::models::sparse::getRewardParameters(*model);
     modelParameters.insert(rewParameters.begin(), rewParameters.end());
     
-    storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
+    storm::modelchecker::parametric::SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
     parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
     
     //start testing
@@ -85,7 +85,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded) {
     auto rewParameters = storm::models::sparse::getRewardParameters(*model);
     modelParameters.insert(rewParameters.begin(), rewParameters.end());
     
-    storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
+    storm::modelchecker::parametric::SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
     parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
     
     //start testing
@@ -115,7 +115,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Infty) {
     auto rewParameters = storm::models::sparse::getRewardParameters(*model);
     modelParameters.insert(rewParameters.begin(), rewParameters.end());
     
-    storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
+    storm::modelchecker::parametric::SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
     parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
 
     //start testing
@@ -141,7 +141,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_4Par) {
     auto rewParameters = storm::models::sparse::getRewardParameters(*model);
     modelParameters.insert(rewParameters.begin(), rewParameters.end());
     
-    storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
+    storm::modelchecker::parametric::SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
     parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
     
     //start testing
@@ -172,7 +172,7 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob) {
     auto rewParameters = storm::models::sparse::getRewardParameters(*model);
     modelParameters.insert(rewParameters.begin(), rewParameters.end());
    
-    storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
+    storm::modelchecker::parametric::SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
     parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
 
     //start testing
@@ -205,7 +205,7 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_stepBounded) {
     auto rewParameters = storm::models::sparse::getRewardParameters(*model);
     modelParameters.insert(rewParameters.begin(), rewParameters.end());
    
-    storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
+    storm::modelchecker::parametric::SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
     parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
 
     //start testing
@@ -239,7 +239,7 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_1Par) {
     auto rewParameters = storm::models::sparse::getRewardParameters(*model);
     modelParameters.insert(rewParameters.begin(), rewParameters.end());
     
-    storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
+    storm::modelchecker::parametric::SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
     parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
     
     //start testing
@@ -270,7 +270,7 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_Const) {
     auto rewParameters = storm::models::sparse::getRewardParameters(*model);
     modelParameters.insert(rewParameters.begin(), rewParameters.end());
     
-    storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
+    storm::modelchecker::parametric::SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
     parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
 
     //start testing

src/test/modelchecker/SparseMdpParameterLiftingTest.cpp

@@ -7,7 +7,7 @@
 
 #include "utility/storm.h"
 #include "storm/models/sparse/Model.h"
-#include "storm/modelchecker/parametric/ParameterLifting.h"
+#include "storm/modelchecker/parametric/SparseMdpParameterLifting.h"
 
 TEST(SparseMdpParameterLiftingTest, two_dice_Prob) {
     
@@ -24,7 +24,7 @@ TEST(SparseMdpParameterLiftingTest, two_dice_Prob) {
     auto rewParameters = storm::models::sparse::getRewardParameters(*model);
     modelParameters.insert(rewParameters.begin(), rewParameters.end());
     
-    storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
+    storm::modelchecker::parametric::SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
     parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
     
     auto allSatRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters);
@@ -54,7 +54,7 @@ TEST(SparseMdpParameterLiftingTest, two_dice_Prob_bounded) {
     auto rewParameters = storm::models::sparse::getRewardParameters(*model);
     modelParameters.insert(rewParameters.begin(), rewParameters.end());
     
-    storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
+    storm::modelchecker::parametric::SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
     parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
     
     auto allSatRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters);
@@ -82,7 +82,7 @@ TEST(SparseMdpParameterLiftingTest, coin_Prob) {
     auto rewParameters = storm::models::sparse::getRewardParameters(*model);
     modelParameters.insert(rewParameters.begin(), rewParameters.end());
     
-    storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
+    storm::modelchecker::parametric::SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
     parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
     
     //start testing
@@ -112,7 +112,7 @@ TEST(SparseMdpParameterLiftingTest, brp_Prop) {
     auto rewParameters = storm::models::sparse::getRewardParameters(*model);
     modelParameters.insert(rewParameters.begin(), rewParameters.end());
     
-    storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
+    storm::modelchecker::parametric::SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
     parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
     
     //start testing
@@ -143,7 +143,7 @@ TEST(SparseMdpParameterLiftingTest, brp_Rew) {
     auto rewParameters = storm::models::sparse::getRewardParameters(*model);
     modelParameters.insert(rewParameters.begin(), rewParameters.end());
     
-    storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
+    storm::modelchecker::parametric::SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
     parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
     
    //start testing
@@ -173,7 +173,7 @@ TEST(SparseMdpParameterLiftingTest, brp_Rew_bounded) {
     auto rewParameters = storm::models::sparse::getRewardParameters(*model);
     modelParameters.insert(rewParameters.begin(), rewParameters.end());
     
-    storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
+    storm::modelchecker::parametric::SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
     parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
     
    //start testing
@@ -204,7 +204,7 @@ TEST(SparseMdpParameterLiftingTest, Brp_Rew_Infty) {
     auto rewParameters = storm::models::sparse::getRewardParameters(*model);
     modelParameters.insert(rewParameters.begin(), rewParameters.end());
     
-    storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
+    storm::modelchecker::parametric::SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
     parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
 
     //start testing
@@ -230,7 +230,7 @@ TEST(SparseMdpParameterLiftingTest, Brp_Rew_4Par) {
     auto rewParameters = storm::models::sparse::getRewardParameters(*model);
     modelParameters.insert(rewParameters.begin(), rewParameters.end());
     
-    storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
+    storm::modelchecker::parametric::SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
     parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
     
     //start testing