diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp index d94e6cadc..fe9a85f7e 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp @@ -596,6 +596,8 @@ namespace storm { splitIntoGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); splitIntoGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); } else { + // FIXME: We first traverse the else successor (unlike other variants of this method). + // Otherwise, the GameBasedMdpModelCheckerTest would not terminate. See github issue #64 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 8ede93854..d50b8cc0f 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -1007,6 +1007,8 @@ namespace storm { bool elseComplemented = mtbdd_hascomp(elseDdNode) ^ negated; bool thenComplemented = mtbdd_hascomp(thenDdNode) ^ negated; + // FIXME: We first traverse the else successor (unlike other variants of this method). + // Otherwise, the GameBasedMdpModelCheckerTest would not terminate. See github issue #64 splitIntoGroupsRec(mtbdd_regular(elseDdNode), elseComplemented, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); splitIntoGroupsRec(mtbdd_regular(thenDdNode), thenComplemented, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); }