From cedae194e385a2b138599c0305786f11ac1de434 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 22 Mar 2018 19:15:27 +0100 Subject: [PATCH] towards labeling generation in dd to sparse conversion --- .../abstraction/GameBasedMdpModelChecker.cpp | 7 ++-- src/storm/storage/dd/Add.cpp | 31 ++++++++++++++--- src/storm/storage/dd/Add.h | 2 +- src/storm/storage/dd/cudd/InternalCuddAdd.cpp | 29 +++++++++++----- src/storm/storage/dd/cudd/InternalCuddAdd.h | 6 ++-- .../storage/dd/sylvan/InternalSylvanAdd.cpp | 34 ++++++++++++------- .../storage/dd/sylvan/InternalSylvanAdd.h | 6 ++-- 7 files changed, 83 insertions(+), 32 deletions(-) diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index ea0a72349..ac3250f19 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -476,9 +476,12 @@ namespace storm { } else { STORM_LOG_TRACE("Using hybrid solving."); - storm::dd::Odd odd = (maybeMin || maybeMax || targetStates).createOdd(); + auto relevantStates = maybeMin || maybeMax || targetStates; + auto relevantStatesAdd = relevantStates.template toAdd(); + storm::dd::Odd odd = relevantStates.createOdd(); - std::pair, std::vector> transitionMatrixLabeling = game.getTransitionMatrix().toLabeledMatrix(game.getRowVariables(), game.getColumnVariables(), game.getNondeterminismVariables(), odd, odd, true); + auto relevantStatesTransitionMatrix = game.getTransitionMatrix() * relevantStatesAdd * relevantStatesAdd.swapVariables(game.getRowColumnMetaVariablePairs()); + std::pair, std::vector> transitionMatrixLabeling = relevantStatesTransitionMatrix.toLabeledMatrix(game.getRowVariables(), game.getColumnVariables(), game.getNondeterminismVariables(), game.getPlayer1Variables(), odd, odd, true); auto const& transitionMatrix = transitionMatrixLabeling.first; auto const& labeling = transitionMatrixLabeling.second; diff --git a/src/storm/storage/dd/Add.cpp b/src/storm/storage/dd/Add.cpp index 91c35c67a..80b707639 100644 --- a/src/storm/storage/dd/Add.cpp +++ b/src/storm/storage/dd/Add.cpp @@ -9,6 +9,7 @@ #include "storm/storage/dd/Odd.h" #include "storm/storage/SparseMatrix.h" +#include "storm/storage/BitVector.h" #include "storm/utility/constants.h" #include "storm/utility/macros.h" @@ -703,14 +704,15 @@ namespace storm { } // Create the canonical row group sizes and build the matrix. - return toLabeledMatrix(rowMetaVariables, columnMetaVariables, groupMetaVariables, rowOdd, columnOdd).first; + return toLabeledMatrix(rowMetaVariables, columnMetaVariables, groupMetaVariables, groupMetaVariables, rowOdd, columnOdd).first; } template - std::pair, std::vector> Add::toLabeledMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd, bool buildLabeling) const { + std::pair, std::vector> Add::toLabeledMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, std::set const& labelMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd, bool buildLabeling) const { std::vector ddRowVariableIndices; std::vector ddColumnVariableIndices; std::vector ddGroupVariableIndices; + storm::storage::BitVector ddLabelVariableIndices; std::set rowAndColumnMetaVariables; for (auto const& variable : rowMetaVariables) { @@ -736,7 +738,25 @@ namespace storm { } } std::sort(ddGroupVariableIndices.begin(), ddGroupVariableIndices.end()); - + if (buildLabeling) { + std::set ddLabelVariableIndicesSet; + for (auto const& variable : labelMetaVariables) { + DdMetaVariable const& metaVariable = this->getDdManager().getMetaVariable(variable); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddLabelVariableIndicesSet.insert(ddVariable.getIndex()); + } + } + + ddLabelVariableIndices = storm::storage::BitVector(ddGroupVariableIndices.size()); + uint64_t position = 0; + for (auto const& index : ddGroupVariableIndices) { + if (ddLabelVariableIndicesSet.find(index) != ddLabelVariableIndicesSet.end()) { + ddLabelVariableIndices.set(position); + } + ++position; + } + } + Bdd columnVariableCube = Bdd::getCube(this->getDdManager(), columnMetaVariables); // Start by computing the offsets (in terms of rows) for each row group. @@ -763,7 +783,7 @@ namespace storm { // Create the group labelings if requested. std::vector groupLabels; if (buildLabeling) { - groupLabels = internalAdd.decodeGroupLabels(ddGroupVariableIndices); + groupLabels = internalAdd.decodeGroupLabels(ddGroupVariableIndices, ddLabelVariableIndices); STORM_LOG_ASSERT(groupLabels.size() == groups.size(), "Mismatching label sizes."); } @@ -794,7 +814,8 @@ namespace storm { if (buildLabeling) { uint64_t currentLabel = groupLabels[i]; - statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, labeling, [currentLabel] (uint_fast64_t a, uint_fast64_t l) { return currentLabel; }); + std::cout << "current label is " << currentLabel << std::endl; + // statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, labeling, [currentLabel] (uint_fast64_t a, uint_fast64_t l) { return currentLabel; }); } } diff --git a/src/storm/storage/dd/Add.h b/src/storm/storage/dd/Add.h index c50b4c010..ba6b5644d 100644 --- a/src/storm/storage/dd/Add.h +++ b/src/storm/storage/dd/Add.h @@ -655,7 +655,7 @@ namespace storm { * @return The matrix that is represented by this ADD and a vector corresponding to row labeling * (if requested). */ - std::pair, std::vector> toLabeledMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd, bool buildLabeling = false) const; + std::pair, std::vector> toLabeledMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, std::set const& labelMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd, bool buildLabeling = false) const; /*! * Converts the ADD to a row-grouped (sparse) matrix and the given vector to a row-grouped vector. diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp index ea0ca6d1f..6e5a57e4a 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp @@ -6,6 +6,7 @@ #include "storm/storage/dd/Odd.h" #include "storm/storage/SparseMatrix.h" +#include "storm/storage/BitVector.h" #include "storm/utility/constants.h" #include "storm/utility/macros.h" @@ -525,14 +526,15 @@ namespace storm { } template - std::vector InternalAdd::decodeGroupLabels(std::vector const& ddGroupVariableIndices) const { + std::vector InternalAdd::decodeGroupLabels(std::vector const& ddGroupVariableIndices, storm::storage::BitVector const& ddLabelVariableIndices) const { std::vector result; - decodeGroupLabelsRec(this->getCuddDdNode(), result, ddGroupVariableIndices, 0, ddGroupVariableIndices.size(), 0); + std::cout << ddLabelVariableIndices << std::endl; + decodeGroupLabelsRec(this->getCuddDdNode(), result, ddGroupVariableIndices, ddLabelVariableIndices, 0, ddGroupVariableIndices.size(), 0); return result; } template - void InternalAdd::decodeGroupLabelsRec(DdNode* dd, std::vector& labels, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint64_t label) const { + void InternalAdd::decodeGroupLabelsRec(DdNode* dd, std::vector& labels, std::vector const& ddGroupVariableIndices, storm::storage::BitVector const& ddLabelVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint64_t label) const { // For the empty DD, we do not need to create a group. if (dd == Cudd_ReadZero(ddManager->getCuddManager().getManager())) { return; @@ -540,12 +542,23 @@ namespace storm { if (currentLevel == maxLevel) { labels.push_back(label); - } else if (ddGroupVariableIndices[currentLevel] < Cudd_NodeReadIndex(dd)) { - decodeGroupLabelsRec(dd, labels, ddGroupVariableIndices, currentLevel + 1, maxLevel, label << 1); - decodeGroupLabelsRec(dd, labels, ddGroupVariableIndices, currentLevel + 1, maxLevel, (label << 1) | 1); } else { - decodeGroupLabelsRec(Cudd_E(dd), labels, ddGroupVariableIndices, currentLevel + 1, maxLevel, label << 1); - decodeGroupLabelsRec(Cudd_T(dd), labels, ddGroupVariableIndices, currentLevel + 1, maxLevel, (label << 1) | 1 ); + uint64_t elseLabel = label; + uint64_t thenLabel = label; + + std::cout << "currentLevel " << currentLevel << " is in labels? " << ddLabelVariableIndices.get(currentLevel) << std::endl; + if (ddLabelVariableIndices.get(currentLevel)) { + elseLabel <<= 1; + thenLabel = (thenLabel << 1) | 1; + } + + if (ddGroupVariableIndices[currentLevel] < Cudd_NodeReadIndex(dd)) { + decodeGroupLabelsRec(dd, labels, ddGroupVariableIndices, ddLabelVariableIndices, currentLevel + 1, maxLevel, elseLabel); + decodeGroupLabelsRec(dd, labels, ddGroupVariableIndices, ddLabelVariableIndices, currentLevel + 1, maxLevel, thenLabel); + } else { + decodeGroupLabelsRec(Cudd_E(dd), labels, ddGroupVariableIndices, ddLabelVariableIndices, currentLevel + 1, maxLevel, elseLabel); + decodeGroupLabelsRec(Cudd_T(dd), labels, ddGroupVariableIndices, ddLabelVariableIndices, currentLevel + 1, maxLevel, thenLabel); + } } } diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.h b/src/storm/storage/dd/cudd/InternalCuddAdd.h index bb53f68d4..cab873353 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.h +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.h @@ -575,9 +575,10 @@ namespace storm { * The labeling is then made by interpreting the group encodings as binary encodings. * * @param ddGroupVariableIndices The indices of the variables that are used to distinguish the groups. + * @param ddLabelVariableIndices The indices of variables that are considered as labels. * @return A vector of ADDs that are the separate groups (wrt. to the encoding of the given variables). */ - std::vector decodeGroupLabels(std::vector const& ddGroupVariableIndices) const; + std::vector decodeGroupLabels(std::vector const& ddGroupVariableIndices, storm::storage::BitVector const& ddLabelVariableIndices) const; /*! * Simultaneously splits the ADD and the given vector ADD into several ADDs that differ in the encoding of @@ -676,12 +677,13 @@ namespace storm { * @param dd The DD to split. * @param labels A vector that is to be filled with the labels of the individual groups. * @param ddGroupVariableIndices The (sorted) indices of all DD group variables that need to be considered. + * @param ddLabelVariableIndices A bit vector indicating which variables are considered label variables. * @param currentLevel The currently considered level in the DD. * @param maxLevel The number of levels that need to be considered. * @param remainingMetaVariables The meta variables that remain in the DDs after the groups have been split. * @param label The currently followed label. */ - void decodeGroupLabelsRec(DdNode* dd, std::vector& labels, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint64_t label) const; + void decodeGroupLabelsRec(DdNode* dd, std::vector& labels, std::vector const& ddGroupVariableIndices, storm::storage::BitVector const& ddLabelVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint64_t label) const; /*! * Splits the given DDs into the groups using the given group variables. diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp index 4a7784015..96dcbcc75 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -5,6 +5,7 @@ #include "storm/storage/dd/DdManager.h" #include "storm/storage/SparseMatrix.h" +#include "storm/storage/BitVector.h" #include "storm/utility/macros.h" #include "storm/utility/constants.h" @@ -922,14 +923,14 @@ namespace storm { } template - std::vector InternalAdd::decodeGroupLabels(std::vector const& ddGroupVariableIndices) const { + std::vector InternalAdd::decodeGroupLabels(std::vector const& ddGroupVariableIndices, storm::storage::BitVector const& ddLabelVariableIndices) const { std::vector result; - decodeGroupLabelsRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), result, ddGroupVariableIndices, 0, ddGroupVariableIndices.size(), 0); + decodeGroupLabelsRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), result, ddGroupVariableIndices, ddLabelVariableIndices, 0, ddGroupVariableIndices.size(), 0); return result; } template - void InternalAdd::decodeGroupLabelsRec(MTBDD dd, std::vector& labels, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint64_t label) const { + void InternalAdd::decodeGroupLabelsRec(MTBDD dd, std::vector& labels, std::vector const& ddGroupVariableIndices, storm::storage::BitVector const& ddLabelVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint64_t label) const { // For the empty DD, we do not need to create a group. if (mtbdd_isleaf(dd) && mtbdd_iszero(dd)) { return; @@ -937,17 +938,26 @@ namespace storm { if (currentLevel == maxLevel) { labels.push_back(label); - } else if (mtbdd_isleaf(dd) || ddGroupVariableIndices[currentLevel] < mtbdd_getvar(dd)) { - decodeGroupLabelsRec(dd, labels, ddGroupVariableIndices, currentLevel + 1, maxLevel, label << 1); - decodeGroupLabelsRec(dd, labels, ddGroupVariableIndices, currentLevel + 1, maxLevel, (label << 1) | 1); } else { - // Otherwise, we compute the ODDs for both the then- and else successors. - MTBDD thenDdNode = mtbdd_gethigh(dd); - MTBDD elseDdNode = mtbdd_getlow(dd); - - decodeGroupLabelsRec(mtbdd_regular(elseDdNode), labels, ddGroupVariableIndices, currentLevel + 1, maxLevel, label << 1); - decodeGroupLabelsRec(mtbdd_regular(thenDdNode), labels, ddGroupVariableIndices, currentLevel + 1, maxLevel, (label << 1) | 1 ); + uint64_t elseLabel = label; + uint64_t thenLabel = label; + if (ddLabelVariableIndices.get(currentLevel)) { + elseLabel <<= 1; + thenLabel = (thenLabel << 1) | 1; + } + + if (mtbdd_isleaf(dd) || ddGroupVariableIndices[currentLevel] < mtbdd_getvar(dd)) { + decodeGroupLabelsRec(dd, labels, ddGroupVariableIndices, ddLabelVariableIndices, currentLevel + 1, maxLevel, elseLabel); + decodeGroupLabelsRec(dd, labels, ddGroupVariableIndices, ddLabelVariableIndices, currentLevel + 1, maxLevel, thenLabel); + } else { + // Otherwise, we compute the ODDs for both the then- and else successors. + MTBDD thenDdNode = mtbdd_gethigh(dd); + MTBDD elseDdNode = mtbdd_getlow(dd); + + decodeGroupLabelsRec(mtbdd_regular(elseDdNode), labels, ddGroupVariableIndices, ddLabelVariableIndices, currentLevel + 1, maxLevel, elseLabel); + decodeGroupLabelsRec(mtbdd_regular(thenDdNode), labels, ddGroupVariableIndices, ddLabelVariableIndices, currentLevel + 1, maxLevel, thenLabel); + } } } diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h index 6c3cae256..449ba0bbc 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h @@ -566,9 +566,10 @@ namespace storm { * The labeling is then made by interpreting the group encodings as binary encodings. * * @param ddGroupVariableIndices The indices of the variables that are used to distinguish the groups. + * @param ddLabelVariableIndices The indices of variables that are considered as labels. * @return A vector of ADDs that are the separate groups (wrt. to the encoding of the given variables). */ - std::vector decodeGroupLabels(std::vector const& ddGroupVariableIndices) const; + std::vector decodeGroupLabels(std::vector const& ddGroupVariableIndices, storm::storage::BitVector const& ddLabelVariableIndices) const; /*! * Simultaneously splits the ADD and the given vector ADD into several ADDs that differ in the encoding of @@ -666,12 +667,13 @@ namespace storm { * @param dd The DD to split. * @param labels A vector that is to be filled with the labels of the individual groups. * @param ddGroupVariableIndices The (sorted) indices of all DD group variables that need to be considered. + * @param ddLabelVariableIndices A bit vector indicating which variables are considered label variables. * @param currentLevel The currently considered level in the DD. * @param maxLevel The number of levels that need to be considered. * @param remainingMetaVariables The meta variables that remain in the DDs after the groups have been split. * @param label The currently followed label. */ - void decodeGroupLabelsRec(MTBDD dd, std::vector& labels, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint64_t label) const; + void decodeGroupLabelsRec(MTBDD dd, std::vector& labels, std::vector const& ddGroupVariableIndices, storm::storage::BitVector const& ddLabelVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint64_t label) const; /*! * Splits the given matrix DD into the groups using the given group variables.