diff --git a/resources/examples/testfiles/dft/symmetry7.dft b/resources/examples/testfiles/dft/symmetry7.dft new file mode 100644 index 0000000000..0beba5d8c9 --- /dev/null +++ b/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; + diff --git a/src/storm-dft/storage/DFTIsomorphism.h b/src/storm-dft/storage/DFTIsomorphism.h index 4a4abb434f..c7f585685f 100644 --- a/src/storm-dft/storage/DFTIsomorphism.h +++ b/src/storm-dft/storage/DFTIsomorphism.h @@ -4,12 +4,9 @@ #include #include -#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 const& left, BijectionCandidates const& right, DFT 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 + bool checkCompatibility(std::unordered_map> const& left, std::unordered_map> 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; } diff --git a/src/storm-dft/utility/SymmetryFinder.cpp b/src/storm-dft/utility/SymmetryFinder.cpp index 0d71c92954..744ff4ef19 100644 --- a/src/storm-dft/utility/SymmetryFinder.cpp +++ b/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::findSymmetries(sto // Colour the DFT elements to find candidates for symmetries storm::dft::storage::DFTColouring colouring(dft); - std::vector vec; - vec.reserve(dft.nrElements()); - storm::utility::iota_n(std::back_inserter(vec), dft.nrElements(), 0); - storm::dft::storage::BijectionCandidates completeCategories = colouring.colourSubdft(vec); + std::vector subDftIndices(storm::utility::vector::buildVectorForRange(size_t(0), dft.nrElements())); + storm::dft::storage::BijectionCandidates completeCategories = colouring.colourSubdft(subDftIndices); std::map>> res; // Find symmetries for gates diff --git a/src/storm/utility/iota_n.h b/src/storm/utility/iota_n.h deleted file mode 100644 index 9f3115090e..0000000000 --- a/src/storm/utility/iota_n.h +++ /dev/null @@ -1,10 +0,0 @@ -#pragma once - -namespace storm { -namespace utility { -template -void iota_n(OutputIterator first, Size n, Assignable value) { - std::generate_n(first, n, [&value]() { return value++; }); -} -} // namespace utility -} // namespace storm diff --git a/src/test/storm-dft/storage/SymmetryTest.cpp b/src/test/storm-dft/storage/SymmetryTest.cpp index 6323dd215e..4bbe21ac31 100644 --- a/src/test/storm-dft/storage/SymmetryTest.cpp +++ b/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);