Symred on mcs seems to work now

Former-commit-id: d6a830f8a1

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<size_t> newStarts;
-                            for (size_t symmetryStarts : mSymmetries[i].second) {
-                                newStarts.push_back(symmetryStarts + parentLength);
+                            std::vector<std::vector<size_t>> newSymmetries;
+                            for (size_t index = 1; index < mSymmetries[j].second.size(); ++index) {
+                                // Get symmetric start by applying the bijection
+                                std::vector<size_t> 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;
                         }
                     }

src/storage/dft/SymmetricUnits.h

@@ -64,6 +64,7 @@ namespace storm {
             }
             
             void sortHierarchical(size_t parent, std::vector<size_t>& candidates) {
+                // Find subsymmetries of current symmetry
                 std::vector<size_t> 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<std::vector<size_t>> 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<std::vector<size_t>> 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