Improved sparse mdp model checking: Now allows hints for expected rewards

src/storm/modelchecker/hints/ExplicitModelCheckerHint.cpp

@@ -4,12 +4,12 @@ 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) {
+        ExplicitModelCheckerHint<ValueType>::ExplicitModelCheckerHint(boost::optional<std::vector<ValueType>> const& resultHint, boost::optional<storm::storage::TotalScheduler> const& schedulerHint) : resultHint(resultHint), schedulerHint(schedulerHint), forceApplicationOfHints(false) {
             // 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) {
+        ExplicitModelCheckerHint<ValueType>::ExplicitModelCheckerHint(boost::optional<std::vector<ValueType>>&& resultHint, boost::optional<storm::storage::TotalScheduler>&& schedulerHint) : resultHint(resultHint), schedulerHint(schedulerHint), forceApplicationOfHints(false) {
             // Intentionally left empty
         }
         
@@ -73,6 +73,16 @@ namespace storm {
             this->schedulerHint = schedulerHint;
         }
     
+        template<typename ValueType>
+        bool ExplicitModelCheckerHint<ValueType>::getForceApplicationOfHints() const {
+            return forceApplicationOfHints;
+        }
+    
+        template<typename ValueType>
+        void ExplicitModelCheckerHint<ValueType>::setForceApplicationOfHints(bool value) {
+            forceApplicationOfHints = value;
+        }
+    
         template class ExplicitModelCheckerHint<double>;
         template class ExplicitModelCheckerHint<storm::RationalNumber>;
         template class ExplicitModelCheckerHint<storm::RationalFunction>;

src/storm/modelchecker/hints/ExplicitModelCheckerHint.h

@@ -10,6 +10,10 @@
 namespace storm {
     namespace modelchecker {
         
+        /*!
+         * This class contains information that might accelerate the model checking process.
+         * @note The model checker has to make sure whether a given hint is actually applicable and thus a hint might be ignored.
+         */
         template<typename ValueType>
         class ExplicitModelCheckerHint : public ModelCheckerHint {
         public:
@@ -37,9 +41,16 @@ namespace storm {
             void setSchedulerHint(boost::optional<storage::TotalScheduler> const& schedulerHint);
             void setSchedulerHint(boost::optional<storage::TotalScheduler>&& schedulerHint);
             
+            // If set, this option forces the application of the specified hints. This means that the model checker may skip some checks to increase performance.
+            // This might yield wrong results on certain models, e.g., when computing maximal probabilities on an MDP that has an end component consisting only of maybestates.
+            bool getForceApplicationOfHints() const;
+            void setForceApplicationOfHints(bool value);
+            
         private:
             boost::optional<std::vector<ValueType>> resultHint;
             boost::optional<storm::storage::TotalScheduler> schedulerHint;
+            
+            bool forceApplicationOfHints;
         };
         
     }

src/storm/modelchecker/hints/ModelCheckerHint.h

@@ -8,8 +8,9 @@ namespace storm {
         class ExplicitModelCheckerHint;
         
         
-        /*
-         * This class contains information that might accelerate the solving process
+        /*!
+         * This class contains information that might accelerate the model checking process.
+         * @note The model checker has to make sure whether a given hint is actually applicable and thus a hint might be ignored.
          */
         class ModelCheckerHint {
         public:

src/storm/modelchecker/parametric/SparseInstantiationModelChecker.cpp

@@ -24,6 +24,17 @@ namespace storm {
                 currentCheckTask->setProduceSchedulers(checkTask.isProduceSchedulersSet());
             }
             
+            template <typename SparseModelType, typename ConstantType>
+            storm::modelchecker::ModelCheckerHint& SparseInstantiationModelChecker<SparseModelType, ConstantType>::getHint() {
+                return currentCheckTask->getHint();
+            }
+            
+            template <typename SparseModelType, typename ConstantType>
+            storm::modelchecker::ModelCheckerHint const& SparseInstantiationModelChecker<SparseModelType, ConstantType>::getHint() const {
+                return currentCheckTask->getHint();
+            }
+            
+            
             template class SparseInstantiationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
             template class SparseInstantiationModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
 

src/storm/modelchecker/parametric/SparseInstantiationModelChecker.h

@@ -3,6 +3,7 @@
 #include "storm/logic/Formulas.h"
 #include "storm/modelchecker/CheckTask.h"
 #include "storm/modelchecker/results/CheckResult.h"
+#include "storm/modelchecker/hints/ModelCheckerHint.h"
 #include "storm/utility/parametric.h"
 
 namespace storm {
@@ -20,7 +21,10 @@ namespace storm {
                 void specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask);
                 
                 virtual std::unique_ptr<CheckResult> check(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) = 0;
-
+                
+                storm::modelchecker::ModelCheckerHint& getHint();
+                storm::modelchecker::ModelCheckerHint const& getHint() const;
+                
             protected:
                 
                 SparseModelType const& parametricModel;

src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

@@ -144,8 +144,12 @@ 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.getHint());
-            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
+            auto ret = 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(), 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));
+            }
+            return result;
         }
 
 		template<typename SparseMdpModelType>

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

@@ -121,13 +121,8 @@ namespace storm {
                         // the accumulated probability of going from state i to some 'yes' state.
                         std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(maybeStates, statesWithProbability1);
                         
-                        // Prepare the solution vector for the maybestates. Apply the hint, if given and applicable
-                        std::vector<ValueType> x(submatrix.getRowGroupCount());
-                        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));
+                        // Now compute the results for the maybeStates
+                        MDPSparseModelCheckingHelperReturnType<ValueType> resultForMaybeStates = computeValuesOnlyMaybeStates(goal, transitionMatrix, backwardTransitions, maybeStates, submatrix, b, produceScheduler, minMaxLinearEquationSolverFactory, hint, goal.minimize(), storm::utility::zero<ValueType>(), storm::utility::one<ValueType>());
                         
                         // Set values of resulting vector according to result.
                         storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, resultForMaybeStates.values);
@@ -161,23 +156,44 @@ namespace storm {
             }
             
             template<typename ValueType>
-            MDPSparseModelCheckingHelperReturnType<ValueType> SparseMdpPrctlHelper<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) {
-                // If requested, we will produce a scheduler.
-                std::unique_ptr<storm::storage::TotalScheduler> scheduler;
-                
-                // make sure that the solution vector has the correct size.
-                x.resize(submatrix.getRowGroupCount());
+            MDPSparseModelCheckingHelperReturnType<ValueType> SparseMdpPrctlHelper<ValueType>::computeValuesOnlyMaybeStates(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix<ValueType> const& submatrix, std::vector<ValueType> const& b, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint, bool skipECWithinMaybeStatesCheck, boost::optional<ValueType> const& lowerResultBound, boost::optional<ValueType> const& upperResultBound) {
                 
-                // Solve the corresponding system of equations.
+                // Set up the solver
                 std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = storm::solver::configureMinMaxLinearEquationSolver(goal, minMaxLinearEquationSolverFactory, submatrix);
+                if (lowerResultBound) {
+                    solver->setLowerBound(lowerResultBound.get());
+                }
+                if (upperResultBound) {
+                    solver->setUpperBound(upperResultBound.get());
+                }
+                // the scheduler hint is only applicable if it induces no BSCC consisting of maybestates
+                if(hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().hasSchedulerHint() &&
+                   (hint.template asExplicitModelCheckerHint<ValueType>().getForceApplicationOfHints() || skipECWithinMaybeStatesCheck ||
+                    storm::utility::graph::performProb1(transitionMatrix.transposeSelectedRowsFromRowGroups(hint.template asExplicitModelCheckerHint<ValueType>().getSchedulerHint().getChoices()), maybeStates, ~maybeStates).full())) {
+                    solver->setSchedulerHint(hint.template asExplicitModelCheckerHint<ValueType>().getSchedulerHint().getSchedulerForSubsystem(maybeStates));
+                }
                 solver->setTrackScheduler(produceScheduler);
+                
+                // Create the solution vector.
+                std::vector<ValueType> x;
+                // The result hint is only applicable if there are no End Components consisting of maybestates
+                if(hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().hasResultHint() &&
+                   (hint.template asExplicitModelCheckerHint<ValueType>().getForceApplicationOfHints() || skipECWithinMaybeStatesCheck || solver->hasSchedulerHint() ||
+                    storm::utility::graph::performProb1A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, maybeStates, ~maybeStates).full())) {
+                    x = storm::utility::vector::filterVector(hint.template asExplicitModelCheckerHint<ValueType>().getResultHint(), maybeStates);
+                } else {
+                    x = std::vector<ValueType>(submatrix.getRowGroupCount(), lowerResultBound ? lowerResultBound.get() : storm::utility::zero<ValueType>());
+                }
+                
+                // Solve the corresponding system of equations.
                 solver->solveEquations(x, b);
                 
+                // If requested, a scheduler was produced
                 if (produceScheduler) {
-                    scheduler = solver->getScheduler();
+                   return MDPSparseModelCheckingHelperReturnType<ValueType>(std::move(x), std::move(solver->getScheduler()));
+                } else {
+                    return MDPSparseModelCheckingHelperReturnType<ValueType>(std::move(x));
                 }
-                
-                return MDPSparseModelCheckingHelperReturnType<ValueType>(std::move(x), std::move(scheduler));
             }
 
             template<typename ValueType>
@@ -247,17 +263,28 @@ namespace storm {
                 return result;
             }
             
-
             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, ModelCheckerHint const& hint) {
+            MDPSparseModelCheckingHelperReturnType<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, bool produceScheduler, 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,
+                return computeReachabilityRewardsHelper(storm::solver::SolveGoal(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, hint);
+                                                        targetStates, qualitative, produceScheduler, minMaxLinearEquationSolverFactory, hint);
+            }
+            
+            template<typename ValueType>
+            template<typename RewardModelType>
+            MDPSparseModelCheckingHelperReturnType<ValueType> SparseMdpPrctlHelper<ValueType>::computeReachabilityRewards(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, 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(goal, 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, produceScheduler, minMaxLinearEquationSolverFactory, hint);
             }
             
 #ifdef STORM_HAVE_CARL
@@ -265,7 +292,7 @@ namespace storm {
             std::vector<ValueType> SparseMdpPrctlHelper<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) {
                 // Only compute the result if the reward model is not empty.
                 STORM_LOG_THROW(!intervalRewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
-                return computeReachabilityRewardsHelper(dir, transitionMatrix, backwardTransitions, \
+                return computeReachabilityRewardsHelper(storm::solver::SolveGoal(dir), transitionMatrix, backwardTransitions, \
                                                         [&] (uint_fast64_t rowCount, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates) {
                                                             std::vector<ValueType> result;
                                                             result.reserve(rowCount);
@@ -275,7 +302,7 @@ namespace storm {
                                                             }
                                                             return result;
                                                         }, \
-                                                        targetStates, qualitative, minMaxLinearEquationSolverFactory);
+                                                        targetStates, qualitative, false, minMaxLinearEquationSolverFactory).values;
             }
             
             template<>
@@ -285,14 +312,14 @@ 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, ModelCheckerHint const& hint) {
+            MDPSparseModelCheckingHelperReturnType<ValueType> SparseMdpPrctlHelper<ValueType>::computeReachabilityRewardsHelper(storm::solver::SolveGoal const& goal, 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, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint) {
                 
                 std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices();
                 
                 // Determine which states have a reward of infinity by definition.
                 storm::storage::BitVector infinityStates;
                 storm::storage::BitVector trueStates(transitionMatrix.getRowGroupCount(), true);
-                if (dir == OptimizationDirection::Minimize) {
+                if (goal.minimize()) {
                     STORM_LOG_WARN("Results of reward computation may be too low, because of zero-reward loops.");
                     infinityStates = storm::utility::graph::performProb1E(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, trueStates, targetStates);
                 } else {
@@ -307,6 +334,15 @@ namespace storm {
                 // Create resulting vector.
                 std::vector<ValueType> result(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
                 
+                // Set values of resulting vector that are known exactly.
+                storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::infinity<ValueType>());
+                
+                // If requested, we will produce a scheduler.
+                std::unique_ptr<storm::storage::TotalScheduler> scheduler;
+                if (produceScheduler) {
+                    scheduler = std::make_unique<storm::storage::TotalScheduler>(transitionMatrix.getRowGroupCount());
+                }
+                
                 // Check whether we need to compute exact rewards for some states.
                 if (qualitative) {
                     STORM_LOG_INFO("The rewards for the initial states were determined in a preprocessing step. No exact rewards were computed.");
@@ -337,36 +373,37 @@ namespace storm {
                                 }
                             }
                         }
-                                                
-                        // 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.
-                        solver->solveEquations(dir, x, b);
                         
+                        // Now compute the results for the maybeStates
+                        MDPSparseModelCheckingHelperReturnType<ValueType> resultForMaybeStates = computeValuesOnlyMaybeStates(goal, transitionMatrix, backwardTransitions, maybeStates, submatrix, b, produceScheduler, minMaxLinearEquationSolverFactory, hint, !goal.minimize(), storm::utility::zero<ValueType>());
+
                         // Set values of resulting vector according to result.
-                        storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, x);
+                        storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, resultForMaybeStates.values);
+                        
+                        if (produceScheduler) {
+                            storm::storage::Scheduler const& subscheduler = *resultForMaybeStates.scheduler;
+                            uint_fast64_t currentSubState = 0;
+                            for (auto maybeState : maybeStates) {
+                                scheduler->setChoice(maybeState, subscheduler.getChoice(currentSubState));
+                                ++currentSubState;
+                            }
+                        }
                     }
                 }
                 
-                // Set values of resulting vector that are known exactly.
-                storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::infinity<ValueType>());
+                // Finally, if we need to produce a scheduler, we also need to figure out the parts of the scheduler for
+                // the states with reward infinity.
+                if (produceScheduler) {
+                    storm::storage::PartialScheduler relevantQualitativeScheduler;
+                    if (!goal.minimize()) {
+                        relevantQualitativeScheduler = storm::utility::graph::computeSchedulerProb0E(infinityStates, transitionMatrix);
+                    }
+                    for (auto const& stateChoicePair : relevantQualitativeScheduler) {
+                        scheduler->setChoice(stateChoicePair.first, stateChoicePair.second);
+                    }
+                }
                 
-                return result;
+                return MDPSparseModelCheckingHelperReturnType<ValueType>(std::move(result), std::move(scheduler));
             }
             
             template<typename ValueType>
@@ -669,13 +706,15 @@ 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, ModelCheckerHint const& hint);
+            template MDPSparseModelCheckingHelperReturnType<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, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory<double> const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint);
+            template MDPSparseModelCheckingHelperReturnType<double> SparseMdpPrctlHelper<double>::computeReachabilityRewards(storm::solver::SolveGoal const& goal, 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, bool produceScheduler, 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, ModelCheckerHint const& hint);
+            template MDPSparseModelCheckingHelperReturnType<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, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory<storm::RationalNumber> const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint);
+            template MDPSparseModelCheckingHelperReturnType<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeReachabilityRewards(storm::solver::SolveGoal const& goal, 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, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory<storm::RationalNumber> const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint);
 #endif
         }
     }

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

@@ -39,7 +39,7 @@ namespace storm {
 
                 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> computeValuesOnlyMaybeStates(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix<ValueType> const& submatrix, std::vector<ValueType> const& b, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint(), bool skipECWithinMaybeStatesCheck = false, boost::optional<ValueType> const& lowerResultBound = boost::none, boost::optional<ValueType> const& upperResultBound = 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());
                 
@@ -52,7 +52,10 @@ 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, ModelCheckerHint const& hint = ModelCheckerHint());
+                static MDPSparseModelCheckingHelperReturnType<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, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint());
+                
+                template<typename RewardModelType>
+                static MDPSparseModelCheckingHelperReturnType<ValueType> computeReachabilityRewards(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, 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);
@@ -63,7 +66,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, ModelCheckerHint const& hint = ModelCheckerHint());
+                static MDPSparseModelCheckingHelperReturnType<ValueType> computeReachabilityRewardsHelper(storm::solver::SolveGoal const& goal, 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, bool produceScheduler, 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/solver/MinMaxLinearEquationSolver.cpp

@@ -114,6 +114,16 @@ namespace storm {
             setUpperBound(upper);
         }
         
+        template<typename ValueType>
+        void MinMaxLinearEquationSolver<ValueType>::setSchedulerHint(storm::storage::TotalScheduler&& scheduler) {
+            schedulerHint = scheduler;
+        }
+        
+        template<typename ValueType>
+        bool MinMaxLinearEquationSolver<ValueType>::hasSchedulerHint() const {
+            return schedulerHint.is_initialized();
+        }
+        
         template<typename ValueType>
         MinMaxLinearEquationSolverFactory<ValueType>::MinMaxLinearEquationSolverFactory(bool trackScheduler) : trackScheduler(trackScheduler) {
             // Intentionally left empty.

src/storm/solver/MinMaxLinearEquationSolver.h

@@ -159,6 +159,16 @@ namespace storm {
              * Sets bounds for the solution that can potentially used by the solver.
              */
             void setBounds(ValueType const& lower, ValueType const& upper);
+            
+            /*!
+             * Sets a scheduler that might be considered by the solver as an initial guess
+             */
+            void setSchedulerHint(storm::storage::TotalScheduler&& scheduler);
+            
+            /*!
+             * Returns true iff a scheduler hint was defined
+             */
+             bool hasSchedulerHint() const;
 
         protected:
             /// The optimization direction to use for calls to functions that do not provide it explicitly. Can also be unset.
@@ -176,6 +186,9 @@ namespace storm {
             // An upper bound if one was set.
             boost::optional<ValueType> upperBound;
             
+            // A scheduler that might be considered by the solver as an initial guess
+            boost::optional<storm::storage::TotalScheduler> schedulerHint;
+            
         private:
             /// Whether some of the generated data during solver calls should be cached.
             bool cachingEnabled;

src/storm/solver/StandardMinMaxLinearEquationSolver.cpp

@@ -97,7 +97,7 @@ namespace storm {
         template<typename ValueType>
         bool StandardMinMaxLinearEquationSolver<ValueType>::solveEquationsPolicyIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
             // Create the initial scheduler.
-            std::vector<storm::storage::sparse::state_type> scheduler(this->A.getRowGroupCount());
+            std::vector<storm::storage::sparse::state_type> scheduler = this->schedulerHint ? this->schedulerHint->getChoices() : std::vector<storm::storage::sparse::state_type>(this->A.getRowGroupCount());
             
             // Get a vector for storing the right-hand side of the inner equation system.
             if(!auxiliaryRowGroupVector) {
@@ -229,6 +229,19 @@ namespace storm {
             if (!auxiliaryRowGroupVector.get()) {
                 auxiliaryRowGroupVector = std::make_unique<std::vector<ValueType>>(A.getRowGroupCount());
             }
+            
+            if(this->schedulerHint) {
+                // Resolve the nondeterminism according to the scheduler hint and solve the resulting equation system.
+                storm::storage::SparseMatrix<ValueType> submatrix = this->A.selectRowsFromRowGroups(this->schedulerHint->getChoices(), true);
+                submatrix.convertToEquationSystem();
+                storm::utility::vector::selectVectorValues<ValueType>(*auxiliaryRowGroupVector, this->schedulerHint->getChoices(), this->A.getRowGroupIndices(), b);
+
+                auto submatrixSolver = linearEquationSolverFactory->create(std::move(submatrix));
+                if (this->lowerBound) { submatrixSolver->setLowerBound(this->lowerBound.get()); }
+                if (this->upperBound) { submatrixSolver->setUpperBound(this->upperBound.get()); }
+                submatrixSolver->solveEquations(x, *auxiliaryRowGroupVector);
+            }
+            
             std::vector<ValueType>* newX = auxiliaryRowGroupVector.get();
             
             std::vector<ValueType>* currentX = &x;

src/storm/storage/SparseMatrix.cpp

@@ -1043,6 +1043,54 @@ namespace storm {
             
             return transposedMatrix;
         }
+            
+        template <typename ValueType>
+        SparseMatrix<ValueType> SparseMatrix<ValueType>::transposeSelectedRowsFromRowGroups(std::vector<uint_fast64_t> const& rowGroupChoices, bool keepZeros) const {
+            index_type rowCount = this->getColumnCount();
+            index_type columnCount = this->getRowGroupCount();
+            
+            // Get the overall entry count as well as the number of entries of each column
+            index_type entryCount = 0;
+            std::vector<index_type> rowIndications(columnCount + 1);
+            auto rowGroupChoiceIt = rowGroupChoices.begin();
+            for (index_type rowGroup = 0;  rowGroup < columnCount; ++rowGroup, ++rowGroupChoiceIt) {
+                for(auto const& entry : this->getRow(rowGroup, *rowGroupChoiceIt)) {
+                    if(keepZeros || !storm::utility::isZero(entry.getValue())) {
+                        ++entryCount;
+                        ++rowIndications[entry.getColumn() + 1];
+                    }
+                }
+            }
+            
+            // Now compute the accumulated offsets.
+            for (index_type i = 1; i < rowCount + 1; ++i) {
+                rowIndications[i] = rowIndications[i - 1] + rowIndications[i];
+            }
+            
+            std::vector<MatrixEntry<index_type, ValueType>> columnsAndValues(entryCount);
+            
+            // Create an array that stores the index for the next value to be added for
+            // each row in the transposed matrix. Initially this corresponds to the previously
+            // computed accumulated offsets.
+            std::vector<index_type> nextIndices = rowIndications;
+            
+            // Now we are ready to actually fill in the values of the transposed matrix.
+            rowGroupChoiceIt = rowGroupChoices.begin();
+            for (index_type rowGroup = 0;  rowGroup < columnCount; ++rowGroup, ++rowGroupChoiceIt) {
+                for(auto const& entry : this->getRow(rowGroup, *rowGroupChoiceIt)) {
+                    if(keepZeros || !storm::utility::isZero(entry.getValue())) {
+                        columnsAndValues[nextIndices[entry.getColumn()]] = std::make_pair(rowGroup, entry.getValue());
+                        ++nextIndices[entry.getColumn()];
+                    }
+                }
+            }
+            
+            // TODO: remove this assertion
+            auto result = storm::storage::SparseMatrix<ValueType>(std::move(columnCount), std::move(rowIndications), std::move(columnsAndValues), boost::none);
+            STORM_LOG_ASSERT(result == selectRowsFromRowGroups(rowGroupChoices, false).transpose(false, keepZeros), "Expected that the two matrices are equal");
+            return result;
+         //   return storm::storage::SparseMatrix<ValueType>(std::move(columnCount), std::move(rowIndications), std::move(columnsAndValues), boost::none);
+        }
         
         template<typename ValueType>
         void SparseMatrix<ValueType>::convertToEquationSystem() {

src/storm/storage/SparseMatrix.h

@@ -673,8 +673,7 @@ namespace storm {
             /*!
              * Selects exactly one row from each row group of this matrix and returns the resulting matrix.
              *
-             * @param rowGroupToRowIndexMapping A mapping from each row group index to a selected row in this group.
-             * @param insertDiagonalEntries If set to true, the resulting matrix will have zero entries in column i for
+s             * @param insertDiagonalEntries If set to true, the resulting matrix will have zero entries in column i for
              * each row in row group i. This can then be used for inserting other values later.
              * @return A submatrix of the current matrix by selecting one row out of each row group.
              */
@@ -701,6 +700,17 @@ namespace storm {
              */
             storm::storage::SparseMatrix<value_type> transpose(bool joinGroups = false, bool keepZeros = false) const;
             
+            
+            /*!
+             * Transposes the matrix w.r.t. the selected rows.
+             * This is equivalent to selectRowsFromRowGroups(rowGroupChoices, false).transpose(false, keepZeros) but avoids creating one intermediate matrix.
+             *
+             * @param rowGroupChoices A mapping from each row group index to a selected row in this group.
+             * @param keepZeros A flag indicating whether entries with value zero should be kept.
+             *
+             */
+            SparseMatrix<ValueType> transposeSelectedRowsFromRowGroups(std::vector<uint_fast64_t> const& rowGroupChoices, bool keepZeros = false) const;
+            
             /*!
              * Transforms the matrix into an equation system. That is, it transforms the matrix A into a matrix (1-A).
              */