From 5d8419336f86084c262a6433d9ea985d887a2b8a Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 2 Mar 2020 06:34:28 +0100
Subject: [PATCH] InternalAdds: Added a comment related to GitHub issue #64
---
src/storm/storage/dd/cudd/InternalCuddAdd.cpp | 2 ++
src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp | 2 ++
2 files changed, 4 insertions(+)
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);
}