diff --git a/src/storage/dft/DFTStateGenerationInfo.h b/src/storage/dft/DFTStateGenerationInfo.h index d4bbdee8b..e700d8700 100644 --- a/src/storage/dft/DFTStateGenerationInfo.h +++ b/src/storage/dft/DFTStateGenerationInfo.h @@ -75,22 +75,30 @@ namespace storm { * Generate more symmetries by combining two symmetries */ void generateSymmetries(storm::storage::DFTIndependentSymmetries const& symmetries) { + // Iterate over possible children for (size_t i = 0; i < mSymmetries.size(); ++i) { size_t childStart = mSymmetries[i].second[0]; size_t childLength = mSymmetries[i].first; + // Iterate over possible parents 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); + std::vector> newSymmetries; + for (size_t index = 1; index < mSymmetries[j].second.size(); ++index) { + // Get symmetric start by applying the bijection + std::vector newStarts; + for (size_t symmetryStarts : mSymmetries[i].second) { + newStarts.push_back(symmetryStarts + mSymmetries[j].second[index]); + } + newSymmetries.push_back(newStarts); } // Insert after child - mSymmetries.insert(mSymmetries.begin() + i + 1, std::make_pair(childLength, newStarts)); - ++i; + for (size_t index = 0; index < newSymmetries.size(); ++index) { + mSymmetries.insert(mSymmetries.begin() + i + 1 + index, std::make_pair(childLength, newSymmetries[index])); + } + i += mSymmetries[j].second.size(); break; } } diff --git a/src/storage/dft/SymmetricUnits.h b/src/storage/dft/SymmetricUnits.h index 33c8efeae..82d747115 100644 --- a/src/storage/dft/SymmetricUnits.h +++ b/src/storage/dft/SymmetricUnits.h @@ -64,6 +64,7 @@ namespace storm { } void sortHierarchical(size_t parent, std::vector& candidates) { + // Find subsymmetries of current symmetry std::vector children; for (int i = candidates.size() - 1; i >= 0; --i) { size_t currentRoot = candidates[i]; @@ -74,16 +75,23 @@ namespace storm { candidates.erase(candidates.begin()+i); } } + + // Find child symmetries which are created by parent and other child symmetries 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); + // Iterate over all possible symmetry groups + for (size_t index = 1; index < groups.at(parent).front().size(); ++index) { + std::vector> possibleSymmetry = createSymmetry(groups.at(parent), groups.at(children[i]), index); + 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[i]); + groups.erase(children[j]); + children.erase(children.begin() + j); + } } } } + + // Apply sorting recursively while (!children.empty()) { // Insert largest element size_t largestChild = children.back(); @@ -98,9 +106,9 @@ namespace storm { for (auto const& cl : groups) { sortedGroups.push_back(cl.first); } - // Sort by length of symmetry + // Sort by length of symmetry or (if equal) by lower first element std::sort(sortedGroups.begin(), sortedGroups.end(), [&](const size_t left, const size_t right) { - return groups.at(left).size() < groups.at(right).size(); + return groups.at(left).size() < groups.at(right).size() || (groups.at(left).size() == groups.at(right).size() && groups.at(left).front().front() < groups.at(left).front().front()); }); // Sort hierarchical