all (core) modelcheckers: Devided the canHandle method into a static and a non-static part. This allows to detect incompatibility before building the model.

5 years ago · d9176dc867
18 changed files with 148 additions and 101 deletions
--- a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp
+++ b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp
@ -24,22 +24,17 @@ namespace storm {
        }
        
        template <typename ModelType>
-        bool HybridCtmcCslModelChecker<ModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
-            return HybridCtmcCslModelChecker<ModelType>::canHandleImplementation<ValueType>(checkTask);
-        }
-        
-        template <typename ModelType>
-        template<typename CValueType, typename std::enable_if<storm::NumberTraits<CValueType>::SupportsExponential, int>::type>
-        bool HybridCtmcCslModelChecker<ModelType>::canHandleImplementation(CheckTask<storm::logic::Formula, CValueType> const& checkTask) const {
-            storm::logic::Formula const& formula = checkTask.getFormula();
-            return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTimeOperatorsAllowed(true).setRewardAccumulationAllowed(true));
+        bool HybridCtmcCslModelChecker<ModelType>::canHandleStatic(CheckTask<storm::logic::Formula, ValueType> const& checkTask) {
+            auto fragment = storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTimeOperatorsAllowed(true).setRewardAccumulationAllowed(true);
+            if (!storm::NumberTraits<ValueType>::SupportsExponential) {
+                fragment.setBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false).setInstantaneousFormulasAllowed(false);
+            }
+            return checkTask.getFormula().isInFragment(fragment);
        }
        
        template <typename ModelType>
-        template<typename CValueType, typename std::enable_if<!storm::NumberTraits<CValueType>::SupportsExponential, int>::type>
-        bool HybridCtmcCslModelChecker<ModelType>::canHandleImplementation(CheckTask<storm::logic::Formula, CValueType> const& checkTask) const {
-            storm::logic::Formula const& formula = checkTask.getFormula();
-            return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTimeOperatorsAllowed(true).setBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false).setInstantaneousFormulasAllowed(false));
+        bool HybridCtmcCslModelChecker<ModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
+            return canHandleStatic(checkTask);
        }
        
        template<typename ModelType>
--- a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.h
+++ b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.h
@ -20,6 +20,9 @@ namespace storm {
            static const storm::dd::DdType DdType = ModelType::DdType;

            explicit HybridCtmcCslModelChecker(ModelType const& model);
+
+            // Returns false, if this task can certainly not be handled by this model checker (independent of the concrete model).
+            static bool canHandleStatic(CheckTask<storm::logic::Formula, ValueType> const& checkTask);
            
            // The implemented methods of the AbstractModelChecker interface.
            virtual bool canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const override;
@ -33,14 +36,7 @@ namespace storm {
            virtual std::unique_ptr<CheckResult> computeCumulativeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) override;
            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override;
            virtual std::unique_ptr<CheckResult> computeReachabilityTimes(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override;
-
-        private:
-            template<typename CValueType = ValueType, typename std::enable_if<storm::NumberTraits<CValueType>::SupportsExponential, int>::type = 0>
-            bool canHandleImplementation(CheckTask<storm::logic::Formula, CValueType> const& checkTask) const;
-            
-            template<typename CValueType = ValueType, typename std::enable_if<!storm::NumberTraits<CValueType>::SupportsExponential, int>::type = 0>
-            bool canHandleImplementation(CheckTask<storm::logic::Formula, CValueType> const& checkTask) const;
-            
+        
        };
        
    } // namespace modelchecker
--- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp
+++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp
@ -29,23 +29,18 @@ namespace storm {
            // Intentionally left empty.
        }
        
-        template <typename SparseCtmcModelType>
-        bool SparseCtmcCslModelChecker<SparseCtmcModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
-            return SparseCtmcCslModelChecker<SparseCtmcModelType>::canHandleImplementation<ValueType>(checkTask);
-        }
-        
-        template <typename SparseCtmcModelType>
-        template<typename CValueType, typename std::enable_if<storm::NumberTraits<CValueType>::SupportsExponential, int>::type>
-        bool SparseCtmcCslModelChecker<SparseCtmcModelType>::canHandleImplementation(CheckTask<storm::logic::Formula, CValueType> const& checkTask) const {
-            storm::logic::Formula const& formula = checkTask.getFormula();
-            return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTotalRewardFormulasAllowed(true).setRewardAccumulationAllowed(true));
+        template <typename ModelType>
+        bool SparseCtmcCslModelChecker<ModelType>::canHandleStatic(CheckTask<storm::logic::Formula, ValueType> const& checkTask) {
+            auto fragment = storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTimeOperatorsAllowed(true).setTotalRewardFormulasAllowed(true).setRewardAccumulationAllowed(true);
+            if (!storm::NumberTraits<ValueType>::SupportsExponential) {
+                fragment.setBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false).setInstantaneousFormulasAllowed(false);
+            }
+            return checkTask.getFormula().isInFragment(fragment);
        }
        
        template <typename SparseCtmcModelType>
-        template<typename CValueType, typename std::enable_if<!storm::NumberTraits<CValueType>::SupportsExponential, int>::type>
-        bool SparseCtmcCslModelChecker<SparseCtmcModelType>::canHandleImplementation(CheckTask<storm::logic::Formula, CValueType> const& checkTask) const {
-            storm::logic::Formula const& formula = checkTask.getFormula();
-            return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTotalRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false).setInstantaneousFormulasAllowed(false));
+        bool SparseCtmcCslModelChecker<SparseCtmcModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
+            return canHandleStatic(checkTask);
        }
        
        template <typename SparseCtmcModelType>
--- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h
+++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h
@ -21,6 +21,9 @@ namespace storm {
            
            explicit SparseCtmcCslModelChecker(SparseCtmcModelType const& model);
            
+            // Returns false, if this task can certainly not be handled by this model checker (independent of the concrete model).
+            static bool canHandleStatic(CheckTask<storm::logic::Formula, ValueType> const& checkTask);
+            
            // The implemented methods of the AbstractModelChecker interface.
            virtual bool canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const override;
            virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(Environment const& env, CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) override;
@ -40,13 +43,6 @@ namespace storm {
             */
            std::vector<ValueType> computeAllTransientProbabilities(Environment const& env, CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask);

-        private:
-            template<typename CValueType = ValueType, typename std::enable_if<storm::NumberTraits<CValueType>::SupportsExponential, int>::type = 0>
-            bool canHandleImplementation(CheckTask<storm::logic::Formula, CValueType> const& checkTask) const;
-
-            template<typename CValueType = ValueType, typename std::enable_if<!storm::NumberTraits<CValueType>::SupportsExponential, int>::type = 0>
-            bool canHandleImplementation(CheckTask<storm::logic::Formula, CValueType> const& checkTask) const;
-
        };
        
    } // namespace modelchecker
--- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
+++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
@ -27,38 +27,31 @@ namespace storm {
            // Intentionally left empty.
        }
        
-        template<typename SparseMarkovAutomatonModelType>
-        bool SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
-            return SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::canHandleImplementation<ValueType>(checkTask);
-        }
-        
-        template <typename SparseMarkovAutomatonModelType>
-        template<typename CValueType, typename std::enable_if<storm::NumberTraits<CValueType>::SupportsExponential, int>::type>
-        bool SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::canHandleImplementation(CheckTask<storm::logic::Formula, CValueType> const& checkTask) const {
-            storm::logic::Formula const& formula = checkTask.getFormula();
-            if(formula.isInFragment(storm::logic::csl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageRewardFormulasAllowed(true).setRewardAccumulationAllowed(true))) {
+        template <typename ModelType>
+        bool SparseMarkovAutomatonCslModelChecker<ModelType>::canHandleStatic(CheckTask<storm::logic::Formula, ValueType> const& checkTask, bool* requiresSingleInitialState) {
+            auto singleObjectiveFragment = storm::logic::csl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageRewardFormulasAllowed(true).setRewardAccumulationAllowed(true);
+            auto multiObjectiveFragment = storm::logic::multiObjective().setTimeAllowed(true).setTimeBoundedUntilFormulasAllowed(true);
+            if (!storm::NumberTraits<ValueType>::SupportsExponential) {
+                singleObjectiveFragment.setBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false).setInstantaneousFormulasAllowed(false);
+                multiObjectiveFragment.setTimeBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false).setInstantaneousFormulasAllowed(false);
+            }
+            if (checkTask.getFormula().isInFragment(singleObjectiveFragment)) {
                return true;
-            } else {
-                // Check whether we consider a multi-objective formula
-                // For multi-objective model checking, each initial state  requires an individual scheduler (in contrast to single objective model checking). Let's exclude multiple initial states.
-                if (this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false;
-                if (!checkTask.isOnlyInitialStatesRelevantSet()) return false;
-                return formula.isInFragment(storm::logic::multiObjective().setTimeAllowed(true).setTimeBoundedUntilFormulasAllowed(true));
+            } else if (checkTask.isOnlyInitialStatesRelevantSet() && checkTask.getFormula().isInFragment(multiObjectiveFragment)) {
+                if (requiresSingleInitialState) {
+                    *requiresSingleInitialState = true;
+                }
            }
+            return false;
        }
        
-        template <typename SparseMarkovAutomatonModelType>
-        template<typename CValueType, typename std::enable_if<!storm::NumberTraits<CValueType>::SupportsExponential, int>::type>
-        bool SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::canHandleImplementation(CheckTask<storm::logic::Formula, CValueType> const& checkTask) const {
-            storm::logic::Formula const& formula = checkTask.getFormula();
-            if(formula.isInFragment(storm::logic::prctl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageRewardFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false).setInstantaneousFormulasAllowed(false))) {
-                return true;
+        template<typename SparseMarkovAutomatonModelType>
+        bool SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
+            bool requiresSingleInitialState = false;
+            if (canHandleStatic(checkTask, &requiresSingleInitialState)) {
+                return !requiresSingleInitialState || this->getModel().getInitialStates().getNumberOfSetBits() == 1;
            } else {
-                // Check whether we consider a multi-objective formula
-                // For multi-objective model checking, each initial state  requires an individual scheduler (in contrast to single objective model checking). Let's exclude multiple initial states.
-                if (this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false;
-                if (!checkTask.isOnlyInitialStatesRelevantSet()) return false;
-                return formula.isInFragment(storm::logic::multiObjective().setTimeAllowed(true).setTimeBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false).setInstantaneousFormulasAllowed(false));
+                return false;
            }
        }
        
--- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
+++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
@ -19,6 +19,12 @@ namespace storm {
            
            explicit SparseMarkovAutomatonCslModelChecker(SparseMarkovAutomatonModelType const& model);
            
+            /*!
+             * Returns false, if this task can certainly not be handled by this model checker (independent of the concrete model).
+             * @param requiresSingleInitialState if not nullptr, this flag is set to true iff checking this formula requires a model with a single initial state
+             */
+            static bool canHandleStatic(CheckTask<storm::logic::Formula, ValueType> const& checkTask, bool* requiresSingleInitialState = nullptr);
+            
            // The implemented methods of the AbstractModelChecker interface.
            virtual bool canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const override;
            virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(Environment const& env, CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) override;
@ -29,13 +35,6 @@ namespace storm {
            virtual std::unique_ptr<CheckResult> computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula, ValueType> const& checkTask) override;
            virtual std::unique_ptr<CheckResult> computeReachabilityTimes(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override;
            virtual std::unique_ptr<CheckResult> checkMultiObjectiveFormula(Environment const& env, CheckTask<storm::logic::MultiObjectiveFormula, ValueType> const& checkTask) override;
-
-        private:
-            template<typename CValueType = ValueType, typename std::enable_if<storm::NumberTraits<CValueType>::SupportsExponential, int>::type = 0>
-            bool canHandleImplementation(CheckTask<storm::logic::Formula, CValueType> const& checkTask) const;
-            
-            template<typename CValueType = ValueType, typename std::enable_if<!storm::NumberTraits<CValueType>::SupportsExponential, int>::type = 0>
-            bool canHandleImplementation(CheckTask<storm::logic::Formula, CValueType> const& checkTask) const;
        };
    }
 }
--- a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
+++ b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
@ -32,11 +32,16 @@ namespace storm {
        }
        
        template<typename ModelType>
-        bool HybridDtmcPrctlModelChecker<ModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
+        bool HybridDtmcPrctlModelChecker<ModelType>::canHandleStatic(CheckTask<storm::logic::Formula, ValueType> const& checkTask) {
            storm::logic::Formula const& formula = checkTask.getFormula();
            return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true).setRewardAccumulationAllowed(true));
        }
-                
+        
+        template<typename ModelType>
+        bool HybridDtmcPrctlModelChecker<ModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
+            return canHandleStatic(checkTask);
+        }
+        
        template<typename ModelType>
        std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<ModelType>::computeUntilProbabilities(Environment const& env, CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) {
            storm::logic::UntilFormula const& pathFormula = checkTask.getFormula();
--- a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h
+++ b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h
@ -19,6 +19,11 @@ namespace storm {

            explicit HybridDtmcPrctlModelChecker(ModelType const& model);
            
+            /*!
+             * Returns false, if this task can certainly not be handled by this model checker (independent of the concrete model).
+             */
+            static bool canHandleStatic(CheckTask<storm::logic::Formula, ValueType> const& checkTask);
+            
            // The implemented methods of the AbstractModelChecker interface.
            virtual bool canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const override;
            virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(Environment const& env, CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) override;
--- a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
+++ b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
@ -38,20 +38,28 @@ namespace storm {
        }
        
        template<typename ModelType>
-        bool HybridMdpPrctlModelChecker<ModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
+        bool HybridMdpPrctlModelChecker<ModelType>::canHandleStatic(CheckTask<storm::logic::Formula, ValueType> const& checkTask, bool* requiresSingleInitialState) {
            storm::logic::Formula const& formula = checkTask.getFormula();
            if (formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true).setRewardAccumulationAllowed(true))) {
                return true;
+            } else if (checkTask.isOnlyInitialStatesRelevantSet() && formula.isInFragment(storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true))) {
+                if (requiresSingleInitialState) {
+                    *requiresSingleInitialState = true;
+                }
+            }
+            return false;
+        }
+        
+        template<typename ModelType>
+        bool HybridMdpPrctlModelChecker<ModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
+            bool requiresSingleInitialState = false;
+            if (canHandleStatic(checkTask, &requiresSingleInitialState)) {
+                return !requiresSingleInitialState || this->getModel().getInitialStates().getNonZeroCount() == 1;
            } else {
-                // Check whether we consider a multi-objective formula
-                // For multi-objective model checking, each state requires an individual scheduler (in contrast to single-objective model checking). Let's exclude that multiple states are relevant
-                if(this->getModel().getInitialStates().getNonZeroCount() > 1) return false;
-                if(!checkTask.isOnlyInitialStatesRelevantSet()) return false;
-                return formula.isInFragment(storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true));
+                return false;
            }
-
        }
-                
+        
        template<typename ModelType>
        std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<ModelType>::computeUntilProbabilities(Environment const& env, CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) {
            storm::logic::UntilFormula const& pathFormula = checkTask.getFormula();
--- a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h
+++ b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h
@ -26,6 +26,12 @@ namespace storm {

            explicit HybridMdpPrctlModelChecker(ModelType const& model);
            
+            /*!
+             * Returns false, if this task can certainly not be handled by this model checker (independent of the concrete model).
+             * @param requiresSingleInitialState if not nullptr, this flag is set to true iff checking this formula requires a model with a single initial state
+             */
+            static bool canHandleStatic(CheckTask<storm::logic::Formula, ValueType> const& checkTask, bool* requiresSingleInitialState = nullptr);
+            
            // The implemented methods of the AbstractModelChecker interface.
            virtual bool canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const override;
            virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(Environment const& env, CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) override;
--- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
+++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
@ -32,17 +32,29 @@ namespace storm {
        }
        
        template<typename SparseDtmcModelType>
-        bool SparseDtmcPrctlModelChecker<SparseDtmcModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
+        bool SparseDtmcPrctlModelChecker<SparseDtmcModelType>::canHandleStatic(CheckTask<storm::logic::Formula, ValueType> const& checkTask, bool* requiresSingleInitialState) {
            storm::logic::Formula const& formula = checkTask.getFormula();
            if (formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setConditionalRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true).setRewardAccumulationAllowed(true))) {
                return true;
-            } else if (formula.isInFragment(storm::logic::quantiles())) {
-                if (this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false;
+            } else if (checkTask.isOnlyInitialStatesRelevantSet() && formula.isInFragment(storm::logic::quantiles())) {
+                if (requiresSingleInitialState) {
+                    *requiresSingleInitialState = true;
+                }
                return true;
            }
            return false;
        }
        
+        template<typename SparseDtmcModelType>
+        bool SparseDtmcPrctlModelChecker<SparseDtmcModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
+            bool requiresSingleInitialState = false;
+            if (canHandleStatic(checkTask, &requiresSingleInitialState)) {
+                return !requiresSingleInitialState || this->getModel().getInitialStates().getNumberOfSetBits() == 1;
+            } else {
+                return false;
+            }
+        }
+        
        template<typename SparseDtmcModelType>
        std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeBoundedUntilProbabilities(Environment const& env, CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) {
            storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula();
--- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
+++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
@ -18,6 +18,12 @@ namespace storm {
                        
            explicit SparseDtmcPrctlModelChecker(SparseDtmcModelType const& model);
            
+            /*!
+             * Returns false, if this task can certainly not be handled by this model checker (independent of the concrete model).
+             * @param requiresSingleInitialState if not nullptr, this flag is set to true iff checking this formula requires a model with a single initial state
+             */
+            static bool canHandleStatic(CheckTask<storm::logic::Formula, ValueType> const& checkTask, bool* requiresSingleInitialState = nullptr);
+            
            // The implemented methods of the AbstractModelChecker interface.
            virtual bool canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const override;
            virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(Environment const& env, CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) override;
--- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
+++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
@ -39,23 +39,32 @@ namespace storm {
        }
        
        template<typename SparseMdpModelType>
-        bool SparseMdpPrctlModelChecker<SparseMdpModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
+        bool SparseMdpPrctlModelChecker<SparseMdpModelType>::canHandleStatic(CheckTask<storm::logic::Formula, ValueType> const& checkTask, bool* requiresSingleInitialState) {
            storm::logic::Formula const& formula = checkTask.getFormula();
            if (formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true).setRewardAccumulationAllowed(true))) {
                return true;
-            } else if (formula.isInFragment(storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true).setTimeBoundedCumulativeRewardFormulasAllowed(true).setStepBoundedCumulativeRewardFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true))) {
-                // Check whether we consider a multi-objective formula
-                // For multi-objective model checking, each initial state requires an individual scheduler (in contrast to single-objective model checking). Let's exclude multiple initial states.
-                if (this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false;
-                if (!checkTask.isOnlyInitialStatesRelevantSet()) return false;
-                return true;
-            } else if (formula.isInFragment(storm::logic::quantiles())) {
-                if (this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false;
-                return true;
+            } else if (checkTask.isOnlyInitialStatesRelevantSet()) {
+                auto multiObjectiveFragment = storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true).setTimeBoundedCumulativeRewardFormulasAllowed(true).setStepBoundedCumulativeRewardFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true);
+                if (formula.isInFragment(multiObjectiveFragment) || formula.isInFragment(storm::logic::quantiles())) {
+                    if (requiresSingleInitialState) {
+                        *requiresSingleInitialState = true;
+                    }
+                    return true;
+                }
            }
            return false;
        }
        
+        template<typename SparseMdpModelType>
+        bool SparseMdpPrctlModelChecker<SparseMdpModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
+            bool requiresSingleInitialState = false;
+            if (canHandleStatic(checkTask, &requiresSingleInitialState)) {
+                return !requiresSingleInitialState || this->getModel().getInitialStates().getNumberOfSetBits() == 1;
+            } else {
+                return false;
+            }
+        }
+        
        template<typename SparseMdpModelType>
        std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeBoundedUntilProbabilities(Environment const& env, CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) {
            storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula();
--- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h
+++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h
@ -18,6 +18,12 @@ namespace storm {
            
            explicit SparseMdpPrctlModelChecker(SparseMdpModelType const& model);
            
+            /*!
+             * Returns false, if this task can certainly not be handled by this model checker (independent of the concrete model).
+             * @param requiresSingleInitialState if not nullptr, this flag is set to true iff checking this formula requires a model with a single initial state
+             */
+            static bool canHandleStatic(CheckTask<storm::logic::Formula, ValueType> const& checkTask, bool* requiresSingleInitialState = nullptr);
+            
            // The implemented methods of the AbstractModelChecker interface.
            virtual bool canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const override;
            virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(Environment const& env, CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) override;
--- a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp
+++ b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp
@ -29,11 +29,16 @@ namespace storm {
        }
        
        template<typename ModelType>
-        bool SymbolicDtmcPrctlModelChecker<ModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
+        bool SymbolicDtmcPrctlModelChecker<ModelType>::canHandleStatic(CheckTask<storm::logic::Formula, ValueType> const& checkTask) {
            storm::logic::Formula const& formula = checkTask.getFormula();
            return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true).setRewardAccumulationAllowed(true));
        }
        
+        template<typename ModelType>
+        bool SymbolicDtmcPrctlModelChecker<ModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
+            return canHandleStatic(checkTask);
+        }
+        
        template<typename ModelType>
        std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<ModelType>::computeUntilProbabilities(Environment const& env, CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) {
            storm::logic::UntilFormula const& pathFormula = checkTask.getFormula();
--- a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h
+++ b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h
@ -17,6 +17,9 @@ namespace storm {

            explicit SymbolicDtmcPrctlModelChecker(ModelType const& model);
            
+            // Returns false, if this task can certainly not be handled by this model checker (independent of the concrete model).
+            static bool canHandleStatic(CheckTask<storm::logic::Formula, ValueType> const& checkTask);
+            
            // The implemented methods of the AbstractModelChecker interface.
            virtual bool canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const override;
            virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(Environment const& env, CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) override;
--- a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp
+++ b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp
@ -29,11 +29,16 @@ namespace storm {
        }
        
        template<typename ModelType>
-        bool SymbolicMdpPrctlModelChecker<ModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
+        bool SymbolicMdpPrctlModelChecker<ModelType>::canHandleStatic(CheckTask<storm::logic::Formula, ValueType> const& checkTask) {
            storm::logic::Formula const& formula = checkTask.getFormula();
            return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true).setRewardAccumulationAllowed(true));
        }
        
+        template<typename ModelType>
+        bool SymbolicMdpPrctlModelChecker<ModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
+            return canHandleStatic(checkTask);
+        }
+        
        template<typename ModelType>
        std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<ModelType>::computeUntilProbabilities(Environment const& env, CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) {
            storm::logic::UntilFormula const& pathFormula = checkTask.getFormula();
--- a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h
+++ b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h
@ -18,6 +18,9 @@ namespace storm {

            explicit SymbolicMdpPrctlModelChecker(ModelType const& model);
            
+            // Returns false, if this task can certainly not be handled by this model checker (independent of the concrete model).
+            static bool canHandleStatic(CheckTask<storm::logic::Formula, ValueType> const& checkTask);
+            
            // The implemented methods of the AbstractModelChecker interface.
            virtual bool canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const override;
            virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(Environment const& env, CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) override;