From a21715cbc38d249c9b060e7a06d95212b425f6d7 Mon Sep 17 00:00:00 2001 From: Mavo Date: Sat, 12 Mar 2016 00:15:47 +0100 Subject: [PATCH] Nested symmetries seem to work for at least binary symmetries Former-commit-id: dfa2052d1802239b4f8ae800a1a2b6cf14f97772 --- src/storage/dft/DFT.cpp | 27 ++++-- src/storage/dft/DFTStateGenerationInfo.h | 28 +++++- src/storage/dft/SymmetricUnits.h | 110 ++++++++++++++++++++++- 3 files changed, 155 insertions(+), 10 deletions(-) diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index e9b4c659e..dd771f230 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -110,22 +110,35 @@ namespace storm { visitQueue.push(mTopLevelIndex); stateIndex = performStateGenerationInfoDFS(generationInfo, visitQueue, visited, stateIndex); } else { - for (auto const& symmetryGroup : symmetries.groups) { - assert(!symmetryGroup.second.empty()); + for (size_t symmetryIndex : symmetries.sortedSymmetries) { + assert(!visited[symmetryIndex]); + auto const& symmetryGroup = symmetries.groups.at(symmetryIndex); + assert(!symmetryGroup.empty()); // Insert all elements of first subtree of each symmetry size_t groupIndex = stateIndex; - for (std::vector const& symmetryElement : symmetryGroup.second) { - stateIndex = generateStateInfo(generationInfo, symmetryElement[0], visited, stateIndex); + for (std::vector const& symmetryElement : symmetryGroup) { + if (visited[symmetryElement[0]]) { + groupIndex = std::min(groupIndex, generationInfo.getStateIndex(symmetryElement[0])); + } else { + stateIndex = generateStateInfo(generationInfo, symmetryElement[0], visited, stateIndex); + } } size_t offset = stateIndex - groupIndex; // Mirror symmetries - size_t noSymmetricElements = symmetryGroup.second.front().size(); + size_t noSymmetricElements = symmetryGroup.front().size(); assert(noSymmetricElements > 1); - for (std::vector symmetricElements : symmetryGroup.second) { + for (std::vector symmetricElements : symmetryGroup) { assert(symmetricElements.size() == noSymmetricElements); + if (visited[symmetricElements[1]]) { + // Elements already mirrored + for (size_t index : symmetricElements) { + assert(visited[index]); + } + continue; + } // Initialize for original element size_t originalElement = symmetricElements[0]; @@ -181,6 +194,8 @@ namespace storm { stateIndex = performStateGenerationInfoDFS(generationInfo, visitQueue, visited, stateIndex); } } + + generationInfo.generateSymmetries(symmetries); STORM_LOG_TRACE(generationInfo); assert(stateIndex == mStateVectorSize); diff --git a/src/storage/dft/DFTStateGenerationInfo.h b/src/storage/dft/DFTStateGenerationInfo.h index 4b3ef92c9..d4bbdee8b 100644 --- a/src/storage/dft/DFTStateGenerationInfo.h +++ b/src/storage/dft/DFTStateGenerationInfo.h @@ -10,7 +10,7 @@ namespace storm { std::vector mIdToStateIndex; // id -> index first bit in state std::map> mSeqRestrictionPreElements; // id -> list of restriction pre elements; std::map> mSeqRestrictionPostElements; // id -> list of restriction post elements; - std::vector>> mSymmetries; // pair (lenght of symmetry group, vector indicating the starting points of the symmetry groups) + std::vector>> mSymmetries; // pair (length of symmetry group, vector indicating the starting points of the symmetry groups) public: @@ -70,6 +70,32 @@ namespace storm { void addSymmetry(size_t length, std::vector& startingIndices) { mSymmetries.push_back(std::make_pair(length, startingIndices)); } + + /** + * Generate more symmetries by combining two symmetries + */ + void generateSymmetries(storm::storage::DFTIndependentSymmetries const& symmetries) { + for (size_t i = 0; i < mSymmetries.size(); ++i) { + size_t childStart = mSymmetries[i].second[0]; + size_t childLength = mSymmetries[i].first; + for (size_t j = i+1; j < mSymmetries.size(); ++j) { + size_t parentStart = mSymmetries[j].second[0]; + size_t parentLength = mSymmetries[j].first; + // Check if child lies in parent + if (parentStart <= childStart && childStart + childLength < parentStart + parentLength) { + // Get symmetric start by applying the bijection + std::vector newStarts; + for (size_t symmetryStarts : mSymmetries[i].second) { + newStarts.push_back(symmetryStarts + parentLength); + } + // Insert after child + mSymmetries.insert(mSymmetries.begin() + i + 1, std::make_pair(childLength, newStarts)); + ++i; + break; + } + } + } + } size_t getSymmetrySize() const { return mSymmetries.size(); diff --git a/src/storage/dft/SymmetricUnits.h b/src/storage/dft/SymmetricUnits.h index 58a70e492..33c8efeae 100644 --- a/src/storage/dft/SymmetricUnits.h +++ b/src/storage/dft/SymmetricUnits.h @@ -1,19 +1,123 @@ #pragma once +#include "src/utility/macros.h" + namespace storm { namespace storage { struct DFTIndependentSymmetries { std::map>> groups; + std::vector sortedSymmetries; + + bool existsInFirstSymmetry(size_t index, size_t value) { + for (std::vector symmetry : groups[index]) { + if (symmetry.front() == value) { + return true; + } + } + return false; + } + + bool existsInSymmetry(size_t index, size_t value) { + for (std::vector symmetry : groups[index]) { + for (size_t index : symmetry) { + if (index == value) { + return true; + } + } + } + return false; + } + + /** + * Apply symmetry and get bijection. Result is symmetry(value)[index] + * + * @param symmetry The symmetry. + * @param value The value to apply the bijection to. + * @param index The index of the symmetry group to apply. + * @return Symmetric value, -1 if the bijection could not be applied. + */ + int applySymmetry(std::vector> const& symmetry, size_t value, size_t index) const { + for (std::vector element : symmetry) { + if (element[0] == value) { + return element[index]; + } + } + return -1; + } + + std::vector> createSymmetry(std::vector> parentSymmetry, std::vector> childSymmetry, size_t index) { + std::vector> result; + for (std::vector childSymmetry : childSymmetry) { + std::vector symmetry; + for (size_t child : childSymmetry) { + int bijectionValue = applySymmetry(parentSymmetry, child, index); + if (bijectionValue >= 0) { + symmetry.push_back(bijectionValue); + } else { + return result; + } + } + result.push_back(symmetry); + } + return result; + } + + void sortHierarchical(size_t parent, std::vector& candidates) { + std::vector children; + for (int i = candidates.size() - 1; i >= 0; --i) { + size_t currentRoot = candidates[i]; + if (existsInSymmetry(parent, currentRoot)) { + // Is child + STORM_LOG_TRACE(currentRoot << " is child of " << parent); + children.insert(children.begin(), currentRoot); + candidates.erase(candidates.begin()+i); + } + } + for (size_t i = 0; i < children.size(); ++i) { + std::vector> possibleSymmetry = createSymmetry(groups.at(parent), groups.at(children[i]), 1); + for (size_t j = i + 1; j < children.size(); ++j) { + if (possibleSymmetry == groups.at(children[j])) { + STORM_LOG_TRACE("Child " << children[j] << " ignored as created by symmetries " << parent << " and " << children[j]); + groups.erase(children[j]); + children.erase(children.begin() + j); + } + } + } + while (!children.empty()) { + // Insert largest element + size_t largestChild = children.back(); + children.pop_back(); + sortHierarchical(largestChild, children); + sortedSymmetries.push_back(largestChild); + } + } + DFTIndependentSymmetries(std::map>> groups) : groups(groups) { + std::vector sortedGroups; + for (auto const& cl : groups) { + sortedGroups.push_back(cl.first); + } + // Sort by length of symmetry + std::sort(sortedGroups.begin(), sortedGroups.end(), [&](const size_t left, const size_t right) { + return groups.at(left).size() < groups.at(right).size(); + }); + // Sort hierarchical + while (!sortedGroups.empty()) { + // Insert largest element + size_t currentRoot = sortedGroups.back(); + sortedGroups.pop_back(); + sortHierarchical(currentRoot, sortedGroups); + sortedSymmetries.push_back(currentRoot); + } } }; inline std::ostream& operator<<(std::ostream& os, DFTIndependentSymmetries const& s) { - for(auto const& cl : s.groups) { - os << "Symmetry group for " << cl.first << std::endl; - for(auto const& eqClass : cl.second) { + for(size_t index : s.sortedSymmetries) { + os << "Symmetry group for " << index << std::endl; + for(auto const& eqClass : s.groups.at(index)) { for(auto const& i : eqClass) { os << i << " "; }