diff --git a/src/storm/storage/dd/Add.h b/src/storm/storage/dd/Add.h index 4ab7c2983..f74b75dd2 100644 --- a/src/storm/storage/dd/Add.h +++ b/src/storm/storage/dd/Add.h @@ -581,8 +581,10 @@ namespace storm { /*! * Converts the ADD to a row-grouped vector while respecting the row group sizes of the provided matrix. * That is, if the vector has a zero entry for some row in a row group for which the matrix has a non-zero - * row, the value at the vector will be correctly set to zero. Note: this function assumes that the meta - * variables used to distinguish different row groups are at the very top of the ADD. + * row, the value at the vector will be correctly set to zero. + * @note: This function assumes that the meta variables used to distinguish different row groups + * are at the very top of the ADD. + * @note: The order of the rows within the groups could be inconsistent with the order obtained by other toMatrix/toVector methods. * * @param matrix The symbolic matrix whose row group sizes to respect. * @param rowGroupIndices A vector specifying the sizes of the row groups. @@ -631,6 +633,7 @@ namespace storm { * 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. Note: this function assumes that * the meta variables used to distinguish different row groups are at the very top of the ADD. + * @note: The order of the rows within the groups could be inconsistent with the order obtained by other toMatrix/toVector methods. * * @param groupMetaVariables The meta variables that are used to distinguish different row groups. * @param rowOdd The ODD used for determining the correct row. @@ -644,6 +647,7 @@ namespace storm { * 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. + * @note: The order of the rows within the groups could be inconsistent with the order obtained by other toMatrix/toVector methods. * * @param rowMetaVariables The meta variables that encode the rows of the matrix. * @param columnMetaVariables The meta variables that encode the columns of the matrix. @@ -676,6 +680,7 @@ namespace storm { * 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. + * @note: The order of the rows within the groups could be inconsistent with the order obtained by other toMatrix/toVector methods. * * @param vector The symbolic vector to convert. * @param groupMetaVariables The meta variables that are used to distinguish different row groups. @@ -691,6 +696,7 @@ namespace storm { * 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. + * @note: The order of the rows within the groups could be inconsistent with the order obtained by other toMatrix/toVector methods. * * @param vectors The symbolic vectors to convert. * @param groupMetaVariables The meta variables that are used to distinguish different row groups. diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp index 98760a293..b988a6808 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp @@ -596,8 +596,8 @@ namespace storm { splitIntoGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); splitIntoGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); } else { - splitIntoGroupsRec(Cudd_T(dd), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); splitIntoGroupsRec(Cudd_E(dd), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + splitIntoGroupsRec(Cudd_T(dd), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); } } diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp index c8501a25f..3e3d9dfbc 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -1023,8 +1023,8 @@ namespace storm { bool elseComplemented = mtbdd_hascomp(elseDdNode) ^ negated; bool thenComplemented = mtbdd_hascomp(thenDdNode) ^ negated; - splitIntoGroupsRec(mtbdd_regular(thenDdNode), thenComplemented, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); splitIntoGroupsRec(mtbdd_regular(elseDdNode), elseComplemented, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + splitIntoGroupsRec(mtbdd_regular(thenDdNode), thenComplemented, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); } }