created a modelCheckerHint class that allows to store all kinds of hints that a model checker might make use of

src/storm/modelchecker/CheckTask.h

@@ -2,12 +2,14 @@
 #define STORM_MODELCHECKER_CHECKTASK_H_
 
 #include <boost/optional.hpp>
+#include <memory>
 
 #include "storm/logic/Formulas.h"
 #include "storm/utility/constants.h"
 
 #include "storm/solver/OptimizationDirection.h"
 #include "storm/logic/ComparisonType.h"
+#include "storm/modelchecker/hints/ModelCheckerHint.h"
 
 namespace storm {
     namespace logic {
@@ -32,7 +34,7 @@ namespace storm {
             /*!
              * Creates a task object with the default options for the given formula.
              */
-            CheckTask(FormulaType const& formula, bool onlyInitialStatesRelevant = false) : formula(formula) {
+            CheckTask(FormulaType const& formula, bool onlyInitialStatesRelevant = false) : formula(formula), hint(new ModelCheckerHint()) {
                 this->onlyInitialStatesRelevant = onlyInitialStatesRelevant;
                 this->produceSchedulers = false;
                 this->qualitative = false;
@@ -80,7 +82,7 @@ namespace storm {
              */
             template<typename NewFormulaType>
             CheckTask<NewFormulaType, ValueType> substituteFormula(NewFormulaType const& newFormula) const {
-                return CheckTask<NewFormulaType, ValueType>(newFormula, this->optimizationDirection, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers, this->resultHint);
+                return CheckTask<NewFormulaType, ValueType>(newFormula, this->optimizationDirection, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers, this->hint);
             }
             
             /*!
@@ -191,34 +193,23 @@ namespace storm {
             }
             
             /*!
-             * sets a vector that may serve as a hint for the (quantitative) model-checking result
+             * sets a hint that might contain information that speeds up the modelchecking process (if supported by the model checker)
              */
-            void setResultHint(std::vector<ValueType> const& hint){
-                this->resultHint = hint;
+            void setHint(ModelCheckerHint const& hint) {
+                this->hint = std::make_shared<ModelCheckerHint>(hint);
             }
-            
-            /*!
-             * sets a vector that may serve as a hint for the (quantitative) model-checking result
-             */
-            void setResultHint(std::vector<ValueType>&& hint){
-                this->resultHint = hint;
-            }
-            
-            /*!
-             * Retrieves whether there is a vector that may serve as a hint for the (quantitative) model-checking result
-             */
-            bool isResultHintSet() const {
-                return static_cast<bool>(resultHint);
+            void setHint(ModelCheckerHint&& hint){
+                this->hint = std::make_shared<ModelCheckerHint>(hint);
             }
             
             /*!
-             * Retrieves the vector that may serve as a hint for the (quantitative) model-checking result
+             * Retrieves a hint that might contain information that speeds up the modelchecking process (if supported by the model checker)
              */
-            std::vector<ValueType> const& getResultVectorHint() const {
-                return resultHint.get();
+            ModelCheckerHint const& getHint() const {
+                return *hint;
             }
-            boost::optional<std::vector<ValueType>> const& getOptionalResultVectorHint() const{
-                return resultHint;
+            ModelCheckerHint& getHint() {
+                return *hint;
             }
             
         private:
@@ -236,7 +227,7 @@ namespace storm {
              * @param produceSchedulers If supported by the model checker and the model formalism, schedulers to achieve
              * a value will be produced if this flag is set.
              */
-            CheckTask(std::reference_wrapper<FormulaType const> const& formula, boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<std::string> const& rewardModel, bool onlyInitialStatesRelevant, boost::optional<storm::logic::Bound<ValueType>> const& bound, bool qualitative, bool produceSchedulers, boost::optional<std::vector<ValueType>> const& resultHint) : formula(formula), optimizationDirection(optimizationDirection), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), bound(bound), qualitative(qualitative), produceSchedulers(produceSchedulers), resultHint(resultHint) {
+            CheckTask(std::reference_wrapper<FormulaType const> const& formula, boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<std::string> const& rewardModel, bool onlyInitialStatesRelevant, boost::optional<storm::logic::Bound<ValueType>> const& bound, bool qualitative, bool produceSchedulers, std::shared_ptr<ModelCheckerHint> const& hint) : formula(formula), optimizationDirection(optimizationDirection), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), bound(bound), qualitative(qualitative), produceSchedulers(produceSchedulers), hint(hint) {
                 // Intentionally left empty.
             }
             
@@ -262,10 +253,8 @@ namespace storm {
             // if this flag is set.
             bool produceSchedulers;
             
-            // If supported by the model checker and the model formalism, this vector serves as initial guess for the
-            // solution.
-            boost::optional<std::vector<ValueType>> resultHint;
-       //     boost::optional<storm::storage::Scheduler> schedulerHint; //TODO: will need two schedulers for games
+            // A hint that might contain information that speeds up the modelchecking process (if supported by the model checker)
+            std::shared_ptr<ModelCheckerHint> hint;
         };
         
     }

src/storm/modelchecker/hints/ExplicitModelCheckerHint.cpp

@@ -0,0 +1,81 @@
+#include "storm/modelchecker/hints/ExplicitModelCheckerHint.h"
+#include "storm/adapters/CarlAdapter.h"
+namespace storm {
+    namespace modelchecker {
+           
+        template<typename ValueType>
+        ExplicitModelCheckerHint<ValueType>::ExplicitModelCheckerHint(boost::optional<std::vector<ValueType>> const& resultHint, boost::optional<storm::storage::TotalScheduler> const& schedulerHint) : resultHint(resultHint), schedulerHint(schedulerHint) {
+            // Intentionally left empty
+        }
+        
+        template<typename ValueType>
+        ExplicitModelCheckerHint<ValueType>::ExplicitModelCheckerHint(boost::optional<std::vector<ValueType>>&& resultHint, boost::optional<storm::storage::TotalScheduler>&& schedulerHint) : resultHint(resultHint), schedulerHint(schedulerHint) {
+            // Intentionally left empty
+        }
+        
+        template<typename ValueType>
+        bool ExplicitModelCheckerHint<ValueType>::isEmpty() const {
+            return !resultHint.is_initialized() && !schedulerHint.is_initialized();
+        }
+        
+        template<typename ValueType>
+        bool ExplicitModelCheckerHint<ValueType>::isExplicitModelCheckerHint() const {
+            return true;
+        }
+    
+        template<typename ValueType>
+        bool ExplicitModelCheckerHint<ValueType>::hasResultHint() const {
+            return resultHint.is_initialized();
+        }
+        
+        template<typename ValueType>
+        std::vector<ValueType> const& ExplicitModelCheckerHint<ValueType>::getResultHint() const {
+            return *resultHint;
+        }
+        
+        template<typename ValueType>
+        std::vector<ValueType>& ExplicitModelCheckerHint<ValueType>::getResultHint() {
+            return *resultHint;
+        }
+    
+        template<typename ValueType>
+        void ExplicitModelCheckerHint<ValueType>::setResultHint(boost::optional<std::vector<ValueType>> const& resultHint) {
+            this->resultHint = resultHint;
+        }
+      
+        template<typename ValueType>
+        void ExplicitModelCheckerHint<ValueType>::setResultHint(boost::optional<std::vector<ValueType>>&& resultHint) {
+            this->resultHint = resultHint;
+        }
+        
+        template<typename ValueType>
+        bool ExplicitModelCheckerHint<ValueType>::hasSchedulerHint() const {
+            return schedulerHint.is_initialized();
+        }
+        
+        template<typename ValueType>
+        storm::storage::TotalScheduler const& ExplicitModelCheckerHint<ValueType>::getSchedulerHint() const {
+            return *schedulerHint;
+        }
+        
+        template<typename ValueType>
+        storm::storage::TotalScheduler& ExplicitModelCheckerHint<ValueType>::getSchedulerHint() {
+            return *schedulerHint;
+        }
+    
+        template<typename ValueType>
+        void ExplicitModelCheckerHint<ValueType>::setSchedulerHint(boost::optional<storm::storage::TotalScheduler> const& schedulerHint) {
+            this->schedulerHint = schedulerHint;
+        }
+      
+        template<typename ValueType>
+        void ExplicitModelCheckerHint<ValueType>::setSchedulerHint(boost::optional<storm::storage::TotalScheduler>&& schedulerHint) {
+            this->schedulerHint = schedulerHint;
+        }
+    
+        template class ExplicitModelCheckerHint<double>;
+        template class ExplicitModelCheckerHint<storm::RationalNumber>;
+        template class ExplicitModelCheckerHint<storm::RationalFunction>;
+        
+    }
+}

src/storm/modelchecker/hints/ExplicitModelCheckerHint.h

@@ -0,0 +1,48 @@
+#ifndef STORM_MODELCHECKER_HINTS_EXPLICITMODELCHECKERHINT_H
+#define STORM_MODELCHECKER_HINTS_EXPLICITMODELCHECKERHINT_H
+
+#include <vector>
+#include <boost/optional.hpp>
+
+#include "storm/modelchecker/hints/ModelCheckerHint.h"
+#include "storm/storage/TotalScheduler.h"
+
+namespace storm {
+    namespace modelchecker {
+        
+        template<typename ValueType>
+        class ExplicitModelCheckerHint : public ModelCheckerHint {
+        public:
+            
+            ExplicitModelCheckerHint(ExplicitModelCheckerHint<ValueType> const& other) = default;
+            ExplicitModelCheckerHint(ExplicitModelCheckerHint<ValueType>&& other) = default;
+            ExplicitModelCheckerHint(boost::optional<std::vector<ValueType>> const& resultHint = boost::none, boost::optional<storm::storage::TotalScheduler> const& schedulerHint = boost::none);
+            ExplicitModelCheckerHint(boost::optional<std::vector<ValueType>>&& resultHint, boost::optional<storm::storage::TotalScheduler>&& schedulerHint = boost::none);
+            
+            // Returns true iff this hint does not contain any information
+            virtual bool isEmpty() const override;
+            
+            // Returns true iff this is an explicit model checker hint
+            virtual bool isExplicitModelCheckerHint() const override;
+            
+            bool hasResultHint() const;
+            std::vector<ValueType> const& getResultHint() const;
+            std::vector<ValueType>& getResultHint();
+            void setResultHint(boost::optional<std::vector<ValueType>> const& resultHint);
+            void setResultHint(boost::optional<std::vector<ValueType>>&& resultHint);
+    
+            bool hasSchedulerHint() const;
+            storm::storage::TotalScheduler const& getSchedulerHint() const;
+            storm::storage::TotalScheduler& getSchedulerHint();
+            void setSchedulerHint(boost::optional<storage::TotalScheduler> const& schedulerHint);
+            void setSchedulerHint(boost::optional<storage::TotalScheduler>&& schedulerHint);
+            
+        private:
+            boost::optional<std::vector<ValueType>> resultHint;
+            boost::optional<storm::storage::TotalScheduler> schedulerHint;
+        };
+        
+    }
+}
+
+#endif /* STORM_MODELCHECKER_HINTS_EXPLICITMODELCHECKERHINT_H */

src/storm/modelchecker/hints/ModelCheckerHint.cpp

@@ -0,0 +1,34 @@
+#include "storm/modelchecker/hints/ModelCheckerHint.h"
+#include "storm/modelchecker/hints/ExplicitModelCheckerHint.h"
+#include "storm/adapters/CarlAdapter.h"
+
+namespace storm {
+    namespace modelchecker {
+           
+        bool ModelCheckerHint::isEmpty() const {
+            return true;
+        }
+        
+        bool ModelCheckerHint::isExplicitModelCheckerHint() const {
+            return false;
+        }
+            
+        template<typename ValueType>
+        ExplicitModelCheckerHint<ValueType> const& ModelCheckerHint::asExplicitModelCheckerHint() const {
+            return dynamic_cast<ExplicitModelCheckerHint<ValueType> const&>(*this);
+        }
+            
+        template<typename ValueType>
+        ExplicitModelCheckerHint<ValueType>& ModelCheckerHint::asExplicitModelCheckerHint() {
+            return dynamic_cast<ExplicitModelCheckerHint<ValueType>&>(*this);
+        }
+        
+        template ExplicitModelCheckerHint<double> const& ModelCheckerHint::asExplicitModelCheckerHint() const;
+        template ExplicitModelCheckerHint<double>& ModelCheckerHint::asExplicitModelCheckerHint();
+        template ExplicitModelCheckerHint<storm::RationalNumber> const& ModelCheckerHint::asExplicitModelCheckerHint() const;
+        template ExplicitModelCheckerHint<storm::RationalNumber>& ModelCheckerHint::asExplicitModelCheckerHint();
+        template ExplicitModelCheckerHint<storm::RationalFunction> const& ModelCheckerHint::asExplicitModelCheckerHint() const;
+        template ExplicitModelCheckerHint<storm::RationalFunction>& ModelCheckerHint::asExplicitModelCheckerHint();
+
+    }
+}

src/storm/modelchecker/hints/ModelCheckerHint.h

@@ -0,0 +1,36 @@
+#ifndef STORM_MODELCHECKER_HINTS_MODELCHECKERHINT_H
+#define STORM_MODELCHECKER_HINTS_MODELCHECKERHINT_H
+
+namespace storm {
+    namespace modelchecker {
+        
+        template<typename ValueType>
+        class ExplicitModelCheckerHint;
+        
+        
+        /*
+         * This class contains information that might accelerate the solving process
+         */
+        class ModelCheckerHint {
+        public:
+            
+            ModelCheckerHint() = default;
+            
+            // Returns true iff this hint does not contain any information
+            virtual bool isEmpty() const;
+            
+            // Returns true iff this is an explicit model checker hint
+            virtual bool isExplicitModelCheckerHint() const;
+            
+            template<typename ValueType>
+            ExplicitModelCheckerHint<ValueType>& asExplicitModelCheckerHint();
+            
+            template<typename ValueType>
+            ExplicitModelCheckerHint<ValueType> const& asExplicitModelCheckerHint() const;
+            
+        };
+        
+    }
+}
+
+#endif /* STORM_MODELCHECKER_HINTS_MODELCHECKERHINT_H */

src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp

@@ -2,6 +2,7 @@
 
 #include "storm/logic/FragmentSpecification.h"
 #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+#include "storm/modelchecker/hints/ExplicitModelCheckerHint.h"
 
 #include "storm/exceptions/InvalidArgumentException.h"
 #include "storm/exceptions/InvalidStateException.h"
@@ -22,7 +23,7 @@ namespace storm {
 
                 // Check if there are some optimizations implemented for the specified property
                 if(!this->currentCheckTask->isQualitativeSet() && this->currentCheckTask->getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true))) {
-                    return checkWithResultHint(modelChecker);
+                    return checkWithHint(modelChecker);
                 } else {
                     return modelChecker.check(*this->currentCheckTask);
                 }
@@ -30,18 +31,12 @@ namespace storm {
             
                 
             template <typename SparseModelType, typename ConstantType>
-            std::unique_ptr<CheckResult> SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>::checkWithResultHint(storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>>& modelchecker) {
-                
-                // Insert the hint if it exists
-                if(resultOfLastCheck) {
-                    this->currentCheckTask->setResultHint(std::move(*resultOfLastCheck));
-                }
-                
+            std::unique_ptr<CheckResult> SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>::checkWithHint(storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>>& modelchecker) {
                 // Check the formula and store the result as a hint for the next call.
-                // For qualitative properties, we still want a quantitative result hint. Hence we perform the subformula
+                // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula
                 if(this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
                     std::unique_ptr<storm::modelchecker::CheckResult> result = modelchecker.check(*this->currentCheckTask);
-                    resultOfLastCheck = result->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
+                    this->currentCheckTask->setHint(ExplicitModelCheckerHint<ConstantType>(result->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()));
                     return result;
                 } else {
                     std::unique_ptr<storm::modelchecker::CheckResult> quantitativeResult;
@@ -54,7 +49,7 @@ namespace storm {
                         STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Checking with result hint is only implemented for probability or reward operator formulas");
                     }
                     std::unique_ptr<storm::modelchecker::CheckResult> qualitativeResult = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
-                    resultOfLastCheck = std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector());
+                    this->currentCheckTask->setHint(ExplicitModelCheckerHint<ConstantType>(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector())));
                     return qualitativeResult;
                 }
             }

src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.h

@@ -26,13 +26,9 @@ namespace storm {
             protected:
                 
                 // Considers the result of the last check as a hint for the current check
-                std::unique_ptr<CheckResult> checkWithResultHint(storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>>& modelChecker);
-                
+                std::unique_ptr<CheckResult> checkWithHint(storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>>& modelChecker);
                 
                 storm::utility::ModelInstantiator<SparseModelType, storm::models::sparse::Dtmc<ConstantType>> modelInstantiator;
-                
-                // Stores the result of the last check in order to use it as a hint for the next check. (If this is supported by the property)
-                boost::optional<std::vector<ConstantType>> resultOfLastCheck;
             };
         }
     }

src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp

@@ -2,6 +2,7 @@
 
 #include "storm/logic/FragmentSpecification.h"
 #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+#include "storm/modelchecker/hints/ExplicitModelCheckerHint.h"
 
 #include "storm/exceptions/InvalidArgumentException.h"
 #include "storm/exceptions/InvalidStateException.h"
@@ -33,16 +34,15 @@ namespace storm {
             template <typename SparseModelType, typename ConstantType>
             std::unique_ptr<CheckResult> SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>::checkWithResultHint(storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>>& modelchecker) {
                 
-                // Insert the hint if it exists
-                if(resultOfLastCheck) {
-                    this->currentCheckTask->setResultHint(std::move(*resultOfLastCheck));
-                }
+                this->currentCheckTask->setProduceSchedulers(true);
                 
                 // Check the formula and store the result as a hint for the next call.
-                // For qualitative properties, we still want a quantitative result hint. Hence we perform the subformula
+                // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula
                 if(this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
                     std::unique_ptr<storm::modelchecker::CheckResult> result = modelchecker.check(*this->currentCheckTask);
-                    resultOfLastCheck = result->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
+                    storm::storage::Scheduler const& scheduler = result->template asExplicitQuantitativeCheckResult<ConstantType>().getScheduler();
+                    this->currentCheckTask->setHint(ExplicitModelCheckerHint<ConstantType>(result->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector(),
+                                                                                           dynamic_cast<storm::storage::TotalScheduler const&>(scheduler)));
                     return result;
                 } else {
                     std::unique_ptr<storm::modelchecker::CheckResult> quantitativeResult;
@@ -52,10 +52,12 @@ namespace storm {
                     } else if (this->currentCheckTask->getFormula().isRewardOperatorFormula()) {
                         quantitativeResult = modelchecker.computeRewards(this->currentCheckTask->getFormula().asRewardOperatorFormula().getMeasureType(), newCheckTask);
                     } else {
-                        STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Checking with result hint is only implemented for probability or reward operator formulas");
+                        STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Checking with hint is only implemented for probability or reward operator formulas");
                     }
                     std::unique_ptr<storm::modelchecker::CheckResult> qualitativeResult = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
-                    resultOfLastCheck = std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector());
+                    storm::storage::Scheduler& scheduler = qualitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getScheduler();
+                    this->currentCheckTask->setHint(ExplicitModelCheckerHint<ConstantType>(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()),
+                                                                                           std::move(dynamic_cast<storm::storage::TotalScheduler const&>(scheduler))));
                     return qualitativeResult;
                 }
             }

src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.h

@@ -29,10 +29,6 @@ namespace storm {
                 std::unique_ptr<CheckResult> checkWithResultHint(storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>>& modelChecker);
                 
                 storm::utility::ModelInstantiator<SparseModelType, storm::models::sparse::Mdp<ConstantType>> modelInstantiator;
-                
-                                
-                // Stores the result of the last check in order to use it as a hint for the next check. (If this is supported by the property)
-                boost::optional<std::vector<ConstantType>> resultOfLastCheck;
             };
         }
     }

src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp

@@ -69,7 +69,7 @@ namespace storm {
             std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
             ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
             ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
-            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory, checkTask.getOptionalResultVectorHint());
+            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory, checkTask.getHint());
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
         }
         
@@ -103,7 +103,7 @@ namespace storm {
             storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
             std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
             ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
-            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeReachabilityRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory, checkTask.getOptionalResultVectorHint());
+            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeReachabilityRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory, checkTask.getHint());
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
         }
 

src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

@@ -86,7 +86,7 @@ namespace storm {
             std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
             ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
             ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
-            auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet(), *minMaxLinearEquationSolverFactory, checkTask.getOptionalResultVectorHint());
+            auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet(), *minMaxLinearEquationSolverFactory, checkTask.getHint());
             std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret.values)));
             if (checkTask.isProduceSchedulersSet() && ret.scheduler) {
                 result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::move(ret.scheduler));
@@ -144,7 +144,7 @@ namespace storm {
             STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
             std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
             ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
-            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory, checkTask.getOptionalResultVectorHint());
+            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory, checkTask.getHint());
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
         }
 

src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp

@@ -9,6 +9,7 @@
 #include "storm/solver/LinearEquationSolver.h"
 
 #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+#include "storm/modelchecker/hints/ExplicitModelCheckerHint.h"
 
 #include "storm/exceptions/InvalidStateException.h"
 #include "storm/exceptions/InvalidPropertyException.h"
@@ -49,7 +50,7 @@ namespace storm {
             
             template<typename ValueType, typename RewardModelType>
 
-            std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeUntilProbabilities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory, boost::optional<std::vector<ValueType>> const& resultHint) {
+            std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeUntilProbabilities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory, ModelCheckerHint const& hint) {
                 // We need to identify the states which have to be taken out of the matrix, i.e.
                 // all states that have probability 0 and 1 of satisfying the until-formula.
                 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiStates, psiStates);
@@ -84,8 +85,8 @@ namespace storm {
                         // This is the initial guess for the iterative solvers. It should be safe as for all
                         // 'maybe' states we know that the probability is strictly larger than 0.
                         std::vector<ValueType> x(maybeStates.getNumberOfSetBits(), storm::utility::convertNumber<ValueType>(0.5));
-                        if(resultHint){
-                            storm::utility::vector::selectVectorValues(x, maybeStates, resultHint.get());
+                        if(hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().hasResultHint()) {
+                            storm::utility::vector::selectVectorValues(x, maybeStates, hint.template asExplicitModelCheckerHint<ValueType>().getResultHint());
                         }
 
                         // Prepare the right-hand side of the equation system. For entry i this corresponds to
@@ -161,12 +162,12 @@ namespace storm {
             }
             
             template<typename ValueType, typename RewardModelType>
-            std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory, boost::optional<std::vector<ValueType>> const& resultHint) {
-                return computeReachabilityRewards(transitionMatrix, backwardTransitions, [&] (uint_fast64_t numberOfRows, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates) { return rewardModel.getTotalRewardVector(numberOfRows, transitionMatrix, maybeStates); }, targetStates, qualitative, linearEquationSolverFactory, resultHint);
+            std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory, ModelCheckerHint const& hint) {
+                return computeReachabilityRewards(transitionMatrix, backwardTransitions, [&] (uint_fast64_t numberOfRows, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates) { return rewardModel.getTotalRewardVector(numberOfRows, transitionMatrix, maybeStates); }, targetStates, qualitative, linearEquationSolverFactory, hint);
             }
 
             template<typename ValueType, typename RewardModelType>
-            std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& totalStateRewardVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory, boost::optional<std::vector<ValueType>> const& resultHint) {
+            std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& totalStateRewardVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory, ModelCheckerHint const& hint) {
 
                 return computeReachabilityRewards(transitionMatrix, backwardTransitions,
                                                   [&] (uint_fast64_t numberOfRows, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const& maybeStates) {
@@ -174,11 +175,11 @@ namespace storm {
                                                       storm::utility::vector::selectVectorValues(result, maybeStates, totalStateRewardVector);
                                                       return result;
                                                   },
-                                                  targetStates, qualitative, linearEquationSolverFactory, resultHint);
+                                                  targetStates, qualitative, linearEquationSolverFactory, hint);
             }
             
             template<typename ValueType, typename RewardModelType>
-            std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory, boost::optional<std::vector<ValueType>> const& resultHint) {
+            std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory, ModelCheckerHint const& hint) {
                 // Determine which states have a reward of infinity by definition.
                 storm::storage::BitVector trueStates(transitionMatrix.getRowCount(), true);
                 storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(backwardTransitions, trueStates, targetStates);
@@ -209,8 +210,8 @@ namespace storm {
                         // Initialize the x vector with the hint (if available) or with 1 for each element.
                         // This is the initial guess for the iterative solvers.
                         std::vector<ValueType> x(submatrix.getColumnCount(), storm::utility::one<ValueType>());
-                        if(resultHint){
-                            storm::utility::vector::selectVectorValues(x, maybeStates, resultHint.get());
+                        if(hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().hasResultHint()) {
+                            storm::utility::vector::selectVectorValues(x, maybeStates, hint.template asExplicitModelCheckerHint<ValueType>().getResultHint());
                         }
                         
                         // Prepare the right-hand side of the equation system.

src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h

@@ -6,6 +6,7 @@
 #include <boost/optional.hpp>
 
 #include "storm/models/sparse/StandardRewardModel.h"
+#include "storm/modelchecker/hints/ModelCheckerHint.h"
 
 #include "storm/storage/SparseMatrix.h"
 #include "storm/storage/BitVector.h"
@@ -25,7 +26,7 @@ namespace storm {
                 
                 static std::vector<ValueType> computeNextProbabilities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
                 
-                static std::vector<ValueType> computeUntilProbabilities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory, boost::optional<std::vector<ValueType>> const& resultHint = boost::none);
+                static std::vector<ValueType> computeUntilProbabilities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint());
 
                 static std::vector<ValueType> computeGloballyProbabilities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
                 
@@ -34,9 +35,9 @@ namespace storm {
                 static std::vector<ValueType> computeInstantaneousRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
 
 
-                static std::vector<ValueType> computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory, boost::optional<std::vector<ValueType>> const& resultHint = boost::none);
+                static std::vector<ValueType> computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint());
                 
-                static std::vector<ValueType> computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& totalStateRewardVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory, boost::optional<std::vector<ValueType>> const& resultHint = boost::none);
+                static std::vector<ValueType> computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& totalStateRewardVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint());
 
                 static std::vector<ValueType> computeLongRunAverageProbabilities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& psiStates, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
 
@@ -49,7 +50,7 @@ namespace storm {
                 static std::vector<ValueType> computeConditionalRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
                 
             private:
-                static std::vector<ValueType> computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory, boost::optional<std::vector<ValueType>> const& resultHint = boost::none);
+                static std::vector<ValueType> computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint());
 
                 struct BaierTransformedModel {
                     BaierTransformedModel() : noTargetStates(false) {

src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

@@ -1,6 +1,7 @@
  #include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h"
 
 #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+#include "storm/modelchecker/hints/ExplicitModelCheckerHint.h"
 
 #include "storm/models/sparse/StandardRewardModel.h"
 
@@ -73,7 +74,7 @@ namespace storm {
             }
             
             template<typename ValueType>
-            MDPSparseModelCheckingHelperReturnType<ValueType> SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, boost::optional<std::vector<ValueType>> const& resultHint) {
+            MDPSparseModelCheckingHelperReturnType<ValueType> SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint) {
                 STORM_LOG_THROW(!(qualitative && produceScheduler), storm::exceptions::InvalidSettingsException, "Cannot produce scheduler when performing qualitative model checking only.");
                      
                 // We need to identify the states which have to be taken out of the matrix, i.e.
@@ -122,8 +123,8 @@ namespace storm {
                         
                         // Prepare the solution vector for the maybestates. Apply the hint, if given and applicable
                         std::vector<ValueType> x(submatrix.getRowGroupCount());
-                        if(resultHint && (goal.minimize() || (maybeStates & storm::utility::graph::performProb0E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, maybeStates, ~maybeStates)).empty())) {
-                            storm::utility::vector::selectVectorValues(x, maybeStates, *resultHint);
+                        if(!hint.isEmpty() && (goal.minimize() || (maybeStates & storm::utility::graph::performProb0E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, maybeStates, ~maybeStates)).empty())) {
+                            storm::utility::vector::selectVectorValues(x, maybeStates, hint.template asExplicitModelCheckerHint<ValueType>().getResultHint());
                         }
                         
                         MDPSparseModelCheckingHelperReturnType<ValueType> resultForMaybeStates = computeUntilProbabilitiesOnlyMaybeStates(goal, submatrix, b, produceScheduler, minMaxLinearEquationSolverFactory, std::move(x));
@@ -180,9 +181,9 @@ namespace storm {
             }
 
             template<typename ValueType>
-            MDPSparseModelCheckingHelperReturnType<ValueType> SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, boost::optional<std::vector<ValueType>> const& resultHint) {
+            MDPSparseModelCheckingHelperReturnType<ValueType> SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint) {
                 storm::solver::SolveGoal goal(dir);
-                return std::move(computeUntilProbabilities(goal, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, produceScheduler, minMaxLinearEquationSolverFactory, resultHint));
+                return std::move(computeUntilProbabilities(goal, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, produceScheduler, minMaxLinearEquationSolverFactory, hint));
             }
            
             template<typename ValueType>
@@ -249,14 +250,14 @@ namespace storm {
 
             template<typename ValueType>
             template<typename RewardModelType>
-            std::vector<ValueType> SparseMdpPrctlHelper<ValueType>::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, boost::optional<std::vector<ValueType>> const& resultHint) {
+            std::vector<ValueType> SparseMdpPrctlHelper<ValueType>::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint) {
                 // Only compute the result if the model has at least one reward this->getModel().
                 STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
                 return computeReachabilityRewardsHelper(dir, transitionMatrix, backwardTransitions,
                                                         [&rewardModel] (uint_fast64_t rowCount, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates) {
                                                             return rewardModel.getTotalRewardVector(rowCount, transitionMatrix, maybeStates);
                                                         },
-                                                        targetStates, qualitative, minMaxLinearEquationSolverFactory, resultHint);
+                                                        targetStates, qualitative, minMaxLinearEquationSolverFactory, hint);
             }
             
 #ifdef STORM_HAVE_CARL
@@ -284,7 +285,7 @@ namespace storm {
 #endif
             
             template<typename ValueType>
-            std::vector<ValueType> SparseMdpPrctlHelper<ValueType>::computeReachabilityRewardsHelper(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, boost::optional<std::vector<ValueType>> const& resultHint) {
+            std::vector<ValueType> SparseMdpPrctlHelper<ValueType>::computeReachabilityRewardsHelper(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint) {
                 
                 std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices();
                 
@@ -337,14 +338,24 @@ namespace storm {
                             }
                         }
                                                 
-                        // Create vector for results for maybe states. If applicable, consider the given hint
-                        std::vector<ValueType> x(maybeStates.getNumberOfSetBits(), storm::utility::zero<ValueType>());
-                        if(resultHint && (dir == OptimizationDirection::Maximize || (maybeStates & storm::utility::graph::performProb0E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, maybeStates, ~maybeStates)).empty())) {
-                            storm::utility::vector::selectVectorValues(x, maybeStates, *resultHint);
+                        // Create vector for results for maybe states and a solver object.
+                        std::vector<ValueType> x;
+                        std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(std::move(submatrix));
+                        
+                        // If applicable, consider the given hint(s)
+                        if(hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().hasResultHint() &&
+                            (hint.template asExplicitModelCheckerHint<ValueType>().hasSchedulerHint() ||
+                             dir == OptimizationDirection::Maximize ||
+                             (maybeStates & storm::utility::graph::performProb0E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, maybeStates, ~maybeStates)).empty())) {
+                            x = storm::utility::vector::filterVector(hint.template asExplicitModelCheckerHint<ValueType>().getResultHint(), maybeStates);
+                        } else {
+                            x = std::vector<ValueType>(maybeStates.getNumberOfSetBits(), storm::utility::zero<ValueType>());
+                        }
+                        if(hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().hasSchedulerHint()) {
+                            solver->setSchedulerHint(hint.template asExplicitModelCheckerHint<ValueType>().getSchedulerHint().getSchedulerForSubsystem(maybeStates));
                         }
                         
                         // Solve the corresponding system of equations.
-                        std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(std::move(submatrix));
                         solver->solveEquations(dir, x, b);
                         
                         // Set values of resulting vector according to result.
@@ -658,13 +669,13 @@ namespace storm {
             template class SparseMdpPrctlHelper<double>;
             template std::vector<double> SparseMdpPrctlHelper<double>::computeInstantaneousRewards(OptimizationDirection dir, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::models::sparse::StandardRewardModel<double> const& rewardModel, uint_fast64_t stepCount, storm::solver::MinMaxLinearEquationSolverFactory<double> const& minMaxLinearEquationSolverFactory);
             template std::vector<double> SparseMdpPrctlHelper<double>::computeCumulativeRewards(OptimizationDirection dir, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::models::sparse::StandardRewardModel<double> const& rewardModel, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory<double> const& minMaxLinearEquationSolverFactory);
-            template std::vector<double> SparseMdpPrctlHelper<double>::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::models::sparse::StandardRewardModel<double> const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<double> const& minMaxLinearEquationSolverFactory, boost::optional<std::vector<double>> const& resultHint);
+            template std::vector<double> SparseMdpPrctlHelper<double>::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::models::sparse::StandardRewardModel<double> const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<double> const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint);
 
 #ifdef STORM_HAVE_CARL
             template class SparseMdpPrctlHelper<storm::RationalNumber>;
             template std::vector<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeInstantaneousRewards(OptimizationDirection dir, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, uint_fast64_t stepCount, storm::solver::MinMaxLinearEquationSolverFactory<storm::RationalNumber> const& minMaxLinearEquationSolverFactory);
             template std::vector<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeCumulativeRewards(OptimizationDirection dir, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory<storm::RationalNumber> const& minMaxLinearEquationSolverFactory);
-            template std::vector<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<storm::RationalNumber> const& minMaxLinearEquationSolverFactory, boost::optional<std::vector<storm::RationalNumber>> const& resultHint);
+            template std::vector<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<storm::RationalNumber> const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint);
 #endif
         }
     }

src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h

@@ -3,6 +3,7 @@
 
 #include <vector>
 
+#include "storm/modelchecker/hints/ModelCheckerHint.h"
 #include "storm/storage/SparseMatrix.h"
 #include "storm/storage/MaximalEndComponent.h"
 #include "MDPModelCheckingHelperReturnType.h"
@@ -36,11 +37,11 @@ namespace storm {
 
                 static std::vector<ValueType> computeNextProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
 
-                static MDPSparseModelCheckingHelperReturnType<ValueType> computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, boost::optional<std::vector<ValueType>> const& resultHint = boost::none);
+                static MDPSparseModelCheckingHelperReturnType<ValueType> computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint());
 
                 static MDPSparseModelCheckingHelperReturnType<ValueType> computeUntilProbabilitiesOnlyMaybeStates(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix<ValueType> const& submatrix, std::vector<ValueType> const& b, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, std::vector<ValueType>&& x = std::vector<ValueType>());
                 
-                static MDPSparseModelCheckingHelperReturnType<ValueType> computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, boost::optional<std::vector<ValueType>> const& resultHint = boost::none);
+                static MDPSparseModelCheckingHelperReturnType<ValueType> computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint());
                 
                 static std::vector<ValueType> computeGloballyProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, bool useMecBasedTechnique = false);
                 
@@ -51,7 +52,7 @@ namespace storm {
                 static std::vector<ValueType> computeCumulativeRewards(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
                 
                 template<typename RewardModelType>
-                static std::vector<ValueType> computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, boost::optional<std::vector<ValueType>> const& resultHint = boost::none);
+                static std::vector<ValueType> computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint());
 
 #ifdef STORM_HAVE_CARL
                 static std::vector<ValueType> computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::models::sparse::StandardRewardModel<storm::Interval> const& intervalRewardModel, bool lowerBoundOfIntervals, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
@@ -62,7 +63,7 @@ namespace storm {
                 static std::unique_ptr<CheckResult> computeConditionalProbabilities(OptimizationDirection dir, storm::storage::sparse::state_type initialState, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
                 
             private:
-                static std::vector<ValueType> computeReachabilityRewardsHelper(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, boost::optional<std::vector<ValueType>> const& resultHint = boost::none);
+                static std::vector<ValueType> computeReachabilityRewardsHelper(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint());
     
                 static ValueType computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec);
 

src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp

@@ -175,6 +175,12 @@ namespace storm {
             return *scheduler.get();
         }
         
+        template<typename ValueType>
+        storm::storage::Scheduler& ExplicitQuantitativeCheckResult<ValueType>::getScheduler() {
+            STORM_LOG_THROW(this->hasScheduler(), storm::exceptions::InvalidOperationException, "Unable to retrieve non-existing scheduler.");
+            return *scheduler.get();
+        }
+        
         template<typename ValueType>
         void print(std::ostream& out, ValueType const& value) {
             if (value == storm::utility::infinity<ValueType>()) {

src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h

@@ -64,6 +64,7 @@ namespace storm {
             bool hasScheduler() const;
             void setScheduler(std::unique_ptr<storm::storage::Scheduler>&& scheduler);
             storm::storage::Scheduler const& getScheduler() const;
+            storm::storage::Scheduler& getScheduler();
             
         private:
             // The values of the quantitative check result.

src/storm/storage/TotalScheduler.cpp

@@ -1,6 +1,7 @@
 #include "storm/storage/TotalScheduler.h"
 #include "storm/exceptions/InvalidArgumentException.h"
 #include "storm/utility/Hash.h"
+#include "storm/utility/vector.h"
 
 namespace storm {
     namespace storage {
@@ -43,6 +44,10 @@ namespace storm {
             return choices;
         }
         
+        TotalScheduler TotalScheduler::getSchedulerForSubsystem(storm::storage::BitVector const& subsystem) const {
+            return TotalScheduler(storm::utility::vector::filterVector(choices, subsystem));
+        }
+        
         std::ostream& operator<<(std::ostream& out, TotalScheduler const& scheduler) {
             out << "total scheduler (defined on " << scheduler.choices.size() << " states) [ ";
             for (uint_fast64_t state = 0; state < scheduler.choices.size() - 1; ++state) {

src/storm/storage/TotalScheduler.h

@@ -5,6 +5,7 @@
 #include <ostream>
 
 #include "storm/storage/Scheduler.h"
+#include "storm/storage/BitVector.h"
 
 namespace storm {
     namespace storage {
@@ -49,6 +50,13 @@ namespace storm {
             
             std::vector<uint_fast64_t> const& getChoices() const;
             
+            /*!
+             * Constructs the scheduler for the subsystem indicated by the given BitVector
+             *
+             * @param subsystem A BitVector whose i-th entry is true iff state i is part of the subsystem
+             */
+            TotalScheduler getSchedulerForSubsystem(storm::storage::BitVector const& subsystem) const;
+            
             friend std::ostream& operator<<(std::ostream& out, TotalScheduler const& scheduler);
             friend struct std::hash<storm::storage::TotalScheduler>;