From 36c410875ca3dd432f3ba75ce679071bc6b68e52 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 2 Mar 2020 06:31:39 +0100 Subject: [PATCH] Revert "InternalAdds: Making the different splitIntoGroups implementations more consistent to each other (in the sense that the Dd is traversed in the same order)." This reverts commit cefe43f2bfd1b5201d3b5aedec53cfd626132456. Apparently, the GameBasedMdpModelCheckerTest does not terminate when the Dd groups are retrieved in a different order. See github issue #64 --- src/storm/storage/dd/Add.h | 10 ++++++++-- src/storm/storage/dd/cudd/InternalCuddAdd.cpp | 2 +- src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp | 2 +- 3 files changed, 10 insertions(+), 4 deletions(-) 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); } }