From 64d3273630181d7fedeef91f6987d7be1fea4126 Mon Sep 17 00:00:00 2001 From: sjunges Date: Tue, 9 Feb 2016 23:40:03 +0100 Subject: [PATCH] updates on isomorphism Former-commit-id: 7bc9a91eab0a2c9906cf17e00a9d5bbd03e73722 --- src/storage/dft/DFTElements.h | 1 - src/storage/dft/DFTIsomorphism.h | 190 +++++++++++++++++++++++++++++-- 2 files changed, 183 insertions(+), 8 deletions(-) diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index 663c5b230..fe340a43a 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -158,7 +158,6 @@ namespace storm { - protected: // virtual bool checkIsomorphicSubDftHelper(DFTElement const& otherElem, std::vector>& mapping, std::vector const& order ) const = 0; diff --git a/src/storage/dft/DFTIsomorphism.h b/src/storage/dft/DFTIsomorphism.h index 2b6016ca4..e9a58d559 100644 --- a/src/storage/dft/DFTIsomorphism.h +++ b/src/storage/dft/DFTIsomorphism.h @@ -1,25 +1,201 @@ #pragma once #include +#include +#include "DFTElementType.h" +#include "DFTElements.h" namespace storm { namespace storage { + + + struct GateGroupToHash { + static constexpr uint_fast64_t fivebitmask = (1 << 6) - 1; + static constexpr uint_fast64_t eightbitmaks = (1 << 8) - 1; + + /** + * Hash function, which ensures that the colours are sorted according to their rank. + */ + uint_fast64_t operator()(DFTElementType type, size_t nrChildren, size_t nrParents, size_t nrPDEPs, size_t rank) const { + // Sets first bit to 1 + uint_fast64_t groupHash = static_cast(1) << 63; + //Assumes 5 bits for the rank, + groupHash |= (static_cast(rank) & fivebitmask) << (62 - 5); + // 8 bits for the nrChildren, + groupHash |= (static_cast(nrChildren) & eightbitmaks) << (62 - 5 - 8); + // 5 bits for nrParents, + groupHash |= (static_cast(nrParents) & fivebitmask) << (62 - 5 - 8 - 5); + // 5 bits for nrPDEPs, + groupHash |= (static_cast(nrPDEPs) & fivebitmask) << (62 - 5 - 8 - 5 - 5); + // 5 bits for the type + groupHash |= (static_cast(type) & fivebitmask) << (62 - 5 - 8 - 5 - 5 - 5); + return groupHash; + } + + }; + /** - * Saves isomorphism between subtrees + * */ - class DFTIsomorphism { - std::vector> classes; + template + class BijectionCandidates { + std::unordered_map> groupCandidates; + std::unordered_map, std::vector> beCandidates; + }; + + + /** - * Saves sets of isomorphic subtrees + * Saves isomorphism between subtrees */ - class DFTIsomorphisms { - std::vector isomorphisms; + template + class DFTIsomorphismCheck { + /// Coloured nodes as provided by the input: left hand side + BijectionCandidates const& bleft; + /// Coloured nodes as provided by the input: right hand side. + BijectionCandidates const& bright; + /// Whether the colourings are compatible + bool candidatesCompatible = true; + /// Current bijection + std::map bijection; + /// Current permutations of right hand side groups which lead to the homomorphism. + /// Contains only colours with more than one member. + BijectionCandidates currentPermutations; + + public: + DFTIsomorphismCheck(BijectionCandidates const& left, BijectionCandidates const& right) : bleft(left), bright(right) + { + checkCompatibility(); + } + + /** + * Checks whether the candidates are compatible, that is, checks the colours and the number of members for each colour. + * @return True iff compatible, ie if the preliminary check allows for a isomorphism. + */ + bool compatible() { + return candidatesCompatible; + } + + + /** + * Returns the isomorphism + * Can only be called after the findIsomorphism procedure returned that an isomorphism has found. + * @see findIsomorphism + */ + std::vector> getIsomorphism() const { + + } - void addIsomorphismClass(DFTIsomorphism const &) { + /** + * Check whether an isomorphism exists. + * + * @return true iff an isomorphism exists. + */ + bool findIsomorphism() { + if(!candidatesCompatible) return false; + constructInitialBijection(); + while(!check()) { + // continue our search + if(!findNextBijection()) { + // No further bijections to check, no is + return false; + } + } + return true; + } + + protected: + + void constructInitialBijection() { + assert(candidatesCompatible); + // We first construct the currentPermutations, which helps to determine the current state of the check. + for(auto const& colour : bright.beCandidates) { + if(colour.second.size()>1) { + currentPermutations.beCandidates.insert(colour); + } + } + + for(auto const& colour : bright.groupCandidates) { + if(colour.second.size()>1) { + currentPermutations.groupCandidates.insert(colour); + } + } + + // Constructing the initial homomorphism based on the right hand side instead of the current permutations allows us + // to treat trivial and non-trivial classes in one go. + for(auto const& colour : bleft.beCandidates) { + zipVectorsIntoMap(colour.second, bright.beCandidates.find(colour.first)->second, bijection); + } + + for(auto const& colour : bleft.groupCandidates) { + zipVectorsIntoMap(colour.second, bright.groupCandidates.find(colour.first)->second, bijection); + } } + + bool findNextBijection() { + return false; + } + + + /** + * + */ + bool check() { + + } + + private: + /** + * Returns true if the colours are compatible. + */ + bool checkCompatibility() { + if(bleft.groupCandidates.size() != bright.groupCandidates.size()) { + candidatesCompatible = false; + } + else if(bleft.beCandidates.size() != bright.beCandidates.size()) { + candidatesCompatible = false; + } + else { + for (auto const &gc : bleft.groupCandidates) { + if (bright.groupCandidates.count(gc.first) == 0) { + candidatesCompatible = false; + break; + } + } + if(candidatesCompatible) { + for(auto const& bc : bleft.groupCandidates) { + if(bright.beCandidates.count(bc.first) == 0) { + candidatesCompatible = false; + break; + } + } + } + } + } + + /** + * Local helper function for the creation of bijections, should be hidden from api. + */ + void zipVectorsIntoMap(std::vector const& a, std::vector const& b, std::map& map) const { + // Assert should pass due to compatibility check + assert(a.size() == b.size()); + auto it = b.cbegin(); + for(size_t lIndex : a) { + assert(map.count(lIndex) == 0); + map[lIndex] = *it; + ++it; + } + } + + + //std::vector> computeNextCandidate(){ + + //} }; + + } // namespace storm::dft } // namespace storm