From 4c5cdfeafc65b15f16ddcb499273dae7dec37336 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 4 Sep 2017 15:51:34 +0200 Subject: [PATCH] Sparse MDP helper now also respects solver requirements for reachability rewards --- .../helper/SparseMarkovAutomatonCslHelper.cpp | 6 +- .../prctl/helper/HybridMdpPrctlHelper.cpp | 10 +- .../prctl/helper/SparseMdpPrctlHelper.cpp | 333 +++++++++++------- .../prctl/helper/SparseMdpPrctlHelper.h | 4 - .../modules/EigenEquationSolverSettings.cpp | 2 +- .../IterativeMinMaxLinearEquationSolver.cpp | 27 +- .../IterativeMinMaxLinearEquationSolver.h | 2 +- .../solver/MinMaxLinearEquationSolver.cpp | 19 +- src/storm/solver/MinMaxLinearEquationSolver.h | 100 ++++-- 9 files changed, 328 insertions(+), 175 deletions(-) diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index ecf2b6759..d9a58c585 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -89,7 +89,7 @@ namespace storm { } // Check for requirements of the solver. - std::vector requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::UntilProbabilities); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::UntilProbabilities); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(aProbabilistic); @@ -376,7 +376,7 @@ namespace storm { std::vector x(numberOfSspStates); // Check for requirements of the solver. - std::vector requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::StochasticShortestPath); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::StochasticShortestPath); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(sspMatrix); @@ -584,7 +584,7 @@ namespace storm { std::vector b = probabilisticChoiceRewards; // Check for requirements of the solver. - std::vector requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::ReachabilityRewards); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::ReachabilityRewards); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); auto solver = minMaxLinearEquationSolverFactory.create(std::move(aProbabilistic)); diff --git a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp index b94b8ad9c..24fe1326f 100644 --- a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp @@ -72,15 +72,15 @@ namespace storm { // Finally cut away all columns targeting non-maybe states. submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); - // Create the solution vector. - std::vector x(maybeStates.getNonZeroCount(), storm::utility::zero()); - // Translate the symbolic matrix/vector to their explicit representations and solve the equation system. std::pair, std::vector> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd); // Check for requirements of the solver. - std::vector requirements = linearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::UntilProbabilities); + 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 x(maybeStates.getNonZeroCount(), storm::utility::zero()); std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(explicitRepresentation.first)); solver->setRequirementsChecked(); @@ -274,7 +274,7 @@ namespace storm { std::pair, std::vector> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd); // Check for requirements of the solver. - std::vector requirements = linearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::ReachabilityRewards); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::ReachabilityRewards); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); // Now solve the resulting equation system. diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 884396c10..a90c6bbfc 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -85,6 +85,203 @@ namespace storm { return result; } + template + std::vector computeValidSchedulerHint(storm::solver::MinMaxLinearEquationSolverSystemType const& type, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& filterStates, storm::storage::BitVector const& targetStates) { + std::unique_ptr> validScheduler = std::make_unique>(maybeStates.size()); + + if (type == storm::solver::MinMaxLinearEquationSolverSystemType::UntilProbabilities) { + 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); + } else { + STORM_LOG_ASSERT(false, "Unexpected equation system type."); + } + + // Extract the relevant parts of the scheduler for the solver. + std::vector schedulerHint(maybeStates.getNumberOfSetBits()); + auto maybeIt = maybeStates.begin(); + for (auto& choice : schedulerHint) { + choice = validScheduler->getChoice(*maybeIt).getDeterministicChoice(); + ++maybeIt; + } + return schedulerHint; + } + + template + struct SparseMdpHintType { + bool hasSchedulerHint() const { + return static_cast(schedulerHint); + } + + bool hasValueHint() const { + return static_cast(valueHint); + } + + bool hasLowerResultBound() const { + return static_cast(lowerResultBound); + } + + ValueType const& getLowerResultBound() const { + return lowerResultBound.get(); + } + + bool hasUpperResultBound() const { + return static_cast(upperResultBound); + } + + ValueType const& getUpperResultBound() const { + return upperResultBound.get(); + } + + std::vector& getSchedulerHint() { + return schedulerHint.get(); + } + + std::vector& getValueHint() { + return valueHint.get(); + } + + boost::optional> schedulerHint; + boost::optional> valueHint; + boost::optional lowerResultBound; + boost::optional upperResultBound; + }; + + template + void extractHintInformationForMaybeStates(SparseMdpHintType& hintStorage, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& maybeStates, boost::optional const& selectedChoices, ModelCheckerHint const& hint, bool skipECWithinMaybeStatesCheck) { + + // Deal with scheduler hint. + if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().hasSchedulerHint()) { + if (hintStorage.hasSchedulerHint()) { + STORM_LOG_WARN("A scheduler hint was provided, but the solver requires a specific one. The provided scheduler hint will be ignored."); + } else { + auto const& schedulerHint = hint.template asExplicitModelCheckerHint().getSchedulerHint(); + std::vector hintChoices; + + // The scheduler hint is only applicable if it induces no BSCC consisting of maybe states. + bool hintApplicable; + if (!skipECWithinMaybeStatesCheck) { + hintChoices.reserve(maybeStates.size()); + for (uint_fast64_t state = 0; state < maybeStates.size(); ++state) { + hintChoices.push_back(schedulerHint.getChoice(state).getDeterministicChoice()); + } + hintApplicable = storm::utility::graph::performProb1(transitionMatrix.transposeSelectedRowsFromRowGroups(hintChoices), maybeStates, ~maybeStates).full(); + } else { + hintApplicable = true; + } + + if (hintApplicable) { + // Compute the hint w.r.t. the given subsystem. + hintChoices.clear(); + hintChoices.reserve(maybeStates.getNumberOfSetBits()); + for (auto const& state : maybeStates) { + uint_fast64_t hintChoice = schedulerHint.getChoice(state).getDeterministicChoice(); + if (selectedChoices) { + uint_fast64_t firstChoice = transitionMatrix.getRowGroupIndices()[state]; + uint_fast64_t lastChoice = firstChoice + hintChoice; + hintChoice = 0; + for (uint_fast64_t choice = selectedChoices->getNextSetIndex(firstChoice); choice < lastChoice; choice = selectedChoices->getNextSetIndex(choice + 1)) { + ++hintChoice; + } + } + hintChoices.push_back(hintChoice); + } + hintStorage.schedulerHint = std::move(hintChoices); + } + } + } + + // Deal with solution value hint. Only applicable if there are no End Components consisting of maybe states. + if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().hasResultHint() && (skipECWithinMaybeStatesCheck || hintStorage.hasSchedulerHint() || storm::utility::graph::performProb1A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, maybeStates, ~maybeStates).full())) { + hintStorage.valueHint = storm::utility::vector::filterVector(hint.template asExplicitModelCheckerHint().getResultHint(), maybeStates); + } + } + + template + SparseMdpHintType computeHints(storm::solver::MinMaxLinearEquationSolverSystemType 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, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, boost::optional const& selectedChoices = boost::none) { + SparseMdpHintType result; + + // Check for requirements of the solver. + storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(type); + if (!(hint.isExplicitModelCheckerHint() && hint.asExplicitModelCheckerHint().getNoEndComponentsInMaybeStates()) && !requirements.empty()) { + if (requirements.requires(storm::solver::MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler)) { + STORM_LOG_DEBUG("Computing valid scheduler hint, because the solver requires it."); + result.schedulerHint = computeValidSchedulerHint(type, transitionMatrix, backwardTransitions, maybeStates, phiStates, targetStates); + requirements.set(storm::solver::MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler, false); + } + STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "There are unchecked requirements of the solver."); + } + + bool skipEcWithinMaybeStatesCheck = dir == storm::OptimizationDirection::Minimize || (hint.isExplicitModelCheckerHint() && hint.asExplicitModelCheckerHint().getNoEndComponentsInMaybeStates()); + extractHintInformationForMaybeStates(result, transitionMatrix, backwardTransitions, maybeStates, selectedChoices, hint, skipEcWithinMaybeStatesCheck); + + result.lowerResultBound = storm::utility::zero(); + if (type == storm::solver::MinMaxLinearEquationSolverSystemType::UntilProbabilities) { + result.upperResultBound = storm::utility::one(); + } else if (type == storm::solver::MinMaxLinearEquationSolverSystemType::ReachabilityRewards) { + // Intentionally left empty. + } else { + STORM_LOG_ASSERT(false, "Unexpected equation system type."); + } + + return result; + } + + template + struct MaybeStateResult { + MaybeStateResult(std::vector&& values) : values(std::move(values)) { + // Intentionally left empty. + } + + bool hasScheduler() const { + return static_cast(scheduler); + } + + std::vector const& getScheduler() const { + return scheduler.get(); + } + + std::vector const& getValues() const { + return values; + } + + std::vector values; + boost::optional> scheduler; + }; + + template + MaybeStateResult computeValuesForMaybeStates(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& submatrix, std::vector const& b, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, SparseMdpHintType& hint) { + + // Set up the solver. + std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(goal, minMaxLinearEquationSolverFactory, submatrix); + solver->setRequirementsChecked(); + if (hint.hasLowerResultBound()) { + solver->setLowerBound(hint.getLowerResultBound()); + } + if (hint.hasUpperResultBound()) { + solver->setUpperBound(hint.getUpperResultBound()); + } + if (hint.hasSchedulerHint()) { + solver->setInitialScheduler(std::move(hint.getSchedulerHint())); + } + solver->setTrackScheduler(produceScheduler); + + // Initialize the solution vector. + std::vector x = hint.hasValueHint() ? std::move(hint.getValueHint()) : std::vector(submatrix.getRowGroupCount(), hint.hasLowerResultBound() ? hint.getLowerResultBound() : storm::utility::zero()); + + // Solve the corresponding system of equations. + solver->solveEquations(x, b); + + // Create result. + MaybeStateResult result(std::move(x)); + + // If requested, return the requested scheduler. + if (produceScheduler) { + result.scheduler = std::move(solver->getSchedulerChoices()); + } + return result; + } + template MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint) { STORM_LOG_THROW(!(qualitative && produceScheduler), storm::exceptions::InvalidSettingsException, "Cannot produce scheduler when performing qualitative model checking only."); @@ -154,42 +351,17 @@ namespace storm { // the accumulated probability of going from state i to some 'yes' state. std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(maybeStates, statesWithProbability1); - // obtain hint information if possible - bool skipEcWithinMaybeStatesCheck = goal.minimize() || (hint.isExplicitModelCheckerHint() && hint.asExplicitModelCheckerHint().getNoEndComponentsInMaybeStates()); - std::pair>, boost::optional>> hintInformation = extractHintInformationForMaybeStates(transitionMatrix, backwardTransitions, maybeStates, boost::none, hint, skipEcWithinMaybeStatesCheck); - - // Check for requirements of the solver. - std::vector requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::UntilProbabilities); - if (!requirements.empty()) { - std::unique_ptr> validScheduler; - for (auto const& requirement : requirements) { - if (requirement == storm::solver::MinMaxLinearEquationSolverRequirement::ValidSchedulerHint) { - // If the solver requires a valid scheduler (a scheduler that produces non-zero - // probabilities for all maybe states), we need to compute such a scheduler now. - validScheduler = std::make_unique>(maybeStates.size()); - storm::utility::graph::computeSchedulerProbGreater0E(transitionMatrix, backwardTransitions, phiStates, statesWithProbability1, *validScheduler, boost::none); - - STORM_LOG_WARN_COND(hintInformation.second, "A scheduler hint was provided, but the solver requires a valid scheduler hint. The hint will be ignored."); - - hintInformation.second = std::vector(maybeStates.getNumberOfSetBits()); - auto maybeIt = maybeStates.begin(); - for (auto& choice : hintInformation.second.get()) { - choice = validScheduler->getChoice(*maybeIt).getDeterministicChoice(); - } - } else { - STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); - } - } - } - + // Obtain proper hint information either from the provided hint or from requirements of the solver. + SparseMdpHintType hintInformation = computeHints(storm::solver::MinMaxLinearEquationSolverSystemType::UntilProbabilities, hint, goal.direction(), transitionMatrix, backwardTransitions, maybeStates, phiStates, statesWithProbability1, minMaxLinearEquationSolverFactory); + // Now compute the results for the maybe states. - std::pair, boost::optional>> resultForMaybeStates = computeValuesOnlyMaybeStates(goal, submatrix, b, produceScheduler, minMaxLinearEquationSolverFactory, std::move(hintInformation.first), std::move(hintInformation.second), storm::utility::zero(), storm::utility::one()); + MaybeStateResult resultForMaybeStates = computeValuesForMaybeStates(goal, submatrix, b, produceScheduler, minMaxLinearEquationSolverFactory, hintInformation); // Set values of resulting vector according to result. - storm::utility::vector::setVectorValues(result, maybeStates, resultForMaybeStates.first); + storm::utility::vector::setVectorValues(result, maybeStates, resultForMaybeStates.getValues()); if (produceScheduler) { - std::vector const& subChoices = resultForMaybeStates.second.get(); + std::vector const& subChoices = resultForMaybeStates.getScheduler(); auto subChoiceIt = subChoices.begin(); for (auto maybeState : maybeStates) { scheduler->setChoice(*subChoiceIt, maybeState); @@ -222,89 +394,6 @@ namespace storm { return MDPSparseModelCheckingHelperReturnType(std::move(result), std::move(scheduler)); } - - template - std::pair>, boost::optional>> SparseMdpPrctlHelper::extractHintInformationForMaybeStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& maybeStates, boost::optional const& selectedChoices, ModelCheckerHint const& hint, bool skipECWithinMaybeStatesCheck) { - - // Scheduler hint - boost::optional> subSchedulerChoices; - if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().hasSchedulerHint()) { - auto const& schedulerHint = hint.template asExplicitModelCheckerHint().getSchedulerHint(); - std::vector hintChoices; - - // the scheduler hint is only applicable if it induces no BSCC consisting of maybestates - bool hintApplicable; - if (!skipECWithinMaybeStatesCheck) { - hintChoices.reserve(maybeStates.size()); - for (uint_fast64_t state = 0; state < maybeStates.size(); ++state) { - hintChoices.push_back(schedulerHint.getChoice(state).getDeterministicChoice()); - } - hintApplicable = storm::utility::graph::performProb1(transitionMatrix.transposeSelectedRowsFromRowGroups(hintChoices), maybeStates, ~maybeStates).full(); - } else { - hintApplicable = true; - } - - if (hintApplicable) { - // Compute the hint w.r.t. the given subsystem - hintChoices.clear(); - hintChoices.reserve(maybeStates.getNumberOfSetBits()); - for (auto const& state : maybeStates) { - uint_fast64_t hintChoice = schedulerHint.getChoice(state).getDeterministicChoice(); - if (selectedChoices) { - uint_fast64_t firstChoice = transitionMatrix.getRowGroupIndices()[state]; - uint_fast64_t lastChoice = firstChoice + hintChoice; - hintChoice = 0; - for (uint_fast64_t choice = selectedChoices->getNextSetIndex(firstChoice); choice < lastChoice; choice = selectedChoices->getNextSetIndex(choice + 1)) { - ++hintChoice; - } - } - hintChoices.push_back(hintChoice); - } - subSchedulerChoices = std::move(hintChoices); - } - } - - // Solution value hint - boost::optional> subValues; - // The result hint is only applicable if there are no End Components consisting of maybestates - if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().hasResultHint() && - (skipECWithinMaybeStatesCheck || subSchedulerChoices || - storm::utility::graph::performProb1A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, maybeStates, ~maybeStates).full())) { - subValues = storm::utility::vector::filterVector(hint.template asExplicitModelCheckerHint().getResultHint(), maybeStates); - } - return std::make_pair(std::move(subValues), std::move(subSchedulerChoices)); - } - - template - std::pair, boost::optional>> SparseMdpPrctlHelper::computeValuesOnlyMaybeStates(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& submatrix, std::vector const& b, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, boost::optional>&& hintValues, boost::optional>&& hintChoices, boost::optional const& lowerResultBound, boost::optional const& upperResultBound) { - - // Set up the solver. - std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(goal, minMaxLinearEquationSolverFactory, submatrix); - solver->setRequirementsChecked(); - if (lowerResultBound) { - solver->setLowerBound(lowerResultBound.get()); - } - if (upperResultBound) { - solver->setUpperBound(upperResultBound.get()); - } - if (hintChoices) { - solver->setSchedulerHint(std::move(hintChoices.get())); - } - solver->setTrackScheduler(produceScheduler); - - // Initialize the solution vector. - std::vector x = hintValues ? std::move(hintValues.get()) : std::vector(submatrix.getRowGroupCount(), lowerResultBound ? lowerResultBound.get() : storm::utility::zero()); - - // Solve the corresponding system of equations. - solver->solveEquations(x, b); - - // If requested, return the requested scheduler. - if (produceScheduler) { - return std::pair, boost::optional>>(std::move(x), std::move(solver->getSchedulerChoices())); - } else { - return std::pair, boost::optional>>(std::move(x), boost::none); - } - } template MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint) { @@ -462,6 +551,7 @@ namespace storm { // Prepare matrix and vector for the equation system. storm::storage::SparseMatrix submatrix; std::vector b; + // Remove rows and columns from the original transition probability matrix for states whose reward values are already known. // If there are infinity states, we additionaly have to remove choices of maybeState that lead to infinity boost::optional selectedChoices; // if not given, all maybeState choices are selected @@ -475,18 +565,17 @@ namespace storm { storm::utility::vector::filterVectorInPlace(b, *selectedChoices); } - // obtain hint information if possible - bool skipEcWithinMaybeStatesCheck = !goal.minimize() || (hint.isExplicitModelCheckerHint() && hint.asExplicitModelCheckerHint().getNoEndComponentsInMaybeStates()); - std::pair>, boost::optional>> hintInformation = extractHintInformationForMaybeStates(transitionMatrix, backwardTransitions, maybeStates, selectedChoices, hint, skipEcWithinMaybeStatesCheck); + // Obtain proper hint information either from the provided hint or from requirements of the solver. + SparseMdpHintType hintInformation = computeHints(storm::solver::MinMaxLinearEquationSolverSystemType::ReachabilityRewards, hint, goal.direction(), transitionMatrix, backwardTransitions, maybeStates, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), targetStates, minMaxLinearEquationSolverFactory, selectedChoices); - // Now compute the results for the maybeStates - std::pair, boost::optional>> resultForMaybeStates = computeValuesOnlyMaybeStates(goal, submatrix, b, produceScheduler, minMaxLinearEquationSolverFactory, std::move(hintInformation.first), std::move(hintInformation.second), storm::utility::zero(), boost::none); + // Now compute the results for the maybe states. + MaybeStateResult resultForMaybeStates = computeValuesForMaybeStates(goal, submatrix, b, produceScheduler, minMaxLinearEquationSolverFactory, hintInformation); // Set values of resulting vector according to result. - storm::utility::vector::setVectorValues(result, maybeStates, resultForMaybeStates.first); + storm::utility::vector::setVectorValues(result, maybeStates, resultForMaybeStates.getValues()); if (produceScheduler) { - std::vector const& subChoices = resultForMaybeStates.second.get(); + std::vector const& subChoices = resultForMaybeStates.getScheduler(); auto subChoiceIt = subChoices.begin(); if (selectedChoices) { for (auto maybeState : maybeStates) { @@ -678,7 +767,7 @@ namespace storm { storm::storage::SparseMatrix sspMatrix = sspMatrixBuilder.build(currentChoice, numberOfSspStates, numberOfSspStates); // Check for requirements of the solver. - std::vector requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::StochasticShortestPath); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::StochasticShortestPath); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); std::vector sspResult(numberOfSspStates); diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h index e82c89cc2..5cf2bcfaf 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h @@ -39,10 +39,6 @@ namespace storm { static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); - static std::pair>, boost::optional>> extractHintInformationForMaybeStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& maybeStates, boost::optional const& selectedChoices, ModelCheckerHint const& hint, bool skipECWithinMaybeStatesCheck); - - static std::pair, boost::optional>> computeValuesOnlyMaybeStates(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& submatrix, std::vector const& b, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, boost::optional>&& hintValues = boost::none, boost::optional>&& hintChoices = boost::none, boost::optional const& lowerResultBound = boost::none, boost::optional const& upperResultBound = boost::none); - static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); static std::vector computeGloballyProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useMecBasedTechnique = false); diff --git a/src/storm/settings/modules/EigenEquationSolverSettings.cpp b/src/storm/settings/modules/EigenEquationSolverSettings.cpp index cc3589937..ea25da11d 100644 --- a/src/storm/settings/modules/EigenEquationSolverSettings.cpp +++ b/src/storm/settings/modules/EigenEquationSolverSettings.cpp @@ -101,7 +101,7 @@ namespace storm { // This list does not include the precision, because this option is shared with other modules. bool optionsSet = isLinearEquationSystemMethodSet() || isPreconditioningMethodSet() || isMaximalIterationCountSet(); - STORM_LOG_WARN_COND(storm::settings::getModule().getEquationSolver() == storm::solver::EquationSolverType::Gmmxx || !optionsSet, "eigen is not selected as the preferred equation solver, so setting options for eigen might have no effect."); + STORM_LOG_WARN_COND(storm::settings::getModule().getEquationSolver() == storm::solver::EquationSolverType::Eigen || !optionsSet, "Eigen is not selected as the preferred equation solver, so setting options for eigen might have no effect."); return true; } diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index 4980c32c3..0718db5b8 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -108,7 +108,7 @@ namespace storm { template bool IterativeMinMaxLinearEquationSolver::solveEquationsPolicyIteration(OptimizationDirection dir, std::vector& x, std::vector const& b) const { // Create the initial scheduler. - std::vector scheduler = this->hasSchedulerHint() ? this->choicesHint.get() : std::vector(this->A->getRowGroupCount()); + std::vector scheduler = this->hasInitialScheduler() ? this->getInitialScheduler() : std::vector(this->A->getRowGroupCount()); // Get a vector for storing the right-hand side of the inner equation system. if(!auxiliaryRowGroupVector) { @@ -135,9 +135,6 @@ namespace storm { uint64_t iterations = 0; do { // Solve the equation system for the 'DTMC'. - // FIXME: we need to remove the 0- and 1- states to make the solution unique. - // HOWEVER: if we start with a valid scheduler, then we will never get an illegal one, because staying - // within illegal MECs will never strictly improve the value. Is this true? solver->solveEquations(x, subB); // Go through the multiplication result and see whether we can improve any of the choices. @@ -218,15 +215,23 @@ namespace storm { } template - std::vector IterativeMinMaxLinearEquationSolver::getRequirements(MinMaxLinearEquationSolverSystemType const& equationSystemType, boost::optional const& direction) const { - std::vector requirements; + MinMaxLinearEquationSolverRequirements IterativeMinMaxLinearEquationSolver::getRequirements(MinMaxLinearEquationSolverSystemType const& equationSystemType, boost::optional const& direction) const { + MinMaxLinearEquationSolverRequirements requirements; + if (equationSystemType == MinMaxLinearEquationSolverSystemType::UntilProbabilities) { if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration) { if (!direction || direction.get() == OptimizationDirection::Maximize) { - requirements.push_back(MinMaxLinearEquationSolverRequirement::ValidSchedulerHint); + requirements.set(MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler); + } + } + } else if (equationSystemType == MinMaxLinearEquationSolverSystemType::ReachabilityRewards) { + if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration) { + if (!direction || direction.get() == OptimizationDirection::Minimize) { + requirements.set(MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler); } } } + return requirements; } @@ -246,11 +251,11 @@ namespace storm { auxiliaryRowGroupVector = std::make_unique>(this->A->getRowGroupCount()); } - if (this->hasSchedulerHint()) { - // Resolve the nondeterminism according to the scheduler hint - storm::storage::SparseMatrix submatrix = this->A->selectRowsFromRowGroups(this->choicesHint.get(), true); + if (this->hasInitialScheduler()) { + // Resolve the nondeterminism according to the initial scheduler. + storm::storage::SparseMatrix submatrix = this->A->selectRowsFromRowGroups(this->getInitialScheduler(), true); submatrix.convertToEquationSystem(); - storm::utility::vector::selectVectorValues(*auxiliaryRowGroupVector, this->choicesHint.get(), this->A->getRowGroupIndices(), b); + storm::utility::vector::selectVectorValues(*auxiliaryRowGroupVector, this->getInitialScheduler(), this->A->getRowGroupIndices(), b); // Solve the resulting equation system. // Note that the linEqSolver might consider a slightly different interpretation of "equalModuloPrecision". Hence, we iteratively increase its precision. diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h index ac51de473..85aeb3843 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h @@ -50,7 +50,7 @@ namespace storm { ValueType getPrecision() const; bool getRelative() const; - virtual std::vector getRequirements(MinMaxLinearEquationSolverSystemType const& equationSystemType, boost::optional const& direction = boost::none) const override; + virtual MinMaxLinearEquationSolverRequirements getRequirements(MinMaxLinearEquationSolverSystemType const& equationSystemType, boost::optional const& direction = boost::none) const override; private: bool solveEquationsPolicyIteration(OptimizationDirection dir, std::vector& x, std::vector const& b) const; diff --git a/src/storm/solver/MinMaxLinearEquationSolver.cpp b/src/storm/solver/MinMaxLinearEquationSolver.cpp index ba0847ded..ace2aa3db 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/MinMaxLinearEquationSolver.cpp @@ -128,18 +128,23 @@ namespace storm { } template - void MinMaxLinearEquationSolver::setSchedulerHint(std::vector&& choices) { - choicesHint = std::move(choices); + void MinMaxLinearEquationSolver::setInitialScheduler(std::vector&& choices) { + initialScheduler = std::move(choices); } template - bool MinMaxLinearEquationSolver::hasSchedulerHint() const { - return choicesHint.is_initialized(); + bool MinMaxLinearEquationSolver::hasInitialScheduler() const { + return static_cast(initialScheduler); } template - std::vector MinMaxLinearEquationSolver::getRequirements(MinMaxLinearEquationSolverSystemType const& equationSystemType, boost::optional const& direction) const { - return std::vector(); + std::vector const& MinMaxLinearEquationSolver::getInitialScheduler() const { + return initialScheduler.get(); + } + + template + MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolver::getRequirements(MinMaxLinearEquationSolverSystemType const& equationSystemType, boost::optional const& direction) const { + return MinMaxLinearEquationSolverRequirements(); } template @@ -210,7 +215,7 @@ namespace storm { } template - std::vector MinMaxLinearEquationSolverFactory::getRequirements(MinMaxLinearEquationSolverSystemType const& equationSystemType, boost::optional const& direction) const { + MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolverFactory::getRequirements(MinMaxLinearEquationSolverSystemType const& equationSystemType, boost::optional const& direction) const { // Create dummy solver and ask it for requirements. std::unique_ptr> solver = this->create(); return solver->getRequirements(equationSystemType, direction); diff --git a/src/storm/solver/MinMaxLinearEquationSolver.h b/src/storm/solver/MinMaxLinearEquationSolver.h index 240820579..2f2188eaf 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.h +++ b/src/storm/solver/MinMaxLinearEquationSolver.h @@ -29,19 +29,72 @@ namespace storm { StochasticShortestPath }; - // Possible requirements of solvers. Note that the order must not be changed as it shall be guaranteed that the - // solver announces requirements in the order in which they appear in this list. - enum class MinMaxLinearEquationSolverRequirement { - // Graph requirements. - NoEndComponents, - - // Hint requirements. - ValidSchedulerHint, - ValidValueHint, - - // Global bounds requirements. - GlobalUpperBound, - GlobalLowerBound + class MinMaxLinearEquationSolverRequirements { + public: + enum class Element { + NoEndComponents, NoZeroRewardEndComponents, ValidInitialScheduler, GlobalLowerBound, GlobalUpperBound + }; + + MinMaxLinearEquationSolverRequirements() : noEndComponents(false), noZeroRewardEndComponents(false), validInitialScheduler(false), globalLowerBound(false), globalUpperBound(false) { + // Intentionally left empty. + } + + MinMaxLinearEquationSolverRequirements& setNoEndComponents(bool value = true) { + noEndComponents = value; + return *this; + } + + MinMaxLinearEquationSolverRequirements& setNoZeroRewardEndComponents(bool value = true) { + noZeroRewardEndComponents = value; + return *this; + } + + MinMaxLinearEquationSolverRequirements& setValidInitialScheduler(bool value = true) { + validInitialScheduler = value; + return *this; + } + + MinMaxLinearEquationSolverRequirements& setGlobalLowerBound(bool value = true) { + globalLowerBound = value; + return *this; + } + + MinMaxLinearEquationSolverRequirements& setGlobalUpperBound(bool value = true) { + globalUpperBound = value; + return *this; + } + + MinMaxLinearEquationSolverRequirements& set(Element const& element, bool value = true) { + switch (element) { + case Element::NoEndComponents: noEndComponents = value; break; + case Element::NoZeroRewardEndComponents: noZeroRewardEndComponents = value; break; + case Element::ValidInitialScheduler: validInitialScheduler = value; break; + case Element::GlobalLowerBound: globalLowerBound = value; break; + case Element::GlobalUpperBound: globalUpperBound = value; break; + } + return *this; + } + + bool requires(Element const& element) { + switch (element) { + case Element::NoEndComponents: return noEndComponents; break; + case Element::NoZeroRewardEndComponents: return noZeroRewardEndComponents; break; + case Element::ValidInitialScheduler: return validInitialScheduler; break; + case Element::GlobalLowerBound: return globalLowerBound; break; + case Element::GlobalUpperBound: return globalUpperBound; break; + } + } + + bool empty() const { + return !noEndComponents && !noZeroRewardEndComponents && !validInitialScheduler && !globalLowerBound && !globalUpperBound; + } + + private: + bool noEndComponents; + bool noZeroRewardEndComponents; + bool validInitialScheduler; + bool globalLowerBound; + bool globalUpperBound; }; /*! @@ -171,20 +224,25 @@ namespace storm { void setBounds(ValueType const& lower, ValueType const& upper); /*! - * Sets a scheduler that might be considered by the solver as an initial guess + * Sets a valid initial scheduler that is required by some solvers (see requirements of solvers). + */ + void setInitialScheduler(std::vector&& choices); + + /*! + * Returns true iff an initial scheduler is set. */ - void setSchedulerHint(std::vector&& choices); + bool hasInitialScheduler() const; /*! - * Returns true iff a scheduler hint was defined + * Retrieves the initial scheduler if one was set. */ - bool hasSchedulerHint() const; + std::vector const& getInitialScheduler() const; /*! * Retrieves the requirements of this solver for solving equations with the current settings. The requirements * are guaranteed to be ordered according to their appearance in the SolverRequirement type. */ - virtual std::vector getRequirements(MinMaxLinearEquationSolverSystemType const& equationSystemType, boost::optional const& direction = boost::none) const; + virtual MinMaxLinearEquationSolverRequirements getRequirements(MinMaxLinearEquationSolverSystemType const& equationSystemType, boost::optional const& direction = boost::none) const; /*! * Notifies the solver that the requirements for solving equations have been checked. If this has not been @@ -215,8 +273,8 @@ namespace storm { // An upper bound if one was set. boost::optional upperBound; - // Scheduler choices that might be considered by the solver as an initial guess - boost::optional> choicesHint; + // A scheduler that can be used by solvers that require a valid initial scheduler. + boost::optional> initialScheduler; private: /// Whether some of the generated data during solver calls should be cached. @@ -247,7 +305,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. */ - std::vector getRequirements(MinMaxLinearEquationSolverSystemType const& equationSystemType, boost::optional const& direction = boost::none) const; + MinMaxLinearEquationSolverRequirements getRequirements(MinMaxLinearEquationSolverSystemType const& equationSystemType, boost::optional const& direction = boost::none) const; void setRequirementsChecked(bool value = true); bool isRequirementsCheckedSet() const;