From 4284c633f4bbef188ef3d19713f0ba72c62a757e Mon Sep 17 00:00:00 2001 From: Mavo Date: Thu, 10 Mar 2016 16:56:28 +0100 Subject: [PATCH] StateGenerationInfo does not use DFS for symmetries Former-commit-id: 7111f5764a28aa38e3b7a751a8006a1e11fd0c8b --- src/storage/dft/DFT.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index c40fadceb..650712ebd 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -113,10 +113,11 @@ namespace storm { for (auto const& symmetryGroup : symmetries.groups) { assert(!symmetryGroup.second.empty()); - // Perform DFS for first subtree of each symmetry - visitQueue.push(symmetryGroup.first); + // Insert all elements of first subtree of each symmetry size_t groupIndex = stateIndex; - stateIndex = performStateGenerationInfoDFS(generationInfo, visitQueue, visited, stateIndex); + for (std::vector const& symmetryElement : symmetryGroup.second) { + stateIndex = generateStateInfo(generationInfo, symmetryElement[0], visited, stateIndex); + } size_t offset = stateIndex - groupIndex; // Mirror symmetries