From 733bec60bd56efdf2965e7c78f024d0f999432dd Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 22 Mar 2018 16:46:19 +0100 Subject: [PATCH] started on hybrid solution of abstraction --- .../abstraction/GameBasedMdpModelChecker.cpp | 110 ++++++++++-------- .../abstraction/GameBasedMdpModelChecker.h | 5 + .../settings/modules/AbstractionSettings.cpp | 17 ++- .../settings/modules/AbstractionSettings.h | 10 ++ src/storm/storage/dd/Add.cpp | 25 +++- src/storm/storage/dd/Add.h | 33 +++--- src/storm/storage/dd/cudd/InternalCuddAdd.cpp | 25 ++++ src/storm/storage/dd/cudd/InternalCuddAdd.h | 22 ++++ .../storage/dd/sylvan/InternalSylvanAdd.cpp | 30 +++++ .../storage/dd/sylvan/InternalSylvanAdd.h | 22 ++++ 10 files changed, 232 insertions(+), 67 deletions(-) diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index f2cb7a3d2..ea0a72349 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -32,7 +32,6 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/CoreSettings.h" -#include "storm/settings/modules/AbstractionSettings.h" #include "storm/utility/prism.h" #include "storm/utility/macros.h" @@ -50,7 +49,7 @@ namespace storm { using storm::abstraction::QuantitativeGameResultMinMax; template - GameBasedMdpModelChecker::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule().getPrecision()), reuseQualitativeResults(false), reuseQuantitativeResults(false) { + GameBasedMdpModelChecker::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule().getPrecision()), reuseQualitativeResults(false), reuseQuantitativeResults(false), solveMode(storm::settings::getModule().getSolveMode()) { model.requireNoUndefinedConstants(); if (model.isPrismProgram()) { storm::prism::Program const& originalProgram = model.asPrismProgram(); @@ -424,54 +423,73 @@ namespace storm { // (6) if we arrived at this point and no refinement was made, we need to compute the quantitative solution. if (!qualitativeRefinement) { // At this point, we know that we cannot answer the query without further numeric computation. - - storm::dd::Add initialStatesAdd = initialStates.template toAdd(); - STORM_LOG_TRACE("Starting numerical solution step."); - auto quantitativeStart = std::chrono::high_resolution_clock::now(); - - QuantitativeGameResultMinMax quantitativeResult; - - // (7) Solve the min values and check whether we can give the answer already. - quantitativeResult.min = computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Minimize, game, qualitativeResult, initialStatesAdd, maybeMin, reuseQuantitativeResults ? previousMinQuantitativeResult : boost::none); - previousMinQuantitativeResult = quantitativeResult.min; - result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Minimize, quantitativeResult.min.getInitialStatesRange()); - if (result) { - printStatistics(*abstractor, game); - return result; - } - - // (8) Solve the max values and check whether we can give the answer already. - quantitativeResult.max = computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Maximize, game, qualitativeResult, initialStatesAdd, maybeMax, boost::make_optional(quantitativeResult.min)); - result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Maximize, quantitativeResult.max.getInitialStatesRange()); - if (result) { - printStatistics(*abstractor, game); - return result; - } - auto quantitativeEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_DEBUG("Obtained quantitative bounds [" << quantitativeResult.min.getInitialStatesRange().first << ", " << quantitativeResult.max.getInitialStatesRange().second << "] on the actual value for the initial states in " << std::chrono::duration_cast(quantitativeEnd - quantitativeStart).count() << "ms."); - - // (9) Check whether the lower and upper bounds are close enough to terminate with an answer. - result = checkForResultAfterQuantitativeCheck(quantitativeResult.min.getInitialStatesRange().first, quantitativeResult.max.getInitialStatesRange().second, comparator); - if (result) { - printStatistics(*abstractor, game); - return result; + // Solve abstraction using the selected mode. + if (solveMode == storm::settings::modules::AbstractionSettings::SolveMode::Dd) { + STORM_LOG_TRACE("Using dd-based solving."); + storm::dd::Add initialStatesAdd = initialStates.template toAdd(); + + auto quantitativeStart = std::chrono::high_resolution_clock::now(); + + QuantitativeGameResultMinMax quantitativeResult; + + // (7) Solve the min values and check whether we can give the answer already. + quantitativeResult.min = computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Minimize, game, qualitativeResult, initialStatesAdd, maybeMin, reuseQuantitativeResults ? previousMinQuantitativeResult : boost::none); + previousMinQuantitativeResult = quantitativeResult.min; + result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Minimize, quantitativeResult.min.getInitialStatesRange()); + if (result) { + printStatistics(*abstractor, game); + return result; + } + + // (8) Solve the max values and check whether we can give the answer already. + quantitativeResult.max = computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Maximize, game, qualitativeResult, initialStatesAdd, maybeMax, boost::make_optional(quantitativeResult.min)); + result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Maximize, quantitativeResult.max.getInitialStatesRange()); + if (result) { + printStatistics(*abstractor, game); + return result; + } + + auto quantitativeEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_DEBUG("Obtained quantitative bounds [" << quantitativeResult.min.getInitialStatesRange().first << ", " << quantitativeResult.max.getInitialStatesRange().second << "] on the actual value for the initial states in " << std::chrono::duration_cast(quantitativeEnd - quantitativeStart).count() << "ms."); + + // (9) Check whether the lower and upper bounds are close enough to terminate with an answer. + result = checkForResultAfterQuantitativeCheck(quantitativeResult.min.getInitialStatesRange().first, quantitativeResult.max.getInitialStatesRange().second, comparator); + if (result) { + printStatistics(*abstractor, game); + return result; + } + + // Make sure that all strategies are still valid strategies. + STORM_LOG_ASSERT(quantitativeResult.min.getPlayer1Strategy().isZero() || quantitativeResult.min.getPlayer1Strategy().template toAdd().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for min is illegal."); + STORM_LOG_ASSERT(quantitativeResult.max.getPlayer1Strategy().isZero() || quantitativeResult.max.getPlayer1Strategy().template toAdd().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for max is illegal."); + STORM_LOG_ASSERT(quantitativeResult.min.getPlayer2Strategy().isZero() || quantitativeResult.min.getPlayer2Strategy().template toAdd().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for min is illegal."); + STORM_LOG_ASSERT(quantitativeResult.max.getPlayer2Strategy().isZero() || quantitativeResult.max.getPlayer2Strategy().template toAdd().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for max is illegal."); + + auto quantitativeRefinementStart = std::chrono::high_resolution_clock::now(); + // (10) If we arrived at this point, it means that we have all qualitative and quantitative + // information about the game, but we could not yet answer the query. In this case, we need to refine. + refiner.refine(game, transitionMatrixBdd, quantitativeResult); + auto quantitativeRefinementEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_DEBUG("Quantitative refinement completed in " << std::chrono::duration_cast(quantitativeRefinementEnd - quantitativeRefinementStart).count() << "ms."); + } else { + STORM_LOG_TRACE("Using hybrid solving."); + + storm::dd::Odd odd = (maybeMin || maybeMax || targetStates).createOdd(); + + std::pair, std::vector> transitionMatrixLabeling = game.getTransitionMatrix().toLabeledMatrix(game.getRowVariables(), game.getColumnVariables(), game.getNondeterminismVariables(), odd, odd, true); + auto const& transitionMatrix = transitionMatrixLabeling.first; + auto const& labeling = transitionMatrixLabeling.second; + + std::cout << transitionMatrix << std::endl; + for (auto const& e : labeling) { + std::cout << e << std::endl; + } + + exit(-1); } - // Make sure that all strategies are still valid strategies. - STORM_LOG_ASSERT(quantitativeResult.min.getPlayer1Strategy().isZero() || quantitativeResult.min.getPlayer1Strategy().template toAdd().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for min is illegal."); - STORM_LOG_ASSERT(quantitativeResult.max.getPlayer1Strategy().isZero() || quantitativeResult.max.getPlayer1Strategy().template toAdd().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for max is illegal."); - STORM_LOG_ASSERT(quantitativeResult.min.getPlayer2Strategy().isZero() || quantitativeResult.min.getPlayer2Strategy().template toAdd().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for min is illegal."); - STORM_LOG_ASSERT(quantitativeResult.max.getPlayer2Strategy().isZero() || quantitativeResult.max.getPlayer2Strategy().template toAdd().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for max is illegal."); - - auto quantitativeRefinementStart = std::chrono::high_resolution_clock::now(); - // (10) If we arrived at this point, it means that we have all qualitative and quantitative - // information about the game, but we could not yet answer the query. In this case, we need to refine. - refiner.refine(game, transitionMatrixBdd, quantitativeResult); - auto quantitativeRefinementEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_DEBUG("Quantitative refinement completed in " << std::chrono::duration_cast(quantitativeRefinementEnd - quantitativeRefinementStart).count() << "ms."); - } auto iterationEnd = std::chrono::high_resolution_clock::now(); STORM_LOG_DEBUG("Iteration " << iterations << " took " << std::chrono::duration_cast(iterationEnd - iterationStart).count() << "ms."); diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h index 8c105cfc4..dd6c7cb2f 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h @@ -14,6 +14,8 @@ #include "storm/logic/Bound.h" +#include "storm/settings/modules/AbstractionSettings.h" + #include "storm/utility/ConstantsComparator.h" #include "storm/utility/solver.h" #include "storm/utility/graph.h" @@ -95,6 +97,9 @@ namespace storm { /// A flag indicating whether to reuse the quantitative results. bool reuseQuantitativeResults; + + /// The mode selected for solving the abstraction. + storm::settings::modules::AbstractionSettings::SolveMode solveMode; }; } } diff --git a/src/storm/settings/modules/AbstractionSettings.cpp b/src/storm/settings/modules/AbstractionSettings.cpp index 9570810f1..947b7b7ca 100644 --- a/src/storm/settings/modules/AbstractionSettings.cpp +++ b/src/storm/settings/modules/AbstractionSettings.cpp @@ -22,6 +22,7 @@ namespace storm { const std::string AbstractionSettings::pivotHeuristicOptionName = "pivot-heuristic"; const std::string AbstractionSettings::reuseResultsOptionName = "reuse"; const std::string AbstractionSettings::restrictToRelevantStatesOptionName = "relevant"; + const std::string AbstractionSettings::solveModeOptionName = "solve"; AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) { std::vector methods = {"games", "bisimulation", "bisim"}; @@ -42,7 +43,13 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(splitModes)) .setDefaultValueString("all").build()) .build()); - + + std::vector solveModes = {"dd", "hybrid"}; + this->addOption(storm::settings::OptionBuilder(moduleName, solveModeOptionName, true, "Sets how the abstractions are solved.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(solveModes)) + .setDefaultValueString("dd").build()) + .build()); + this->addOption(storm::settings::OptionBuilder(moduleName, addAllGuardsOptionName, true, "Sets whether all guards are added as initial predicates.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff)) .setDefaultValueString("on").build()) @@ -98,6 +105,14 @@ namespace storm { return SplitMode::All; } + AbstractionSettings::SolveMode AbstractionSettings::getSolveMode() const { + std::string solveModeAsString = this->getOption(solveModeOptionName).getArgumentByName("mode").getValueAsString(); + if (solveModeAsString == "dd") { + return SolveMode::Dd; + } + return SolveMode::Hybrid; + } + bool AbstractionSettings::isAddAllGuardsSet() const { return this->getOption(addAllGuardsOptionName).getArgumentByName("value").getValueAsString() == "on"; } diff --git a/src/storm/settings/modules/AbstractionSettings.h b/src/storm/settings/modules/AbstractionSettings.h index 7c2a98f66..2b361b273 100644 --- a/src/storm/settings/modules/AbstractionSettings.h +++ b/src/storm/settings/modules/AbstractionSettings.h @@ -27,6 +27,10 @@ namespace storm { All, None, Qualitative, Quantitative }; + enum class SolveMode { + Dd, Hybrid + }; + /*! * Creates a new set of abstraction settings. */ @@ -100,6 +104,11 @@ namespace storm { */ bool isRestrictToRelevantStatesSet() const; + /*! + * Retrieves the mode with which to solve the games. + */ + SolveMode getSolveMode() const; + const static std::string moduleName; private: @@ -112,6 +121,7 @@ namespace storm { const static std::string pivotHeuristicOptionName; const static std::string reuseResultsOptionName; const static std::string restrictToRelevantStatesOptionName; + const static std::string solveModeOptionName; }; } diff --git a/src/storm/storage/dd/Add.cpp b/src/storm/storage/dd/Add.cpp index 9e91b2123..91c35c67a 100644 --- a/src/storm/storage/dd/Add.cpp +++ b/src/storm/storage/dd/Add.cpp @@ -703,11 +703,11 @@ namespace storm { } // Create the canonical row group sizes and build the matrix. - return toMatrix(rowMetaVariables, columnMetaVariables, groupMetaVariables, rowOdd, columnOdd); + return toLabeledMatrix(rowMetaVariables, columnMetaVariables, groupMetaVariables, rowOdd, columnOdd).first; } template - storm::storage::SparseMatrix Add::toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { + 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::vector ddRowVariableIndices; std::vector ddColumnVariableIndices; std::vector ddGroupVariableIndices; @@ -760,12 +760,24 @@ namespace storm { groups.push_back(Add(this->getDdManager(), internalAdd, rowAndColumnMetaVariables)); } + // Create the group labelings if requested. + std::vector groupLabels; + if (buildLabeling) { + groupLabels = internalAdd.decodeGroupLabels(ddGroupVariableIndices); + STORM_LOG_ASSERT(groupLabels.size() == groups.size(), "Mismatching label sizes."); + } + // Create the actual storage for the non-zero entries. std::vector> columnsAndValues(this->getNonZeroCount()); // Now compute the indices at which the individual rows start. std::vector rowIndications(rowGroupIndices.back() + 1); + std::vector labeling; + if (buildLabeling) { + labeling.resize(rowGroupIndices.back()); + } + std::vector> statesWithGroupEnabled(groups.size()); InternalAdd stateToRowGroupCount = this->getDdManager().template getAddZero(); for (uint_fast64_t i = 0; i < groups.size(); ++i) { @@ -779,6 +791,11 @@ namespace storm { statesWithGroupEnabled[i] = groupNotZero.existsAbstract(columnMetaVariables).template toAdd(); statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::plus()); + + if (buildLabeling) { + uint64_t currentLabel = groupLabels[i]; + statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, labeling, [currentLabel] (uint_fast64_t a, uint_fast64_t l) { return currentLabel; }); + } } // Since we modified the rowGroupIndices, we need to restore the correct values. @@ -812,9 +829,9 @@ namespace storm { } rowIndications[0] = 0; - return storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)); + return std::make_pair(storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)), labeling); } - + template std::pair, std::vector> Add::toMatrixVector(storm::dd::Add const& vector, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { std::set rowMetaVariables; diff --git a/src/storm/storage/dd/Add.h b/src/storm/storage/dd/Add.h index 1a4a811d5..c50b4c010 100644 --- a/src/storm/storage/dd/Add.h +++ b/src/storm/storage/dd/Add.h @@ -640,6 +640,23 @@ namespace storm { */ storm::storage::SparseMatrix toMatrix(std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; + /*! + * Converts the ADD to a row-grouped (sparse) matrix. The given offset-labeled DDs are used to determine the + * correct row and column, respectively, for each entry. If requested, it builds a labeling of the rows + * that is derived from the group variable encodings. Note: this function assumes that the meta variables + * used to distinguish different row groups are at the very top of the ADD. + * + * @param rowMetaVariables The meta variables that encode the rows of the matrix. + * @param columnMetaVariables The meta variables that encode the columns of the matrix. + * @param groupMetaVariables The meta variables that are used to distinguish different row groups. + * @param rowOdd The ODD used for determining the correct row. + * @param columnOdd The ODD used for determining the correct column. + * @param buildLabeling If false, no labeling vector is built. + * @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; + /*! * Converts the ADD to a row-grouped (sparse) matrix and the given vector to a row-grouped vector. * The given offset-labeled DDs are used to determine the correct row and column, respectively, for each @@ -721,22 +738,6 @@ namespace storm { */ operator InternalAdd() const; - /*! - * Converts the ADD to a row-grouped (sparse) double matrix. If the optional vector is given, it is also - * translated to an explicit row-grouped vector with the same row-grouping. The given offset-labeled DDs - * are used to determine the correct row and column, respectively, for each entry. Note: this function - * assumes that the meta variables used to distinguish different row groups are at the very top of the ADD. - * - * @param rowMetaVariables The meta variables that encode the rows of the matrix. - * @param columnMetaVariables The meta variables that encode the columns of the matrix. - * @param groupMetaVariables The meta variables that are used to distinguish different row groups. - * @param rowOdd The ODD used for determining the correct row. - * @param columnOdd The ODD used for determining the correct column. - * @return The matrix that is represented by this ADD and and a vector corresponding to the symbolic vector - * (if it was given). - */ - storm::storage::SparseMatrix toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; - /*! * Converts the ADD to a row-grouped (sparse) double matrix and the given vector to an equally row-grouped * explicit vector. The given offset-labeled DDs are used to determine the correct row and column, diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp index 11c6b12ca..ea0ca6d1f 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp @@ -524,6 +524,31 @@ namespace storm { } } + template + std::vector InternalAdd::decodeGroupLabels(std::vector const& ddGroupVariableIndices) const { + std::vector result; + decodeGroupLabelsRec(this->getCuddDdNode(), result, ddGroupVariableIndices, 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 { + // For the empty DD, we do not need to create a group. + if (dd == Cudd_ReadZero(ddManager->getCuddManager().getManager())) { + return; + } + + 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 ); + } + } + template std::vector> InternalAdd::splitIntoGroups(std::vector const& ddGroupVariableIndices) const { std::vector> result; diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.h b/src/storm/storage/dd/cudd/InternalCuddAdd.h index 2262d5da0..bb53f68d4 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.h +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.h @@ -570,6 +570,15 @@ namespace storm { */ std::vector> splitIntoGroups(std::vector const& ddGroupVariableIndices) const; + /*! + * Splits the ADD into several ADDs that differ in the encoding of the given group variables (given via indices). + * 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. + * @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; + /*! * Simultaneously splits the ADD and the given vector ADD into several ADDs that differ in the encoding of * the given group variables (given via indices). @@ -661,6 +670,19 @@ namespace storm { */ void splitIntoGroupsRec(DdNode* dd, std::vector>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const; + /*! + * Splits the given matrix DD into the labelings of the gropus using the given group variables. + * + * @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 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; + /*! * 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 0173f6aac..4a7784015 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -921,6 +921,36 @@ namespace storm { } } + template + std::vector InternalAdd::decodeGroupLabels(std::vector const& ddGroupVariableIndices) const { + std::vector result; + decodeGroupLabelsRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), result, ddGroupVariableIndices, 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 { + // For the empty DD, we do not need to create a group. + if (mtbdd_isleaf(dd) && mtbdd_iszero(dd)) { + return; + } + + 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 ); + + } + } + template std::vector> InternalAdd::splitIntoGroups(std::vector const& ddGroupVariableIndices) const { std::vector> result; diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h index 5137caf15..6c3cae256 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h @@ -561,6 +561,15 @@ namespace storm { */ std::vector> splitIntoGroups(std::vector const& ddGroupVariableIndices) const; + /*! + * Splits the ADD into several ADDs that differ in the encoding of the given group variables (given via indices). + * 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. + * @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; + /*! * Simultaneously splits the ADD and the given vector ADD into several ADDs that differ in the encoding of * the given group variables (given via indices). @@ -651,6 +660,19 @@ namespace storm { */ void composeWithExplicitVectorRec(MTBDD dd, bool negated, std::vector const* offsets, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const; + /*! + * Splits the given matrix DD into the labelings of the gropus using the given group variables. + * + * @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 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; + /*! * Splits the given matrix DD into the groups using the given group variables. *