From 6685b358f07df97ae43890d90493e14fb76f7f7e Mon Sep 17 00:00:00 2001 From: Mavo Date: Mon, 22 Feb 2016 18:31:52 +0100 Subject: [PATCH] Symmetry mirrored in state vector Former-commit-id: 7e5a578c44d7c47637f5575621a648edeb13282f --- examples/dft/symmetry3.dft | 12 +++++++ examples/dft/symmetry4.dft | 12 +++++++ src/storage/dft/DFT.cpp | 73 ++++++++++++++++++++++++++++++-------- src/storage/dft/DFT.h | 2 +- 4 files changed, 84 insertions(+), 15 deletions(-) create mode 100644 examples/dft/symmetry3.dft create mode 100644 examples/dft/symmetry4.dft diff --git a/examples/dft/symmetry3.dft b/examples/dft/symmetry3.dft new file mode 100644 index 000000000..edda963f9 --- /dev/null +++ b/examples/dft/symmetry3.dft @@ -0,0 +1,12 @@ +toplevel "A"; +"A" and "B" "B'" "B''"; +"B" and "C" "D"; +"B'" and "C'" "D'"; +"B''" and "C''" "D''"; +"C" lambda=0.5 dorm=0; +"D" lambda=0.5 dorm=0; +"C'" lambda=0.5 dorm=0; +"D'" lambda=0.5 dorm=0; +"C''" lambda=0.5 dorm=0; +"D''" lambda=0.5 dorm=0; + diff --git a/examples/dft/symmetry4.dft b/examples/dft/symmetry4.dft new file mode 100644 index 000000000..f401fc241 --- /dev/null +++ b/examples/dft/symmetry4.dft @@ -0,0 +1,12 @@ +toplevel "A"; +"A" and "B" "B'" "C" "C'"; +"B" and "D" "E"; +"B'" and "D'" "E'"; +"C" or "F"; +"C'" or "F'"; +"D" lambda=0.5 dorm=0; +"E" lambda=0.5 dorm=0; +"D'" lambda=0.5 dorm=0; +"E'" lambda=0.5 dorm=0; +"F" lambda=0.5 dorm=0; +"F'" lambda=0.5 dorm=0; diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index c88fbee1c..03812c937 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -72,22 +72,60 @@ namespace storm { // Use symmetry // Collect all elements in the first subtree // TODO make recursive to use for nested subtrees - + DFTStateGenerationInfo generationInfo(nrElements()); // Perform DFS and insert all elements of subtree sequentially size_t stateIndex = 0; std::queue visitQueue; - std::set visited; - size_t firstRoot; + storm::storage::BitVector visited(nrElements(), false); + if (symmetries.groups.empty()) { - firstRoot = mTopLevelIndex; + // Perform DFS for whole tree + visitQueue.push(mTopLevelIndex); + stateIndex = performStateGenerationInfoDFS(generationInfo, visitQueue, visited, stateIndex); } else { - firstRoot = symmetries.groups.begin()->first; + // Perform DFS for first subtree of each symmetry + for (auto const& symmetryGroup : symmetries.groups) { + visitQueue.push(symmetryGroup.first); + size_t stateIndexBefore = stateIndex; + stateIndex = performStateGenerationInfoDFS(generationInfo, visitQueue, visited, stateIndex); + size_t offset = stateIndex - stateIndexBefore; + + // Mirror symmetries + assert(!symmetryGroup.second.empty()); + for (std::vector symmetricElements : symmetryGroup.second) { + assert(symmetricElements.size() > 1); + size_t originalElement = symmetricElements[0]; + size_t index = generationInfo.getStateIndex(originalElement); + size_t activationIndex = isRepresentative(originalElement) ? generationInfo.getSpareActivationIndex(originalElement) : 0; + size_t usageIndex = mElements[originalElement]->isSpareGate() ? generationInfo.getSpareUsageIndex(originalElement) : 0; + + // Mirror symmetry for each element + for (size_t i = 1; i < symmetricElements.size(); ++i) { + size_t symmetricElement = symmetricElements[i]; + visited.set(symmetricElement); + + generationInfo.addStateIndex(symmetricElement, index + offset * i); + stateIndex += 2; + + assert((activationIndex > 0) == isRepresentative(symmetricElement)); + if (activationIndex > 0) { + generationInfo.addSpareActivationIndex(symmetricElement, activationIndex + offset * i); + ++stateIndex; + } + + assert((usageIndex > 0) == mElements[symmetricElement]->isSpareGate()); + if (usageIndex > 0) { + generationInfo.addSpareUsageIndex(symmetricElement, usageIndex + offset * i); + stateIndex += generationInfo.usageInfoBits(); + } + } + } + } } - visitQueue.push(firstRoot); - stateIndex = performStateGenerationInfoDFS(generationInfo, visitQueue, visited, stateIndex); - + + // TODO symmetries in dependencies? // Consider dependencies for (size_t idDependency : getDependencies()) { std::shared_ptr const> dependency = getDependency(idDependency); @@ -96,24 +134,31 @@ namespace storm { visitQueue.push(dependency->dependentEvent()->id()); } stateIndex = performStateGenerationInfoDFS(generationInfo, visitQueue, visited, stateIndex); - - assert(stateIndex = mStateVectorSize); + + // Visit all remaining states + for (size_t i = 0; i < visited.size(); ++i) { + if (!visited[i]) { + visitQueue.push(i); + stateIndex = performStateGenerationInfoDFS(generationInfo, visitQueue, visited, stateIndex); + } + } STORM_LOG_TRACE(generationInfo); - + assert(stateIndex == mStateVectorSize); + assert(visited.full()); return generationInfo; } template - size_t DFT::performStateGenerationInfoDFS(DFTStateGenerationInfo& generationInfo, std::queue& visitQueue, std::set& visited, size_t stateIndex) const { + size_t DFT::performStateGenerationInfoDFS(DFTStateGenerationInfo& generationInfo, std::queue& visitQueue, storm::storage::BitVector& visited, size_t stateIndex) const { while (!visitQueue.empty()) { size_t id = visitQueue.front(); visitQueue.pop(); - if (visited.count(id) == 1) { + if (visited[id]) { // Already visited continue; } - visited.insert(id); + visited.set(id); DFTElementPointer element = mElements[id]; // Insert children diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h index d8d6aa9bc..d3da06776 100644 --- a/src/storage/dft/DFT.h +++ b/src/storage/dft/DFT.h @@ -128,7 +128,7 @@ namespace storm { DFTStateGenerationInfo buildStateGenerationInfo(storm::storage::DFTIndependentSymmetries const& symmetries) const; - size_t performStateGenerationInfoDFS(DFTStateGenerationInfo& generationInfo, std::queue& visitQueue, std::set& visited, size_t stateIndex) const; + size_t performStateGenerationInfoDFS(DFTStateGenerationInfo& generationInfo, std::queue& visitQueue, storm::storage::BitVector& visited, size_t stateIndex) const; size_t stateVectorSize() const { return mStateVectorSize;