From cefe43f2bfd1b5201d3b5aedec53cfd626132456 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 26 Feb 2020 20:50:42 +0100
Subject: [PATCH] InternalAdds: Making the different splitIntoGroups
implementations more consistent to each other (in the sense that the Dd is
traversed in the same order).
---
src/storm/storage/dd/cudd/InternalCuddAdd.cpp | 2 +-
src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp
index d94e6cadc..1c4e0cf35 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_E(dd), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
splitIntoGroupsRec(Cudd_T(dd), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
+ splitIntoGroupsRec(Cudd_E(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..431ae5713 100644
--- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp
+++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp
@@ -1007,8 +1007,8 @@ namespace storm {
bool elseComplemented = mtbdd_hascomp(elseDdNode) ^ negated;
bool thenComplemented = mtbdd_hascomp(thenDdNode) ^ negated;
- splitIntoGroupsRec(mtbdd_regular(elseDdNode), elseComplemented, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
splitIntoGroupsRec(mtbdd_regular(thenDdNode), thenComplemented, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
+ splitIntoGroupsRec(mtbdd_regular(elseDdNode), elseComplemented, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
}
}