started on hybrid MDP helper respecting solver requirements

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

@@ -25,6 +25,36 @@ namespace storm {
     namespace modelchecker {
         namespace helper {
             
+            template <typename ValueType>
+            std::vector<uint64_t> computeValidInitialScheduler(uint64_t numberOfMaybeStates, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& b) {
+                std::vector<uint64_t> result(numberOfMaybeStates);
+                storm::storage::BitVector targetStates(numberOfMaybeStates);
+                
+                for (uint64_t state = 0; state < numberOfMaybeStates; ++state) {
+                    // Record all states with non-zero probability of moving directly to the target states.
+                    for (uint64_t row = transitionMatrix.getRowGroupIndices()[state]; row < transitionMatrix.getRowGroupIndices()[state + 1]; ++row) {
+                        if (!storm::utility::isZero(b[row])) {
+                            targetStates.set(state);
+                            result[state] = row - transitionMatrix.getRowGroupIndices()[state];
+                        }
+                    }
+                }
+                
+                if (!targetStates.full()) {
+                    storm::storage::Scheduler<ValueType> validScheduler(numberOfMaybeStates);
+                    storm::storage::SparseMatrix<ValueType> backwardTransitions = transitionMatrix.transpose(true);
+                    storm::utility::graph::computeSchedulerProbGreater0E(transitionMatrix, backwardTransitions, storm::storage::BitVector(numberOfMaybeStates, true), targetStates, validScheduler, boost::none);
+                    
+                    for (uint64_t state = 0; state < numberOfMaybeStates; ++state) {
+                        if (!targetStates.get(state)) {
+                            result[state] = validScheduler.getChoice(state).getDeterministicChoice();
+                        }
+                    }
+                }
+                
+                return result;
+            }
+            
             template<storm::dd::DdType DdType, typename ValueType>
             std::unique_ptr<CheckResult> HybridMdpPrctlHelper<DdType, ValueType>::computeUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
                 // We need to identify the states which have to be taken out of the matrix, i.e. all states that have
@@ -75,14 +105,26 @@ namespace storm {
                         // Translate the symbolic matrix/vector to their explicit representations and solve the equation system.
                         std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd);
                         
-                        // Check for requirements of the solver.
-                        storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::UntilProbabilities);
-                        STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
-
                         // Create the solution vector.
                         std::vector<ValueType> x(maybeStates.getNonZeroCount(), storm::utility::zero<ValueType>());
+
+                        // Check for requirements of the solver.
+                        storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::UntilProbabilities, dir);
+                        boost::optional<std::vector<uint64_t>> initialScheduler;
+                        if (!requirements.empty()) {
+                            if (requirements.requires(storm::solver::MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler)) {
+                                STORM_LOG_DEBUG("Computing valid scheduler hint, because the solver requires it.");
+                                initialScheduler = computeValidInitialScheduler<ValueType>(x.size(), explicitRepresentation.first, explicitRepresentation.second);
+
+                                requirements.set(storm::solver::MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler, false);
+                            }
+                            STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
+                        }
                         
                         std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(std::move(explicitRepresentation.first));
+                        if (initialScheduler) {
+                            solver->setInitialScheduler(std::move(initialScheduler.get()));
+                        }
                         solver->setRequirementsChecked();
                         solver->solveEquations(dir, x, explicitRepresentation.second);
                         
@@ -247,7 +289,7 @@ namespace storm {
                         // non-maybe states in the matrix.
                         storm::dd::Add<DdType, ValueType> submatrix = transitionMatrix * maybeStatesAdd;
                         
-                        // Then compute the state reward vector to use in the computation.
+                        // Then compute the reward vector to use in the computation.
                         storm::dd::Add<DdType, ValueType> subvector = rewardModel.getTotalRewardVector(maybeStatesAdd, submatrix, model.getColumnVariables());
                         if (!rewardModel.hasStateActionRewards() && !rewardModel.hasTransitionRewards()) {
                             // If the reward model neither has state-action nor transition rewards, we need to multiply

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

@@ -87,12 +87,12 @@ namespace storm {
             
             template<typename ValueType>
             std::vector<uint_fast64_t> computeValidSchedulerHint(storm::solver::MinMaxLinearEquationSolverSystemType const& type, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& filterStates, storm::storage::BitVector const& targetStates) {
-                std::unique_ptr<storm::storage::Scheduler<ValueType>> validScheduler = std::make_unique<storm::storage::Scheduler<ValueType>>(maybeStates.size());
+                storm::storage::Scheduler<ValueType> validScheduler(maybeStates.size());
 
                 if (type == storm::solver::MinMaxLinearEquationSolverSystemType::UntilProbabilities) {
-                    storm::utility::graph::computeSchedulerProbGreater0E(transitionMatrix, backwardTransitions, filterStates, targetStates, *validScheduler, boost::none);
+                    storm::utility::graph::computeSchedulerProbGreater0E(transitionMatrix, backwardTransitions, filterStates, targetStates, validScheduler, boost::none);
                 } else if (type == storm::solver::MinMaxLinearEquationSolverSystemType::ReachabilityRewards) {
-                    storm::utility::graph::computeSchedulerProb1E(maybeStates | targetStates, transitionMatrix, backwardTransitions, filterStates, targetStates, *validScheduler);
+                    storm::utility::graph::computeSchedulerProb1E(maybeStates | targetStates, transitionMatrix, backwardTransitions, filterStates, targetStates, validScheduler);
                 } else {
                     STORM_LOG_ASSERT(false, "Unexpected equation system type.");
                 }
@@ -101,7 +101,7 @@ namespace storm {
                 std::vector<uint_fast64_t> schedulerHint(maybeStates.getNumberOfSetBits());
                 auto maybeIt = maybeStates.begin();
                 for (auto& choice : schedulerHint) {
-                    choice = validScheduler->getChoice(*maybeIt).getDeterministicChoice();
+                    choice = validScheduler.getChoice(*maybeIt).getDeterministicChoice();
                     ++maybeIt;
                 }
                 return schedulerHint;

src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp

@@ -225,10 +225,8 @@ namespace storm {
                     }
                 }
             } else if (equationSystemType == MinMaxLinearEquationSolverSystemType::ReachabilityRewards) {
-                if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::PolicyIteration) {
-                    if (!direction || direction.get() == OptimizationDirection::Minimize) {
-                        requirements.set(MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler);
-                    }
+                if (!direction || direction.get() == OptimizationDirection::Minimize) {
+                    requirements.set(MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler);
                 }
             }
             

src/storm/storage/SparseMatrix.h

@@ -688,7 +688,7 @@ namespace storm {
             /*!
              * Selects exactly one row from each row group of this matrix and returns the resulting matrix.
              *
-s             * @param insertDiagonalEntries If set to true, the resulting matrix will have zero entries in column i for
+             * @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.
              */
@@ -715,7 +715,6 @@ s             * @param insertDiagonalEntries If set to true, the resulting matri
              */
             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.