From e3320ee0867680d29b744a2bbb860179dc9807a1 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 10 Apr 2015 17:57:24 +0200 Subject: [PATCH] Started working on hybrid MDP model checker. Former-commit-id: 63a8efb93c8283fdfa4c6ee3a8558db3557dd46a --- .../prctl/HybridMdpPrctlModelChecker.cpp | 328 ++++++++++++++++++ .../prctl/HybridMdpPrctlModelChecker.h | 44 +++ .../prctl/SparseMdpPrctlModelChecker.cpp | 12 +- src/storage/dd/CuddAdd.cpp | 96 +++++ src/storage/dd/CuddAdd.h | 45 ++- src/utility/cli.h | 7 + src/utility/graph.h | 2 +- 7 files changed, 525 insertions(+), 9 deletions(-) create mode 100644 src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp create mode 100644 src/modelchecker/prctl/HybridMdpPrctlModelChecker.h diff --git a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp new file mode 100644 index 000000000..9f1c263f4 --- /dev/null +++ b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp @@ -0,0 +1,328 @@ +#include "src/modelchecker/prctl/HybridMdpPrctlModelChecker.h" + +#include "src/storage/dd/CuddOdd.h" + +#include "src/utility/macros.h" +#include "src/utility/graph.h" + +#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" +#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" +#include "src/modelchecker/results/HybridQuantitativeCheckResult.h" + +#include "src/exceptions/InvalidStateException.h" +#include "src/exceptions/InvalidPropertyException.h" + +namespace storm { + namespace modelchecker { + template + HybridMdpPrctlModelChecker::HybridMdpPrctlModelChecker(storm::models::symbolic::Mdp const& model, std::unique_ptr>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { + // Intentionally left empty. + } + + template + HybridMdpPrctlModelChecker::HybridMdpPrctlModelChecker(storm::models::symbolic::Mdp const& model) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(new storm::utility::solver::MinMaxLinearEquationSolverFactory()) { + // Intentionally left empty. + } + + template + bool HybridMdpPrctlModelChecker::canHandle(storm::logic::Formula const& formula) const { + return formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula(); + } + + template + std::unique_ptr HybridMdpPrctlModelChecker::computeUntilProbabilitiesHelper(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { + // We need to identify the states which have to be taken out of the matrix, i.e. all states that have + // probability 0 and 1 of satisfying the until-formula. + std::pair, storm::dd::Bdd> statesWithProbability01; + if (minimize) { + statesWithProbability01 = storm::utility::graph::performProb01Min(model, phiStates, psiStates); + } else { + statesWithProbability01 = storm::utility::graph::performProb01Max(model, phiStates, psiStates); + } + storm::dd::Bdd maybeStates = !statesWithProbability01.first && !statesWithProbability01.second && model.getReachableStates(); + + // Perform some logging. + STORM_LOG_INFO("Found " << statesWithProbability01.first.getNonZeroCount() << " 'no' states."); + STORM_LOG_INFO("Found " << statesWithProbability01.second.getNonZeroCount() << " 'yes' states."); + STORM_LOG_INFO("Found " << maybeStates.getNonZeroCount() << " 'maybe' states."); + + // Check whether we need to compute exact probabilities for some states. + if (qualitative) { + // Set the values for all maybe-states to 0.5 to indicate that their probability values are neither 0 nor 1. + return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), statesWithProbability01.second.toAdd() + maybeStates.toAdd() * model.getManager().getConstant(0.5))); + } else { + // If there are maybe states, we need to solve an equation system. + if (!maybeStates.isZero()) { + // Create the ODD for the translation between symbolic and explicit storage. + storm::dd::Odd odd(maybeStates); + + // Create the matrix and the vector for the equation system. + storm::dd::Add maybeStatesAdd = maybeStates.toAdd(); + + // Start by cutting away all rows that do not belong to maybe states. Note that this leaves columns targeting + // non-maybe states in the matrix. + storm::dd::Add submatrix = transitionMatrix * maybeStatesAdd; + + // Then compute the vector that contains the one-step probabilities to a state with probability 1 for all + // maybe states. + storm::dd::Add prob1StatesAsColumn = statesWithProbability01.second.toAdd(); + prob1StatesAsColumn = prob1StatesAsColumn.swapVariables(model.getRowColumnMetaVariablePairs()); + storm::dd::Add subvector = submatrix * prob1StatesAsColumn; + subvector = subvector.sumAbstract(model.getColumnVariables()); + + // Finally cut away all columns targeting non-maybe states and convert the matrix into the matrix needed + // for solving the equation system (i.e. compute (I-A)). + submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); + submatrix = (model.getRowColumnIdentity() * maybeStatesAdd) - submatrix; + + // Create the solution vector. + std::vector x(maybeStates.getNonZeroCount(), ValueType(0.5)); + + // Translate the symbolic matrix/vector to their explicit representations and solve the equation system. + storm::storage::SparseMatrix explicitSubmatrix = submatrix.toMatrix(model.getNondeterminismVariables(), odd, odd); + std::vector b = subvector.template toVector(odd); + + std::unique_ptr> solver = linearEquationSolverFactory.create(explicitSubmatrix); + solver->solveEquationSystem(minimize, x, b); + + // Return a hybrid check result that stores the numerical values explicitly. + return std::unique_ptr(new storm::modelchecker::HybridQuantitativeCheckResult(model.getReachableStates(), model.getReachableStates() && !maybeStates, statesWithProbability01.second.toAdd(), maybeStates, odd, x)); + } else { + return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), statesWithProbability01.second.toAdd())); + } + } + } + + template + std::unique_ptr HybridMdpPrctlModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); + std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); + SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); + SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); + return this->computeUntilProbabilitiesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + } + + template + std::unique_ptr HybridMdpPrctlModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); + SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); + return std::unique_ptr(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), this->computeNextProbabilitiesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()))); + } + + template + storm::dd::Add HybridMdpPrctlModelChecker::computeNextProbabilitiesHelper(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& nextStates) { + storm::dd::Add result = transitionMatrix * nextStates.swapVariables(model.getRowColumnMetaVariablePairs()).toAdd(); + return result.sumAbstract(model.getColumnVariables()); + } + + template + std::unique_ptr HybridMdpPrctlModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); + std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); + std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); + SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); + SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); + return this->computeBoundedUntilProbabilitiesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + } + + template + std::unique_ptr HybridMdpPrctlModelChecker::computeBoundedUntilProbabilitiesHelper(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { + // We need to identify the states which have to be taken out of the matrix, i.e. all states that have + // probability 0 or 1 of satisfying the until-formula. + storm::dd::Bdd statesWithProbabilityGreater0; + if (minimize) { + statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0A(model, transitionMatrix.notZero(), phiStates, psiStates); + } else { + statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0E(model, transitionMatrix.notZero(), phiStates, psiStates); + } + storm::dd::Bdd maybeStates = statesWithProbabilityGreater0 && !psiStates && model.getReachableStates(); + + // If there are maybe states, we need to perform matrix-vector multiplications. + if (!maybeStates.isZero()) { + // Create the ODD for the translation between symbolic and explicit storage. + storm::dd::Odd odd(maybeStates); + + // Create the matrix and the vector for the equation system. + storm::dd::Add maybeStatesAdd = maybeStates.toAdd(); + + // Start by cutting away all rows that do not belong to maybe states. Note that this leaves columns targeting + // non-maybe states in the matrix. + storm::dd::Add submatrix = transitionMatrix * maybeStatesAdd; + + // Then compute the vector that contains the one-step probabilities to a state with probability 1 for all + // maybe states. + storm::dd::Add prob1StatesAsColumn = psiStates.toAdd().swapVariables(model.getRowColumnMetaVariablePairs()); + storm::dd::Add subvector = (submatrix * prob1StatesAsColumn).sumAbstract(model.getColumnVariables()); + + // Finally cut away all columns targeting non-maybe states. + submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); + + // Create the solution vector. + std::vector x(maybeStates.getNonZeroCount(), storm::utility::zero()); + + // Translate the symbolic matrix/vector to their explicit representations. + storm::storage::SparseMatrix explicitSubmatrix = submatrix.toMatrix(model.getNondeterminismVariables(), odd, odd); + std::vector b = subvector.template toVector(odd); + + std::unique_ptr> solver = linearEquationSolverFactory.create(explicitSubmatrix); + solver->performMatrixVectorMultiplication(minimize, x, &b, stepBound); + + // Return a hybrid check result that stores the numerical values explicitly. + return std::unique_ptr(new storm::modelchecker::HybridQuantitativeCheckResult(model.getReachableStates(), model.getReachableStates() && !maybeStates, psiStates.toAdd(), maybeStates, odd, x)); + } else { + return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), psiStates.toAdd())); + } + } + + template + std::unique_ptr HybridMdpPrctlModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); + return this->computeCumulativeRewardsHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + } + + template + std::unique_ptr HybridMdpPrctlModelChecker::computeCumulativeRewardsHelper(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { + // Only compute the result if the model has at least one reward this->getModel(). + STORM_LOG_THROW(model.hasStateRewards() || model.hasTransitionRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); + + // Compute the reward vector to add in each step based on the available reward models. + storm::dd::Add totalRewardVector = model.hasStateRewards() ? model.getStateRewardVector() : model.getManager().getAddZero(); + if (model.hasTransitionRewards()) { + totalRewardVector += (transitionMatrix * model.getTransitionRewardMatrix()).sumAbstract(model.getColumnVariables()); + } + + // Create the ODD for the translation between symbolic and explicit storage. + storm::dd::Odd odd(model.getReachableStates()); + + // Create the solution vector. + std::vector x(model.getNumberOfStates(), storm::utility::zero()); + + // Translate the symbolic matrix/vector to their explicit representations. + storm::storage::SparseMatrix explicitMatrix = transitionMatrix.toMatrix(model.getNondeterminismVariables(), odd, odd); + std::vector b = totalRewardVector.template toVector(odd); + + // Perform the matrix-vector multiplication. + std::unique_ptr> solver = linearEquationSolverFactory.create(explicitMatrix); + solver->performMatrixVectorMultiplication(minimize, x, &b, stepBound); + + // Return a hybrid check result that stores the numerical values explicitly. + return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().getAddZero(), model.getReachableStates(), odd, x)); + } + + template + std::unique_ptr HybridMdpPrctlModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); + return this->computeInstantaneousRewardsHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + } + + template + std::unique_ptr HybridMdpPrctlModelChecker::computeInstantaneousRewardsHelper(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { + // Only compute the result if the model has at least one reward this->getModel(). + STORM_LOG_THROW(model.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); + + // Create the ODD for the translation between symbolic and explicit storage. + storm::dd::Odd odd(model.getReachableStates()); + + // Create the solution vector (and initialize it to the state rewards of the model). + std::vector x = model.getStateRewardVector().template toVector(odd); + + // Translate the symbolic matrix to its explicit representations. + storm::storage::SparseMatrix explicitMatrix = transitionMatrix.toMatrix(model.getNondeterminismVariables(), odd, odd); + + // Perform the matrix-vector multiplication. + std::unique_ptr> solver = linearEquationSolverFactory.create(explicitMatrix); + solver->performMatrixVectorMultiplication(minimize, x, nullptr, stepBound); + + // Return a hybrid check result that stores the numerical values explicitly. + return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().getAddZero(), model.getReachableStates(), odd, x)); + } + + template + std::unique_ptr HybridMdpPrctlModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); + SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); + return this->computeReachabilityRewardsHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getOptionalStateRewardVector(), this->getModel().getOptionalTransitionRewardMatrix(), subResult.getTruthValuesVector(), *this->linearEquationSolverFactory, qualitative); + } + + template + std::unique_ptr HybridMdpPrctlModelChecker::computeReachabilityRewardsHelper(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, boost::optional> const& stateRewardVector, boost::optional> const& transitionRewardMatrix, storm::dd::Bdd const& targetStates, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory, bool qualitative) { + + // Only compute the result if there is at least one reward model. + STORM_LOG_THROW(stateRewardVector || transitionRewardMatrix, storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); + + // Determine which states have a reward of infinity by definition. + storm::dd::Bdd infinityStates; + storm::dd::Bdd transitionMatrixBdd = transitionMatrix.notZero(); + if (minimize) { + infinityStates = storm::utility::graph::performProb1A(model, transitionMatrixBdd, model.getReachableStates(), targetStates, storm::utility::graph::performProbGreater0A(model, transitionMatrixBdd, model.getManager().getBddZero(), targetStates)); + } else { + infinityStates = storm::utility::graph::performProb1E(model, transitionMatrixBdd, model.getReachableStates(), targetStates, storm::utility::graph::performProbGreater0E(model, transitionMatrixBdd, model.getManager().getBddZero(), targetStates)); + } + infinityStates = !infinityStates && model.getReachableStates(); + storm::dd::Bdd maybeStates = (!targetStates && !infinityStates) && model.getReachableStates(); + STORM_LOG_INFO("Found " << infinityStates.getNonZeroCount() << " 'infinity' states."); + STORM_LOG_INFO("Found " << targetStates.getNonZeroCount() << " 'target' states."); + STORM_LOG_INFO("Found " << maybeStates.getNonZeroCount() << " 'maybe' states."); + + // Check whether we need to compute exact rewards for some states. + if (qualitative) { + // Set the values for all maybe-states to 1 to indicate that their reward values + // are neither 0 nor infinity. + return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), infinityStates.toAdd() * model.getManager().getConstant(storm::utility::infinity()) + maybeStates.toAdd() * model.getManager().getConstant(storm::utility::one()))); + } else { + // If there are maybe states, we need to solve an equation system. + if (!maybeStates.isZero()) { + // Create the ODD for the translation between symbolic and explicit storage. + storm::dd::Odd odd(maybeStates); + + // Create the matrix and the vector for the equation system. + storm::dd::Add maybeStatesAdd = maybeStates.toAdd(); + + // Start by cutting away all rows that do not belong to maybe states. Note that this leaves columns targeting + // non-maybe states in the matrix. + storm::dd::Add submatrix = transitionMatrix * maybeStatesAdd; + + // Then compute the state reward vector to use in the computation. + storm::dd::Add subvector = stateRewardVector ? maybeStatesAdd * stateRewardVector.get() : model.getManager().getAddZero(); + if (transitionRewardMatrix) { + subvector += (submatrix * transitionRewardMatrix.get()).sumAbstract(model.getColumnVariables()); + } + + // Finally cut away all columns targeting non-maybe states and convert the matrix into the matrix needed + // for solving the equation system (i.e. compute (I-A)). + submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); + submatrix = (model.getRowColumnIdentity() * maybeStatesAdd) - submatrix; + + // Create the solution vector. + std::vector x(maybeStates.getNonZeroCount(), ValueType(0.5)); + + // Translate the symbolic matrix/vector to their explicit representations. + storm::storage::SparseMatrix explicitSubmatrix = submatrix.toMatrix(model.getNondeterminismVariables(), odd, odd); + std::vector b = subvector.template toVector(odd); + + // Now solve the resulting equation system. + std::unique_ptr> solver = linearEquationSolverFactory.create(explicitSubmatrix); + solver->solveEquationSystem(minimize, x, b); + + // Return a hybrid check result that stores the numerical values explicitly. + return std::unique_ptr(new storm::modelchecker::HybridQuantitativeCheckResult(model.getReachableStates(), model.getReachableStates() && !maybeStates, infinityStates.toAdd() * model.getManager().getConstant(storm::utility::infinity()), maybeStates, odd, x)); + } else { + return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), infinityStates.toAdd() * model.getManager().getConstant(storm::utility::infinity()))); + } + } + } + + template + storm::models::symbolic::Mdp const& HybridMdpPrctlModelChecker::getModel() const { + return this->template getModelAs>(); + } + + template class HybridMdpPrctlModelChecker; + } +} \ No newline at end of file diff --git a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h new file mode 100644 index 000000000..24a33ee79 --- /dev/null +++ b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h @@ -0,0 +1,44 @@ +#ifndef STORM_MODELCHECKER_HYBRIDMDPPRCTLMODELCHECKER_H_ +#define STORM_MODELCHECKER_HYBRIDMDPPRCTLMODELCHECKER_H_ + +#include "src/modelchecker/propositional/SymbolicPropositionalModelChecker.h" +#include "src/models/symbolic/Mdp.h" +#include "src/utility/solver.h" + +namespace storm { + namespace modelchecker { + template + class HybridMdpPrctlModelChecker : public SymbolicPropositionalModelChecker { + public: + explicit HybridMdpPrctlModelChecker(storm::models::symbolic::Mdp const& model); + explicit HybridMdpPrctlModelChecker(storm::models::symbolic::Mdp const& model, std::unique_ptr>&& linearEquationSolverFactory); + + // The implemented methods of the AbstractModelChecker interface. + virtual bool canHandle(storm::logic::Formula const& formula) const override; + virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + + protected: + storm::models::symbolic::Mdp const& getModel() const override; + + private: + // The methods that perform the actual checking. + static std::unique_ptr computeBoundedUntilProbabilitiesHelper(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); + static storm::dd::Add computeNextProbabilitiesHelper(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& nextStates); + static std::unique_ptr computeUntilProbabilitiesHelper(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeCumulativeRewardsHelper(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeInstantaneousRewardsHelper(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeReachabilityRewardsHelper(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, boost::optional> const& stateRewardVector, boost::optional> const& transitionRewardMatrix, storm::dd::Bdd const& targetStates, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory, bool qualitative); + + // An object that is used for retrieving linear equation solvers. + std::unique_ptr> linearEquationSolverFactory; + }; + + } // namespace modelchecker +} // namespace storm + +#endif /* STORM_MODELCHECKER_HYBRIDMDPPRCTLMODELCHECKER_H_ */ diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index bc4bb8a8e..0d46f40c9 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -66,7 +66,7 @@ namespace storm { template std::unique_ptr SparseMdpPrctlModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic."); + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); @@ -90,7 +90,7 @@ namespace storm { template std::unique_ptr SparseMdpPrctlModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic."); + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeNextProbabilitiesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, subResult.getTruthValuesVector()))); @@ -160,7 +160,7 @@ namespace storm { template std::unique_ptr SparseMdpPrctlModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic."); + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); @@ -200,7 +200,7 @@ namespace storm { template std::unique_ptr SparseMdpPrctlModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic."); + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeCumulativeRewardsHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, rewardPathFormula.getDiscreteTimeBound()))); } @@ -222,7 +222,7 @@ namespace storm { template std::unique_ptr SparseMdpPrctlModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic."); + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeInstantaneousRewardsHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, rewardPathFormula.getDiscreteTimeBound()))); } @@ -310,7 +310,7 @@ namespace storm { template std::unique_ptr SparseMdpPrctlModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic."); + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeReachabilityRewardsHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel().getTransitionMatrix(), this->getModel().getOptionalStateRewardVector(), this->getModel().getOptionalTransitionRewardMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), *this->MinMaxLinearEquationSolverFactory, qualitative))); diff --git a/src/storage/dd/CuddAdd.cpp b/src/storage/dd/CuddAdd.cpp index 8152083cd..2bc170615 100644 --- a/src/storage/dd/CuddAdd.cpp +++ b/src/storage/dd/CuddAdd.cpp @@ -428,6 +428,62 @@ namespace storm { return result; } + template + std::vector Add::toVector(std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd) const { + std::set rowMetaVariables; + + // Prepare the proper sets of meta variables. + for (auto const& variable : this->getContainedMetaVariables()) { + if (groupMetaVariables.find(variable) != groupMetaVariables.end()) { + continue; + } + + rowMetaVariables.insert(variable); + } + std::vector ddGroupVariableIndices; + for (auto const& variable : groupMetaVariables) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddGroupVariableIndices.push_back(ddVariable.getIndex()); + } + } + std::vector ddRowVariableIndices; + for (auto const& variable : rowMetaVariables) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddRowVariableIndices.push_back(ddVariable.getIndex()); + } + } + + // Start by computing the offsets (in terms of rows) for each row group. + Add stateToNumberOfChoices = this->notZero().toAdd().sumAbstract(groupMetaVariables); + std::vector rowGroupIndices = stateToNumberOfChoices.toVector(rowOdd); + rowGroupIndices.resize(rowGroupIndices.size() + 1); + uint_fast64_t tmp = 0; + uint_fast64_t tmp2 = 0; + for (uint_fast64_t i = 1; i < rowGroupIndices.size(); ++i) { + tmp2 = rowGroupIndices[i]; + rowGroupIndices[i] = rowGroupIndices[i - 1] + tmp; + std::swap(tmp, tmp2); + } + rowGroupIndices[0] = 0; + + // Then split the symbolic vector into groups. + std::vector> groups; + splitGroupsRec(this->getCuddDdNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size(), rowMetaVariables); + + // Now iterate over the groups and add them to the resulting vector. + std::vector result(rowGroupIndices.back(), storm::utility::zero()); + for (uint_fast64_t i = 0; i < groups.size(); ++i) { + auto const& dd = groups[i]; + + toVectorRec(dd.getCuddDdNode(), result, rowGroupIndices, rowOdd, 0, ddRowVariableIndices.size(), 0, ddRowVariableIndices); + addToVectorRec(dd.notZero().toAdd().getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices); + } + + return result; + } + storm::storage::SparseMatrix Add::toMatrix() const { std::set rowVariables; std::set columnVariables; @@ -520,6 +576,26 @@ namespace storm { return storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(trivialRowGroupIndices)); } + storm::storage::SparseMatrix Add::toMatrix(std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { + std::set rowMetaVariables; + std::set columnMetaVariables; + + for (auto const& variable : this->getContainedMetaVariables()) { + // If the meta variable is a group meta variable, we do not insert it into the set of row/column meta variables. + if (groupMetaVariables.find(variable) != groupMetaVariables.end()) { + continue; + } + + if (variable.getName().size() > 0 && variable.getName().back() == '\'') { + columnMetaVariables.insert(variable); + } else { + rowMetaVariables.insert(variable); + } + } + + return toMatrix(rowMetaVariables, columnMetaVariables, groupMetaVariables, rowOdd, columnOdd); + } + storm::storage::SparseMatrix Add::toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { std::vector ddRowVariableIndices; std::vector ddColumnVariableIndices; @@ -625,6 +701,26 @@ namespace storm { return storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)); } + template + void Add::toVectorRec(DdNode const* dd, std::vector& result, std::vector& rowGroupOffsets, Odd const& rowOdd, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector const& ddRowVariableIndices) { + // For the empty DD, we do not need to add any entries. + if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { + return; + } + + // If we are at the maximal level, the value to be set is stored as a constant in the DD. + if (currentRowLevel == maxLevel) { + result[rowGroupOffsets[currentRowOffset]] = Cudd_V(dd); + ++rowGroupOffsets[currentRowOffset]; + } else if (ddRowVariableIndices[currentRowLevel] < dd->index) { + toVectorRec(dd, result, rowGroupOffsets, rowOdd.getElseSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset, ddRowVariableIndices); + toVectorRec(dd, result, rowGroupOffsets, rowOdd.getThenSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), ddRowVariableIndices); + } else { + toVectorRec(Cudd_E(dd), result, rowGroupOffsets, rowOdd.getElseSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset, ddRowVariableIndices); + toVectorRec(Cudd_T(dd), result, rowGroupOffsets, rowOdd.getThenSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), ddRowVariableIndices); + } + } + void Add::toMatrixRec(DdNode const* dd, std::vector& rowIndications, std::vector>& columnsAndValues, std::vector const& rowGroupOffsets, Odd const& rowOdd, Odd const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector const& ddRowVariableIndices, std::vector const& ddColumnVariableIndices, bool generateValues) const { // For the empty DD, we do not need to add any entries. if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { diff --git a/src/storage/dd/CuddAdd.h b/src/storage/dd/CuddAdd.h index 8d01839d6..78e29eb4f 100644 --- a/src/storage/dd/CuddAdd.h +++ b/src/storage/dd/CuddAdd.h @@ -512,7 +512,7 @@ namespace storm { /*! * Converts the ADD to a vector. * - * @return The double vector that is represented by this ADD. + * @return The vector that is represented by this ADD. */ template std::vector toVector() const; @@ -522,11 +522,23 @@ namespace storm { * each entry. * * @param rowOdd The ODD used for determining the correct row. - * @return The double vector that is represented by this ADD. + * @return The vector that is represented by this ADD. */ template std::vector toVector(storm::dd::Odd const& rowOdd) const; + /*! + * Converts the ADD to a row-grouped vector. The given offset-labeled DD is used to determine the correct + * row group of each entry. Note that the group meta variables are assumed to be at the very top in the + * variable ordering. + * + * @param groupMetaVariables The meta variables responsible for the row-grouping. + * @param rowOdd The ODD used for determining the correct row. + * @return The vector that is represented by this ADD. + */ + template + std::vector toVector(std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd) const; + /*! * Converts the ADD to a (sparse) double matrix. All contained non-primed variables are assumed to encode the * row, whereas all primed variables are assumed to encode the column. @@ -558,6 +570,18 @@ namespace storm { */ storm::storage::SparseMatrix toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; + /*! + * Converts the ADD to a row-grouped (sparse) double matrix. The given offset-labeled DDs are used to + * determine the correct row and column, respectively, for each entry. Note: this function assumes that + * the meta variables used to distinguish different row groups are at the very top of the ADD. + * + * @param groupMetaVariables The meta variables that are used to distinguish different row groups. + * @param rowOdd The ODD used for determining the correct row. + * @param columnOdd The ODD used for determining the correct column. + * @return The matrix that is represented by this ADD. + */ + storm::storage::SparseMatrix toMatrix(std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; + /*! * Converts the ADD to a row-grouped (sparse) double matrix. The given offset-labeled DDs are used to * determine the correct row and column, respectively, for each entry. Note: this function assumes that @@ -659,6 +683,23 @@ namespace storm { */ void toMatrixRec(DdNode const* dd, std::vector& rowIndications, std::vector>& columnsAndValues, std::vector const& rowGroupOffsets, Odd const& rowOdd, Odd const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector const& ddRowVariableIndices, std::vector const& ddColumnVariableIndices, bool generateValues = true) const; + /*! + * Helper function to convert the DD into a (sparse) vector. + * + * @param dd The DD to convert. + * @param result The vector that will hold the values upon successful completion. + * @param rowGroupOffsets The row offsets at which a given row group starts. Note this vector is modified in + * the computation. More concretely, each entry i in the vector will be increased by one iff there was a + * non-zero entry in that row-group. + * @param rowOdd The ODD used for the row translation. + * @param currentRowLevel The currently considered row level in the DD. + * @param maxLevel The number of levels that need to be considered. + * @param currentRowOffset The current row offset. + * @param ddRowVariableIndices The (sorted) indices of all DD row variables that need to be considered. + */ + template + void toVectorRec(DdNode const* dd, std::vector& result, std::vector& rowGroupOffsets, Odd const& rowOdd, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector const& ddRowVariableIndices); + /*! * Splits the given matrix DD into the groups using the given group variables. * diff --git a/src/utility/cli.h b/src/utility/cli.h index c7c8d1235..f32c25291 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -69,6 +69,7 @@ log4cplus::Logger printer; #include "src/modelchecker/csl/SparseCtmcCslModelChecker.h" #include "src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h" #include "src/modelchecker/csl/HybridCtmcCslModelChecker.h" +#include "src/modelchecker/prctl/HybridMdpPrctlModelChecker.h" #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" @@ -518,6 +519,12 @@ namespace storm { if (modelchecker.canHandle(*formula.get())) { result = modelchecker.check(*formula.get()); } + } else if (model->getType() == storm::models::ModelType::Mdp) { + std::shared_ptr> mdp = model->template as>(); + storm::modelchecker::HybridMdpPrctlModelChecker modelchecker(*mdp); + if (modelchecker.canHandle(*formula.get())) { + result = modelchecker.check(*formula.get()); + } } else { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented."); } diff --git a/src/utility/graph.h b/src/utility/graph.h index 6e950bcd2..5e55e611c 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -947,7 +947,7 @@ namespace storm { result.second = performProb1E(model, transitionMatrix, phiStates, psiStates, !result.first && model.getReachableStates()); return result; } - + template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { std::pair, storm::dd::Bdd> result;