From 9bda63179536b0c6482be36f361210c11dbed62d Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 6 Sep 2017 10:53:31 +0200 Subject: [PATCH] symbolic MDP helper respecting solver requirements --- .../prctl/helper/SymbolicMdpPrctlHelper.cpp | 15 ++++++- ...ymbolicEliminationLinearEquationSolver.cpp | 13 ++++-- .../SymbolicEliminationLinearEquationSolver.h | 8 +++- .../solver/SymbolicLinearEquationSolver.cpp | 43 ++++++++++++------ .../solver/SymbolicLinearEquationSolver.h | 34 +++++++++++--- .../SymbolicMinMaxLinearEquationSolver.cpp | 41 ++++++++++++----- .../SymbolicMinMaxLinearEquationSolver.h | 3 ++ .../SymbolicNativeLinearEquationSolver.cpp | 13 ++++-- .../SymbolicNativeLinearEquationSolver.h | 21 +++++++-- src/storm/utility/graph.cpp | 45 ++++++++++++++++++- src/storm/utility/graph.h | 6 +++ 11 files changed, 199 insertions(+), 43 deletions(-) diff --git a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp index c53724306..a4c418b3c 100644 --- a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp @@ -29,6 +29,8 @@ namespace storm { if (type == storm::solver::MinMaxLinearEquationSolverSystemType::UntilProbabilities) { result = storm::utility::graph::computeSchedulerProbGreater0E(model, transitionMatrix.notZero(), maybeStates, targetStates); + } else if (type == storm::solver::MinMaxLinearEquationSolverSystemType::ReachabilityRewards) { + result = storm::utility::graph::computeSchedulerProb1E(model, transitionMatrix.notZero(), maybeStates, targetStates, maybeStates || targetStates); } return result; @@ -240,7 +242,18 @@ namespace storm { // Check requirements of solver. storm::solver::MinMaxLinearEquationSolverRequirements requirements = solver->getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::ReachabilityRewards, dir); - STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Could not establish requirements of solver."); + boost::optional> initialScheduler; + if (!requirements.empty()) { + if (requirements.requires(storm::solver::MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler)) { + STORM_LOG_DEBUG("Computing valid scheduler, because the solver requires it."); + initialScheduler = computeValidSchedulerHint(storm::solver::MinMaxLinearEquationSolverSystemType::ReachabilityRewards, model, transitionMatrix, maybeStates, targetStates); + requirements.set(storm::solver::MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler, false); + } + STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Could not establish requirements of solver."); + } + if (initialScheduler) { + solver->setInitialScheduler(initialScheduler.get()); + } solver->setRequirementsChecked(); storm::dd::Add result = solver->solveEquations(dir, model.getManager().template getAddZero(), subvector); diff --git a/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp b/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp index bcbc41085..44689d990 100644 --- a/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp @@ -11,8 +11,13 @@ namespace storm { namespace solver { template - SymbolicEliminationLinearEquationSolver::SymbolicEliminationLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) : SymbolicLinearEquationSolver(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs) { - storm::dd::DdManager& ddManager = A.getDdManager(); + SymbolicEliminationLinearEquationSolver::SymbolicEliminationLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) : SymbolicEliminationLinearEquationSolver(allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs) { + this->setMatrix(A); + } + + template + SymbolicEliminationLinearEquationSolver::SymbolicEliminationLinearEquationSolver(storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) : SymbolicLinearEquationSolver(allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs) { + storm::dd::DdManager& ddManager = allRows.getDdManager(); // Create triple-layered meta variables for all original meta variables. We will use them later in the elimination process. for (auto const& metaVariablePair : this->rowColumnMetaVariablePairs) { @@ -104,8 +109,8 @@ namespace storm { } template - std::unique_ptr> SymbolicEliminationLinearEquationSolverFactory::create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const { - return std::make_unique>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs); + std::unique_ptr> SymbolicEliminationLinearEquationSolverFactory::create(storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const { + return std::make_unique>(allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs); } template diff --git a/src/storm/solver/SymbolicEliminationLinearEquationSolver.h b/src/storm/solver/SymbolicEliminationLinearEquationSolver.h index a77ac2a8c..45b0f0b12 100644 --- a/src/storm/solver/SymbolicEliminationLinearEquationSolver.h +++ b/src/storm/solver/SymbolicEliminationLinearEquationSolver.h @@ -15,7 +15,9 @@ namespace storm { class SymbolicEliminationLinearEquationSolver : public SymbolicLinearEquationSolver { public: SymbolicEliminationLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs); - + + SymbolicEliminationLinearEquationSolver(storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs); + virtual storm::dd::Add solveEquations(storm::dd::Add const& x, storm::dd::Add const& b) const override; private: @@ -34,7 +36,9 @@ namespace storm { template class SymbolicEliminationLinearEquationSolverFactory : public SymbolicLinearEquationSolverFactory { public: - virtual std::unique_ptr> create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const; + using SymbolicLinearEquationSolverFactory::create; + + virtual std::unique_ptr> create(storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const override; SymbolicEliminationLinearEquationSolverSettings& getSettings(); SymbolicEliminationLinearEquationSolverSettings const& getSettings() const; diff --git a/src/storm/solver/SymbolicLinearEquationSolver.cpp b/src/storm/solver/SymbolicLinearEquationSolver.cpp index 75fe87254..066b7b19b 100644 --- a/src/storm/solver/SymbolicLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicLinearEquationSolver.cpp @@ -20,10 +20,15 @@ namespace storm { namespace solver { template - SymbolicLinearEquationSolver::SymbolicLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) : A(A), allRows(allRows), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs) { + SymbolicLinearEquationSolver::SymbolicLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) : SymbolicLinearEquationSolver(allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs) { + this->setMatrix(A); + } + + template + SymbolicLinearEquationSolver::SymbolicLinearEquationSolver(storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) : allRows(allRows), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs) { // Intentionally left empty. } - + template storm::dd::Add SymbolicLinearEquationSolver::multiply(storm::dd::Add const& x, storm::dd::Add const* b, uint_fast64_t n) const { storm::dd::Add xCopy = x; @@ -46,21 +51,33 @@ namespace storm { } template - std::unique_ptr> GeneralSymbolicLinearEquationSolverFactory::create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const { + storm::dd::DdManager& SymbolicLinearEquationSolver::getDdManager() const { + return this->allRows.getDdManager(); + } + + template + std::unique_ptr> SymbolicLinearEquationSolverFactory::create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const { + std::unique_ptr> solver = this->create(allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs); + solver->setMatrix(A); + return solver; + } + + template + std::unique_ptr> GeneralSymbolicLinearEquationSolverFactory::create(storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const { storm::solver::EquationSolverType equationSolver = storm::settings::getModule().getEquationSolver(); switch (equationSolver) { - case storm::solver::EquationSolverType::Elimination: return std::make_unique>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs); + case storm::solver::EquationSolverType::Elimination: return std::make_unique>(allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs); break; - case storm::solver::EquationSolverType::Native: return std::make_unique>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs); + case storm::solver::EquationSolverType::Native: return std::make_unique>(allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs); break; default: STORM_LOG_WARN("The selected equation solver is not available in the dd engine. Falling back to native solver."); - return std::make_unique>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs); + return std::make_unique>(allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs); } } template - std::unique_ptr> GeneralSymbolicLinearEquationSolverFactory::create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const { + std::unique_ptr> GeneralSymbolicLinearEquationSolverFactory::create(storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const { auto const& coreSettings = storm::settings::getModule(); storm::solver::EquationSolverType equationSolver = coreSettings.getEquationSolver(); @@ -74,27 +91,27 @@ namespace storm { } switch (equationSolver) { - case storm::solver::EquationSolverType::Elimination: return std::make_unique>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs); + case storm::solver::EquationSolverType::Elimination: return std::make_unique>(allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs); break; case storm::solver::EquationSolverType::Native: - return std::make_unique>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs); + return std::make_unique>(allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs); break; default: STORM_LOG_WARN("The selected equation solver is not available in the dd engine. Falling back to elimination solver."); - return std::make_unique>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs); + return std::make_unique>(allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs); } } template - std::unique_ptr> GeneralSymbolicLinearEquationSolverFactory::create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const { + std::unique_ptr> GeneralSymbolicLinearEquationSolverFactory::create(storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const { storm::solver::EquationSolverType equationSolver = storm::settings::getModule().getEquationSolver(); switch (equationSolver) { - case storm::solver::EquationSolverType::Elimination: return std::make_unique>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs); + case storm::solver::EquationSolverType::Elimination: return std::make_unique>(allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs); break; default: STORM_LOG_WARN("The selected equation solver is not available in the DD setting. Falling back to elimination solver."); - return std::make_unique>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs); + return std::make_unique>(allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs); } } diff --git a/src/storm/solver/SymbolicLinearEquationSolver.h b/src/storm/solver/SymbolicLinearEquationSolver.h index 15b503175..9b3c3b490 100644 --- a/src/storm/solver/SymbolicLinearEquationSolver.h +++ b/src/storm/solver/SymbolicLinearEquationSolver.h @@ -5,6 +5,7 @@ #include #include "storm/storage/expressions/Variable.h" +#include "storm/storage/dd/DdManager.h" #include "storm/storage/dd/DdType.h" #include "storm/adapters/RationalFunctionAdapter.h" @@ -46,7 +47,20 @@ namespace storm { * variables. */ SymbolicLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs); - + + /*! + * Constructs a symbolic linear equation solver with the given meta variable sets and pairs. Note that in + * this version, the coefficient matrix has to be set manually afterwards. + * + * @param diagonal An ADD characterizing the elements on the diagonal of the matrix. + * @param allRows A BDD characterizing all rows of the equation system. + * @param rowMetaVariables The meta variables used to encode the rows of the matrix. + * @param columnMetaVariables The meta variables used to encode the columns of the matrix. + * @param rowColumnMetaVariablePairs The pairs of row meta variables and the corresponding column meta + * variables. + */ + SymbolicLinearEquationSolver(storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs); + /*! * Solves the equation system A*x = b. The matrix A is required to be square and have a unique solution. * The solution of the set of linear equations will be written to the vector x. Note that the matrix A has @@ -74,6 +88,8 @@ namespace storm { void setMatrix(storm::dd::Add const& newA); protected: + storm::dd::DdManager& getDdManager() const; + // The matrix defining the coefficients of the linear equation system. storm::dd::Add A; @@ -93,25 +109,33 @@ namespace storm { template class SymbolicLinearEquationSolverFactory { public: - virtual std::unique_ptr> create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const = 0; + virtual std::unique_ptr> create(storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const = 0; + + std::unique_ptr> create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const; }; template class GeneralSymbolicLinearEquationSolverFactory : public SymbolicLinearEquationSolverFactory { public: - virtual std::unique_ptr> create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const; + using SymbolicLinearEquationSolverFactory::create; + + virtual std::unique_ptr> create(storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const; }; template class GeneralSymbolicLinearEquationSolverFactory : public SymbolicLinearEquationSolverFactory { public: - virtual std::unique_ptr> create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const; + using SymbolicLinearEquationSolverFactory::create; + + virtual std::unique_ptr> create(storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const; }; template class GeneralSymbolicLinearEquationSolverFactory : public SymbolicLinearEquationSolverFactory { public: - virtual std::unique_ptr> create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const; + using SymbolicLinearEquationSolverFactory::create; + + virtual std::unique_ptr> create(storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const; }; } // namespace solver diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp index 9dc9e7c93..18fa0fcd3 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp @@ -107,6 +107,11 @@ namespace storm { uint_fast64_t iterations = 0; bool converged = false; + // If we were given an initial scheduler, we take its solution as the starting point. + if (this->hasInitialScheduler()) { + xCopy = solveEquationsWithScheduler(this->getInitialScheduler(), xCopy, b); + } + while (!converged && iterations < this->settings.getMaximalNumberOfIterations()) { // Compute tmp = A * x + b storm::dd::Add xCopyAsColumn = xCopy.swapVariables(this->rowColumnMetaVariablePairs); @@ -137,6 +142,30 @@ namespace storm { return xCopy; } + template + storm::dd::Add SymbolicMinMaxLinearEquationSolver::solveEquationsWithScheduler(storm::dd::Bdd const& scheduler, storm::dd::Add const& x, storm::dd::Add const& b) const { + + std::unique_ptr> solver = linearEquationSolverFactory->create(this->allRows, this->rowMetaVariables, this->columnMetaVariables, this->rowColumnMetaVariablePairs); + storm::dd::Add diagonal = (storm::utility::dd::getRowColumnDiagonal(x.getDdManager(), this->rowColumnMetaVariablePairs) && this->allRows).template toAdd(); + return solveEquationsWithScheduler(*solver, scheduler, x, b, diagonal); + } + + template + storm::dd::Add SymbolicMinMaxLinearEquationSolver::solveEquationsWithScheduler(SymbolicLinearEquationSolver& solver, storm::dd::Bdd const& scheduler, storm::dd::Add const& x, storm::dd::Add const& b, storm::dd::Add const& diagonal) const { + + // Apply scheduler to the matrix and vector. + storm::dd::Add schedulerA = diagonal - scheduler.ite(this->A, scheduler.getDdManager().template getAddZero()).sumAbstract(this->choiceVariables); + storm::dd::Add schedulerB = scheduler.ite(b, scheduler.getDdManager().template getAddZero()).sumAbstract(this->choiceVariables); + + // Set the matrix for the solver. + solver.setMatrix(schedulerA); + + // Solve for the value of the scheduler. + storm::dd::Add schedulerX = solver.solveEquations(x, schedulerB); + + return schedulerX; + } + template storm::dd::Add SymbolicMinMaxLinearEquationSolver::solveEquationsPolicyIteration(storm::solver::OptimizationDirection const& dir, storm::dd::Add const& x, storm::dd::Add const& b) const { // Set up the environment. @@ -148,17 +177,12 @@ namespace storm { // Choose initial scheduler. storm::dd::Bdd scheduler = this->hasInitialScheduler() ? this->getInitialScheduler() : this->A.sumAbstract(this->columnMetaVariables).maxAbstractRepresentative(this->choiceVariables); - // And apply it to the matrix and vector. - storm::dd::Add schedulerA = diagonal - scheduler.ite(this->A, scheduler.getDdManager().template getAddZero()).sumAbstract(this->choiceVariables); - storm::dd::Add schedulerB = scheduler.ite(b, scheduler.getDdManager().template getAddZero()).sumAbstract(this->choiceVariables); - // Initialize linear equation solver. - std::unique_ptr> linearEquationSolver = linearEquationSolverFactory->create(schedulerA, this->allRows, this->rowMetaVariables, this->columnMetaVariables, this->rowColumnMetaVariablePairs); + std::unique_ptr> linearEquationSolver = linearEquationSolverFactory->create(this->allRows, this->rowMetaVariables, this->columnMetaVariables, this->rowColumnMetaVariablePairs); // Iteratively solve and improve the scheduler. while (!converged && iterations < this->settings.getMaximalNumberOfIterations()) { - // Solve for the value of the scheduler. - storm::dd::Add schedulerX = linearEquationSolver->solveEquations(currentSolution, schedulerB); + storm::dd::Add schedulerX = solveEquationsWithScheduler(*linearEquationSolver, scheduler, currentSolution, b, diagonal); // Policy improvement step. storm::dd::Add choiceValues = this->A.multiplyMatrix(schedulerX.swapVariables(this->rowColumnMetaVariablePairs), this->columnMetaVariables) + b; @@ -177,9 +201,6 @@ namespace storm { // Set up next iteration. if (!converged) { scheduler = nextScheduler; - schedulerA = diagonal - scheduler.ite(this->A, scheduler.getDdManager().template getAddZero()).sumAbstract(this->choiceVariables); - linearEquationSolver->setMatrix(schedulerA); - schedulerB = scheduler.ite(b, scheduler.getDdManager().template getAddZero()).sumAbstract(this->choiceVariables); } currentSolution = schedulerX; diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h index e9e76ee6e..b0f70ac39 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h +++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h @@ -139,6 +139,9 @@ namespace storm { bool isRequirementsCheckedSet() const; private: + storm::dd::Add solveEquationsWithScheduler(storm::dd::Bdd const& scheduler, storm::dd::Add const& x, storm::dd::Add const& b) const; + storm::dd::Add solveEquationsWithScheduler(SymbolicLinearEquationSolver& solver, storm::dd::Bdd const& scheduler, storm::dd::Add const& x, storm::dd::Add const& b, storm::dd::Add const& diagonal) const; + storm::dd::Add solveEquationsValueIteration(storm::solver::OptimizationDirection const& dir, storm::dd::Add const& x, storm::dd::Add const& b) const; storm::dd::Add solveEquationsPolicyIteration(storm::solver::OptimizationDirection const& dir, storm::dd::Add const& x, storm::dd::Add const& b) const; diff --git a/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp b/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp index 2d0e82a1d..9132ac710 100644 --- a/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp @@ -54,13 +54,18 @@ namespace storm { } template - SymbolicNativeLinearEquationSolver::SymbolicNativeLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, SymbolicNativeLinearEquationSolverSettings const& settings) : SymbolicLinearEquationSolver(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs), settings(settings) { + SymbolicNativeLinearEquationSolver::SymbolicNativeLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, SymbolicNativeLinearEquationSolverSettings const& settings) : SymbolicNativeLinearEquationSolver(allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, settings) { + this->setMatrix(A); + } + + template + SymbolicNativeLinearEquationSolver::SymbolicNativeLinearEquationSolver(storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, SymbolicNativeLinearEquationSolverSettings const& settings) : SymbolicLinearEquationSolver(allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs), settings(settings) { // Intentionally left empty. } template storm::dd::Add SymbolicNativeLinearEquationSolver::solveEquations(storm::dd::Add const& x, storm::dd::Add const& b) const { - storm::dd::DdManager& manager = this->A.getDdManager(); + storm::dd::DdManager& manager = this->getDdManager(); // Start by computing the Jacobi decomposition of the matrix A. storm::dd::Bdd diagonal = storm::utility::dd::getRowColumnDiagonal(x.getDdManager(), this->rowColumnMetaVariablePairs); @@ -106,8 +111,8 @@ namespace storm { } template - std::unique_ptr> SymbolicNativeLinearEquationSolverFactory::create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const { - return std::make_unique>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, settings); + std::unique_ptr> SymbolicNativeLinearEquationSolverFactory::create(storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const { + return std::make_unique>(allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, settings); } template diff --git a/src/storm/solver/SymbolicNativeLinearEquationSolver.h b/src/storm/solver/SymbolicNativeLinearEquationSolver.h index 60e00ddf7..23b166a7c 100644 --- a/src/storm/solver/SymbolicNativeLinearEquationSolver.h +++ b/src/storm/solver/SymbolicNativeLinearEquationSolver.h @@ -50,7 +50,20 @@ namespace storm { * @param settings The settings to use. */ SymbolicNativeLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, SymbolicNativeLinearEquationSolverSettings const& settings = SymbolicNativeLinearEquationSolverSettings()); - + + /*! + * Constructs a symbolic linear equation solver with the given meta variable sets and pairs. + * + * @param diagonal An ADD characterizing the elements on the diagonal of the matrix. + * @param allRows A BDD characterizing all rows of the equation system. + * @param rowMetaVariables The meta variables used to encode the rows of the matrix. + * @param columnMetaVariables The meta variables used to encode the columns of the matrix. + * @param rowColumnMetaVariablePairs The pairs of row meta variables and the corresponding column meta + * variables. + * @param settings The settings to use. + */ + SymbolicNativeLinearEquationSolver(storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, SymbolicNativeLinearEquationSolverSettings const& settings = SymbolicNativeLinearEquationSolverSettings()); + /*! * Solves the equation system A*x = b. The matrix A is required to be square and have a unique solution. * The solution of the set of linear equations will be written to the vector x. Note that the matrix A has @@ -70,9 +83,11 @@ namespace storm { }; template - class SymbolicNativeLinearEquationSolverFactory { + class SymbolicNativeLinearEquationSolverFactory : SymbolicLinearEquationSolverFactory { public: - virtual std::unique_ptr> create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const; + using SymbolicLinearEquationSolverFactory::create; + + virtual std::unique_ptr> create(storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const override; SymbolicNativeLinearEquationSolverSettings& getSettings(); SymbolicNativeLinearEquationSolverSettings const& getSettings() const; diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 4464ed2be..1cd70c0fd 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -896,7 +896,7 @@ namespace storm { uint_fast64_t iterations = 0; while (!frontier.isZero()) { - storm::dd::Bdd statesAndChoicesWithProbabilityGreater0E = statesWithProbabilityGreater0E.inverseRelationalProduct(transitionMatrix, model.getRowVariables(), model.getColumnVariables()); + storm::dd::Bdd statesAndChoicesWithProbabilityGreater0E = statesWithProbabilityGreater0E.inverseRelationalProductWithExtendedRelation(transitionMatrix, model.getRowVariables(), model.getColumnVariables()); frontier = phiStates && statesAndChoicesWithProbabilityGreater0E.existsAbstract(model.getNondeterminismVariables()) && !statesWithProbabilityGreater0E; scheduler = scheduler || (frontier && statesAndChoicesWithProbabilityGreater0E).existsAbstractRepresentative(model.getNondeterminismVariables()); statesWithProbabilityGreater0E |= frontier; @@ -1019,6 +1019,41 @@ namespace storm { return statesWithProbability1E; } + template + storm::dd::Bdd computeSchedulerProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbability1E) { + // Initialize environment for backward search. + storm::dd::DdManager const& manager = model.getManager(); + storm::dd::Bdd scheduler = manager.getBddZero(); + + storm::dd::Bdd innerStates = manager.getBddZero(); + + uint64_t iterations = 0; + bool innerLoopDone = false; + while (!innerLoopDone) { + storm::dd::Bdd temporary = statesWithProbability1E.swapVariables(model.getRowColumnMetaVariablePairs()); + temporary = transitionMatrix.implies(temporary).universalAbstract(model.getColumnVariables()); + + storm::dd::Bdd temporary2 = innerStates.inverseRelationalProductWithExtendedRelation(transitionMatrix, model.getRowVariables(), model.getColumnVariables()); + temporary &= temporary2; + temporary &= phiStates; + + // Extend the scheduler for those states that have not been seen as inner states before. + scheduler |= (temporary && !innerStates).existsAbstractRepresentative(model.getNondeterminismVariables()); + + temporary = temporary.existsAbstract(model.getNondeterminismVariables()); + temporary |= psiStates; + + if (innerStates == temporary) { + innerLoopDone = true; + } else { + innerStates = temporary; + } + ++iterations; + } + + return scheduler; + } + template std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { std::pair, storm::dd::Bdd> result; @@ -1512,6 +1547,8 @@ namespace storm { template storm::dd::Bdd performProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0E); + template storm::dd::Bdd computeSchedulerProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbability1E); + template std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); @@ -1546,6 +1583,8 @@ namespace storm { template storm::dd::Bdd performProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0E); + template storm::dd::Bdd computeSchedulerProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbability1E); + template std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); @@ -1580,6 +1619,8 @@ namespace storm { template storm::dd::Bdd performProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0E); + template storm::dd::Bdd computeSchedulerProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbability1E); + template std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); @@ -1610,6 +1651,8 @@ namespace storm { template storm::dd::Bdd performProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0E); + template storm::dd::Bdd computeSchedulerProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbability1E); + template std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); diff --git a/src/storm/utility/graph.h b/src/storm/utility/graph.h index 69a07770c..010e68feb 100644 --- a/src/storm/utility/graph.h +++ b/src/storm/utility/graph.h @@ -521,6 +521,12 @@ namespace storm { template storm::dd::Bdd performProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0E); + /*! + * Computes a scheduler satisfying phi until psi with probability 1. + */ + template + storm::dd::Bdd computeSchedulerProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbability1E); + template std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates);