From 4991a3ec5e6cfd9e23bd3a42f102a9f37aa02a1d Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 28 Sep 2017 12:14:27 +0200 Subject: [PATCH 1/3] checking solver requirements for PLA --- ...SparseDtmcParameterLiftingModelChecker.cpp | 48 +++++++++++++++++-- .../SparseDtmcParameterLiftingModelChecker.h | 8 ++-- 2 files changed, 49 insertions(+), 7 deletions(-) diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp index 119e3791d..150a9d86c 100644 --- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp @@ -6,6 +6,8 @@ #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h" +#include "storm/modelchecker/prctl/helper/BaierUpperRewardBoundsComputer.h" #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/solver/StandardMinMaxLinearEquationSolver.h" @@ -17,6 +19,8 @@ #include "storm/exceptions/InvalidPropertyException.h" #include "storm/exceptions/NotSupportedException.h" #include "storm/exceptions/UnexpectedException.h" +#include "storm/exceptions/UncheckedRequirementException.h" + namespace storm { namespace modelchecker { @@ -27,7 +31,7 @@ namespace storm { } template - SparseDtmcParameterLiftingModelChecker::SparseDtmcParameterLiftingModelChecker(std::unique_ptr>&& solverFactory) : solverFactory(std::move(solverFactory)) { + SparseDtmcParameterLiftingModelChecker::SparseDtmcParameterLiftingModelChecker(std::unique_ptr>&& solverFactory) : solverFactory(std::move(solverFactory)), solvingRequiresUpperRewardBounds(false) { // Intentionally left empty } @@ -109,6 +113,8 @@ namespace storm { // We know some bounds for the results so set them lowerResultBound = storm::utility::zero(); upperResultBound = storm::utility::one(); + // No requirements for bounded formulas + solverFactory->setRequirementsChecked(true); } template @@ -139,6 +145,12 @@ namespace storm { // We know some bounds for the results so set them lowerResultBound = storm::utility::zero(); upperResultBound = storm::utility::one(); + + auto req = solverFactory->getRequirements(storm::solver::EquationSystemType::UntilProbabilities); + req.clearBounds(); + req.clearNoEndComponents(); // We never have end components within the maybestates (assuming graph-preserving instantiations). + STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "Unchecked solver requirement."); + solverFactory->setRequirementsChecked(true); } template @@ -172,6 +184,17 @@ namespace storm { // We only know a lower bound for the result lowerResultBound = storm::utility::zero(); + + auto req = solverFactory->getRequirements(storm::solver::EquationSystemType::ReachabilityRewards); + req.clearNoEndComponents(); // We never have end components within the maybestates (assuming graph-preserving instantiations). + req.clearLowerBounds(); + if (req.requiresUpperBounds()) { + solvingRequiresUpperRewardBounds = true; + req.clearUpperBounds(); + } + STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "Unchecked solver requirement."); + solverFactory->setRequirementsChecked(true); + } @@ -200,6 +223,9 @@ namespace storm { // We only know a lower bound for the result lowerResultBound = storm::utility::zero(); + + // No requirements for bounded reward formula + solverFactory->setRequirementsChecked(true); } template @@ -228,7 +254,23 @@ namespace storm { } auto solver = solverFactory->create(parameterLifter->getMatrix()); if (lowerResultBound) solver->setLowerBound(lowerResultBound.get()); - if (upperResultBound) solver->setUpperBound(upperResultBound.get()); + if (upperResultBound) { + solver->setUpperBound(upperResultBound.get()); + } else if (solvingRequiresUpperRewardBounds) { + // For the min-case, we use DS-MPI, for the max-case variant 2 of the Baier et al. paper (CAV'17). + std::vector oneStepProbs; + oneStepProbs.reserve(parameterLifter->getMatrix().getRowCount()); + for (uint64_t row = 0; row < parameterLifter->getMatrix().getRowCount(); ++row) { + oneStepProbs.push_back(storm::utility::one() - parameterLifter->getMatrix().getRowSum(row)); + } + if (dirForParameters == storm::OptimizationDirection::Minimize) { + storm::modelchecker::helper::DsMpiMdpUpperRewardBoundsComputer dsmpi(parameterLifter->getMatrix(), parameterLifter->getVector(), oneStepProbs); + solver->setUpperBounds(dsmpi.computeUpperBounds()); + } else { + storm::modelchecker::helper::BaierUpperRewardBoundsComputer baier(parameterLifter->getMatrix(), parameterLifter->getVector(), oneStepProbs); + solver->setUpperBound(baier.computeUpperBound()); + } + } if (!stepBound) solver->setTrackScheduler(true); if (storm::solver::minimize(dirForParameters) && minSchedChoices && !stepBound) solver->setInitialScheduler(std::move(minSchedChoices.get())); if (storm::solver::maximize(dirForParameters) && maxSchedChoices && !stepBound) solver->setInitialScheduler(std::move(maxSchedChoices.get())); @@ -247,7 +289,7 @@ namespace storm { } // Invoke the solver - if(stepBound) { + if (stepBound) { assert(*stepBound > 0); x = std::vector(maybeStates.getNumberOfSetBits(), storm::utility::zero()); solver->repeatedMultiply(dirForParameters, x, ¶meterLifter->getVector(), *stepBound); diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h index d6f51032b..b4a8644b6 100644 --- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h +++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h @@ -12,7 +12,6 @@ #include "storm/solver/MinMaxLinearEquationSolver.h" #include "storm/logic/FragmentSpecification.h" - namespace storm { namespace modelchecker { @@ -49,12 +48,13 @@ namespace storm { storm::storage::BitVector maybeStates; std::vector resultsForNonMaybeStates; boost::optional stepBound; - + std::unique_ptr> instantiationChecker; - + std::unique_ptr> parameterLifter; std::unique_ptr> solverFactory; - + bool solvingRequiresUpperRewardBounds; + // Results from the most recent solver call. boost::optional> minSchedChoices, maxSchedChoices; std::vector x; From 3f6464c59d30854c15cd639fbb9aedba48c51730 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 28 Sep 2017 12:15:37 +0200 Subject: [PATCH 2/3] Enforce no end components when we want to compute a scheduler from a minmax equation system --- .../IterativeMinMaxLinearEquationSolver.cpp | 5 +++++ src/storm/solver/LpMinMaxLinearEquationSolver.cpp | 15 +++++++++++++++ src/storm/solver/LpMinMaxLinearEquationSolver.h | 2 ++ 3 files changed, 22 insertions(+) diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index 0ddd5b5fe..70d2de0c1 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -255,6 +255,11 @@ namespace storm { // Start by copying the requirements of the linear equation solver. MinMaxLinearEquationSolverRequirements requirements(this->linearEquationSolverFactory->getRequirements()); + // In case we perform value iteration and need to retrieve a scheduler, end components are forbidden + if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings::SolutionMethod::ValueIteration && isTrackSchedulerSet()) { + requirements.requireNoEndComponents(); + } + // Guide requirements by whether or not we force soundness. if (this->getSettings().getForceSoundness()) { // Only add requirements for value iteration here as the policy iteration requirements are indifferent diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp index 2f360f513..0369d301d 100644 --- a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp @@ -108,6 +108,21 @@ namespace storm { StandardMinMaxLinearEquationSolver::clearCache(); } + + template + MinMaxLinearEquationSolverRequirements LpMinMaxLinearEquationSolver::getRequirements(EquationSystemType const& equationSystemType, boost::optional const& direction) const { + + MinMaxLinearEquationSolverRequirements requirements; + + // In case we need to retrieve a scheduler, end components are forbidden + if (isTrackSchedulerSet()) { + requirements.requireNoEndComponents(); + } + + return requirements; + } + + template LpMinMaxLinearEquationSolverFactory::LpMinMaxLinearEquationSolverFactory(bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory(MinMaxMethodSelection::LinearProgramming, trackScheduler), lpSolverFactory(std::make_unique>()) { // Intentionally left empty diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.h b/src/storm/solver/LpMinMaxLinearEquationSolver.h index a31ac710b..3e5af458f 100644 --- a/src/storm/solver/LpMinMaxLinearEquationSolver.h +++ b/src/storm/solver/LpMinMaxLinearEquationSolver.h @@ -18,6 +18,8 @@ namespace storm { virtual void clearCache() const override; + virtual MinMaxLinearEquationSolverRequirements getRequirements(EquationSystemType const& equationSystemType, boost::optional const& direction = boost::none) const override; + private: std::unique_ptr> lpSolverFactory; }; From 4afaca7f84d5b38fc21f4ca44558f339b3cc897e Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 28 Sep 2017 12:15:54 +0200 Subject: [PATCH 3/3] fixed missing return statements --- src/storm/settings/modules/EigenEquationSolverSettings.cpp | 1 + src/storm/settings/modules/NativeEquationSolverSettings.cpp | 1 + 2 files changed, 2 insertions(+) diff --git a/src/storm/settings/modules/EigenEquationSolverSettings.cpp b/src/storm/settings/modules/EigenEquationSolverSettings.cpp index 3047a13a4..e43bda28b 100644 --- a/src/storm/settings/modules/EigenEquationSolverSettings.cpp +++ b/src/storm/settings/modules/EigenEquationSolverSettings.cpp @@ -113,6 +113,7 @@ namespace storm { case EigenEquationSolverSettings::LinearEquationMethod::DGMRES: out << "dgmres"; break; case EigenEquationSolverSettings::LinearEquationMethod::SparseLU: out << "sparselu"; break; } + return out; } } // namespace modules diff --git a/src/storm/settings/modules/NativeEquationSolverSettings.cpp b/src/storm/settings/modules/NativeEquationSolverSettings.cpp index d797a968a..d85b10569 100644 --- a/src/storm/settings/modules/NativeEquationSolverSettings.cpp +++ b/src/storm/settings/modules/NativeEquationSolverSettings.cpp @@ -120,6 +120,7 @@ namespace storm { case NativeEquationSolverSettings::LinearEquationMethod::WalkerChae: out << "walkerchae"; break; case NativeEquationSolverSettings::LinearEquationMethod::Power: out << "power"; break; } + return out; } } // namespace modules