From 3556743d7ea953f806366bb59f5765ed5732455c Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 1 Dec 2015 19:40:37 +0100 Subject: [PATCH] more work on introducing relation products Former-commit-id: 6b78fa09d228f812871e823f12dfbb4b6c70af60 --- src/builder/DdPrismModelBuilder.cpp | 2 +- src/storage/dd/Bdd.cpp | 21 +++++++++++++++++-- src/storage/dd/Bdd.h | 19 ++++++++++++++--- src/storage/dd/cudd/InternalCuddBdd.cpp | 20 +++++++++++++++++- src/storage/dd/cudd/InternalCuddBdd.h | 11 +++++++++- src/storage/dd/sylvan/InternalSylvanBdd.cpp | 11 +++++++++- src/storage/dd/sylvan/InternalSylvanBdd.h | 9 ++++++++ .../dd/sylvan/InternalSylvanDdManager.cpp | 5 ++++- 8 files changed, 88 insertions(+), 10 deletions(-) diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index aa55fbcbd..e2c12baa2 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -1174,7 +1174,7 @@ namespace storm { do { STORM_LOG_TRACE("Iteration " << iteration << " of reachability analysis."); changed = false; - storm::dd::Bdd tmp = reachableStates.relationalProduct(transitionBdd, generationInfo.rowMetaVariables); + storm::dd::Bdd tmp = reachableStates.relationalProduct(transitionBdd, generationInfo.rowMetaVariables, generationInfo.columnMetaVariables); storm::dd::Bdd newReachableStates = tmp && (!reachableStates); // Check whether new states were indeed discovered. diff --git a/src/storage/dd/Bdd.cpp b/src/storage/dd/Bdd.cpp index c37b3b223..ad6fe77f2 100644 --- a/src/storage/dd/Bdd.cpp +++ b/src/storage/dd/Bdd.cpp @@ -143,10 +143,10 @@ namespace storm { } template - Bdd Bdd::relationalProduct(Bdd const& relation, std::set const& rowMetaVariables) const { + Bdd Bdd::relationalProduct(Bdd const& relation, std::set const& rowMetaVariables, std::set const& columnMetaVariables) const { std::set tmpMetaVariables = Dd::joinMetaVariables(*this, relation); std::set newMetaVariables; - std::set_difference(tmpMetaVariables.begin(), tmpMetaVariables.end(), rowMetaVariables.begin(), rowMetaVariables.end(), std::inserter(newMetaVariables, newMetaVariables.begin())); + std::set_difference(tmpMetaVariables.begin(), tmpMetaVariables.end(), columnMetaVariables.begin(), columnMetaVariables.end(), std::inserter(newMetaVariables, newMetaVariables.begin())); std::vector> rowVariables; for (auto const& metaVariable : rowMetaVariables) { @@ -159,6 +159,23 @@ namespace storm { return Bdd(this->getDdManager(), internalBdd.relationalProduct(relation, rowVariables), newMetaVariables); } + template + Bdd Bdd::inverseRelationalProduct(Bdd const& relation, std::set const& rowMetaVariables, std::set const& columnMetaVariables) const { + std::set tmpMetaVariables = Dd::joinMetaVariables(*this, relation); + std::set newMetaVariables; + std::set_difference(tmpMetaVariables.begin(), tmpMetaVariables.end(), rowMetaVariables.begin(), rowMetaVariables.end(), std::inserter(newMetaVariables, newMetaVariables.begin())); + + std::vector> columnVariables; + for (auto const& metaVariable : columnMetaVariables) { + DdMetaVariable const& variable = this->getDdManager()->getMetaVariable(metaVariable); + for (auto const& ddVariable : variable.getDdVariables()) { + columnVariables.push_back(ddVariable); + } + } + + return Bdd(this->getDdManager(), internalBdd.inverseRelationalProduct(relation, columnVariables), newMetaVariables); + } + template Bdd Bdd::swapVariables(std::vector> const& metaVariablePairs) const { std::set newContainedMetaVariables; diff --git a/src/storage/dd/Bdd.h b/src/storage/dd/Bdd.h index 3ce2b295a..95a801bee 100644 --- a/src/storage/dd/Bdd.h +++ b/src/storage/dd/Bdd.h @@ -187,13 +187,26 @@ namespace storm { Bdd restrict(Bdd const& constraint) const; /*! - * Computes the relational product of the current BDD and the given BDD representing a relation. + * Computes the relational product of the current BDD and the given BDD representing a relation. Note that + * this operation assumes that the row and column variables are interleaved. * * @param relation The relation to use. * @param rowMetaVariables The row meta variables used in the relation. - * @return The ralational product. + * @param columnMetaVariables The row meta variables used in the relation. + * @return The relational product. */ - Bdd relationalProduct(Bdd const& relation, std::set const& rowMetaVariables) const; + Bdd relationalProduct(Bdd const& relation, std::set const& rowMetaVariables, std::set const& columnMetaVariables) const; + + /*! + * Computes the inverse relational product of the current BDD and the given BDD representing a relation. + * Note that this operation assumes that the row and column variables are interleaved. + * + * @param relation The relation to use. + * @param rowMetaVariables The row meta variables used in the relation. + * @param columnMetaVariables The row meta variables used in the relation. + * @return The inverse relational product. + */ + Bdd inverseRelationalProduct(Bdd const& relation, std::set const& rowMetaVariables, std::set const& columnMetaVariables) const; /*! * Swaps the given pairs of meta variables in the BDD. The pairs of meta variables must be guaranteed to have diff --git a/src/storage/dd/cudd/InternalCuddBdd.cpp b/src/storage/dd/cudd/InternalCuddBdd.cpp index 21250df39..36d99d5cf 100644 --- a/src/storage/dd/cudd/InternalCuddBdd.cpp +++ b/src/storage/dd/cudd/InternalCuddBdd.cpp @@ -37,7 +37,7 @@ namespace storm { InternalBdd result = this->andExists(relation, cube); - // Create the corresponding "from" vector for the variable swap. + // Create the corresponding column variable vector for the variable swap. std::vector> columnVariables; for (auto const& variable : rowVariables) { columnVariables.push_back(InternalBdd(ddManager, ddManager->getCuddManager().bddVar(variable.getIndex() + 1))); @@ -47,6 +47,24 @@ namespace storm { return result; } + InternalBdd InternalBdd::inverseRelationalProduct(InternalBdd const& relation, std::vector> const& columnVariables) const { + InternalBdd cube = ddManager->getBddOne(); + for (auto const& variable : columnVariables) { + cube &= variable; + } + + InternalBdd result = this->andExists(relation, cube); + + // Create the corresponding column variable vector for the variable swap. + std::vector> rowVariables; + for (auto const& variable : rowVariables) { + rowVariables.push_back(InternalBdd(ddManager, ddManager->getCuddManager().bddVar(variable.getIndex() - 1))); + } + result = result.swapVariables(rowVariables, columnVariables); + + return result; + } + InternalBdd InternalBdd::ite(InternalBdd const& thenDd, InternalBdd const& elseDd) const { return InternalBdd(ddManager, this->getCuddBdd().Ite(thenDd.getCuddBdd(), elseDd.getCuddBdd())); } diff --git a/src/storage/dd/cudd/InternalCuddBdd.h b/src/storage/dd/cudd/InternalCuddBdd.h index 8a904424f..2c8951aba 100644 --- a/src/storage/dd/cudd/InternalCuddBdd.h +++ b/src/storage/dd/cudd/InternalCuddBdd.h @@ -84,7 +84,16 @@ namespace storm { * @return The ralational product. */ InternalBdd relationalProduct(InternalBdd const& relation, std::vector> const& rowVariables) const; - + + /*! + * Computes the inverse relational product of the current BDD and the given BDD representing a relation. + * + * @param relation The relation to use. + * @param columnVariables The row variables of the relation represented as individual BDDs. + * @return The ralational product. + */ + InternalBdd inverseRelationalProduct(InternalBdd const& relation, std::vector> const& columnVariables) const; + /*! * Performs an if-then-else with the given operands, i.e. maps all valuations that are mapped to a non-zero * function value to the function values specified by the first DD and all others to the function values diff --git a/src/storage/dd/sylvan/InternalSylvanBdd.cpp b/src/storage/dd/sylvan/InternalSylvanBdd.cpp index 4b1e089c6..f08273001 100644 --- a/src/storage/dd/sylvan/InternalSylvanBdd.cpp +++ b/src/storage/dd/sylvan/InternalSylvanBdd.cpp @@ -1,5 +1,6 @@ #include "src/storage/dd/sylvan/InternalSylvanBdd.h" +#include "src/storage/dd/sylvan/InternalSylvanDdManager.h" #include "src/storage/dd/sylvan/InternalSylvanAdd.h" #include "src/storage/dd/sylvan/SylvanAddIterator.h" @@ -8,7 +9,6 @@ #include "src/utility/macros.h" #include "src/exceptions/NotImplementedException.h" - #include namespace storm { @@ -31,6 +31,15 @@ namespace storm { } InternalBdd InternalBdd::relationalProduct(InternalBdd const& relation, std::vector> const& rowVariables) const { + InternalBdd cube = ddManager->getBddOne(); + for (auto const& variable : rowVariables) { + cube &= variable; + } + + return InternalBdd(ddManager, this->sylvanBdd.RelNext(relation.sylvanBdd, cube.sylvanBdd)); + } + + InternalBdd InternalBdd::inverseRelationalProduct(InternalBdd const& relation, std::vector> const& columnVariables) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); } diff --git a/src/storage/dd/sylvan/InternalSylvanBdd.h b/src/storage/dd/sylvan/InternalSylvanBdd.h index 610b678c0..092321510 100644 --- a/src/storage/dd/sylvan/InternalSylvanBdd.h +++ b/src/storage/dd/sylvan/InternalSylvanBdd.h @@ -74,6 +74,15 @@ namespace storm { */ InternalBdd relationalProduct(InternalBdd const& relation, std::vector> const& rowVariables) const; + /*! + * Computes the inverse relational product of the current BDD and the given BDD representing a relation. + * + * @param relation The relation to use. + * @param columnVariables The row variables of the relation represented as individual BDDs. + * @return The ralational product. + */ + InternalBdd inverseRelationalProduct(InternalBdd const& relation, std::vector> const& columnVariables) const; + /*! * Performs an if-then-else with the given operands, i.e. maps all valuations that are mapped to a non-zero * function value to the function values specified by the first DD and all others to the function values diff --git a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp index 2840196cb..9f6df3e70 100644 --- a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp +++ b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp @@ -8,7 +8,10 @@ namespace storm { namespace dd { uint_fast64_t InternalDdManager::numberOfInstances = 0; - uint_fast64_t InternalDdManager::nextFreeVariableIndex = 0; + + // We let the variables start at an odd offset, since some functions provided by sylvan assume that the source/row + // variables are at odd levels. + uint_fast64_t InternalDdManager::nextFreeVariableIndex = 1; InternalDdManager::InternalDdManager() { if (numberOfInstances == 0) {