From 06bfc17ec6f038e9593560bb0f1a7ef098163d6f Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 2 Apr 2015 17:06:29 +0200 Subject: [PATCH] Started making hybrid (dd/sparse) model checking work. Former-commit-id: 23fac3a67254b486aafe52709de494eefe869abd --- .../prctl/HybridDtmcPrctlModelChecker.cpp | 110 ++++++++++++++++++ .../prctl/HybridDtmcPrctlModelChecker.h | 34 ++++++ .../SymbolicPropositionalModelChecker.h | 1 - .../SymbolicQualitativeCheckResult.cpp | 10 +- .../results/SymbolicQualitativeCheckResult.h | 8 +- .../SymbolicQuantitativeCheckResult.cpp | 26 +++-- .../results/SymbolicQuantitativeCheckResult.h | 6 +- src/models/symbolic/Model.cpp | 10 ++ src/models/symbolic/Model.h | 7 ++ src/settings/modules/GeneralSettings.cpp | 8 +- src/settings/modules/GeneralSettings.h | 2 +- src/storage/dd/CuddAdd.cpp | 8 ++ src/storage/dd/CuddAdd.h | 18 +++ src/utility/cli.h | 55 +++++++-- src/utility/graph.h | 22 +++- 15 files changed, 288 insertions(+), 37 deletions(-) create mode 100644 src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp create mode 100644 src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp new file mode 100644 index 000000000..d71d206a4 --- /dev/null +++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp @@ -0,0 +1,110 @@ +#include "src/modelchecker/prctl/HybridDtmcPrctlModelChecker.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/exceptions/InvalidStateException.h" +#include "src/exceptions/InvalidPropertyException.h" + +namespace storm { + namespace modelchecker { + template + HybridDtmcPrctlModelChecker::HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc const& model, std::unique_ptr>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { + // Intentionally left empty. + } + + template + HybridDtmcPrctlModelChecker::HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc const& model) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(new storm::utility::solver::LinearEquationSolverFactory()) { + // Intentionally left empty. + } + + template + bool HybridDtmcPrctlModelChecker::canHandle(storm::logic::Formula const& formula) const { + return formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula(); + } + + template + storm::dd::Add HybridDtmcPrctlModelChecker::computeUntilProbabilitiesHelper(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory 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 = storm::utility::graph::performProb01(model, transitionMatrix, phiStates, psiStates); + storm::dd::Bdd maybeStates = !statesWithProbability01.first && !statesWithProbability01.second && model.getReachableStates(); + + // Create the ODD for the translation between symbolic and explicit storage. + storm::dd::Odd odd(maybeStates); + + // 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 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 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(odd, odd); + std::vector b = subvector.template toVector(odd); + + std::unique_ptr> solver = linearEquationSolverFactory.create(explicitSubmatrix); + solver->solveEquationSystem(x, b); + + // Now that we have the explicit solution of the system, we need to transform it to a symbolic representation. + storm::dd::Add numericResult; // = storm::dd::Add(x, odd); + return statesWithProbability01.second.toAdd() + numericResult; + } else { + return statesWithProbability01.second.toAdd(); + } + } + + exit(-1); + return storm::dd::Add(); + } + + template + std::unique_ptr HybridDtmcPrctlModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + 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 std::unique_ptr(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), this->computeUntilProbabilitiesHelper(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory))); + } + + template + storm::models::symbolic::Dtmc const& HybridDtmcPrctlModelChecker::getModel() const { + return this->template getModelAs>(); + } + + template class HybridDtmcPrctlModelChecker; + } +} \ No newline at end of file diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h new file mode 100644 index 000000000..ff9e63762 --- /dev/null +++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h @@ -0,0 +1,34 @@ +#ifndef STORM_MODELCHECKER_HYBRIDDTMCPRCTLMODELCHECKER_H_ +#define STORM_MODELCHECKER_HYBRIDDTMCPRCTLMODELCHECKER_H_ + +#include "src/modelchecker/propositional/SymbolicPropositionalModelChecker.h" +#include "src/models/symbolic/Dtmc.h" +#include "src/utility/solver.h" + +namespace storm { + namespace modelchecker { + template + class HybridDtmcPrctlModelChecker : public SymbolicPropositionalModelChecker { + public: + explicit HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc const& model); + explicit HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc 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 computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + + protected: + storm::models::symbolic::Dtmc const& getModel() const override; + + private: + // The methods that perform the actual checking. + static storm::dd::Add computeUntilProbabilitiesHelper(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + // An object that is used for retrieving linear equation solvers. + std::unique_ptr> linearEquationSolverFactory; + }; + + } // namespace modelchecker +} // namespace storm + +#endif /* STORM_MODELCHECKER_HYBRIDDTMCPRCTLMODELCHECKER_H_ */ diff --git a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h index 9865d74b3..96dcea601 100644 --- a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h +++ b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h @@ -2,7 +2,6 @@ #define STORM_MODELCHECKER_SYMBOLICPROPOSITIONALMODELCHECKER_H_ #include "src/modelchecker/AbstractModelChecker.h" - #include "src/models/symbolic/Model.h" namespace storm { diff --git a/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp b/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp index 766e2674f..f2cdf8553 100644 --- a/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp +++ b/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp @@ -6,7 +6,7 @@ namespace storm { namespace modelchecker { template - SymbolicQualitativeCheckResult::SymbolicQualitativeCheckResult(storm::dd::Bdd const& allStates, storm::dd::Bdd const& truthValues) : allStates(allStates), truthValues(truthValues) { + SymbolicQualitativeCheckResult::SymbolicQualitativeCheckResult(storm::dd::Bdd const& reachableStates, storm::dd::Bdd const& truthValues) : reachableStates(reachableStates), truthValues(truthValues) { // Intentionally left empty. } @@ -29,21 +29,23 @@ namespace storm { QualitativeCheckResult& SymbolicQualitativeCheckResult::operator&=(QualitativeCheckResult const& other) { STORM_LOG_THROW(other.isSymbolicQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot perform logical 'and' on check results of incompatible type."); this->truthValues &= other.asSymbolicQualitativeCheckResult().getTruthValuesVector(); + return *this; } template QualitativeCheckResult& SymbolicQualitativeCheckResult::operator|=(QualitativeCheckResult const& other) { STORM_LOG_THROW(other.isSymbolicQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot perform logical 'and' on check results of incompatible type."); this->truthValues |= other.asSymbolicQualitativeCheckResult().getTruthValuesVector(); + return *this; } template void SymbolicQualitativeCheckResult::complement() { - this->truthValues = !this->truthValues && allStates; + this->truthValues = !this->truthValues && reachableStates; } template - storm::dd::Dd const& SymbolicQualitativeCheckResult::getTruthValuesVector() const { + storm::dd::Bdd const& SymbolicQualitativeCheckResult::getTruthValuesVector() const { return truthValues; } @@ -62,5 +64,7 @@ namespace storm { STORM_LOG_THROW(filter.isSymbolicQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot filter symbolic check result with non-symbolic filter."); this->truthValues &= filter.asSymbolicQualitativeCheckResult().getTruthValuesVector(); } + + template class SymbolicQualitativeCheckResult; } } \ No newline at end of file diff --git a/src/modelchecker/results/SymbolicQualitativeCheckResult.h b/src/modelchecker/results/SymbolicQualitativeCheckResult.h index e0c70ead3..88d7a8ac2 100644 --- a/src/modelchecker/results/SymbolicQualitativeCheckResult.h +++ b/src/modelchecker/results/SymbolicQualitativeCheckResult.h @@ -12,7 +12,7 @@ namespace storm { class SymbolicQualitativeCheckResult : public QualitativeCheckResult { public: SymbolicQualitativeCheckResult() = default; - SymbolicQualitativeCheckResult(storm::dd::Bdd const& allStates, storm::dd::Bdd const& truthValues); + SymbolicQualitativeCheckResult(storm::dd::Bdd const& reachableStates, storm::dd::Bdd const& truthValues); SymbolicQualitativeCheckResult(SymbolicQualitativeCheckResult const& other) = default; SymbolicQualitativeCheckResult& operator=(SymbolicQualitativeCheckResult const& other) = default; @@ -30,15 +30,15 @@ namespace storm { virtual QualitativeCheckResult& operator|=(QualitativeCheckResult const& other) override; virtual void complement() override; - storm::dd::Dd const& getTruthValuesVector() const; + storm::dd::Bdd const& getTruthValuesVector() const; virtual std::ostream& writeToStream(std::ostream& out) const override; virtual void filter(QualitativeCheckResult const& filter) override; private: - // The set of all states. - storm::dd::Bdd allStates; + // The set of all reachable states. + storm::dd::Bdd reachableStates; // The values of the qualitative check result. storm::dd::Bdd truthValues; diff --git a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp index 50d7d0ac7..c265efd5c 100644 --- a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp @@ -7,22 +7,23 @@ namespace storm { namespace modelchecker { template - SymbolicQuantitativeCheckResult::SymbolicQuantitativeCheckResult(storm::dd::Add const& allStates, storm::dd::Add const& values) : allStates(allStates), values(values) { + SymbolicQuantitativeCheckResult::SymbolicQuantitativeCheckResult(storm::dd::Bdd const& reachableStates, storm::dd::Add const& values) : reachableStates(reachableStates), values(values) { // Intentionally left empty. } template std::unique_ptr SymbolicQuantitativeCheckResult::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const { - std::unique_ptr> result; - if (comparisonType == storm::logic::ComparisonType::Less || comparisonType == storm::logic::ComparisonType::GreaterEqual) { - result = std::unique_ptr>(new SymbolicQualitativeCheckResult(allStates, values.greaterOrEqual(bound))); - } else { - result = std::unique_ptr>(new SymbolicQualitativeCheckResult(allStates, values.greater(bound))); + storm::dd::Bdd states; + if (comparisonType == storm::logic::ComparisonType::Less) { + states = values.less(bound); + } else if (comparisonType == storm::logic::ComparisonType::LessEqual) { + states = values.lessOrEqual(bound); + } else if (comparisonType == storm::logic::ComparisonType::Greater) { + states = values.greater(bound); + } else if (comparisonType == storm::logic::ComparisonType::GreaterEqual) { + states = values.greaterOrEqual(bound); } - if (comparisonType == storm::logic::ComparisonType::Less || comparisonType == storm::logic::ComparisonType::LessEqual) { - result->complement(); - } - return result; + return std::unique_ptr>(new SymbolicQualitativeCheckResult(reachableStates, values.greaterOrEqual(bound)));; } template @@ -64,7 +65,10 @@ namespace storm { template void SymbolicQuantitativeCheckResult::filter(QualitativeCheckResult const& filter) { STORM_LOG_THROW(filter.isSymbolicQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot filter symbolic check result with non-symbolic filter."); - this->truthValues *= filter.asSymbolicQualitativeCheckResult().getTruthValuesVector().toMtbdd(); + this->values *= filter.asSymbolicQualitativeCheckResult().getTruthValuesVector().toAdd(); } + + // Explicitly instantiate the class. + template class SymbolicQuantitativeCheckResult; } } \ No newline at end of file diff --git a/src/modelchecker/results/SymbolicQuantitativeCheckResult.h b/src/modelchecker/results/SymbolicQuantitativeCheckResult.h index 28490aed2..ee1c172d7 100644 --- a/src/modelchecker/results/SymbolicQuantitativeCheckResult.h +++ b/src/modelchecker/results/SymbolicQuantitativeCheckResult.h @@ -12,7 +12,7 @@ namespace storm { class SymbolicQuantitativeCheckResult : public QuantitativeCheckResult { public: SymbolicQuantitativeCheckResult() = default; - SymbolicQuantitativeCheckResult(storm::dd::Add const& allStates, storm::dd::Add const& values); + SymbolicQuantitativeCheckResult(storm::dd::Bdd const& reachableStates, storm::dd::Add const& values); SymbolicQuantitativeCheckResult(SymbolicQuantitativeCheckResult const& other) = default; SymbolicQuantitativeCheckResult& operator=(SymbolicQuantitativeCheckResult const& other) = default; @@ -35,8 +35,8 @@ namespace storm { virtual void filter(QualitativeCheckResult const& filter) override; private: - // The set of all states. - storm::dd::Add allStates; + // The set of all reachable states. + storm::dd::Bdd reachableStates; // The values of the quantitative check result. storm::dd::Add values; diff --git a/src/models/symbolic/Model.cpp b/src/models/symbolic/Model.cpp index 07b9fda9f..0fe4f0d13 100644 --- a/src/models/symbolic/Model.cpp +++ b/src/models/symbolic/Model.cpp @@ -132,6 +132,16 @@ namespace storm { return labelToExpressionMap; } + template + storm::dd::Add Model::getRowColumnIdentity() const { + storm::dd::Add result = this->getManager().getAddOne(); + for (auto const& pair : this->getRowColumnMetaVariablePairs()) { + result *= this->getManager().getIdentity(pair.first).equals(this->getManager().getIdentity(pair.second)); + result *= this->getManager().getRange(pair.first).toAdd() * this->getManager().getRange(pair.second).toAdd(); + } + return result; + } + template void Model::printModelInformationToStream(std::ostream& out) const { out << "-------------------------------------------------------------- " << std::endl; diff --git a/src/models/symbolic/Model.h b/src/models/symbolic/Model.h index d9bf5eb02..211a4cc66 100644 --- a/src/models/symbolic/Model.h +++ b/src/models/symbolic/Model.h @@ -193,6 +193,13 @@ namespace storm { */ std::vector> const& getRowColumnMetaVariablePairs() const; + /*! + * Retrieves an ADD that represents the diagonal of the transition matrix. + * + * @return An ADD that represents the diagonal of the transition matrix. + */ + storm::dd::Add getRowColumnIdentity() const; + virtual std::size_t getSizeInBytes() const override; virtual void printModelInformationToStream(std::ostream& out) const override; diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp index 2d2d48eee..bd2e03a47 100644 --- a/src/settings/modules/GeneralSettings.cpp +++ b/src/settings/modules/GeneralSettings.cpp @@ -82,9 +82,9 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the state rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, dontFixDeadlockOptionName, false, "If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(dontFixDeadlockOptionShortName).build()); - std::vector engines = {"sparse", "dd"}; + std::vector engines = {"sparse", "hybrid", "dd"}; this->addOption(storm::settings::OptionBuilder(moduleName, engineOptionName, false, "Sets which engine is used for model building and model checking.").setShortName(engineOptionShortName) - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use. Available are {sparse, dd}.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(engines)).setDefaultValueString("sparse").build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use. Available are {sparse, hybrid, dd}.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(engines)).setDefaultValueString("sparse").build()).build()); std::vector linearEquationSolver = {"gmm++", "native"}; this->addOption(storm::settings::OptionBuilder(moduleName, eqSolverOptionName, false, "Sets which solver is preferred for solving systems of linear equations.") @@ -274,6 +274,8 @@ namespace storm { std::string engine = this->getOption(engineOptionName).getArgumentByName("name").getValueAsString(); if (engine == "sparse") { return GeneralSettings::Engine::Sparse; + } else if (engine == "hybrid") { + return GeneralSettings::Engine::Hybrid; } else if (engine == "dd") { return GeneralSettings::Engine::Dd; } @@ -298,7 +300,7 @@ namespace storm { uint_fast64_t propertySources = 0 + (isPropertySet() ? 1 : 0) + (isPropertyFileSet() ? 1 : 0); STORM_LOG_THROW(propertySources <= 1, storm::exceptions::InvalidSettingsException, "Please specify either a file that contains the properties or a property on the command line, but not both."); - STORM_LOG_THROW(this->getEngine() != Engine::Dd || !isExplicitSet(), storm::exceptions::InvalidSettingsException, "Decision-diagram engine can only be used with symbolic input models."); + STORM_LOG_THROW(this->getEngine() == Engine::Sparse || !isExplicitSet(), storm::exceptions::InvalidSettingsException, "Cannot use explicit input models with this engine."); return true; } diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h index 8cab2e14f..e4528f64f 100644 --- a/src/settings/modules/GeneralSettings.h +++ b/src/settings/modules/GeneralSettings.h @@ -14,7 +14,7 @@ namespace storm { class GeneralSettings : public ModuleSettings { public: // An enumeration of all engines. - enum class Engine { Sparse, Dd }; + enum class Engine { Sparse, Hybrid, Dd }; // An enumeration of all available LP solvers. enum class LpSolver { Gurobi, glpk }; diff --git a/src/storage/dd/CuddAdd.cpp b/src/storage/dd/CuddAdd.cpp index 9fb267d7e..72787075b 100644 --- a/src/storage/dd/CuddAdd.cpp +++ b/src/storage/dd/CuddAdd.cpp @@ -300,6 +300,14 @@ namespace storm { return Bdd(this->getDdManager(), this->getCuddAdd().BddThreshold(value), this->getContainedMetaVariables()); } + Bdd Add::less(double value) const { + return Bdd(this->getDdManager(), ~this->getCuddAdd().BddThreshold(value), this->getContainedMetaVariables()); + } + + Bdd Add::lessOrEqual(double value) const { + return Bdd(this->getDdManager(), ~this->getCuddAdd().BddStrictThreshold(value), this->getContainedMetaVariables()); + } + Bdd Add::notZero() const { return this->toBdd(); } diff --git a/src/storage/dd/CuddAdd.h b/src/storage/dd/CuddAdd.h index 02142705e..07cfcc20e 100644 --- a/src/storage/dd/CuddAdd.h +++ b/src/storage/dd/CuddAdd.h @@ -337,6 +337,24 @@ namespace storm { */ Bdd greaterOrEqual(double value) const; + /*! + * Computes a BDD that represents the function in which all assignments with a function value strictly + * lower than the given value are mapped to one and all others to zero. + * + * @param value The value used for the comparison. + * @return The resulting BDD. + */ + Bdd less(double value) const; + + /*! + * Computes a BDD that represents the function in which all assignments with a function value less or equal + * to the given value are mapped to one and all others to zero. + * + * @param value The value used for the comparison. + * @return The resulting BDD. + */ + Bdd lessOrEqual(double value) const; + /*! * Computes a BDD that represents the function in which all assignments with a function value unequal to * zero are mapped to one and all others to zero. diff --git a/src/utility/cli.h b/src/utility/cli.h index 402e96552..202786ba2 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -67,6 +67,9 @@ log4cplus::Logger printer; #include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "src/modelchecker/csl/SparseCtmcCslModelChecker.h" +#include "src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h" +#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" // Headers for counterexample generation. #include "src/counterexamples/MILPMinimalLabelSetGenerator.h" @@ -77,6 +80,7 @@ log4cplus::Logger printer; #include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/InvalidSettingsException.h" #include "src/exceptions/InvalidTypeException.h" +#include "src/exceptions/NotImplementedException.h" namespace storm { namespace utility { @@ -331,7 +335,7 @@ namespace storm { } result = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); - } else if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Dd) { + } else if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Dd || settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) { typename storm::builder::DdPrismModelBuilder::Options options; if (formula) { options = typename storm::builder::DdPrismModelBuilder::Options(*formula.get()); @@ -409,26 +413,24 @@ namespace storm { // If we were requested to generate a counterexample, we now do so. if (settings.isCounterexampleSet()) { - STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException, "Counterexample generation is only available for sparse models."); STORM_LOG_THROW(program, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for non-symbolic model."); generateCounterexample(program.get(), model, formula); } else { - std::shared_ptr> sparseModel = model->template as>(); std::cout << std::endl << "Model checking property: " << *formula << " ..."; std::unique_ptr result; if (model->getType() == storm::models::ModelType::Dtmc) { - std::shared_ptr> dtmc = sparseModel->template as>(); - storm::modelchecker::SparseDtmcEliminationModelChecker modelchecker(*dtmc); + std::shared_ptr> dtmc = model->template as>(); + storm::modelchecker::SparseDtmcPrctlModelChecker modelchecker(*dtmc); if (modelchecker.canHandle(*formula.get())) { result = modelchecker.check(*formula.get()); } else { - storm::modelchecker::SparseDtmcPrctlModelChecker modelchecker2(*dtmc); + storm::modelchecker::SparseDtmcEliminationModelChecker modelchecker2(*dtmc); if (modelchecker2.canHandle(*formula.get())) { modelchecker2.check(*formula.get()); } } } else if (model->getType() == storm::models::ModelType::Mdp) { - std::shared_ptr> mdp = sparseModel->template as>(); + std::shared_ptr> mdp = model->template as>(); #ifdef STORM_HAVE_CUDA if (settings.isCudaSet()) { storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker modelchecker(*mdp); @@ -442,7 +444,7 @@ namespace storm { result = modelchecker.check(*formula.get()); #endif } else if (model->getType() == storm::models::ModelType::Ctmc) { - std::shared_ptr> ctmc = sparseModel->template as>(); + std::shared_ptr> ctmc = model->template as>(); storm::modelchecker::SparseCtmcCslModelChecker modelchecker(*ctmc); result = modelchecker.check(*formula.get()); @@ -451,7 +453,7 @@ namespace storm { if (result) { std::cout << " done." << std::endl; std::cout << "Result (initial states): "; - result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(sparseModel->getInitialStates())); + result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); std::cout << *result << std::endl; } else { std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; @@ -489,6 +491,32 @@ namespace storm { } #endif + template + void verifySymbolicModel(boost::optional const& program, std::shared_ptr> model, std::shared_ptr formula) { + storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); + + std::cout << std::endl << "Model checking property: " << *formula << " ..."; + std::unique_ptr result; + if (model->getType() == storm::models::ModelType::Dtmc) { + std::shared_ptr> dtmc = model->template as>(); + storm::modelchecker::HybridDtmcPrctlModelChecker modelchecker(*dtmc); + if (modelchecker.canHandle(*formula.get())) { + modelchecker.check(*formula.get()); + } + } else { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented."); + } + + if (result) { + std::cout << " done." << std::endl; + std::cout << "Result (initial states): "; + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + std::cout << *result << std::endl; + } else { + std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; + } + } + template void buildAndCheckSymbolicModel(boost::optional const& program, boost::optional> formula) { // Now we are ready to actually build the model. @@ -507,8 +535,15 @@ namespace storm { if (formula) { if (model->isSparseModel()) { verifySparseModel(program, model->as>(), formula.get()); + } else if (model->isSymbolicModel()) { + if (storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) { + verifySymbolicModel(program, model->as>(), formula.get()); + } else { + // Not handled yet. + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented."); + } } else { - // Not handled yet. + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type."); } } } diff --git a/src/utility/graph.h b/src/utility/graph.h index 13d30f34f..a49d9a2a7 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -264,7 +264,7 @@ namespace storm { * @return All states with positive probability. */ template - storm::dd::Bdd performProbGreater0(storm::models::symbolic::DeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { + storm::dd::Bdd performProbGreater0(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { // Initialize environment for backward search. storm::dd::DdManager const& manager = model.getManager(); storm::dd::Bdd lastIterationStates = manager.getBddZero(); @@ -303,6 +303,26 @@ namespace storm { return result; } + /*! + * Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a + * deterministic model. + * + * @param model The (symbolic) model for which to compute the set of states. This is used for retrieving the + * manager and information about the meta variables. + * @param phiStates The BDD containing all phi states of the model. + * @param psiStates The BDD containing all psi states of the model. + * @return A pair of BDDs that represent all states with probability 0 and 1, respectively. + */ + template + static std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { + std::pair, storm::dd::Bdd> result; + storm::dd::Bdd transitionMatrixBdd = transitionMatrix.notZero(); + result.first = performProbGreater0(model, transitionMatrixBdd, phiStates, psiStates); + result.second = !performProbGreater0(model, transitionMatrixBdd, !psiStates && model.getReachableStates(), !result.first && model.getReachableStates()) && model.getReachableStates(); + result.first = !result.first && model.getReachableStates(); + return result; + } + /*! * Computes the sets of states that have probability greater 0 of satisfying phi until psi under at least * one possible resolution of non-determinism in a non-deterministic model. Stated differently,