implemented heuristic for pla that helps to decide with respect to which parameters a region should be splitted

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

@@ -11,13 +11,12 @@
 #include "storm/models/sparse/Dtmc.h"
 #include "storm/models/sparse/Mdp.h"
 
-#include "storm/exceptions/NotSupportedException.h"
-#include "storm/exceptions/InvalidStateException.h"
-#include "storm/exceptions/InvalidArgumentException.h"
-
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/CoreSettings.h"
 #include "storm/exceptions/NotImplementedException.h"
+#include "storm/exceptions/NotSupportedException.h"
+#include "storm/exceptions/InvalidStateException.h"
+#include "storm/exceptions/InvalidArgumentException.h"
 
 
 namespace storm {
@@ -152,6 +151,18 @@ namespace storm {
                 auto regionCopyForResult = region;
                 return std::make_unique<storm::modelchecker::RegionRefinementCheckResult<ParametricType>>(std::move(result), std::move(regionCopyForResult));
             }
+
+        template <typename ParametricType>
+        bool RegionModelChecker<ParametricType>::isRegionSplitEstimateSupported() const {
+            return false;
+        }
+        
+        template <typename ParametricType>
+        std::map<typename RegionModelChecker<ParametricType>::VariableType, double> RegionModelChecker<ParametricType>::getRegionSplitEstimate() const {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Region split estimation is not supported by this region model checker.");
+            return std::map<typename RegionModelChecker<ParametricType>::VariableType, double>();
+        }
+
     
 #ifdef STORM_HAVE_CARL
             template class RegionModelChecker<storm::RationalFunction>;

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

@@ -22,12 +22,13 @@ namespace storm {
         public:
             
             typedef typename storm::storage::ParameterRegion<ParametricType>::CoefficientType CoefficientType;
+            typedef typename storm::storage::ParameterRegion<ParametricType>::VariableType VariableType;
 
             RegionModelChecker();
             virtual ~RegionModelChecker() = default;
             
             virtual bool canHandle(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, ParametricType> const& checkTask) const = 0;
-            virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, ParametricType> const& checkTask) = 0;
+            virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, ParametricType> const& checkTask, bool generateRegionSplitEstimates = false) = 0;
             
             /*!
              * Analyzes the given region.
@@ -57,6 +58,17 @@ namespace storm {
              */
             std::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ParametricType>> performRegionRefinement(Environment const& env, storm::storage::ParameterRegion<ParametricType> const& region, boost::optional<ParametricType> const& coverageThreshold, boost::optional<uint64_t> depthThreshold = boost::none, RegionResultHypothesis const& hypothesis = RegionResultHypothesis::Unknown);
             
+            /*!
+             * Returns true if region split estimation (a) was enabled when model and check task have been specified and (b) is supported by this region model checker.
+             */
+            virtual bool isRegionSplitEstimateSupported() const;
+            
+            /*!
+             * Returns an estimate of the benefit of splitting the last checked region with respect to each parameter. This method should only be called if region split estimation is supported and enabled.
+             * If a parameter is assigned a high value, we should prefer splitting with respect to this parameter.
+             */
+            virtual std::map<VariableType, double> getRegionSplitEstimate() const;
+            
         };
 
     } //namespace modelchecker

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

@@ -19,6 +19,7 @@
 #include "storm/exceptions/InvalidPropertyException.h"
 #include "storm/exceptions/NotSupportedException.h"
 #include "storm/exceptions/UnexpectedException.h"
+#include "storm/exceptions/InvalidOperationException.h"
 #include "storm/exceptions/UncheckedRequirementException.h"
 
 
@@ -31,7 +32,7 @@ namespace storm {
         }
         
         template <typename SparseModelType, typename ConstantType>
-        SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseDtmcParameterLiftingModelChecker(std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>>&& solverFactory) : solverFactory(std::move(solverFactory)), solvingRequiresUpperRewardBounds(false) {
+        SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseDtmcParameterLiftingModelChecker(std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>>&& solverFactory) : solverFactory(std::move(solverFactory)), solvingRequiresUpperRewardBounds(false), regionSplitEstimationsEnabled(false) {
             // Intentionally left empty
         }
         
@@ -47,18 +48,20 @@ namespace storm {
         }
         
         template <typename SparseModelType, typename ConstantType>
-        void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
+        void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates) {
             auto dtmc = parametricModel->template as<SparseModelType>();
-            specify(env, dtmc, checkTask, false);
+            specify(env, dtmc, checkTask, generateRegionSplitEstimates, false);
         }
         
         template <typename SparseModelType, typename ConstantType>
-        void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(Environment const& env, std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool skipModelSimplification) {
-
+        void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(Environment const& env, std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates, bool skipModelSimplification) {
+            
             STORM_LOG_ASSERT(this->canHandle(parametricModel, checkTask), "specified model and formula can not be handled by this.");
-         
+            
             reset();
             
+            regionSplitEstimationsEnabled = generateRegionSplitEstimates;
+            
             if (skipModelSimplification) {
                 this->parametricModel = parametricModel;
                 this->specifyFormula(env, checkTask);
@@ -139,7 +142,7 @@ namespace storm {
                 // 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);
+                parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel->getTransitionMatrix(), b, maybeStates, maybeStates, regionSplitEstimationsEnabled);
             }
             
             // We know some bounds for the results so set them
@@ -179,7 +182,7 @@ namespace storm {
 
                 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);
+                parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel->getTransitionMatrix(), b, maybeStates, maybeStates, regionSplitEstimationsEnabled);
             }
             
             // We only know a lower bound for the result
@@ -297,6 +300,9 @@ namespace storm {
                 } else {
                     maxSchedChoices = solver->getSchedulerChoices();
                 }
+                if (isRegionSplitEstimateSupported()) {
+                    computeRegionSplitEstimates(x, solver->getSchedulerChoices(), region, dirForParameters);
+                }
             }
             
             // Get the result for the complete model (including maybestates)
@@ -309,6 +315,68 @@ namespace storm {
             return std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ConstantType>>(std::move(result));
         }
         
+        template <typename SparseModelType, typename ConstantType>
+        void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::computeRegionSplitEstimates(std::vector<ConstantType> const& quantitativeResult, std::vector<uint_fast64_t> const& schedulerChoices, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
+            std::map<typename RegionModelChecker<typename SparseModelType::ValueType>::VariableType, double> deltaLower, deltaUpper;
+            for (auto const& p : region.getVariables()) {
+                deltaLower.insert(std::make_pair(p, 0.0));
+                deltaUpper.insert(std::make_pair(p, 0.0));
+            }
+            auto const& choiceValuations = parameterLifter->getRowLabels();
+            auto const& matrix = parameterLifter->getMatrix();
+            auto const& vector = parameterLifter->getVector();
+            
+            std::vector<ConstantType> stateResults;
+            for (uint64_t state = 0; state < schedulerChoices.size(); ++state) {
+                uint64_t rowOffset = matrix.getRowGroupIndices()[state];
+                uint64_t optimalChoice = schedulerChoices[state];
+                auto const& optimalChoiceVal = choiceValuations[rowOffset + optimalChoice];
+                assert(optimalChoiceVal.getUnspecifiedParameters().empty());
+                stateResults.clear();
+                for (uint64_t row = rowOffset; row < matrix.getRowGroupIndices()[state + 1]; ++row) {
+                    stateResults.push_back(matrix.multiplyRowWithVector(row, quantitativeResult) + vector[row]);
+                }
+                bool checkUpperParameters = false;
+                do {
+                    auto const& consideredParameters = checkUpperParameters ? optimalChoiceVal.getUpperParameters() : optimalChoiceVal.getLowerParameters();
+                    for (auto const& p : consideredParameters) {
+                        // Find the 'best' choice that assigns the parameter to the other bound
+                        ConstantType bestValue;
+                        bool foundBestValue = false;
+                        for (uint64_t choice = 0; choice < stateResults.size(); ++choice) {
+                            if (choice != optimalChoice) {
+                                auto const& otherBoundParsOfChoice = checkUpperParameters ? choiceValuations[rowOffset + choice].getLowerParameters() : choiceValuations[rowOffset + choice].getUpperParameters();
+                                if (otherBoundParsOfChoice.find(p) != otherBoundParsOfChoice.end()) {
+                                    ConstantType const& choiceValue = stateResults[choice];
+                                    if (!foundBestValue || (storm::solver::minimize(dirForParameters) ? choiceValue < bestValue : choiceValue > bestValue)) {
+                                        foundBestValue = true;
+                                        bestValue = choiceValue;
+                                    }
+                                }
+                            }
+                        }
+                        if (checkUpperParameters) {
+                            deltaLower[p] += storm::utility::convertNumber<double>(bestValue);
+                        } else {
+                            deltaUpper[p] += storm::utility::convertNumber<double>(bestValue);
+                        }
+
+                    }
+                    checkUpperParameters = !checkUpperParameters;
+                } while (checkUpperParameters);
+            }
+            
+            regionSplitEstimates.clear();
+            for (auto const& p : region.getVariables()) {
+                if (deltaLower[p] > deltaUpper[p]) {
+                    regionSplitEstimates.insert(std::make_pair(p, deltaUpper[p]));
+                } else {
+                    regionSplitEstimates.insert(std::make_pair(p, deltaLower[p]));
+                }
+            }
+            
+        }
+        
         template <typename SparseModelType, typename ConstantType>
         void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::reset() {
             maybeStates.resize(0);
@@ -321,6 +389,7 @@ namespace storm {
             x.clear();
             lowerResultBound = boost::none;
             upperResultBound = boost::none;
+            regionSplitEstimationsEnabled = false;
         }
         
         template <typename SparseModelType, typename ConstantType>
@@ -355,6 +424,18 @@ namespace storm {
             return result;
         }
         
+        template <typename SparseModelType, typename ConstantType>
+        bool SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::isRegionSplitEstimateSupported() const {
+            return regionSplitEstimationsEnabled && !stepBound;
+        }
+        
+        template <typename SparseModelType, typename ConstantType>
+        std::map<typename RegionModelChecker<typename SparseModelType::ValueType>::VariableType, double> SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::getRegionSplitEstimate() const {
+            STORM_LOG_THROW(isRegionSplitEstimateSupported(), storm::exceptions::InvalidOperationException, "Region split estimation requested but are not enabled (or supported).");
+            return regionSplitEstimates;
+        }
+
+        
         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

@@ -23,12 +23,15 @@ namespace storm {
             virtual ~SparseDtmcParameterLiftingModelChecker() = default;
             
             virtual bool canHandle(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const override;
-            virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) override;
-            void specify(Environment const& env, std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool skipModelSimplification);
+            virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates = false) override;
+            void specify(Environment const& env, std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates, bool skipModelSimplification);
             
             boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMinScheduler();
             boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMaxScheduler();
 
+            virtual bool isRegionSplitEstimateSupported() const override;
+            virtual std::map<typename RegionModelChecker<typename SparseModelType::ValueType>::VariableType, double> getRegionSplitEstimate() const override;
+            
         protected:
                 
             virtual void specifyBoundedUntilFormula(Environment const& env, CheckTask<storm::logic::BoundedUntilFormula, ConstantType> const& checkTask) override;
@@ -39,7 +42,9 @@ namespace storm {
             virtual storm::modelchecker::SparseInstantiationModelChecker<SparseModelType, ConstantType>& getInstantiationChecker() override;
                 
             virtual std::unique_ptr<CheckResult> computeQuantitativeValues(Environment const& env, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) override;
-                
+            
+            void computeRegionSplitEstimates(std::vector<ConstantType> const& quantitativeResult, std::vector<uint_fast64_t> const& schedulerChoices, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters);
+            
             virtual void reset() override;
                 
         private:
@@ -59,6 +64,9 @@ namespace storm {
             boost::optional<std::vector<uint_fast64_t>> minSchedChoices, maxSchedChoices;
             std::vector<ConstantType> x;
             boost::optional<ConstantType> lowerResultBound, upperResultBound;
+            
+            bool regionSplitEstimationsEnabled;
+            std::map<typename RegionModelChecker<typename SparseModelType::ValueType>::VariableType, double> regionSplitEstimates;
         };
     }
 }

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

@@ -45,13 +45,13 @@ namespace storm {
         }
         
         template <typename SparseModelType, typename ConstantType>
-        void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
+        void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates) {
             auto mdp = parametricModel->template as<SparseModelType>();
-            specify(env, mdp, checkTask, false);
+            specify(env, mdp, checkTask, generateRegionSplitEstimates, false);
         }
         
         template <typename SparseModelType, typename ConstantType>
-        void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(Environment const& env, std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool skipModelSimplification) {
+        void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(Environment const& env, std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates, bool skipModelSimplification) {
 
             STORM_LOG_ASSERT(this->canHandle(parametricModel, checkTask), "specified model and formula can not be handled by this.");
          

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

@@ -25,8 +25,8 @@ namespace storm {
             virtual ~SparseMdpParameterLiftingModelChecker() = default;
             
             virtual bool canHandle(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const override;
-            virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) override;
-            void specify(Environment const& env, std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool skipModelSimplification);
+            virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates = false) override;
+            void specify(Environment const& env, std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates, bool skipModelSimplification);
 
             boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMinScheduler();
             boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMaxScheduler();

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

@@ -15,7 +15,7 @@ namespace storm {
         }
         
         template <typename SparseModelType, typename ImpreciseType, typename PreciseType>
-        void ValidatingSparseDtmcParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
+        void ValidatingSparseDtmcParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates) {
             STORM_LOG_ASSERT(this->canHandle(parametricModel, checkTask), "specified model and formula can not be handled by this.");
         
             auto dtmc = parametricModel->template as<SparseModelType>();
@@ -27,8 +27,8 @@ namespace storm {
             
             auto simplifiedTask = checkTask.substituteFormula(*simplifier.getSimplifiedFormula());
             
-            impreciseChecker.specify(env, simplifier.getSimplifiedModel(), simplifiedTask, true);
-            preciseChecker.specify(env, simplifier.getSimplifiedModel(), simplifiedTask, true);
+            impreciseChecker.specify(env, simplifier.getSimplifiedModel(), simplifiedTask, false, true);
+            preciseChecker.specify(env, simplifier.getSimplifiedModel(), simplifiedTask, false, true);
         }
         
         template <typename SparseModelType, typename ImpreciseType, typename PreciseType>

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

@@ -12,7 +12,7 @@ namespace storm {
             ValidatingSparseDtmcParameterLiftingModelChecker();
             virtual ~ValidatingSparseDtmcParameterLiftingModelChecker() = default;
             
-            virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) override;
+            virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates = false) override;
 
         protected:
             virtual SparseParameterLiftingModelChecker<SparseModelType, ImpreciseType>& getImpreciseChecker() override;

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

@@ -16,7 +16,7 @@ namespace storm {
         
         
         template <typename SparseModelType, typename ImpreciseType, typename PreciseType>
-        void ValidatingSparseMdpParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
+        void ValidatingSparseMdpParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates) {
             STORM_LOG_ASSERT(this->canHandle(parametricModel, checkTask), "specified model and formula can not be handled by this.");
         
             auto mdp = parametricModel->template as<SparseModelType>();
@@ -28,8 +28,8 @@ namespace storm {
             
             auto simplifiedTask = checkTask.substituteFormula(*simplifier.getSimplifiedFormula());
             
-            impreciseChecker.specify(env, simplifier.getSimplifiedModel(), simplifiedTask, true);
-            preciseChecker.specify(env, simplifier.getSimplifiedModel(), simplifiedTask, true);
+            impreciseChecker.specify(env, simplifier.getSimplifiedModel(), simplifiedTask, false, true);
+            preciseChecker.specify(env, simplifier.getSimplifiedModel(), simplifiedTask, false, true);
         }
         
         template <typename SparseModelType, typename ImpreciseType, typename PreciseType>

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

@@ -12,7 +12,7 @@ namespace storm {
             ValidatingSparseMdpParameterLiftingModelChecker();
             virtual ~ValidatingSparseMdpParameterLiftingModelChecker() = default;
             
-            virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) override;
+            virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates = false) override;
 
         protected:
             virtual SparseParameterLiftingModelChecker<SparseModelType, ImpreciseType>& getImpreciseChecker() override;

src/storm-pars/transformer/ParameterLifter.cpp

@@ -12,8 +12,9 @@ namespace storm {
     namespace transformer {
 
         template<typename ParametricType, typename ConstantType>
-        ParameterLifter<ParametricType, ConstantType>::ParameterLifter(storm::storage::SparseMatrix<ParametricType> const& pMatrix, std::vector<ParametricType> const& pVector, storm::storage::BitVector const& selectedRows, storm::storage::BitVector const& selectedColumns) {
+        ParameterLifter<ParametricType, ConstantType>::ParameterLifter(storm::storage::SparseMatrix<ParametricType> const& pMatrix, std::vector<ParametricType> const& pVector, storm::storage::BitVector const& selectedRows, storm::storage::BitVector const& selectedColumns, bool generateRowLabels) {
         
+            
             // get a mapping from old column indices to new ones
             std::vector<uint_fast64_t> oldToNewColumnIndexMapping(selectedColumns.size(), selectedColumns.size());
             uint_fast64_t newIndex = 0;
@@ -45,10 +46,16 @@ namespace storm {
                         ++pMatrixEntryCount;
                     }
                 }
+                
                 ParametricType const& pVectorEntry = pVector[rowIndex];
                 std::set<VariableType> vectorEntryVariables;
                 if (!storm::utility::isConstant(pVectorEntry)) {
                     storm::utility::parametric::gatherOccurringVariables(pVectorEntry, vectorEntryVariables);
+                    if (generateRowLabels) {
+                        // If row labels are to be generated, we do not allow unspecified valuations.
+                        // Therefore, we also 'lift' parameters that only occurr on a vector.
+                        occurringVariables.insert(vectorEntryVariables.begin(), vectorEntryVariables.end());
+                    }
                     nonConstVectorEntries.set(pVectorEntryCount, true);
                 }
                 ++pVectorEntryCount;
@@ -57,6 +64,10 @@ namespace storm {
                 auto rowValuations = getVerticesOfAbstractRegion(occurringVariables);
                 
                 for (auto const& val : rowValuations) {
+                    if (generateRowLabels) {
+                        rowLabels.push_back(val);
+                    }
+                    
                     // Insert matrix entries for each valuation. For non-constant entries, a dummy value is inserted and the function and the valuation are collected.
                     // The placeholder for the collected function/valuation are stored in the matrixAssignment. The matrixAssignment is completed after the matrix is finished
                     for (auto const& entry: pMatrix.getRow(rowIndex)) {
@@ -78,7 +89,8 @@ namespace storm {
                         vector.push_back(storm::utility::one<ConstantType>());
                         AbstractValuation vectorVal(val);
                         for(auto const& vectorVar : vectorEntryVariables) {
-                            if(occurringVariables.find(vectorVar) == occurringVariables.end()) {
+                            if (occurringVariables.find(vectorVar) == occurringVariables.end()) {
+                                assert(!generateRowLabels);
                                 vectorVal.addParameterUnspecified(vectorVar);
                             }
                         }
@@ -148,6 +160,11 @@ namespace storm {
         std::vector<ConstantType> const& ParameterLifter<ParametricType, ConstantType>::getVector() const {
             return vector;
         }
+        
+        template<typename ParametricType, typename ConstantType>
+        std::vector<typename ParameterLifter<ParametricType, ConstantType>::AbstractValuation> const& ParameterLifter<ParametricType, ConstantType>::getRowLabels() const {
+            return rowLabels;
+        }
     
         template<typename ParametricType, typename ConstantType>
         std::vector<typename ParameterLifter<ParametricType, ConstantType>::AbstractValuation> ParameterLifter<ParametricType, ConstantType>::getVerticesOfAbstractRegion(std::set<VariableType> const& variables) const {
@@ -223,6 +240,21 @@ namespace storm {
             return result;
         }
             
+        template<typename ParametricType, typename ConstantType>
+        std::set<typename ParameterLifter<ParametricType, ConstantType>::VariableType> const& ParameterLifter<ParametricType, ConstantType>::AbstractValuation::getLowerParameters() const {
+            return lowerPars;
+        }
+        
+        template<typename ParametricType, typename ConstantType>
+        std::set<typename ParameterLifter<ParametricType, ConstantType>::VariableType> const& ParameterLifter<ParametricType, ConstantType>::AbstractValuation::getUpperParameters() const {
+            return upperPars;
+        }
+        
+        template<typename ParametricType, typename ConstantType>
+        std::set<typename ParameterLifter<ParametricType, ConstantType>::VariableType> const& ParameterLifter<ParametricType, ConstantType>::AbstractValuation::getUnspecifiedParameters() const {
+            return unspecifiedPars;
+        }
+        
         template<typename ParametricType, typename ConstantType>
         std::vector<storm::utility::parametric::Valuation<ParametricType>> ParameterLifter<ParametricType, ConstantType>::AbstractValuation::getConcreteValuations(storm::storage::ParameterRegion<ParametricType> const& region) const {
             auto result = region.getVerticesOfRegion(unspecifiedPars);

src/storm-pars/transformer/ParameterLifter.h

@@ -39,7 +39,7 @@ namespace storm {
              * @param selectedRows a Bitvector that specifies which rows of the matrix and the vector are considered.
              * @param selectedColumns a Bitvector that specifies which columns of the matrix are considered.
              */
-            ParameterLifter(storm::storage::SparseMatrix<ParametricType> const& pMatrix, std::vector<ParametricType> const& pVector, storm::storage::BitVector const& selectedRows, storm::storage::BitVector const& selectedColumns);
+            ParameterLifter(storm::storage::SparseMatrix<ParametricType> const& pMatrix, std::vector<ParametricType> const& pVector, storm::storage::BitVector const& selectedRows, storm::storage::BitVector const& selectedColumns,  bool generateRowLabels = false);
             
             void specifyRegion(storm::storage::ParameterRegion<ParametricType> const& region, storm::solver::OptimizationDirection const& dirForParameters);
             
@@ -49,13 +49,6 @@ namespace storm {
             // Returns the resulting vector. Should only be called AFTER specifying a region
             std::vector<ConstantType> const& getVector() const;
             
-            
-        private:
-            /*
-             * We minimize the number of function evaluations by only calling evaluate() once for each unique pair of function and valuation.
-             * The result of each evaluation is then written to all positions in the matrix (and the vector) where the corresponding (function,valuation) occurred.
-             */
-            
             /*
              * During initialization, the actual regions are not known. Hence, we consider abstract valuations,
              * where it is only known whether a parameter will be set to either the lower/upper bound of the region or whether this is unspecified
@@ -72,6 +65,9 @@ namespace storm {
                 
                 std::size_t getHashValue() const;
                 AbstractValuation getSubValuation(std::set<VariableType> const& pars) const;
+                std::set<VariableType> const& getLowerParameters() const;
+                std::set<VariableType> const& getUpperParameters() const;
+                std::set<VariableType> const& getUnspecifiedParameters() const;
                 
                 /*!
                  * Returns the concrete valuation(s) (w.r.t. the provided region) represented by this abstract valuation.
@@ -83,6 +79,17 @@ namespace storm {
                 std::set<VariableType> lowerPars, upperPars, unspecifiedPars;
             };
             
+            // Returns for each row the abstract valuation for this row
+            // Note: the returned vector might be empty if row label generaion was disabled initially
+            std::vector<AbstractValuation> const& getRowLabels() const;
+
+            
+        private:
+            /*
+             * We minimize the number of function evaluations by only calling evaluate() once for each unique pair of function and valuation.
+             * The result of each evaluation is then written to all positions in the matrix (and the vector) where the corresponding (function,valuation) occurred.
+             */
+            
             /*!
              * Collects all occurring pairs of functions and (abstract) valuations.
              * We also store a placeholder for the result of each pair. The result is computed and written into the placeholder whenever a region and optimization direction is specified.
@@ -121,7 +128,8 @@ namespace storm {
             // Returns the 2^(variables.size()) vertices of the region
             std::vector<AbstractValuation> getVerticesOfAbstractRegion(std::set<VariableType> const& variables) const;
             
-            
+            std::vector<AbstractValuation> rowLabels;
+
             storm::storage::SparseMatrix<ConstantType> matrix; //The resulting matrix;
             std::vector<std::pair<typename storm::storage::SparseMatrix<ConstantType>::iterator, ConstantType&>> matrixAssignment; // Connection of matrix entries with placeholders