From 1e4dbb1e582820109a98bc2cb54878f3b59342d6 Mon Sep 17 00:00:00 2001 From: Mavo Date: Tue, 23 Feb 2016 13:52:06 +0100 Subject: [PATCH] More preparations for counting abstraction Former-commit-id: b283b28fdd41a254f82d5c8ece22286a77b4eeac --- src/storage/dft/DFT.cpp | 72 ++++++++++++++++++++++++++--------------- src/storage/dft/DFT.h | 29 +++++++++++++++++ 2 files changed, 75 insertions(+), 26 deletions(-) diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index 03812c937..b61425953 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -85,22 +85,28 @@ namespace storm { visitQueue.push(mTopLevelIndex); stateIndex = performStateGenerationInfoDFS(generationInfo, visitQueue, visited, stateIndex); } else { - // Perform DFS for first subtree of each symmetry for (auto const& symmetryGroup : symmetries.groups) { + assert(!symmetryGroup.second.empty()); + + // Perform DFS for first subtree of each symmetry visitQueue.push(symmetryGroup.first); - size_t stateIndexBefore = stateIndex; + size_t groupIndex = stateIndex; stateIndex = performStateGenerationInfoDFS(generationInfo, visitQueue, visited, stateIndex); - size_t offset = stateIndex - stateIndexBefore; - + size_t offset = stateIndex - groupIndex; + // Mirror symmetries - assert(!symmetryGroup.second.empty()); + size_t noSymmetricElements = symmetryGroup.second.front().size(); + assert(noSymmetricElements > 1); + for (std::vector symmetricElements : symmetryGroup.second) { - assert(symmetricElements.size() > 1); + assert(symmetricElements.size() == noSymmetricElements); + + // Initialize for original element 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]; @@ -122,6 +128,13 @@ namespace storm { } } } + + // Store starting indices of symmetry groups + std::vector symmetryIndices; + for (size_t i = 0; i < noSymmetricElements; ++i) { + symmetryIndices.push_back(groupIndex + i * offset); + } + generationInfo.addSymmetry(offset, symmetryIndices); } } @@ -146,9 +159,32 @@ namespace storm { STORM_LOG_TRACE(generationInfo); assert(stateIndex == mStateVectorSize); assert(visited.full()); + return generationInfo; } + template + size_t DFT::generateStateInfo(DFTStateGenerationInfo& generationInfo, size_t id, storm::storage::BitVector& visited, size_t stateIndex) const { + assert(!visited[id]); + visited.set(id); + + // Reserve bits for element + generationInfo.addStateIndex(id, stateIndex); + stateIndex += 2; + + if (isRepresentative(id)) { + generationInfo.addSpareActivationIndex(id, stateIndex); + ++stateIndex; + } + + if (mElements[id]->isSpareGate()) { + generationInfo.addSpareUsageIndex(id, stateIndex); + stateIndex += generationInfo.usageInfoBits(); + } + + return stateIndex; + } + template size_t DFT::performStateGenerationInfoDFS(DFTStateGenerationInfo& generationInfo, std::queue& visitQueue, storm::storage::BitVector& visited, size_t stateIndex) const { while (!visitQueue.empty()) { @@ -158,30 +194,14 @@ namespace storm { // Already visited continue; } - visited.set(id); - DFTElementPointer element = mElements[id]; + stateIndex = generateStateInfo(generationInfo, id, visited, stateIndex); // Insert children - if (element->isGate()) { - for (auto const& child : std::static_pointer_cast>(element)->children()) { + if (mElements[id]->isGate()) { + for (auto const& child : std::static_pointer_cast>(mElements[id])->children()) { visitQueue.push(child->id()); } } - - // Reserve bits for element - generationInfo.addStateIndex(id, stateIndex); - stateIndex += 2; - - if (isRepresentative(id)) { - generationInfo.addSpareActivationIndex(id, stateIndex); - ++stateIndex; - } - - if (element->isSpareGate()) { - generationInfo.addSpareUsageIndex(id, stateIndex); - stateIndex += generationInfo.usageInfoBits(); - } - } return stateIndex; } diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h index d3da06776..22d001aaf 100644 --- a/src/storage/dft/DFT.h +++ b/src/storage/dft/DFT.h @@ -41,6 +41,7 @@ namespace storm { std::map mSpareUsageIndex; // id spare -> index first bit in state std::map mSpareActivationIndex; // id spare representative -> index in state std::vector mIdToStateIndex; // id -> index first bit in state + std::vector>> mSymmetries; // pair (lenght of symmetry group, vector indicating the starting points of the symmetry groups) public: @@ -79,6 +80,24 @@ namespace storm { return mSpareActivationIndex.at(id); } + size_t addSymmetry(size_t lenght, std::vector& startingIndices) { + mSymmetries.push_back(std::make_pair(lenght, startingIndices)); + } + + size_t getSymmetrySize() { + return mSymmetries.size(); + } + + size_t getSymmetryLength(size_t pos) { + assert(pos < mSymmetries.size()); + return mSymmetries[pos].first; + } + + std::vector const& getSymmetryIndices(size_t pos) { + assert(pos < mSymmetries.size()); + return mSymmetries[pos].second; + } + friend std::ostream& operator<<(std::ostream& os, DFTStateGenerationInfo const& info) { os << "Id to state index:" << std::endl; for (size_t id = 0; id < info.mIdToStateIndex.size(); ++id) { @@ -92,6 +111,14 @@ namespace storm { for (auto pair : info.mSpareActivationIndex) { os << pair.first << " -> " << pair.second << std::endl; } + os << "Symmetries:" << std::endl; + for (auto pair : info.mSymmetries) { + os << "Length: " << pair.first << ", starting indices: "; + for (size_t index : pair.second) { + os << index << ", "; + } + os << std::endl; + } return os; } @@ -127,6 +154,8 @@ namespace storm { DFT(DFTElementVector const& elements, DFTElementPointer const& tle); DFTStateGenerationInfo buildStateGenerationInfo(storm::storage::DFTIndependentSymmetries const& symmetries) const; + + size_t generateStateInfo(DFTStateGenerationInfo& generationInfo, size_t id, storm::storage::BitVector& visited, size_t stateIndex) const; size_t performStateGenerationInfoDFS(DFTStateGenerationInfo& generationInfo, std::queue& visitQueue, storm::storage::BitVector& visited, size_t stateIndex) const;