From 494f263b7105b49ed5dd596a30e74a966a99aa86 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 1 Dec 2015 20:40:44 +0100 Subject: [PATCH] fixed a wrong assumption for sylvan relnext Former-commit-id: 157e6826c71900d34c5f49ae6453d2dfe9ed7115 --- src/builder/DdPrismModelBuilder.cpp | 12 +++++++++++ src/storage/dd/Bdd.cpp | 20 +++++++++++++++++-- src/storage/dd/cudd/InternalCuddBdd.cpp | 18 ++--------------- src/storage/dd/cudd/InternalCuddBdd.h | 6 ++++-- src/storage/dd/sylvan/InternalSylvanBdd.cpp | 15 +++++++++++--- src/storage/dd/sylvan/InternalSylvanBdd.h | 6 ++++-- .../dd/sylvan/InternalSylvanDdManager.cpp | 6 +++--- 7 files changed, 55 insertions(+), 28 deletions(-) diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index e2c12baa2..993fca443 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -1175,6 +1175,15 @@ namespace storm { STORM_LOG_TRACE("Iteration " << iteration << " of reachability analysis."); changed = false; storm::dd::Bdd tmp = reachableStates.relationalProduct(transitionBdd, generationInfo.rowMetaVariables, generationInfo.columnMetaVariables); + + storm::dd::Bdd tmp2 = reachableStates.andExists(transitionBdd, generationInfo.rowMetaVariables); + tmp2 = tmp2.swapVariables(generationInfo.rowColumnMetaVariablePairs); + + tmp2.exportToDot("tmp2.dot"); + tmp.exportToDot("tmp.dot"); + + assert(tmp == tmp2); + storm::dd::Bdd newReachableStates = tmp && (!reachableStates); // Check whether new states were indeed discovered. @@ -1183,6 +1192,9 @@ namespace storm { } reachableStates |= newReachableStates; + + std::cout << "iter: " << iteration << " with nnz: " << reachableStates.getNonZeroCount() << std::endl; + ++iteration; } while (changed); diff --git a/src/storage/dd/Bdd.cpp b/src/storage/dd/Bdd.cpp index ad6fe77f2..87234b0e1 100644 --- a/src/storage/dd/Bdd.cpp +++ b/src/storage/dd/Bdd.cpp @@ -156,7 +156,15 @@ namespace storm { } } - return Bdd(this->getDdManager(), internalBdd.relationalProduct(relation, rowVariables), newMetaVariables); + 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.relationalProduct(relation, rowVariables, columnVariables), newMetaVariables); } template @@ -165,6 +173,14 @@ namespace storm { std::set newMetaVariables; std::set_difference(tmpMetaVariables.begin(), tmpMetaVariables.end(), rowMetaVariables.begin(), rowMetaVariables.end(), std::inserter(newMetaVariables, newMetaVariables.begin())); + std::vector> rowVariables; + for (auto const& metaVariable : rowMetaVariables) { + DdMetaVariable const& variable = this->getDdManager()->getMetaVariable(metaVariable); + for (auto const& ddVariable : variable.getDdVariables()) { + rowVariables.push_back(ddVariable); + } + } + std::vector> columnVariables; for (auto const& metaVariable : columnMetaVariables) { DdMetaVariable const& variable = this->getDdManager()->getMetaVariable(metaVariable); @@ -173,7 +189,7 @@ namespace storm { } } - return Bdd(this->getDdManager(), internalBdd.inverseRelationalProduct(relation, columnVariables), newMetaVariables); + return Bdd(this->getDdManager(), internalBdd.inverseRelationalProduct(relation, rowVariables, columnVariables), newMetaVariables); } template diff --git a/src/storage/dd/cudd/InternalCuddBdd.cpp b/src/storage/dd/cudd/InternalCuddBdd.cpp index 36d99d5cf..a257c9640 100644 --- a/src/storage/dd/cudd/InternalCuddBdd.cpp +++ b/src/storage/dd/cudd/InternalCuddBdd.cpp @@ -29,39 +29,25 @@ namespace storm { return !(*this == other); } - InternalBdd InternalBdd::relationalProduct(InternalBdd const& relation, std::vector> const& rowVariables) const { + InternalBdd InternalBdd::relationalProduct(InternalBdd const& relation, std::vector> const& rowVariables, std::vector> const& columnVariables) const { InternalBdd cube = ddManager->getBddOne(); for (auto const& variable : rowVariables) { cube &= variable; } InternalBdd result = this->andExists(relation, cube); - - // 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))); - } result = result.swapVariables(rowVariables, columnVariables); - return result; } - InternalBdd InternalBdd::inverseRelationalProduct(InternalBdd const& relation, std::vector> const& columnVariables) const { + InternalBdd InternalBdd::inverseRelationalProduct(InternalBdd const& relation, std::vector> const& rowVariables, 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; } diff --git a/src/storage/dd/cudd/InternalCuddBdd.h b/src/storage/dd/cudd/InternalCuddBdd.h index 2c8951aba..4358e491f 100644 --- a/src/storage/dd/cudd/InternalCuddBdd.h +++ b/src/storage/dd/cudd/InternalCuddBdd.h @@ -81,18 +81,20 @@ namespace storm { * * @param relation The relation to use. * @param rowVariables The row variables of the relation represented as individual BDDs. + * @param columnVariables The column variables of the relation represented as individual BDDs. * @return The ralational product. */ - InternalBdd relationalProduct(InternalBdd const& relation, std::vector> const& rowVariables) const; + InternalBdd relationalProduct(InternalBdd const& relation, std::vector> const& rowVariables, std::vector> const& columnVariables) const; /*! * Computes the inverse relational product of the current BDD and the given BDD representing a relation. * * @param relation The relation to use. + * @param rowVariables The row variables of the relation represented as individual BDDs. * @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; + InternalBdd inverseRelationalProduct(InternalBdd const& relation, std::vector> const& rowVariables, 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 diff --git a/src/storage/dd/sylvan/InternalSylvanBdd.cpp b/src/storage/dd/sylvan/InternalSylvanBdd.cpp index f08273001..c2e72a97a 100644 --- a/src/storage/dd/sylvan/InternalSylvanBdd.cpp +++ b/src/storage/dd/sylvan/InternalSylvanBdd.cpp @@ -30,16 +30,25 @@ namespace storm { return sylvanBdd != other.sylvanBdd; } - InternalBdd InternalBdd::relationalProduct(InternalBdd const& relation, std::vector> const& rowVariables) const { + InternalBdd InternalBdd::relationalProduct(InternalBdd const& relation, std::vector> const& rowVariables, std::vector> const& columnVariables) const { InternalBdd cube = ddManager->getBddOne(); for (auto const& variable : rowVariables) { cube &= variable; } + for (auto const& variable : columnVariables) { + cube &= variable; + } + + this->exportToDot("set.dot", {}); + relation.exportToDot("relation.dot", {}); + cube.exportToDot("cube.dot", {}); - return InternalBdd(ddManager, this->sylvanBdd.RelNext(relation.sylvanBdd, cube.sylvanBdd)); + InternalBdd result(ddManager, this->sylvanBdd.RelNext(relation.sylvanBdd, cube.sylvanBdd)); + result.exportToDot("result.dot", {}); + return result; } - InternalBdd InternalBdd::inverseRelationalProduct(InternalBdd const& relation, std::vector> const& columnVariables) const { + InternalBdd InternalBdd::inverseRelationalProduct(InternalBdd const& relation, std::vector> const& rowVariables, 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 092321510..5777f391d 100644 --- a/src/storage/dd/sylvan/InternalSylvanBdd.h +++ b/src/storage/dd/sylvan/InternalSylvanBdd.h @@ -70,18 +70,20 @@ namespace storm { * * @param relation The relation to use. * @param rowVariables The row variables of the relation represented as individual BDDs. + * @param columnVariables The row variables of the relation represented as individual BDDs. * @return The ralational product. */ - InternalBdd relationalProduct(InternalBdd const& relation, std::vector> const& rowVariables) const; + InternalBdd relationalProduct(InternalBdd const& relation, std::vector> const& rowVariables, std::vector> const& columnVariables) const; /*! * Computes the inverse relational product of the current BDD and the given BDD representing a relation. * * @param relation The relation to use. + * @param rowVariables The row variables of the relation represented as individual BDDs. * @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; + InternalBdd inverseRelationalProduct(InternalBdd const& relation, std::vector> const& rowVariables, 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 diff --git a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp index 9f6df3e70..c30da4863 100644 --- a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp +++ b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp @@ -9,9 +9,9 @@ namespace storm { namespace dd { uint_fast64_t InternalDdManager::numberOfInstances = 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; + // It is important that the variable pairs start at an even offset, because sylvan assumes this to be true for + // some operations. + uint_fast64_t InternalDdManager::nextFreeVariableIndex = 0; InternalDdManager::InternalDdManager() { if (numberOfInstances == 0) {