From 009dabf2f1141c57a44a6cf4b609b5edaec14594 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 20 Nov 2015 15:57:21 +0100 Subject: [PATCH] started cleanining up Former-commit-id: 3db6fbc1b239abace66dbde13ddc9259381b56a8 --- .../prctl/helper/HybridMdpPrctlHelper.cpp | 15 +-- src/storage/dd/Add.cpp | 41 ------- src/storage/dd/Add.h | 11 -- src/storage/dd/cudd/InternalCuddAdd.h | 101 +++++++++++++++--- src/storage/dd/cudd/InternalCuddBdd.h | 69 ++++++------ 5 files changed, 133 insertions(+), 104 deletions(-) diff --git a/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp index 22b104034..2c41c1e94 100644 --- a/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp @@ -149,13 +149,13 @@ namespace storm { STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); // Create the ODD for the translation between symbolic and explicit storage. - storm::dd::Odd odd =model.getReachableStates().createOdd(); + storm::dd::Odd odd = model.getReachableStates().createOdd(); // Translate the symbolic matrix to its explicit representations. storm::storage::SparseMatrix explicitMatrix = transitionMatrix.toMatrix(model.getNondeterminismVariables(), odd, odd); // Create the solution vector (and initialize it to the state rewards of the model). - std::vector x = rewardModel.getStateRewardVector().toVector(model.getNondeterminismVariables(), odd, explicitMatrix.getRowGroupIndices()); + std::vector x = rewardModel.getStateRewardVector().toVector(odd); // Perform the matrix-vector multiplication. std::unique_ptr> solver = linearEquationSolverFactory.create(explicitMatrix); @@ -179,13 +179,16 @@ namespace storm { // Create the solution vector. std::vector x(model.getNumberOfStates(), storm::utility::zero()); + // Before cutting the non-maybe columns, we need to compute the sizes of the row groups. + storm::dd::Add stateActionAdd = (transitionMatrix.notZero().existsAbstract(model.getColumnVariables()) || totalRewardVector.notZero()).template toAdd(); + std::vector rowGroupSizes = stateActionAdd.sumAbstract(model.getNondeterminismVariables()).toVector(odd); + // Translate the symbolic matrix/vector to their explicit representations. - storm::storage::SparseMatrix explicitMatrix = transitionMatrix.toMatrix(model.getNondeterminismVariables(), odd, odd); - std::vector b = totalRewardVector.toVector(model.getNondeterminismVariables(), odd, explicitMatrix.getRowGroupIndices()); + std::pair, std::vector> explicitRepresentation = transitionMatrix.toMatrixVector(totalRewardVector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd); // Perform the matrix-vector multiplication. - std::unique_ptr> solver = linearEquationSolverFactory.create(explicitMatrix); - solver->performMatrixVectorMultiplication(dir, x, &b, stepBound); + std::unique_ptr> solver = linearEquationSolverFactory.create(explicitRepresentation.first); + solver->performMatrixVectorMultiplication(dir, x, &explicitRepresentation.second, stepBound); // Return a hybrid check result that stores the numerical values explicitly. return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), odd, x)); diff --git a/src/storage/dd/Add.cpp b/src/storage/dd/Add.cpp index 8120ab953..b51aab46c 100644 --- a/src/storage/dd/Add.cpp +++ b/src/storage/dd/Add.cpp @@ -390,48 +390,7 @@ namespace storm { internalAdd.composeWithExplicitVector(rowOdd, ddVariableIndices, result, std::plus()); return result; } - - template - std::vector Add::toVector(std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, std::vector const& groupOffsets) const { - std::set rowMetaVariables; - - // Prepare the proper sets of meta variables. - for (auto const& variable : this->getContainedMetaVariables()) { - if (groupMetaVariables.find(variable) != groupMetaVariables.end()) { - continue; - } - rowMetaVariables.insert(variable); - } - std::vector ddGroupVariableIndices; - for (auto const& variable : groupMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddGroupVariableIndices.push_back(ddVariable.getIndex()); - } - } - std::vector ddRowVariableIndices; - for (auto const& variable : rowMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddRowVariableIndices.push_back(ddVariable.getIndex()); - } - } - - // Use the group variables to split the ADD into separate ADDs for each group. - std::vector> groups = internalAdd.splitIntoGroups(ddGroupVariableIndices); - - // Now iterate over the groups and add them to the resulting vector. - std::vector result(groupOffsets.back(), storm::utility::zero()); - for (uint_fast64_t i = 0; i < groups.size(); ++i) { - internalAdd.composeWithExplicitVector(rowOdd, ddRowVariableIndices, groupOffsets, result, std::plus()); - - // FIXME: something more needed? modification of groupOffsets? - } - - return result; - } - template storm::storage::SparseMatrix Add::toMatrix() const { std::set rowVariables; diff --git a/src/storage/dd/Add.h b/src/storage/dd/Add.h index 6991a9dd6..120aef683 100644 --- a/src/storage/dd/Add.h +++ b/src/storage/dd/Add.h @@ -524,17 +524,6 @@ namespace storm { */ std::vector toVector(storm::dd::Odd const& rowOdd) const; - /*! - * Converts the ADD to a row-grouped vector. The given offset-labeled DD is used to determine the correct - * row group of each entry. Note that the group meta variables are assumed to be at the very top in the - * variable ordering. - * - * @param groupMetaVariables The meta variables responsible for the row-grouping. - * @param rowOdd The ODD used for determining the correct row. - * @return The vector that is represented by this ADD. - */ - std::vector toVector(std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, std::vector const& groupOffsets) const; - /*! * Converts the ADD to a (sparse) double matrix. All contained non-primed variables are assumed to encode the * row, whereas all primed variables are assumed to encode the column. diff --git a/src/storage/dd/cudd/InternalCuddAdd.h b/src/storage/dd/cudd/InternalCuddAdd.h index fab7cbef6..45abce994 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.h +++ b/src/storage/dd/cudd/InternalCuddAdd.h @@ -92,7 +92,7 @@ namespace storm { InternalAdd operator!() const; /*! - * Performs a logical or of the current anBd the given ADD. As a prerequisite, the operand ADDs need to be + * Performs a logical or of the current and the given ADD. As a prerequisite, the operand ADDs need to be * 0/1 ADDs. * * @param other The second ADD used for the operation. @@ -281,23 +281,23 @@ namespace storm { InternalAdd maximum(InternalAdd const& other) const; /*! - * Sum-abstracts from the given meta variables. + * Sum-abstracts from the given cube. * - * @param metaVariables The meta variables from which to abstract. + * @param cube The cube from which to abstract. */ InternalAdd sumAbstract(InternalBdd const& cube) const; /*! - * Min-abstracts from the given meta variables. + * Min-abstracts from the given cube. * - * @param metaVariables The meta variables from which to abstract. + * @param cube The cube from which to abstract. */ InternalAdd minAbstract(InternalBdd const& cube) const; /*! - * Max-abstracts from the given meta variables. + * Max-abstracts from the given cube. * - * @param metaVariables The meta variables from which to abstract. + * @param cube The cube from which to abstract. */ InternalAdd maxAbstract(InternalBdd const& cube) const; @@ -313,10 +313,11 @@ namespace storm { bool equalModuloPrecision(InternalAdd const& other, double precision, bool relative = true) const; /*! - * Swaps the given pairs of meta variables in the ADD. The pairs of meta variables must be guaranteed to have - * the same number of underlying ADD variables. + * Swaps the given pairs of DD variables in the ADD. The pairs of meta variables have to be represented by + * ADDs must have equal length. * - * @param metaVariablePairs A vector of meta variable pairs that are to be swapped for one another. + * @param from The vector that specifies the 'from' part of the variable renaming. + * @param to The vector that specifies the 'to' part of the variable renaming. * @return The resulting ADD. */ InternalAdd swapVariables(std::vector> const& from, std::vector> const& to) const; @@ -326,8 +327,7 @@ namespace storm { * variables. * * @param otherMatrix The matrix with which to multiply. - * @param summationMetaVariables The names of the meta variables over which to sum during the matrix- - * matrix multiplication. + * @param summationDdVariables The DD variables (represented as ADDs) over which to sum. * @return An ADD representing the result of the matrix-matrix multiplication. */ InternalAdd multiplyMatrix(InternalAdd const& otherMatrix, std::vector> const& summationDdVariables) const; @@ -406,6 +406,7 @@ namespace storm { /*! * Retrieves the number of encodings that are mapped to a non-zero value. * + * @param The number of DD variables contained in this ADD. * @return The number of encodings that are mapped to a non-zero value. */ virtual uint_fast64_t getNonZeroCount(uint_fast64_t numberOfDdVariables) const; @@ -478,12 +479,15 @@ namespace storm { * Exports the DD to the given file in the dot format. * * @param filename The name of the file to which the DD is to be exported. + * @param ddVariableNamesAsString The names of the DD variables to display in the dot file. */ void exportToDot(std::string const& filename, std::vector const& ddVariableNamesAsStrings) const; /*! * Retrieves an iterator that points to the first meta variable assignment with a non-zero function value. * + * @param fullDdManager The DD manager responsible for this ADD. + * @param metaVariables The meta variables contained in the ADD. * @param enumerateDontCareMetaVariables If set to true, all meta variable assignments are enumerated, even * if a meta variable does not at all influence the the function value. * @return An iterator that points to the first meta variable assignment with a non-zero function value. @@ -493,22 +497,80 @@ namespace storm { /*! * Retrieves an iterator that points past the end of the container. * + * @param fullDdManager The DD manager responsible for this ADD. * @param enumerateDontCareMetaVariables If set to true, all meta variable assignments are enumerated, even * if a meta variable does not at all influence the the function value. * @return An iterator that points past the end of the container. */ AddIterator end(std::shared_ptr const> fullDdManager, bool enumerateDontCareMetaVariables = true) const; + /*! + * Composes the ADD with an explicit vector by performing a specified function between the entries of this + * ADD and the explicit vector. + * + * @param odd The ODD to use for the translation from symbolic to explicit positions. + * @param ddVariableIndices The indices of the DD variables present in this ADD. + * @param targetVector The explicit vector that is to be composed with the ADD. The results are written to + * this vector again. + * @param function The function to perform in the composition. + */ void composeWithExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const; + /*! + * Composes the (row-grouped) ADD with an explicit vector by performing a specified function between the + * entries of this ADD and the explicit vector. + * + * @param odd The ODD to use for the translation from symbolic to explicit positions. + * @param ddVariableIndices The indices of the DD variables present in this ADD. + * @param offsets The offsets + * @param targetVector The explicit vector that is to be composed with the ADD. The results are written to + * this vector again. + * @param function The function to perform in the composition. + */ void composeWithExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector const& offsets, std::vector& targetVector, std::function const& function) const; + /*! + * Splits the ADD into several ADDs that differ in the encoding of the given group variables (given via indices). + * + * @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> splitIntoGroups(std::vector const& ddGroupVariableIndices) const; - void toMatrixComponents(std::vector const& rowGroupIndices, std::vector& rowIndications, std::vector>& columnsAndValues, Odd const& rowOdd, Odd const& columnOdd, std::vector const& ddRowVariableIndices, std::vector const& ddColumnVariableIndices, bool writeValues) 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). + * + * @param vector The vector to split (in addition to the current ADD). + * @param ddGroupVariableIndices The indices of the variables that are used to distinguish the groups. + * @return A vector of pairs of ADDs that are the separate groups of the current ADD and the vector, + * respectively (wrt. to the encoding of the given variables). + */ std::vector, InternalAdd>> splitIntoGroups(InternalAdd vector, std::vector const& ddGroupVariableIndices) const; + /*! + * Translates the ADD into the components needed for constructing a matrix. + * + * @param rowGroupIndices The row group indices. + * @param rowIndications The vector that is to be filled with the row indications. + * @param columnsAndValues The vector that is to be filled with the non-zero entries of the matrix. + * @param rowOdd The ODD used for translating the rows. + * @param columnOdd The ODD used for translating the columns. + * @param ddRowVariableIndices The variable indices of the row variables. + * @param ddColumnVariableIndices The variable indices of the column variables. + * @param writeValues A flag that indicates whether or not to write to the entry vector. If this is not set, + * only the row indications are modified. + */ + void toMatrixComponents(std::vector const& rowGroupIndices, std::vector& rowIndications, std::vector>& columnsAndValues, Odd const& rowOdd, Odd const& columnOdd, std::vector const& ddRowVariableIndices, std::vector const& ddColumnVariableIndices, bool writeValues) const; + + /*! + * Creates an ADD from the given explicit vector. + * + * @param ddManager The manager to use to built the ADD. + * @param values The explicit vector to encode. + * @param odd The ODD to use for the translation. + * @param ddVariableIndices The indices of the variables to use in the ADD. + */ static InternalAdd fromVector(InternalDdManager const* ddManager, std::vector const& values, storm::dd::Odd const& odd, std::vector const& ddVariableIndices); /*! @@ -559,6 +621,17 @@ 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 DDs into the groups using the given group variables. + * + * @param dd1 The first DD to split. + * @param dd2 The second DD to split. + * @param groups A vector that is to be filled with the DDs for 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. + */ void splitIntoGroupsRec(DdNode* dd1, DdNode* dd2, std::vector, InternalAdd>>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const; /*! diff --git a/src/storage/dd/cudd/InternalCuddBdd.h b/src/storage/dd/cudd/InternalCuddBdd.h index 7f74f0b79..38c31cdcb 100644 --- a/src/storage/dd/cudd/InternalCuddBdd.h +++ b/src/storage/dd/cudd/InternalCuddBdd.h @@ -12,14 +12,6 @@ #include "cuddObj.hh" namespace storm { - namespace logic { - enum class ComparisonType; - } - - namespace expressions { - class Variable; - } - namespace storage { class BitVector; } @@ -165,34 +157,34 @@ namespace storm { InternalBdd& complement(); /*! - * Existentially abstracts from the given meta variables. + * Existentially abstracts from the given cube. * - * @param metaVariables The meta variables from which to abstract. + * @param cube The cube from which to abstract. */ InternalBdd existsAbstract(InternalBdd const& cube) const; /*! - * Universally abstracts from the given meta variables. + * Universally abstracts from the given cube. * - * @param metaVariables The meta variables from which to abstract. + * @param cube The cube from which to abstract. */ InternalBdd universalAbstract(InternalBdd const& cube) const; /*! - * Swaps the given pairs of meta variables in the BDD. The pairs of meta variables must be guaranteed to have - * the same number of underlying BDD variables. + * Swaps the given pairs of DD variables in the BDD. The pairs of meta variables have to be represented by + * BDDs must have equal length. * - * @param metaVariablePairs A vector of meta variable pairs that are to be swapped for one another. + * @param from The vector that specifies the 'from' part of the variable renaming. + * @param to The vector that specifies the 'to' part of the variable renaming. * @return The resulting BDD. */ InternalBdd swapVariables(std::vector> const& from, std::vector> const& to) const; /*! - * Computes the logical and of the current and the given BDD and existentially abstracts from the given set - * of variables. + * Computes the logical and of the current and the given BDD and existentially abstracts from the given cube. * * @param other The second BDD for the logical and. - * @param existentialVariables The variables from which to existentially abstract. + * @param cube The cube to existentially abstract. * @return A BDD representing the result. */ InternalBdd andExists(InternalBdd const& other, InternalBdd const& cube) const; @@ -227,6 +219,7 @@ namespace storm { /*! * Retrieves the number of encodings that are mapped to a non-zero value. * + * @param The number of DD variables contained in this BDD. * @return The number of encodings that are mapped to a non-zero value. */ uint_fast64_t getNonZeroCount(uint_fast64_t numberOfDdVariables) const; @@ -270,6 +263,7 @@ namespace storm { * Exports the BDD to the given file in the dot format. * * @param filename The name of the file to which the BDD is to be exported. + * @param ddVariableNamesAsStrings The names of the variables to display in the dot file. */ void exportToDot(std::string const& filename, std::vector const& ddVariableNamesAsStrings) const; @@ -286,6 +280,7 @@ namespace storm { * each entry. * * @param rowOdd The ODD used for determining the correct row. + * @param ddVariableIndices The indices of the DD variables contained in this BDD. * @return The bit vector that is represented by this BDD. */ storm::storage::BitVector toVector(storm::dd::Odd const& rowOdd, std::vector const& ddVariableIndices) const; @@ -293,14 +288,37 @@ namespace storm { /*! * Creates an ODD based on the current BDD. * + * @param ddVariableIndices The indices of the DD variables contained in this BDD. * @return The corresponding ODD. */ Odd createOdd(std::vector const& ddVariableIndices) const; + /*! + * Uses the current BDD to filter values from the explicit vector. + * + * @param odd The ODD used to determine which entries to select. + * @param ddVariableIndices The indices of the DD variables contained in this BDD. + * @param sourceValues The source vector. + * @param targetValues The vector to which to write the selected values. + */ template void filterExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector const& sourceValues, std::vector& targetValues) const; private: + /*! + * Retrieves the CUDD BDD object associated with this DD. + * + * @return The CUDD BDD object associated with this DD. + */ + BDD getCuddBdd() const; + + /*! + * Retrieves the raw DD node of CUDD associated with this BDD. + * + * @return The DD node of CUDD associated with this BDD. + */ + DdNode* getCuddDdNode() const; + /*! * Builds a BDD representing the values that make the given filter function evaluate to true. * @@ -311,6 +329,7 @@ namespace storm { * @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. + * @param filter A function that determines which encodings are to be mapped to true. * @return The resulting (CUDD) BDD node. */ template @@ -369,20 +388,6 @@ namespace storm { template static void filterExplicitVectorRec(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); - /*! - * Retrieves the CUDD BDD object associated with this DD. - * - * @return The CUDD BDD object associated with this DD. - */ - BDD getCuddBdd() const; - - /*! - * Retrieves the raw DD node of CUDD associated with this BDD. - * - * @return The DD node of CUDD associated with this BDD. - */ - DdNode* getCuddDdNode() const; - InternalDdManager const* ddManager; BDD cuddBdd;