From 72166bed37dea44ef66d44438590003b1d5f1cef Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 6 Apr 2015 19:41:46 +0200 Subject: [PATCH] Created new class for storing hybrid check results (symbolic as well as explicit parts) and the surrounding functionality. Former-commit-id: d4ad6da5a1c47ca883a65f4b9bf72018e96a526b --- .../prctl/HybridDtmcPrctlModelChecker.cpp | 17 +-- .../prctl/HybridDtmcPrctlModelChecker.h | 2 +- src/modelchecker/results/CheckResult.cpp | 21 +++ src/modelchecker/results/CheckResult.h | 9 ++ .../results/HybridQuantitativeCheckResult.cpp | 128 ++++++++++++++++++ .../results/HybridQuantitativeCheckResult.h | 69 ++++++++++ .../SymbolicQuantitativeCheckResult.cpp | 2 +- .../results/SymbolicQuantitativeCheckResult.h | 2 +- src/storage/SparseMatrix.cpp | 2 - src/storage/dd/CuddBdd.cpp | 86 +++++++++++- src/storage/dd/CuddBdd.h | 41 ++++++ src/storage/dd/CuddOdd.cpp | 52 ++++++- src/storage/dd/CuddOdd.h | 26 ++++ 13 files changed, 438 insertions(+), 19 deletions(-) create mode 100644 src/modelchecker/results/HybridQuantitativeCheckResult.cpp create mode 100644 src/modelchecker/results/HybridQuantitativeCheckResult.h diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp index b927031e0..9c959be09 100644 --- a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp @@ -7,6 +7,7 @@ #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" @@ -29,7 +30,7 @@ namespace storm { } 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) { + std::unique_ptr 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); @@ -46,7 +47,7 @@ namespace storm { // 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); + 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()) { @@ -86,17 +87,11 @@ namespace storm { solver->solveEquationSystem(x, b); // Now that we have the explicit solution of the system, we need to transform it to a symbolic representation. - STORM_LOG_DEBUG("Converting the explicit result to a symbolic form."); - storm::dd::Add numericResult(model.getManager().asSharedPointer(), x, odd, model.getRowVariables()); - - return statesWithProbability01.second.toAdd() + numericResult; + return std::unique_ptr(new storm::modelchecker::HybridQuantitativeCheckResult(model.getReachableStates(), model.getReachableStates() && !maybeStates, statesWithProbability01.second.toAdd(), maybeStates, odd, x)); } else { - return statesWithProbability01.second.toAdd(); + return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), statesWithProbability01.second.toAdd())); } } - - exit(-1); - return storm::dd::Add(); } template @@ -105,7 +100,7 @@ namespace storm { 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))); + return this->computeUntilProbabilitiesHelper(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); } template diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h index ff9e63762..bc722f57f 100644 --- a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h @@ -22,7 +22,7 @@ namespace storm { 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); + static std::unique_ptr 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; diff --git a/src/modelchecker/results/CheckResult.cpp b/src/modelchecker/results/CheckResult.cpp index b518b0667..e6f0db4aa 100644 --- a/src/modelchecker/results/CheckResult.cpp +++ b/src/modelchecker/results/CheckResult.cpp @@ -8,6 +8,7 @@ #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" +#include "src/modelchecker/results/HybridQuantitativeCheckResult.h" #include "src/utility/macros.h" #include "src/exceptions/InvalidOperationException.h" @@ -22,6 +23,10 @@ namespace storm { return false; } + bool CheckResult::isHybrid() const { + return false; + } + bool CheckResult::isQuantitative() const { return false; } @@ -55,6 +60,10 @@ namespace storm { return false; } + bool CheckResult::isHybridQuantitativeCheckResult() const { + return false; + } + ExplicitQualitativeCheckResult& CheckResult::asExplicitQualitativeCheckResult() { return dynamic_cast(*this); } @@ -108,6 +117,16 @@ namespace storm { SymbolicQuantitativeCheckResult const& CheckResult::asSymbolicQuantitativeCheckResult() const { return dynamic_cast const&>(*this); } + + template + HybridQuantitativeCheckResult& CheckResult::asHybridQuantitativeCheckResult() { + return dynamic_cast&>(*this); + } + + template + HybridQuantitativeCheckResult const& CheckResult::asHybridQuantitativeCheckResult() const { + return dynamic_cast const&>(*this); + } // Explicitly instantiate the template functions. template ExplicitQuantitativeCheckResult& CheckResult::asExplicitQuantitativeCheckResult(); @@ -116,6 +135,8 @@ namespace storm { template SymbolicQualitativeCheckResult const& CheckResult::asSymbolicQualitativeCheckResult() const; template SymbolicQuantitativeCheckResult& CheckResult::asSymbolicQuantitativeCheckResult(); template SymbolicQuantitativeCheckResult const& CheckResult::asSymbolicQuantitativeCheckResult() const; + template HybridQuantitativeCheckResult& CheckResult::asHybridQuantitativeCheckResult(); + template HybridQuantitativeCheckResult const& CheckResult::asHybridQuantitativeCheckResult() const; #ifdef STORM_HAVE_CARL template ExplicitQuantitativeCheckResult& CheckResult::asExplicitQuantitativeCheckResult(); diff --git a/src/modelchecker/results/CheckResult.h b/src/modelchecker/results/CheckResult.h index 05aefd984..93ff1399f 100644 --- a/src/modelchecker/results/CheckResult.h +++ b/src/modelchecker/results/CheckResult.h @@ -16,6 +16,7 @@ namespace storm { template class ExplicitQuantitativeCheckResult; template class SymbolicQualitativeCheckResult; template class SymbolicQuantitativeCheckResult; + template class HybridQuantitativeCheckResult; // The base class of all check results. class CheckResult { @@ -31,12 +32,14 @@ namespace storm { // Methods to retrieve the actual type of the check result. virtual bool isExplicit() const; virtual bool isSymbolic() const; + virtual bool isHybrid() const; virtual bool isQuantitative() const; virtual bool isQualitative() const; virtual bool isExplicitQualitativeCheckResult() const; virtual bool isExplicitQuantitativeCheckResult() const; virtual bool isSymbolicQualitativeCheckResult() const; virtual bool isSymbolicQuantitativeCheckResult() const; + virtual bool isHybridQuantitativeCheckResult() const; virtual bool isResultForAllStates() const; QualitativeCheckResult& asQualitativeCheckResult(); @@ -65,6 +68,12 @@ namespace storm { template SymbolicQuantitativeCheckResult const& asSymbolicQuantitativeCheckResult() const; + + template + HybridQuantitativeCheckResult& asHybridQuantitativeCheckResult(); + + template + HybridQuantitativeCheckResult const& asHybridQuantitativeCheckResult() const; virtual std::ostream& writeToStream(std::ostream& out) const = 0; }; diff --git a/src/modelchecker/results/HybridQuantitativeCheckResult.cpp b/src/modelchecker/results/HybridQuantitativeCheckResult.cpp new file mode 100644 index 000000000..f6bb4136d --- /dev/null +++ b/src/modelchecker/results/HybridQuantitativeCheckResult.cpp @@ -0,0 +1,128 @@ +#include "src/modelchecker/results/HybridQuantitativeCheckResult.h" +#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" + +#include "src/exceptions/InvalidOperationException.h" + +namespace storm { + namespace modelchecker { + template + HybridQuantitativeCheckResult::HybridQuantitativeCheckResult(storm::dd::Bdd const& reachableStates, storm::dd::Bdd const& symbolicStates, storm::dd::Add const& symbolicValues, storm::dd::Bdd const& explicitStates, storm::dd::Odd const& odd, std::vector const& explicitValues) : reachableStates(reachableStates), symbolicStates(symbolicStates), symbolicValues(symbolicValues), explicitStates(explicitStates), odd(odd), explicitValues(explicitValues) { + // Intentionally left empty. + } + + template + std::unique_ptr HybridQuantitativeCheckResult::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const { + storm::dd::Bdd symbolicResult; + + // First compute the symbolic part of the result. + if (comparisonType == storm::logic::ComparisonType::Less) { + symbolicResult = symbolicValues.less(bound); + } else if (comparisonType == storm::logic::ComparisonType::LessEqual) { + symbolicResult = symbolicValues.lessOrEqual(bound); + } else if (comparisonType == storm::logic::ComparisonType::Greater) { + symbolicResult = symbolicValues.greater(bound); + } else if (comparisonType == storm::logic::ComparisonType::GreaterEqual) { + symbolicResult = symbolicValues.greaterOrEqual(bound); + } + + // Then translate the explicit part to a symbolic format and simultaneously to a qualitative result. + symbolicResult |= storm::dd::Bdd(this->reachableStates.getDdManager(), this->explicitValues, this->odd, this->symbolicValues.getContainedMetaVariables(), comparisonType, bound); + + return std::unique_ptr>(new SymbolicQualitativeCheckResult(reachableStates, symbolicResult)); + } + + template + bool HybridQuantitativeCheckResult::isHybrid() const { + return true; + } + + template + bool HybridQuantitativeCheckResult::isResultForAllStates() const { + return true; + } + + template + bool HybridQuantitativeCheckResult::isHybridQuantitativeCheckResult() const { + return true; + } + + template + storm::dd::Bdd const& HybridQuantitativeCheckResult::getSymbolicStates() const { + return symbolicStates; + } + + template + storm::dd::Add const& HybridQuantitativeCheckResult::getSymbolicValueVector() const { + return symbolicValues; + } + + template + storm::dd::Bdd const& HybridQuantitativeCheckResult::getExplicitStates() const { + return explicitStates; + } + + template + storm::dd::Odd const& HybridQuantitativeCheckResult::getOdd() const { + return odd; + } + + template + std::vector const& HybridQuantitativeCheckResult::getExplicitValueVector() const { + return explicitValues; + } + + template + std::ostream& HybridQuantitativeCheckResult::writeToStream(std::ostream& out) const { + out << "["; + bool first = true; + if (!this->symbolicStates.isZero()) { + if (this->symbolicValues.isZero()) { + out << "0"; + } else { + for (auto valuationValuePair : this->symbolicValues) { + if (!first) { + out << ", "; + } else { + first = false; + } + out << valuationValuePair.second; + } + } + } + if (!this->explicitStates.isZero()) { + for (auto const& element : this->explicitValues) { + if (!first) { + out << ", "; + } else { + first = false; + } + out << element; + } + } + out << "]"; + return out; + } + + template + void HybridQuantitativeCheckResult::filter(QualitativeCheckResult const& filter) { + STORM_LOG_THROW(filter.isSymbolicQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot filter hybrid check result with non-symbolic filter."); + + // First, we filter the symbolic values. + this->symbolicStates = this->symbolicStates && filter.asSymbolicQualitativeCheckResult().getTruthValuesVector(); + this->symbolicValues *= symbolicStates.toAdd(); + + // Next, we filter the explicit values. + + // Start by computing the new set of states that is stored explictly and the corresponding ODD. + this->explicitStates = this->explicitStates && filter.asSymbolicQualitativeCheckResult().getTruthValuesVector(); + storm::dd::Odd newOdd(explicitStates); + + // Then compute the new vector of explicit values and set the new data fields. + this->explicitValues = this->odd.filterExplicitVector(explicitStates, this->explicitValues); + this->odd = newOdd; + } + + // Explicitly instantiate the class. + template class HybridQuantitativeCheckResult; + } +} \ No newline at end of file diff --git a/src/modelchecker/results/HybridQuantitativeCheckResult.h b/src/modelchecker/results/HybridQuantitativeCheckResult.h new file mode 100644 index 000000000..d8239f8c9 --- /dev/null +++ b/src/modelchecker/results/HybridQuantitativeCheckResult.h @@ -0,0 +1,69 @@ +#ifndef STORM_MODELCHECKER_HYBRIDQUANTITATIVECHECKRESULT_H_ +#define STORM_MODELCHECKER_HYBRIDQUANTITATIVECHECKRESULT_H_ + +#include "src/storage/dd/DdType.h" +#include "src/storage/dd/CuddAdd.h" +#include "src/storage/dd/CuddBdd.h" +#include "src/storage/dd/CuddOdd.h" +#include "src/modelchecker/results/QuantitativeCheckResult.h" +#include "src/utility/OsDetection.h" + +namespace storm { + namespace modelchecker { + template + class HybridQuantitativeCheckResult : public QuantitativeCheckResult { + public: + HybridQuantitativeCheckResult() = default; + HybridQuantitativeCheckResult(storm::dd::Bdd const& reachableStates, storm::dd::Bdd const& symbolicStates, storm::dd::Add const& symbolicValues, storm::dd::Bdd const& explicitStates, storm::dd::Odd const& odd, std::vector const& explicitValues); + + HybridQuantitativeCheckResult(HybridQuantitativeCheckResult const& other) = default; + HybridQuantitativeCheckResult& operator=(HybridQuantitativeCheckResult const& other) = default; +#ifndef WINDOWS + HybridQuantitativeCheckResult(HybridQuantitativeCheckResult&& other) = default; + HybridQuantitativeCheckResult& operator=(HybridQuantitativeCheckResult&& other) = default; +#endif + + virtual std::unique_ptr compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const override; + + virtual bool isHybrid() const override; + virtual bool isResultForAllStates() const override; + + virtual bool isHybridQuantitativeCheckResult() const override; + + storm::dd::Bdd const& getSymbolicStates() const; + + storm::dd::Add const& getSymbolicValueVector() const; + + storm::dd::Bdd const& getExplicitStates() const; + + storm::dd::Odd const& getOdd() const; + + std::vector const& getExplicitValueVector() const; + + virtual std::ostream& writeToStream(std::ostream& out) const override; + + virtual void filter(QualitativeCheckResult const& filter) override; + + private: + // The set of all reachable states. + storm::dd::Bdd reachableStates; + + // The set of all states whose result is stored symbolically. + storm::dd::Bdd symbolicStates; + + // The symbolic value vector. + storm::dd::Add symbolicValues; + + // The set of all states whose result is stored explicitly. + storm::dd::Bdd explicitStates; + + // The ODD that enables translation of the explicit values to a symbolic format. + storm::dd::Odd odd; + + // The explicit value vector. + std::vector explicitValues; + }; + } +} + +#endif /* STORM_MODELCHECKER_HYBRIDQUANTITATIVECHECKRESULT_H_ */ \ No newline at end of file diff --git a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp index fc18df5c6..088b15a63 100644 --- a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp @@ -42,7 +42,7 @@ namespace storm { } template - storm::dd::Dd const& SymbolicQuantitativeCheckResult::getValueVector() const { + storm::dd::Add const& SymbolicQuantitativeCheckResult::getValueVector() const { return values; } diff --git a/src/modelchecker/results/SymbolicQuantitativeCheckResult.h b/src/modelchecker/results/SymbolicQuantitativeCheckResult.h index ee1c172d7..5f0ba0600 100644 --- a/src/modelchecker/results/SymbolicQuantitativeCheckResult.h +++ b/src/modelchecker/results/SymbolicQuantitativeCheckResult.h @@ -28,7 +28,7 @@ namespace storm { virtual bool isSymbolicQuantitativeCheckResult() const override; - storm::dd::Dd const& getValueVector() const; + storm::dd::Add const& getValueVector() const; virtual std::ostream& writeToStream(std::ostream& out) const override; diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 9a8affbd1..880d15d82 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -730,7 +730,6 @@ namespace storm { } #endif - template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const { std::vector result(rowCount, storm::utility::zero()); @@ -755,7 +754,6 @@ namespace storm { return result; } - template void SparseMatrix::multiplyWithVector(std::vector const& vector, std::vector& result) const { #ifdef STORM_HAVE_INTELTBB diff --git a/src/storage/dd/CuddBdd.cpp b/src/storage/dd/CuddBdd.cpp index b311682f8..6d920f05d 100644 --- a/src/storage/dd/CuddBdd.cpp +++ b/src/storage/dd/CuddBdd.cpp @@ -1,8 +1,10 @@ #include #include +#include -#include "src/storage/dd/CuddBdd.h" #include "src/storage/dd/CuddAdd.h" +#include "src/storage/dd/CuddBdd.h" +#include "src/storage/dd/CuddOdd.h" #include "src/storage/dd/CuddDdManager.h" #include "src/utility/macros.h" @@ -14,6 +16,24 @@ namespace storm { // Intentionally left empty. } + Bdd::Bdd(std::shared_ptr const> ddManager, std::vector const& explicitValues, storm::dd::Odd const& odd, std::set const& metaVariables, storm::logic::ComparisonType comparisonType, double value) : Dd(ddManager, metaVariables) { + switch (comparisonType) { + case storm::logic::ComparisonType::Less: + this->cuddBdd = fromVector(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater(), value, std::placeholders::_1)); + break; + case storm::logic::ComparisonType::LessEqual: + this->cuddBdd = fromVector(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater_equal(), value, std::placeholders::_1)); + break; + case storm::logic::ComparisonType::Greater: + this->cuddBdd = fromVector(ddManager, explicitValues, odd, metaVariables, std::bind(std::less(), value, std::placeholders::_1)); + break; + case storm::logic::ComparisonType::GreaterEqual: + this->cuddBdd = fromVector(ddManager, explicitValues, odd, metaVariables, std::bind(std::less_equal(), value, std::placeholders::_1)); + break; + } + + } + Add Bdd::toAdd() const { return Add(this->getDdManager(), this->getCuddBdd().Add(), this->getContainedMetaVariables()); } @@ -253,6 +273,70 @@ namespace storm { } } + template + BDD Bdd::fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter) { + std::vector ddVariableIndices = getSortedVariableIndices(*ddManager, metaVariables); + uint_fast64_t offset = 0; + return BDD(ddManager->getCuddManager(), fromVectorRec(ddManager->getCuddManager().getManager(), offset, 0, ddVariableIndices.size(), values, odd, ddVariableIndices, filter)); + } + + template + DdNode* Bdd::fromVectorRec(::DdManager* manager, uint_fast64_t& currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector const& values, Odd const& odd, std::vector const& ddVariableIndices, std::function const& filter) { + if (currentLevel == maxLevel) { + // If we are in a terminal node of the ODD, we need to check whether the then-offset of the ODD is one + // (meaning the encoding is a valid one) or zero (meaning the encoding is not valid). Consequently, we + // need to copy the next value of the vector iff the then-offset is greater than zero. + if (odd.getThenOffset() > 0) { + if (filter(values[currentOffset++])) { + return Cudd_ReadOne(manager); + } else { + return Cudd_ReadLogicZero(manager); + } + } else { + return Cudd_ReadZero(manager); + } + } else { + // If the total offset is zero, we can just return the constant zero DD. + if (odd.getThenOffset() + odd.getElseOffset() == 0) { + return Cudd_ReadZero(manager); + } + + // Determine the new else-successor. + DdNode* elseSuccessor = nullptr; + if (odd.getElseOffset() > 0) { + elseSuccessor = fromVectorRec(manager, currentOffset, currentLevel + 1, maxLevel, values, odd.getElseSuccessor(), ddVariableIndices, filter); + } else { + elseSuccessor = Cudd_ReadLogicZero(manager); + } + Cudd_Ref(elseSuccessor); + + // Determine the new then-successor. + DdNode* thenSuccessor = nullptr; + if (odd.getThenOffset() > 0) { + thenSuccessor = fromVectorRec(manager, currentOffset, currentLevel + 1, maxLevel, values, odd.getThenSuccessor(), ddVariableIndices, filter); + } else { + thenSuccessor = Cudd_ReadLogicZero(manager); + } + Cudd_Ref(thenSuccessor); + + // Create a node representing ITE(currentVar, thenSuccessor, elseSuccessor); + DdNode* result = Cudd_bddIthVar(manager, static_cast(ddVariableIndices[currentLevel])); + Cudd_Ref(result); + DdNode* newResult = Cudd_bddIte(manager, result, thenSuccessor, elseSuccessor); + Cudd_Ref(newResult); + + // Dispose of the intermediate results + Cudd_RecursiveDeref(manager, result); + Cudd_RecursiveDeref(manager, thenSuccessor); + Cudd_RecursiveDeref(manager, elseSuccessor); + + // Before returning, we remove the protection imposed by the previous call to Cudd_Ref. + Cudd_Deref(newResult); + + return newResult; + } + } + std::ostream& operator<<(std::ostream& out, const Bdd& bdd) { bdd.exportToDot(); return out; diff --git a/src/storage/dd/CuddBdd.h b/src/storage/dd/CuddBdd.h index 7ba62cceb..1868edf2e 100644 --- a/src/storage/dd/CuddBdd.h +++ b/src/storage/dd/CuddBdd.h @@ -1,6 +1,7 @@ #ifndef STORM_STORAGE_DD_CUDDBDD_H_ #define STORM_STORAGE_DD_CUDDBDD_H_ +#include "src/logic/ComparisonType.h" #include "src/storage/dd/Bdd.h" #include "src/storage/dd/CuddDd.h" #include "src/storage/dd/CuddAdd.h" @@ -20,6 +21,18 @@ namespace storm { template<> class Bdd : public Dd { public: + /*! + * Constructs a BDD representation of all encodings that are in the requested relation with the given value. + * + * @param ddManager The DD manager responsible for the resulting BDD. + * @param explicitValues The explicit values to compare to the given value. + * @param odd The ODD used for the translation from the explicit representation to a symbolic one. + * @param metaVariables The meta variables to use for the symbolic encoding. + * @param comparisonType The relation that needs to hold for the values (wrt. to the given value). + * @param value The value to compare with. + */ + Bdd(std::shared_ptr const> ddManager, std::vector const& explicitValues, storm::dd::Odd const& odd, std::set const& metaVariables, storm::logic::ComparisonType comparisonType, double value); + // Declare the DdManager and DdIterator class as friend so it can access the internals of a DD. friend class DdManager; friend class DdForwardIterator; @@ -274,6 +287,34 @@ namespace storm { */ Bdd(std::shared_ptr const> ddManager, BDD cuddBdd, std::set const& containedMetaVariables = std::set()); + /*! + * Builds a BDD representing the values that make the given filter function evaluate to true. + * + * @param ddManager The manager responsible for the BDD. + * @param values The values that are to be checked against the filter function. + * @param odd The ODD used for the translation. + * @param metaVariables The meta variables used for the translation. + * @param filter The filter that evaluates whether an encoding is to be mapped to 0 or 1. + * @return The resulting (CUDD) BDD. + */ + template + static BDD fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter); + + /*! + * Builds a BDD representing the values that make the given filter function evaluate to true. + * + * @param manager The manager responsible for the BDD. + * @param currentOffset The current offset in the vector. + * @param currentLevel The current level in the DD. + * @param maxLevel The maximal level in the DD. + * @param values The values that are to be checked against the filter function. + * @param odd The ODD used for the translation. + * @param ddVariableIndices The (sorted) list of DD variable indices to use. + * @return The resulting (CUDD) BDD node. + */ + template + static DdNode* fromVectorRec(::DdManager* manager, uint_fast64_t& currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector const& values, Odd const& odd, std::vector const& ddVariableIndices, std::function const& filter); + // The BDD created by CUDD. BDD cuddBdd; }; diff --git a/src/storage/dd/CuddOdd.cpp b/src/storage/dd/CuddOdd.cpp index 31bc42dd6..46ed679b6 100644 --- a/src/storage/dd/CuddOdd.cpp +++ b/src/storage/dd/CuddOdd.cpp @@ -37,7 +37,7 @@ namespace storm { // Now construct the ODD structure from the BDD. std::shared_ptr> rootOdd = buildOddFromBddRec(Cudd_Regular(bdd.getCuddDdNode()), manager->getCuddManager(), 0, Cudd_IsComplement(bdd.getCuddDdNode()), ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels); - + // Finally, move the children of the root ODD into this ODD. this->elseNode = std::move(rootOdd->elseNode); this->thenNode = std::move(rootOdd->thenNode); @@ -95,6 +95,54 @@ namespace storm { return this->elseNode == nullptr && this->thenNode == nullptr; } + std::vector Odd::filterExplicitVector(storm::dd::Bdd const& selectedValues, std::vector const& values) const { + std::vector result(selectedValues.getNonZeroCount()); + + // First, we need to determine the involved DD variables indices. + std::vector ddVariableIndices = selectedValues.getSortedVariableIndices(); + + uint_fast64_t currentIndex = 0; + addSelectedValuesToVectorRec(selectedValues.getCuddDdNode(), selectedValues.getDdManager()->getCuddManager(), 0, Cudd_IsComplement(selectedValues.getCuddDdNode()), ddVariableIndices.size(), ddVariableIndices, 0, *this, result, currentIndex, values); + return result; + } + + void Odd::addSelectedValuesToVectorRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd const& odd, std::vector& result, uint_fast64_t& currentIndex, std::vector const& values) { + // If there are no more values to select, we can directly return. + if (dd == Cudd_ReadLogicZero(manager.getManager()) && !complement) { + return; + } else if (dd == Cudd_ReadOne(manager.getManager()) && complement) { + return; + } + + if (currentLevel == maxLevel) { + // If the DD is not the zero leaf, then the then-offset is 1. + bool selected = false; + if (dd != Cudd_ReadLogicZero(manager.getManager())) { + selected = !complement; + } + + if (selected) { + result[currentIndex++] = values[currentOffset]; + } + } else if (ddVariableIndices[currentLevel] < dd->index) { + // If we skipped a level, we need to enumerate the explicit entries for the case in which the bit is set + // and for the one in which it is not set. + addSelectedValuesToVectorRec(dd, manager, currentLevel + 1, complement, maxLevel, ddVariableIndices, currentOffset, odd.getElseSuccessor(), result, currentIndex, values); + addSelectedValuesToVectorRec(dd, manager, currentLevel + 1, complement, maxLevel, ddVariableIndices, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), result, currentIndex, values); + } else { + // Otherwise, we compute the ODDs for both the then- and else successors. + DdNode* thenDdNode = Cudd_T(dd); + DdNode* elseDdNode = Cudd_E(dd); + + // Determine whether we have to evaluate the successors as if they were complemented. + bool elseComplemented = Cudd_IsComplement(elseDdNode) ^ complement; + bool thenComplemented = Cudd_IsComplement(thenDdNode) ^ complement; + + addSelectedValuesToVectorRec(Cudd_Regular(elseDdNode), manager, currentLevel + 1, elseComplemented, maxLevel, ddVariableIndices, currentOffset, odd.getElseSuccessor(), result, currentIndex, values); + addSelectedValuesToVectorRec(Cudd_Regular(thenDdNode), manager, currentLevel + 1, thenComplemented, maxLevel, ddVariableIndices, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), result, currentIndex, values); + } + } + std::shared_ptr> Odd::buildOddFromAddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector>>>& uniqueTableForLevels) { // Check whether the ODD for this node has already been computed (for this level) and if so, return this instead. auto const& iterator = uniqueTableForLevels[currentLevel].find(dd); @@ -140,7 +188,7 @@ namespace storm { boost::hash_combine(result, key.second); return result; } - + std::shared_ptr> Odd::buildOddFromBddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector, std::shared_ptr>, HashFunctor>>& uniqueTableForLevels) { // Check whether the ODD for this node has already been computed (for this level) and if so, return this instead. auto const& iterator = uniqueTableForLevels[currentLevel].find(std::make_pair(dd, complement)); diff --git a/src/storage/dd/CuddOdd.h b/src/storage/dd/CuddOdd.h index 9269e4ab1..4a03a3c26 100644 --- a/src/storage/dd/CuddOdd.h +++ b/src/storage/dd/CuddOdd.h @@ -103,6 +103,15 @@ namespace storm { */ bool isTerminalNode() const; + /*! + * Filters the given explicit vector using the symbolic representation of which values to select. + * + * @param selectedValues A symbolic representation of which values to select. + * @param values The value vector from which to select the values. + * @return The resulting vector. + */ + std::vector filterExplicitVector(storm::dd::Bdd const& selectedValues, std::vector const& values) const; + private: // Declare a hash functor that is used for the unique tables in the construction process. class HashFunctor { @@ -150,6 +159,23 @@ namespace storm { */ static std::shared_ptr> buildOddFromBddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector, std::shared_ptr>, HashFunctor>>& uniqueTableForLevels); + + /*! + * Adds the selected values the target vector. + * + * @param dd The current node of the DD representing the selected values. + * @param manager The manager responsible for the DD. + * @param currentLevel The currently considered level in the DD. + * @param maxLevel The number of levels that need to be considered. + * @param ddVariableIndices The sorted list of variable indices to use. + * @param currentOffset The offset along the path taken in the DD representing the selected values. + * @param odd The current ODD node. + * @param result The target vector to which to write the values. + * @param currentIndex The index at which the next element is to be written. + * @param values The value vector from which to select the values. + */ + static void addSelectedValuesToVectorRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd const& odd, std::vector& result, uint_fast64_t& currentIndex, std::vector const& values); + // The then- and else-nodes. std::shared_ptr> elseNode; std::shared_ptr> thenNode;