Fixed issue in DFT symmetry computation (#580)

Added compatibility check for corresponding colour class sizes.

resources/examples/testfiles/dft/symmetry7.dft

@@ -0,0 +1,13 @@
+toplevel "A";
+"A" or "M" "N";
+"M" and "M1" "M2" "M3" "M4";
+"N" and "N1" "N2" "N3" "N4";
+"M1" lambda=0.5 dorm=0;
+"M2" lambda=0.5 dorm=0;
+"M3" lambda=0.5 dorm=0;
+"M4" lambda=1 dorm=0;
+"N1" lambda=0.5 dorm=0;
+"N2" lambda=0.5 dorm=0;
+"N3" lambda=1 dorm=0;
+"N4" lambda=1 dorm=0;
+

src/storm-dft/storage/DFTIsomorphism.h

@@ -4,12 +4,9 @@
 #include <utility>
 #include <vector>
 
-#include "storm/exceptions/InvalidArgumentException.h"
-
 #include "storm-dft/storage/DFT.h"
 #include "storm-dft/storage/elements/DFTElementType.h"
 #include "storm-dft/storage/elements/DFTElements.h"
-
 #include "storm/exceptions/InvalidArgumentException.h"
 
 namespace storm::dft {
@@ -380,7 +377,7 @@ class DFTIsomorphismCheck {
    public:
     DFTIsomorphismCheck(BijectionCandidates<ValueType> const& left, BijectionCandidates<ValueType> const& right, DFT<ValueType> const& dft)
         : bleft(left), bright(right), dft(dft) {
-        checkCompatibility();
+        candidatesCompatible = checkCompatibility();
     }
 
     /**
@@ -565,52 +562,50 @@ class DFTIsomorphismCheck {
     }
 
    private:
-    /**
-     * Returns true if the colours are compatible.
+    /*!
+     * Check compatibility of colour classes for specific type.
+     * @param left Left candidates.
+     * @param right Right candidates.
+     * @return True iff left and right are compatible.
      */
-    bool checkCompatibility() {
-        if (bleft.gateCandidates.size() != bright.gateCandidates.size()) {
-            candidatesCompatible = false;
-            return false;
-        }
-        if (bleft.beCandidates.size() != bright.beCandidates.size()) {
-            candidatesCompatible = false;
-            return false;
-        }
-        if (bleft.pdepCandidates.size() != bright.pdepCandidates.size()) {
-            candidatesCompatible = false;
-            return false;
-        }
-        if (bleft.restrictionCandidates.size() != bright.restrictionCandidates.size()) {
-            candidatesCompatible = false;
+    template<typename ColourType>
+    bool checkCompatibility(std::unordered_map<ColourType, std::vector<size_t>> const& left, std::unordered_map<ColourType, std::vector<size_t>> const& right) {
+        if (left.size() != right.size()) {
+            // Different number of colour classes
             return false;
         }
 
-        for (auto const& gc : bleft.gateCandidates) {
-            if (bright.gateCandidates.count(gc.first) == 0) {
-                candidatesCompatible = false;
+        for (auto const& gc : left) {
+            auto it = right.find(gc.first);
+            if (it == right.end()) {
+                // No corresponding colour
                 return false;
-            }
-        }
-        for (auto const& bc : bleft.beCandidates) {
-            if (bright.beCandidates.count(bc.first) == 0) {
-                candidatesCompatible = false;
+            } else if (it->second.size() != gc.second.size()) {
+                // Corresponding colour classes have different number of elements
                 return false;
             }
         }
+        return true;
+    }
 
-        for (auto const& dc : bleft.pdepCandidates) {
-            if (bright.pdepCandidates.count(dc.first) == 0) {
-                candidatesCompatible = false;
-                return false;
-            }
+    /*!
+     * Check if colour classes are compatible in principle.
+     * This checks only excludes non-compatible colour classes. In the positive case, further checks are necessary.
+     *
+     * @return True iff colours are compatible.
+     */
+    bool checkCompatibility() {
+        if (!checkCompatibility(bleft.gateCandidates, bright.gateCandidates)) {
+            return false;
         }
-
-        for (auto const& dc : bleft.restrictionCandidates) {
-            if (bright.restrictionCandidates.count(dc.first) == 0) {
-                candidatesCompatible = false;
-                return false;
-            }
+        if (!checkCompatibility(bleft.beCandidates, bright.beCandidates)) {
+            return false;
+        }
+        if (!checkCompatibility(bleft.pdepCandidates, bright.pdepCandidates)) {
+            return false;
+        }
+        if (!checkCompatibility(bleft.restrictionCandidates, bright.restrictionCandidates)) {
+            return false;
         }
         return true;
     }

src/storm-dft/utility/SymmetryFinder.cpp

@@ -1,8 +1,7 @@
 #include "SymmetryFinder.h"
 
 #include "storm-dft/storage/DFTIsomorphism.h"
-
-#include "storm/utility/iota_n.h"
+#include "storm/utility/vector.h"
 
 namespace storm::dft {
 namespace utility {
@@ -12,10 +11,8 @@ storm::dft::storage::DftSymmetries SymmetryFinder<ValueType>::findSymmetries(sto
     // Colour the DFT elements to find candidates for symmetries
     storm::dft::storage::DFTColouring<ValueType> colouring(dft);
 
-    std::vector<size_t> vec;
-    vec.reserve(dft.nrElements());
-    storm::utility::iota_n(std::back_inserter(vec), dft.nrElements(), 0);
-    storm::dft::storage::BijectionCandidates<ValueType> completeCategories = colouring.colourSubdft(vec);
+    std::vector<size_t> subDftIndices(storm::utility::vector::buildVectorForRange(size_t(0), dft.nrElements()));
+    storm::dft::storage::BijectionCandidates<ValueType> completeCategories = colouring.colourSubdft(subDftIndices);
     std::map<size_t, std::vector<std::vector<size_t>>> res;
 
     // Find symmetries for gates

src/test/storm-dft/storage/SymmetryTest.cpp

@@ -136,6 +136,15 @@ TEST(SymmetryTest, SymmetricFT) {
     EXPECT_EQ(symmetries.getSymmetryGroup(2).size(), 3ul);
     EXPECT_EQ(symmetries.getSymmetryGroup(2)[0].size(), 3ul);
 
+    symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/symmetry7.dft");
+    EXPECT_EQ(symmetries.nrSymmetries(), 3ul);
+    EXPECT_EQ(symmetries.getSymmetryGroup(0).size(), 1ul);
+    EXPECT_EQ(symmetries.getSymmetryGroup(0)[0].size(), 3ul);
+    EXPECT_EQ(symmetries.getSymmetryGroup(5).size(), 1ul);
+    EXPECT_EQ(symmetries.getSymmetryGroup(5)[0].size(), 2ul);
+    EXPECT_EQ(symmetries.getSymmetryGroup(7).size(), 1ul);
+    EXPECT_EQ(symmetries.getSymmetryGroup(7)[0].size(), 2ul);
+
     symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/pdep_symmetry.dft");
     EXPECT_EQ(symmetries.nrSymmetries(), 2ul);
     EXPECT_EQ(symmetries.getSymmetryGroup(2).size(), 4ul);