From bc623d1203b636f48be1639a2f5f2d30da336cce Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Fri, 31 May 2019 18:58:39 +0200 Subject: [PATCH] MinMaxLinearEquationSolver: Added a flag 'hasNoEndComponent' that is true if the system is known to have no end components. This decides if policy iteration does require a valid initial scheduler. Renamed the 'hasNoEndComponents' solver requirement to 'hasUniqueSolution' as this is the actual thing we require for, e.g. sound value iteration. --- ...SparseDtmcParameterLiftingModelChecker.cpp | 9 ++-- .../helper/SparseMarkovAutomatonCslHelper.cpp | 14 +++-- ...ewardBoundedMdpPcaaWeightVectorChecker.cpp | 1 + .../StandardMaPcaaWeightVectorChecker.cpp | 1 + .../pcaa/StandardPcaaWeightVectorChecker.cpp | 48 +++++++++++++++++ .../prctl/helper/HybridMdpPrctlHelper.cpp | 52 +++++++++++-------- .../prctl/helper/SparseMdpPrctlHelper.cpp | 36 +++++++++---- .../prctl/helper/SymbolicMdpPrctlHelper.cpp | 8 +-- .../prctl/helper/rewardbounded/EpochModel.cpp | 1 + .../IterativeMinMaxLinearEquationSolver.cpp | 16 +++--- .../solver/LpMinMaxLinearEquationSolver.cpp | 2 +- .../solver/MinMaxLinearEquationSolver.cpp | 17 ++++-- src/storm/solver/MinMaxLinearEquationSolver.h | 21 +++++++- ...MinMaxLinearEquationSolverRequirements.cpp | 25 +++++---- .../MinMaxLinearEquationSolverRequirements.h | 10 ++-- .../SymbolicMinMaxLinearEquationSolver.cpp | 2 +- .../TopologicalMinMaxLinearEquationSolver.cpp | 17 ++++-- .../solver/MinMaxLinearEquationSolverTest.cpp | 1 + 18 files changed, 197 insertions(+), 84 deletions(-) diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp index a199b3781..1b938f717 100644 --- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp @@ -149,8 +149,8 @@ namespace storm { lowerResultBound = storm::utility::zero(); upperResultBound = storm::utility::one(); - // The solution of the min-max equation system will always be unique (assuming graph-preserving instantiations). - auto req = solverFactory->getRequirements(env, true, boost::none, true); + // The solution of the min-max equation system will always be unique (assuming graph-preserving instantiations, every induced DTMC has the same graph structure). + auto req = solverFactory->getRequirements(env, true, true, boost::none, true); req.clearBounds(); STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked."); solverFactory->setRequirementsChecked(true); @@ -188,8 +188,8 @@ namespace storm { // We only know a lower bound for the result lowerResultBound = storm::utility::zero(); - // The solution of the min-max equation system will always be unique (assuming graph-preserving instantiations). - auto req = solverFactory->getRequirements(env, true, boost::none, true); + // The solution of the min-max equation system will always be unique (assuming graph-preserving instantiations, every induced DTMC has the same graph structure). + auto req = solverFactory->getRequirements(env, true, true, boost::none, true); req.clearLowerBounds(); if (req.upperBounds()) { solvingRequiresUpperRewardBounds = true; @@ -258,6 +258,7 @@ namespace storm { } else { auto solver = solverFactory->create(env, parameterLifter->getMatrix()); solver->setHasUniqueSolution(); + solver->setHasNoEndComponents(); if (lowerResultBound) solver->setLowerBound(lowerResultBound.get()); if (upperResultBound) { solver->setUpperBound(upperResultBound.get()); diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index f813564c2..b1d8ffea9 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -310,13 +310,14 @@ namespace storm { // Create solver. storm::solver::GeneralMinMaxLinearEquationSolverFactory minMaxLinearEquationSolverFactory; - storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, dir); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, true, dir); requirements.clearBounds(); STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked."); if (numberOfProbabilisticChoices > 0) { solver = minMaxLinearEquationSolverFactory.create(env, probMatrix); solver->setHasUniqueSolution(); + solver->setHasNoEndComponents(); solver->setBounds(storm::utility::zero(), storm::utility::one()); solver->setRequirementsChecked(); solver->setCachingEnabled(true); @@ -486,14 +487,15 @@ namespace storm { } // Check for requirements of the solver. - // The solution is unique as we assume non-zeno MAs. + // The min-max system has no end components as we assume non-zeno MAs. storm::solver::GeneralMinMaxLinearEquationSolverFactory minMaxLinearEquationSolverFactory; - storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, dir); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, true, dir); requirements.clearBounds(); STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked."); std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(env, aProbabilistic); solver->setHasUniqueSolution(); + solver->setHasNoEndComponents(); solver->setBounds(storm::utility::zero(), storm::utility::one()); solver->setRequirementsChecked(); solver->setCachingEnabled(true); @@ -819,12 +821,13 @@ namespace storm { // Check for requirements of the solver. storm::solver::GeneralMinMaxLinearEquationSolverFactory minMaxLinearEquationSolverFactory; - storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(underlyingSolverEnvironment, true, dir); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(underlyingSolverEnvironment, true, true, dir); requirements.clearBounds(); STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked."); std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(underlyingSolverEnvironment, sspMatrix); solver->setHasUniqueSolution(); + solver->setHasNoEndComponents(); solver->setLowerBound(storm::utility::zero()); solver->setUpperBound(*std::max_element(lraValuesForEndComponents.begin(), lraValuesForEndComponents.end())); solver->setRequirementsChecked(); @@ -1053,13 +1056,14 @@ namespace storm { // Check for requirements of the solver. // The solution is unique as we assume non-zeno MAs. storm::solver::GeneralMinMaxLinearEquationSolverFactory minMaxLinearEquationSolverFactory; - storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, dir); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, true, dir); requirements.clearLowerBounds(); STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked."); solver = minMaxLinearEquationSolverFactory.create(env, std::move(aProbabilistic)); solver->setLowerBound(storm::utility::zero()); solver->setHasUniqueSolution(true); + solver->setHasNoEndComponents(true); solver->setRequirementsChecked(true); solver->setCachingEnabled(true); } diff --git a/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp index 79eae73bb..4f1d97bf8 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp @@ -318,6 +318,7 @@ namespace storm { storm::solver::GeneralMinMaxLinearEquationSolverFactory minMaxSolverFactory; cachedData.minMaxSolver = minMaxSolverFactory.create(env, epochModel.epochMatrix); cachedData.minMaxSolver->setHasUniqueSolution(); + cachedData.minMaxSolver->setHasNoEndComponents(); cachedData.minMaxSolver->setTrackScheduler(true); cachedData.minMaxSolver->setCachingEnabled(true); auto req = cachedData.minMaxSolver->getRequirements(env); diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp index d43db0d5c..c6a2fa140 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp @@ -301,6 +301,7 @@ namespace storm { storm::solver::GeneralMinMaxLinearEquationSolverFactory minMaxSolverFactory; result->solver = minMaxSolverFactory.create(env, PS.toPS); result->solver->setHasUniqueSolution(true); + result->solver->setHasNoEndComponents(true); // Non-zeno MA result->solver->setTrackScheduler(true); result->solver->setCachingEnabled(true); auto req = result->solver->getRequirements(env, storm::solver::OptimizationDirection::Maximize, false); diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp index 3dd8e8988..b2d9e0dbf 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp @@ -161,6 +161,50 @@ namespace storm { return result; } + template + std::vector computeValidInitialScheduler(storm::storage::SparseMatrix const& matrix, storm::storage::BitVector const& rowsWithSumLessOne) { + std::vector result(matrix.getRowGroupCount()); + auto const& groups = matrix.getRowGroupIndices(); + auto backwardsTransitions = matrix.transpose(true); + storm::storage::BitVector processedStates(result.size(), false); + for (uint64_t state = 0; state < result.size(); ++state) { + if (rowsWithSumLessOne.getNextSetIndex(groups[state]) < groups[state + 1]) { + result[state] = rowsWithSumLessOne.getNextSetIndex(groups[state]) - groups[state]; + processedStates.set(state, true); + } + } + std::vector stack(processedStates.begin(), processedStates.end()); + while (!stack.empty()) { + uint64_t current = stack.back(); + stack.pop_back(); + STORM_LOG_ASSERT(processedStates.get(current), "states on the stack shall be processed."); + for (auto const& entry : backwardsTransitions.getRow(current)) { + uint64_t pred = entry.getColumn(); + if (!processedStates.get(pred)) { + // Find a choice that leads to a processed state + uint64_t predChoice = groups[pred]; + bool foundSuccessor = false; + for (; predChoice < groups[pred + 1]; ++predChoice) { + for (auto const& predEntry : matrix.getRow(predChoice)) { + if (processedStates.get(predEntry.getColumn())) { + foundSuccessor = true; + break; + } + } + if (foundSuccessor) { + break; + } + } + STORM_LOG_ASSERT(foundSuccessor && predChoice < groups[pred + 1], "Predecessor of a processed state should have a processed successor"); + result[pred] = predChoice - groups[pred]; + processedStates.set(pred, true); + stack.push_back(pred); + } + } + } + return result; + } + template void StandardPcaaWeightVectorChecker::unboundedWeightedPhase(Environment const& env, std::vector const& weightedRewardVector, std::vector const& weightVector) { @@ -187,6 +231,10 @@ namespace storm { if (solver->hasUpperBound()) { req.clearUpperBounds(); } + if (req.validInitialScheduler()) { + solver->setInitialScheduler(computeValidInitialScheduler(ecQuotient->matrix, ecQuotient->rowsWithSumLessOne)); + req.clearValidInitialScheduler(); + } STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked."); solver->setRequirementsChecked(true); diff --git a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp index 7cb054574..d1755ef38 100644 --- a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp @@ -146,22 +146,23 @@ namespace storm { } else { // If there are maybe states, we need to solve an equation system. if (!maybeStates.isZero()) { - // If we minimize, we know that the solution to the equation system is unique. - bool uniqueSolution = dir == storm::solver::OptimizationDirection::Minimize; + // If we minimize, we know that the solution to the equation system has no end components + bool hasNoEndComponents = dir == storm::solver::OptimizationDirection::Minimize; // Check for requirements of the solver early so we can adjust the maybe state computation accordingly. storm::solver::GeneralMinMaxLinearEquationSolverFactory linearEquationSolverFactory; - storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(env, uniqueSolution, dir); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(env, hasNoEndComponents, hasNoEndComponents, dir); storm::solver::MinMaxLinearEquationSolverRequirements clearedRequirements = requirements; SolverRequirementsData solverRequirementsData; bool extendMaybeStates = false; if (clearedRequirements.hasEnabledRequirement()) { - if (clearedRequirements.noEndComponents()) { - STORM_LOG_DEBUG("Scheduling EC elimination, because the solver requires it."); + if (clearedRequirements.uniqueSolution()) { + STORM_LOG_DEBUG("Scheduling EC elimination, because the solver requires a unique solution."); extendMaybeStates = true; - clearedRequirements.clearNoEndComponents(); + clearedRequirements.clearUniqueSolution(); + hasNoEndComponents = true; } - if (clearedRequirements.validInitialScheduler()) { + if (clearedRequirements.validInitialScheduler() && !hasNoEndComponents) { STORM_LOG_DEBUG("Scheduling valid scheduler computation, because the solver requires it."); clearedRequirements.clearValidInitialScheduler(); } @@ -210,8 +211,6 @@ namespace storm { // Eliminate the end components and remove the states that are not interesting (target or non-filter). eliminateEndComponentsAndExtendedStatesUntilProbabilities(explicitRepresentation, solverRequirementsData, targetStates); - // The solution becomes unique after end components have been eliminated. - uniqueSolution = true; } else { // Then compute the vector that contains the one-step probabilities to a state with probability 1 for all // maybe states. @@ -240,8 +239,9 @@ namespace storm { std::unique_ptr> solver = linearEquationSolverFactory.create(env, std::move(explicitRepresentation.first)); - // Set whether the equation system will have a unique solution - solver->setHasUniqueSolution(uniqueSolution); + // Set whether the equation system will have a unique solution / no end components + solver->setHasUniqueSolution(hasNoEndComponents); + solver->setHasNoEndComponents(hasNoEndComponents); if (solverRequirementsData.initialScheduler) { solver->setInitialScheduler(std::move(solverRequirementsData.initialScheduler.get())); @@ -251,7 +251,7 @@ namespace storm { solver->solveEquations(env, dir, x, explicitRepresentation.second); // If we included some target and non-filter states in the ODD, we need to expand the result from the solver. - if (requirements.noEndComponents() && solverRequirementsData.ecInformation) { + if (requirements.uniqueSolution() && solverRequirementsData.ecInformation) { std::vector extendedVector(solverRequirementsData.properMaybeStates.getNumberOfSetBits()); solverRequirementsData.ecInformation.get().setValues(extendedVector, solverRequirementsData.properMaybeStates, x); x = std::move(extendedVector); @@ -543,17 +543,20 @@ namespace storm { // If there are maybe states, we need to solve an equation system. if (!maybeStates.isZero()) { // If we maximize, we know that the solution to the equation system is unique. - bool uniqueSolution = dir == storm::solver::OptimizationDirection::Maximize; + bool hasNoEndComponents = dir == storm::solver::OptimizationDirection::Maximize; + bool hasUniqueSolution = hasNoEndComponents; // Check for requirements of the solver this early so we can adapt the maybe states accordingly. storm::solver::GeneralMinMaxLinearEquationSolverFactory linearEquationSolverFactory; - storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(env, uniqueSolution, dir); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(env, hasUniqueSolution, hasNoEndComponents, dir); storm::solver::MinMaxLinearEquationSolverRequirements clearedRequirements = requirements; bool extendMaybeStates = false; if (clearedRequirements.hasEnabledRequirement()) { - if (clearedRequirements.noEndComponents()) { + if (clearedRequirements.uniqueSolution()) { STORM_LOG_DEBUG("Scheduling EC elimination, because the solver requires it."); extendMaybeStates = true; - clearedRequirements.clearNoEndComponents(); + clearedRequirements.clearUniqueSolution(); + hasUniqueSolution = true; + // There might still be end components in which reward is collected. } if (clearedRequirements.validInitialScheduler()) { STORM_LOG_DEBUG("Computing valid scheduler, because the solver requires it."); @@ -611,11 +614,15 @@ namespace storm { storm::storage::BitVector targetStates = computeTargetStatesForReachabilityRewardsFromExplicitRepresentation(explicitRepresentation.first); solverRequirementsData.properMaybeStates = ~targetStates; - if (requirements.noEndComponents()) { + if (requirements.uniqueSolution()) { + STORM_LOG_THROW(!requirements.validInitialScheduler(), storm::exceptions::UncheckedRequirementException, "The underlying solver requires a unique solution and an initial valid scheduler. This is currently not supported for expected reward properties."); + // eliminate the end components with reward 0. + // Note that this may also compute the oneStepTargetProbabilities if upper bounds are required. eliminateEndComponentsAndTargetStatesReachabilityRewards(explicitRepresentation, solverRequirementsData, targetStates, requirements.upperBounds()); // The solution becomes unique after end components have been eliminated. - uniqueSolution = true; - } else { + hasUniqueSolution = true; + } + else { if (requirements.validInitialScheduler()) { // Compute a valid initial scheduler. solverRequirementsData.initialScheduler = computeValidInitialSchedulerForReachabilityRewards(explicitRepresentation.first, solverRequirementsData.properMaybeStates, targetStates); @@ -637,8 +644,9 @@ namespace storm { // Now solve the resulting equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(env); - // Set whether the equation system will have a unique solution - solver->setHasUniqueSolution(uniqueSolution); + // Set whether the equation system will have a unique solution / no end components + solver->setHasUniqueSolution(hasUniqueSolution); + solver->setHasNoEndComponents(hasNoEndComponents); // If the solver requires upper bounds, compute them now. if (requirements.upperBounds()) { @@ -657,7 +665,7 @@ namespace storm { solver->solveEquations(env, dir, x, explicitRepresentation.second); // If we eliminated end components, we need to extend the solution vector. - if (requirements.noEndComponents() && solverRequirementsData.ecInformation) { + if (requirements.uniqueSolution() && solverRequirementsData.ecInformation) { std::vector extendedVector(solverRequirementsData.properMaybeStates.getNumberOfSetBits()); solverRequirementsData.ecInformation.get().setValues(extendedVector, solverRequirementsData.properMaybeStates, x); x = std::move(extendedVector); diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index d8bb7dc32..dcadd10f8 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -205,7 +205,7 @@ namespace storm { template struct SparseMdpHintType { - SparseMdpHintType() : eliminateEndComponents(false), computeUpperBounds(false), uniqueSolution(false) { + SparseMdpHintType() : eliminateEndComponents(false), computeUpperBounds(false), uniqueSolution(false), noEndComponents(false) { // Intentionally left empty. } @@ -265,6 +265,10 @@ namespace storm { return uniqueSolution; } + bool hasNoEndComponents() const { + return noEndComponents; + } + boost::optional> schedulerHint; boost::optional> valueHint; boost::optional lowerResultBound; @@ -273,6 +277,7 @@ namespace storm { bool eliminateEndComponents; bool computeUpperBounds; bool uniqueSolution; + bool noEndComponents; }; template @@ -329,29 +334,36 @@ namespace storm { 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 - // maximize reachability rewards or if the hint tells us that there are no end-compontnes. - result.uniqueSolution = (dir == storm::solver::OptimizationDirection::Minimize && type == SolutionType::UntilProbabilities) + // There are no end components if we minimize until probabilities or + // maximize reachability rewards or if the hint tells us so. + result.noEndComponents = (dir == storm::solver::OptimizationDirection::Minimize && type == SolutionType::UntilProbabilities) || (dir == storm::solver::OptimizationDirection::Maximize && type == SolutionType::ExpectedRewards) || (hint.isExplicitModelCheckerHint() && hint.asExplicitModelCheckerHint().getNoEndComponentsInMaybeStates()); + // If there are no end components, the solution is unique. (Note that the other direction does not hold, + // e.g., end components in which infinite reward is collected. + result.uniqueSolution = result.hasNoEndComponents(); + // 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, produceScheduler); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, result.uniqueSolution, result.noEndComponents, dir, hasSchedulerHint, produceScheduler); if (requirements.hasEnabledRequirement()) { // If the solver still requires no end-components, we have to eliminate them later. - if (requirements.noEndComponents()) { + if (requirements.uniqueSolution()) { STORM_LOG_ASSERT(!result.hasUniqueSolution(), "The solver requires to eliminate the end components although the solution is already assumed to be unique."); - STORM_LOG_DEBUG("Scheduling EC elimination, because the solver requires it."); + STORM_LOG_DEBUG("Scheduling EC elimination, because the solver requires a unique solution."); result.eliminateEndComponents = true; // If end components have been eliminated we can assume a unique solution. result.uniqueSolution = true; - requirements.clearNoEndComponents(); + requirements.clearUniqueSolution(); + // If we compute until probabilities, we can even assume the absence of end components. + // Note that in the case of minimizing expected rewards there might still be end components in which reward is collected. + result.noEndComponents = (type == SolutionType::UntilProbabilities); } - // If the solver requires an initial scheduler, compute one now. - if (requirements.validInitialScheduler()) { + // If the solver requires an initial scheduler, compute one now. Note that any scheduler is valid if there are no end components. + if (requirements.validInitialScheduler() && !result.noEndComponents) { STORM_LOG_DEBUG("Computing valid scheduler, because the solver requires it."); result.schedulerHint = computeValidSchedulerHint(env, type, transitionMatrix, backwardTransitions, maybeStates, phiStates, targetStates); requirements.clearValidInitialScheduler(); @@ -429,6 +441,7 @@ namespace storm { std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(env, std::move(goal), minMaxLinearEquationSolverFactory, std::move(submatrix)); solver->setRequirementsChecked(); solver->setHasUniqueSolution(hint.hasUniqueSolution()); + solver->setHasNoEndComponents(hint.hasNoEndComponents()); if (hint.hasLowerResultBound()) { solver->setLowerBound(hint.getLowerResultBound()); } @@ -1348,7 +1361,7 @@ namespace storm { // Check for requirements of the solver. storm::solver::GeneralMinMaxLinearEquationSolverFactory minMaxLinearEquationSolverFactory; - storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(underlyingSolverEnvironment, true, goal.direction()); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(underlyingSolverEnvironment, true, true, goal.direction()); requirements.clearBounds(); STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked."); @@ -1359,6 +1372,7 @@ namespace storm { solver->setLowerBound(storm::utility::zero()); solver->setUpperBound(*std::max_element(lraValuesForEndComponents.begin(), lraValuesForEndComponents.end())); solver->setHasUniqueSolution(); + solver->setHasNoEndComponents(); solver->setRequirementsChecked(); solver->solveEquations(underlyingSolverEnvironment, sspResult, b); diff --git a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp index f52d7eb17..212151e5e 100644 --- a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp @@ -82,10 +82,10 @@ namespace storm { requirements.clearValidInitialScheduler(); } requirements.clearBounds(); - if (requirements.noEndComponents()) { + if (requirements.uniqueSolution()) { // Check whether there are end components if (storm::utility::graph::performProb0E(model, transitionMatrix.notZero(), maybeStates, !maybeStates && model.getReachableStates()).isZero()) { - requirements.clearNoEndComponents(); + requirements.clearUniqueSolution(); } } STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked."); @@ -253,10 +253,10 @@ namespace storm { requirements.clearValidInitialScheduler(); } requirements.clearLowerBounds(); - if (requirements.noEndComponents()) { + if (requirements.uniqueSolution()) { // Check whether there are end components if (storm::utility::graph::performProb0E(model, transitionMatrixBdd, maybeStates, !maybeStates && model.getReachableStates()).isZero()) { - requirements.clearNoEndComponents(); + requirements.clearUniqueSolution(); } } STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked."); diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/EpochModel.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/EpochModel.cpp index e8b059f32..f48253fca 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/EpochModel.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/EpochModel.cpp @@ -140,6 +140,7 @@ namespace storm { storm::solver::GeneralMinMaxLinearEquationSolverFactory minMaxLinearEquationSolverFactory; minMaxSolver = minMaxLinearEquationSolverFactory.create(env, epochModel.epochMatrix); minMaxSolver->setHasUniqueSolution(); + minMaxSolver->setHasNoEndComponents(); minMaxSolver->setOptimizationDirection(dir); minMaxSolver->setCachingEnabled(true); minMaxSolver->setTrackScheduler(true); diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index becaa1d17..37f9c1ab5 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -241,7 +241,7 @@ namespace storm { if (!this->hasUniqueSolution()) { // Traditional value iteration has no requirements if the solution is unique. // Computing a scheduler is only possible if the solution is unique if (this->isTrackSchedulerSet()) { - requirements.requireNoEndComponents(); + requirements.requireUniqueSolution(); } else { // As we want the smallest (largest) solution for maximizing (minimizing) equation systems, we have to approach the solution from below (above). if (!direction || direction.get() == OptimizationDirection::Maximize) { @@ -255,7 +255,7 @@ namespace storm { } else if (method == MinMaxMethod::IntervalIteration) { // Interval iteration requires a unique solution and lower+upper bounds if (!this->hasUniqueSolution()) { - requirements.requireNoEndComponents(); + requirements.requireUniqueSolution(); } requirements.requireBounds(); } else if (method == MinMaxMethod::RationalSearch) { @@ -263,22 +263,22 @@ namespace storm { requirements.requireLowerBounds(); // The solution needs to be unique in case of minimizing or in cases where we want a scheduler. if (!this->hasUniqueSolution() && (!direction || direction.get() == OptimizationDirection::Minimize || this->isTrackSchedulerSet())) { - requirements.requireNoEndComponents(); + requirements.requireUniqueSolution(); } } else if (method == MinMaxMethod::PolicyIteration) { - if (!this->hasUniqueSolution()) { + // The initial scheduler shall not select an end component + if (!this->hasNoEndComponents()) { requirements.requireValidInitialScheduler(); } } else if (method == MinMaxMethod::SoundValueIteration) { if (!this->hasUniqueSolution()) { - requirements.requireNoEndComponents(); + requirements.requireUniqueSolution(); } requirements.requireBounds(false); } else if (method == MinMaxMethod::ViToPi) { - // Since we want to use value iteration to extract an initial scheduler, it helps to eliminate all end components first. - // TODO: We might get around this, as the initial value iteration scheduler is only a heuristic. + // Since we want to use value iteration to extract an initial scheduler, the solution has to be unique. if (!this->hasUniqueSolution()) { - requirements.requireNoEndComponents(); + requirements.requireUniqueSolution(); } } else { STORM_LOG_THROW(false, storm::exceptions::InvalidEnvironmentException, "Unsupported technique for iterative MinMax linear equation solver."); diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp index 78bc75752..2b371aae3 100644 --- a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp @@ -117,7 +117,7 @@ namespace storm { // In case we need to retrieve a scheduler, the solution has to be unique if (!this->hasUniqueSolution() && this->isTrackSchedulerSet()) { - requirements.requireNoEndComponents(); + requirements.requireUniqueSolution(); } requirements.requireBounds(false); diff --git a/src/storm/solver/MinMaxLinearEquationSolver.cpp b/src/storm/solver/MinMaxLinearEquationSolver.cpp index be724ea0d..df0fef614 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/MinMaxLinearEquationSolver.cpp @@ -19,7 +19,7 @@ namespace storm { namespace solver { template - MinMaxLinearEquationSolver::MinMaxLinearEquationSolver(OptimizationDirectionSetting direction) : direction(direction), trackScheduler(false), uniqueSolution(false), cachingEnabled(false), requirementsChecked(false) { + MinMaxLinearEquationSolver::MinMaxLinearEquationSolver(OptimizationDirectionSetting direction) : direction(direction), trackScheduler(false), uniqueSolution(false), noEndComponents(false), cachingEnabled(false), requirementsChecked(false) { // Intentionally left empty. } @@ -57,7 +57,17 @@ namespace storm { template bool MinMaxLinearEquationSolver::hasUniqueSolution() const { - return uniqueSolution; + return uniqueSolution || noEndComponents; + } + + template + void MinMaxLinearEquationSolver::setHasNoEndComponents(bool value) { + noEndComponents = value; + } + + template + bool MinMaxLinearEquationSolver::hasNoEndComponents() const { + return noEndComponents; } template @@ -161,11 +171,12 @@ namespace storm { } template - MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolverFactory::getRequirements(Environment const& env, bool hasUniqueSolution, boost::optional const& direction, bool hasInitialScheduler, bool trackScheduler) const { + MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolverFactory::getRequirements(Environment const& env, bool hasUniqueSolution, bool hasNoEndComponents, 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); + solver->setHasNoEndComponents(hasNoEndComponents); return solver->getRequirements(env, direction, hasInitialScheduler); } diff --git a/src/storm/solver/MinMaxLinearEquationSolver.h b/src/storm/solver/MinMaxLinearEquationSolver.h index 7ca89dfb9..5ab51dc95 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.h +++ b/src/storm/solver/MinMaxLinearEquationSolver.h @@ -76,10 +76,24 @@ namespace storm { void setHasUniqueSolution(bool value = true); /*! - * Retrieves whether the solution to the min max equation system is assumed to be unique + * Retrieves whether the solution to the min max equation system is assumed to be unique. + * Note that having no end components implies that the solution is unique. Thus, this also returns true if + * `hasNoEndComponents()` returns true. + * Also note that a unique solution does not imply the absence of ECs, because, e.g. in Rmin properties there + * can still be ECs in which infinite reward is collected. */ bool hasUniqueSolution() const; + /*! + * Sets whether the min max equation system is known to not have any end components + */ + void setHasNoEndComponents(bool value = true); + + /*! + * Retrieves whether the min max equation system is known to not have any end components + */ + bool hasNoEndComponents() const; + /*! * Sets whether schedulers are generated when solving equation systems. If the argument is false, the currently * stored scheduler (if any) is deleted. @@ -173,6 +187,9 @@ namespace storm { /// Whether the solver can assume that the min-max equation system has a unique solution bool uniqueSolution; + /// Whether the solver can assume that the min-max equation system has no end components + bool noEndComponents; + /// Whether some of the generated data during solver calls should be cached. bool cachingEnabled; @@ -194,7 +211,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 hasInitialScheduler = false, bool trackScheduler = false) const; + MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, bool hasUniqueSolution = false, bool hasNoEndComponents = false, boost::optional const& direction = boost::none, bool hasInitialScheduler = false, bool trackScheduler = false) const; void setRequirementsChecked(bool value = true); bool isRequirementsCheckedSet() const; diff --git a/src/storm/solver/MinMaxLinearEquationSolverRequirements.cpp b/src/storm/solver/MinMaxLinearEquationSolverRequirements.cpp index e16bbdf54..3e5e867ab 100644 --- a/src/storm/solver/MinMaxLinearEquationSolverRequirements.cpp +++ b/src/storm/solver/MinMaxLinearEquationSolverRequirements.cpp @@ -7,8 +7,8 @@ namespace storm { // Intentionally left empty. } - MinMaxLinearEquationSolverRequirements& MinMaxLinearEquationSolverRequirements::requireNoEndComponents(bool critical) { - noEndComponentsRequirement.enable(critical); + MinMaxLinearEquationSolverRequirements& MinMaxLinearEquationSolverRequirements::requireUniqueSolution(bool critical) { + uniqueSolutionRequirement.enable(critical); return *this; } @@ -33,8 +33,8 @@ namespace storm { return *this; } - SolverRequirement const& MinMaxLinearEquationSolverRequirements::noEndComponents() const { - return noEndComponentsRequirement; + SolverRequirement const& MinMaxLinearEquationSolverRequirements::uniqueSolution() const { + return uniqueSolutionRequirement; } SolverRequirement const& MinMaxLinearEquationSolverRequirements::validInitialScheduler() const { @@ -51,16 +51,15 @@ namespace storm { SolverRequirement const& MinMaxLinearEquationSolverRequirements::get(Element const& element) const { switch (element) { - case Element::NoEndComponents: return noEndComponents(); break; + case Element::UniqueSolution: return uniqueSolution(); break; case Element::ValidInitialScheduler: return validInitialScheduler(); break; case Element::LowerBounds: return lowerBounds(); break; case Element::UpperBounds: return upperBounds(); break; } } - void MinMaxLinearEquationSolverRequirements::clearNoEndComponents() { - noEndComponentsRequirement.clear(); - validInitialSchedulerRequirement.clear(); + void MinMaxLinearEquationSolverRequirements::clearUniqueSolution() { + uniqueSolutionRequirement.clear(); } void MinMaxLinearEquationSolverRequirements::clearValidInitialScheduler() { @@ -81,20 +80,20 @@ namespace storm { } bool MinMaxLinearEquationSolverRequirements::hasEnabledRequirement() const { - return noEndComponentsRequirement || validInitialSchedulerRequirement || lowerBoundsRequirement || upperBoundsRequirement; + return uniqueSolutionRequirement || validInitialSchedulerRequirement || lowerBoundsRequirement || upperBoundsRequirement; } bool MinMaxLinearEquationSolverRequirements::hasEnabledCriticalRequirement() const { - return noEndComponentsRequirement.isCritical() || validInitialSchedulerRequirement.isCritical() || lowerBoundsRequirement.isCritical() || upperBoundsRequirement.isCritical(); + return uniqueSolutionRequirement.isCritical() || validInitialSchedulerRequirement.isCritical() || lowerBoundsRequirement.isCritical() || upperBoundsRequirement.isCritical(); } std::string MinMaxLinearEquationSolverRequirements::getEnabledRequirementsAsString() const { std::string res = "["; bool first = true; - if (noEndComponents()) { + if (uniqueSolution()) { if (!first) { res += ", "; } else {first = false;} - res += "NoEndComponents"; - if (noEndComponents().isCritical()) { + res += "UniqueSolution"; + if (uniqueSolution().isCritical()) { res += "(mandatory)"; } } diff --git a/src/storm/solver/MinMaxLinearEquationSolverRequirements.h b/src/storm/solver/MinMaxLinearEquationSolverRequirements.h index 06ba623c1..38f2f1849 100644 --- a/src/storm/solver/MinMaxLinearEquationSolverRequirements.h +++ b/src/storm/solver/MinMaxLinearEquationSolverRequirements.h @@ -15,7 +15,7 @@ namespace storm { // Requirements that are related to the graph structure of the system. Note that the requirements in this // category are to be interpreted incrementally in the following sense: whenever the system has no end // components then automatically both requirements are fulfilled. - NoEndComponents, + UniqueSolution, ValidInitialScheduler, // Requirements that are related to bounds for the actual solution. @@ -27,19 +27,19 @@ namespace storm { MinMaxLinearEquationSolverRequirements(LinearEquationSolverRequirements const& linearEquationSolverRequirements = LinearEquationSolverRequirements()); - MinMaxLinearEquationSolverRequirements& requireNoEndComponents(bool critical = true); + MinMaxLinearEquationSolverRequirements& requireUniqueSolution(bool critical = true); MinMaxLinearEquationSolverRequirements& requireValidInitialScheduler(bool critical = true); MinMaxLinearEquationSolverRequirements& requireLowerBounds(bool critical = true); MinMaxLinearEquationSolverRequirements& requireUpperBounds(bool critical = true); MinMaxLinearEquationSolverRequirements& requireBounds(bool critical = true); - SolverRequirement const& noEndComponents() const; + SolverRequirement const& uniqueSolution() const; SolverRequirement const& validInitialScheduler() const; SolverRequirement const& lowerBounds() const; SolverRequirement const& upperBounds() const; SolverRequirement const& get(Element const& element) const; - void clearNoEndComponents(); + void clearUniqueSolution(); void clearValidInitialScheduler(); void clearLowerBounds(); void clearUpperBounds(); @@ -54,7 +54,7 @@ namespace storm { std::string getEnabledRequirementsAsString() const; private: - SolverRequirement noEndComponentsRequirement; + SolverRequirement uniqueSolutionRequirement; SolverRequirement validInitialSchedulerRequirement; SolverRequirement lowerBoundsRequirement; SolverRequirement upperBoundsRequirement; diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp index c54df3acf..2ba997ed8 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp @@ -455,7 +455,7 @@ namespace storm { } else if (method == MinMaxMethod::RationalSearch) { requirements.requireLowerBounds(); if (!this->hasUniqueSolution() && (!direction || direction.get() == storm::solver::OptimizationDirection::Minimize)) { - requirements.requireNoEndComponents(); + requirements.requireUniqueSolution(); } } else { STORM_LOG_THROW(false, storm::exceptions::InvalidEnvironmentException, "The selected min max technique is not supported by this solver."); diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp index 998c9d782..d98902694 100644 --- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -181,6 +181,7 @@ namespace storm { } this->sccSolver->setMatrix(*this->A); this->sccSolver->setHasUniqueSolution(this->hasUniqueSolution()); + this->sccSolver->setHasNoEndComponents(this->hasNoEndComponents()); this->sccSolver->setBoundsFromOtherSolver(*this); this->sccSolver->setTrackScheduler(this->isTrackSchedulerSet()); if (this->hasInitialScheduler()) { @@ -194,10 +195,12 @@ namespace storm { if (req.lowerBounds() && this->hasLowerBound()) { req.clearLowerBounds(); } - - // If all requirements of the underlying solver have been passed as requirements to the calling site, we can - // assume that the system has no end components if the underlying solver requires this. - req.clearNoEndComponents(); + if (req.validInitialScheduler() && this->hasInitialScheduler()) { + req.clearValidInitialScheduler(); + } + if (req.uniqueSolution() && this->hasUniqueSolution()) { + req.clearUniqueSolution(); + } STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked."); this->sccSolver->setRequirementsChecked(true); @@ -217,6 +220,7 @@ namespace storm { this->sccSolver->setCachingEnabled(true); } this->sccSolver->setHasUniqueSolution(this->hasUniqueSolution()); + this->sccSolver->setHasNoEndComponents(this->hasNoEndComponents()); this->sccSolver->setTrackScheduler(this->isTrackSchedulerSet()); // SCC Matrix @@ -269,6 +273,9 @@ namespace storm { if (req.validInitialScheduler() && this->hasInitialScheduler()) { req.clearValidInitialScheduler(); } + if (req.uniqueSolution() && this->hasUniqueSolution()) { + req.clearUniqueSolution(); + } STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked."); this->sccSolver->setRequirementsChecked(true); @@ -291,7 +298,7 @@ namespace storm { template MinMaxLinearEquationSolverRequirements TopologicalMinMaxLinearEquationSolver::getRequirements(Environment const& env, boost::optional const& direction, bool const& hasInitialScheduler) const { // Return the requirements of the underlying solver - return GeneralMinMaxLinearEquationSolverFactory().getRequirements(getEnvironmentForUnderlyingSolver(env), this->hasUniqueSolution(), direction, hasInitialScheduler); + return GeneralMinMaxLinearEquationSolverFactory().getRequirements(getEnvironmentForUnderlyingSolver(env), this->hasUniqueSolution(), this->hasNoEndComponents(), direction, hasInitialScheduler, this->isTrackSchedulerSet()); } template diff --git a/src/test/storm/solver/MinMaxLinearEquationSolverTest.cpp b/src/test/storm/solver/MinMaxLinearEquationSolverTest.cpp index 725590bc8..ef565f946 100644 --- a/src/test/storm/solver/MinMaxLinearEquationSolverTest.cpp +++ b/src/test/storm/solver/MinMaxLinearEquationSolverTest.cpp @@ -149,6 +149,7 @@ namespace { auto factory = storm::solver::GeneralMinMaxLinearEquationSolverFactory(); auto solver = factory.create(this->env(), A); solver->setHasUniqueSolution(true); + solver->setHasNoEndComponents(true); solver->setBounds(this->parseNumber("0"), this->parseNumber("2")); storm::solver::MinMaxLinearEquationSolverRequirements req = solver->getRequirements(this->env()); req.clearBounds();