diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 58c94a95b..81c53dfd9 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -426,7 +426,7 @@ namespace storm { } template - SparseMdpHintType computeHints(Environment const& env, SolutionType const& type, ModelCheckerHint const& hint, storm::OptimizationDirection const& dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& targetStates, boost::optional const& selectedChoices = boost::none) { + SparseMdpHintType computeHints(Environment const& env, SolutionType const& type, ModelCheckerHint const& hint, storm::OptimizationDirection const& dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& targetStates, bool produceScheduler, boost::optional const& selectedChoices = boost::none) { SparseMdpHintType result; // The solution to the min-max equation system is unique if we minimize until probabilities or @@ -438,7 +438,7 @@ namespace storm { // Check for requirements of the solver. bool hasSchedulerHint = hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().hasSchedulerHint(); storm::solver::GeneralMinMaxLinearEquationSolverFactory minMaxLinearEquationSolverFactory; - storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, result.uniqueSolution, dir, hasSchedulerHint); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, result.uniqueSolution, dir, hasSchedulerHint, produceScheduler); if (requirements.hasEnabledRequirement()) { // If the solver still requires no end-components, we have to eliminate them later. if (requirements.noEndComponents()) { @@ -737,7 +737,7 @@ namespace storm { // In this case we have have to compute the remaining probabilities. // Obtain proper hint information either from the provided hint or from requirements of the solver. - SparseMdpHintType hintInformation = computeHints(env, SolutionType::UntilProbabilities, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates, phiStates, qualitativeStateSets.statesWithProbability1); + SparseMdpHintType hintInformation = computeHints(env, SolutionType::UntilProbabilities, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates, phiStates, qualitativeStateSets.statesWithProbability1, produceScheduler); // Declare the components of the equation system we will solve. storm::storage::SparseMatrix submatrix; @@ -1222,7 +1222,7 @@ namespace storm { } // Obtain proper hint information either from the provided hint or from requirements of the solver. - SparseMdpHintType hintInformation = computeHints(env, SolutionType::ExpectedRewards, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates, ~qualitativeStateSets.rewardZeroStates, qualitativeStateSets.rewardZeroStates, selectedChoices); + SparseMdpHintType hintInformation = computeHints(env, SolutionType::ExpectedRewards, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates, ~qualitativeStateSets.rewardZeroStates, qualitativeStateSets.rewardZeroStates, produceScheduler, selectedChoices); // Declare the components of the equation system we will solve. storm::storage::SparseMatrix submatrix; diff --git a/src/storm/solver/MinMaxLinearEquationSolver.cpp b/src/storm/solver/MinMaxLinearEquationSolver.cpp index f7cbf4bfe..e9b5a0fdd 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/MinMaxLinearEquationSolver.cpp @@ -161,9 +161,10 @@ namespace storm { } template - MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolverFactory::getRequirements(Environment const& env, bool hasUniqueSolution, boost::optional const& direction, bool const& hasInitialScheduler) const { + MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolverFactory::getRequirements(Environment const& env, bool hasUniqueSolution, boost::optional const& direction, bool hasInitialScheduler, bool trackScheduler) const { // Create dummy solver and ask it for requirements. std::unique_ptr> solver = this->create(env); + solver->setTrackScheduler(trackScheduler); solver->setHasUniqueSolution(hasUniqueSolution); return solver->getRequirements(env, direction, hasInitialScheduler); } diff --git a/src/storm/solver/MinMaxLinearEquationSolver.h b/src/storm/solver/MinMaxLinearEquationSolver.h index 9ea9ac90a..7ca89dfb9 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.h +++ b/src/storm/solver/MinMaxLinearEquationSolver.h @@ -194,7 +194,7 @@ namespace storm { * Retrieves the requirements of the solver that would be created when calling create() right now. The * requirements are guaranteed to be ordered according to their appearance in the SolverRequirement type. */ - MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, bool hasUniqueSolution = false, boost::optional const& direction = boost::none, bool const& hasInitialScheduler = false) const; + MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, bool hasUniqueSolution = false, boost::optional const& direction = boost::none, bool hasInitialScheduler = false, bool trackScheduler = false) const; void setRequirementsChecked(bool value = true); bool isRequirementsCheckedSet() const;