From 0a9f68ed7478428876a0d5d3c51ddb952945535f Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 17 Feb 2016 19:49:01 +0100 Subject: [PATCH] update dft towards cnt.abst Former-commit-id: bce7a7a566ac7f6a9f62d66e8e16429d6a255fac --- src/storage/dft/DFT.cpp | 40 ++++++ src/storage/dft/DFT.h | 10 ++ src/storage/dft/DFTIsomorphism.h | 205 +++++++++++++++++++++++++++---- src/utility/iota_n.h | 13 ++ 4 files changed, 242 insertions(+), 26 deletions(-) create mode 100644 src/utility/iota_n.h diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index a23a70f71..0dedd9fb3 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -3,6 +3,9 @@ #include "DFT.h" #include "src/exceptions/NotSupportedException.h" +#include "DFTIsomorphism.h" +#include "utility/iota_n.h" + namespace storm { namespace storage { @@ -168,6 +171,43 @@ namespace storm { return ISD; } + template + DFTColouring DFT::colourDFT() const { + return DFTColouring(*this); + } + + template + std::vector> DFT::findSymmetries(DFTColouring const& colouring) const { + std::vector vec; + vec.reserve(nrElements()); + storm::utility::iota_n(std::back_inserter(vec), 14, 0); + BijectionCandidates completeCategories = colouring.colourSubdft(vec); + std::vector> res; + for(auto const& colourClass : completeCategories.gateCandidates) { + if(colourClass.second.size() > 1) { + for(auto it1 = colourClass.second.cbegin(); it1 != colourClass.second.cend(); ++it1) { + std::vector sortedParent1Ids = getGate(*it1)->parentIds(); + std::sort(sortedParent1Ids.begin(), sortedParent1Ids.end()); + auto it2 = it1; + for(++it2; it2 != colourClass.second.cend(); ++it2) { + std::vector sortedParent2Ids = getGate(*it2)->parentIds(); + std::sort(sortedParent2Ids.begin(), sortedParent2Ids.end()); + if(sortedParent1Ids == sortedParent2Ids) { + std::cout << "Considering ids " << *it1 << ", " << *it2 << " for isomorphism." << std::endl; + std::vector isubdft1 = getGate(*it1)->independentSubDft(); + std::vector isubdft2 = getGate(*it2)->independentSubDft(); + if(!isubdft1.empty() && !isubdft2.empty() && isubdft1.size() == isubdft2.size()) { + std::cout << "Checking subdfts from " << *it1 << ", " << *it2 << " for isomorphism." << std::endl; + } + } + } + } + } + } + return res; + } + + // Explicitly instantiate the class. template class DFT; diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h index ecea467e4..f2036e7d7 100644 --- a/src/storage/dft/DFT.h +++ b/src/storage/dft/DFT.h @@ -29,6 +29,11 @@ namespace storm { } }; + + // Forward declarations + template class DFTColouring; + + /** * Represents a Dynamic Fault Tree */ @@ -222,6 +227,11 @@ namespace storm { std::string getStateString(DFTStatePointer const& state) const; std::vector getIndependentSubDftRoots(size_t index) const; + + DFTColouring colourDFT() const; + + std::vector> findSymmetries(DFTColouring const& colouring) const; + private: bool elementIndicesCorrect() const { for(size_t i = 0; i < mElements.size(); ++i) { diff --git a/src/storage/dft/DFTIsomorphism.h b/src/storage/dft/DFTIsomorphism.h index e9a58d559..6258b05bc 100644 --- a/src/storage/dft/DFTIsomorphism.h +++ b/src/storage/dft/DFTIsomorphism.h @@ -1,9 +1,12 @@ #pragma once +#include #include #include +#include #include "DFTElementType.h" #include "DFTElements.h" +#include "DFT.h" namespace storm { namespace storage { @@ -34,14 +37,102 @@ namespace storage { }; + + template + struct BEColourClass { + BEColourClass() = default; + BEColourClass(ValueType a, ValueType p, size_t h) : aRate(a), pRate(p), hash(h) {} + + ValueType aRate; + ValueType pRate; + size_t hash; + }; + + template + bool operator==(BEColourClass const& lhs, BEColourClass const& rhs) { + return lhs.hash == rhs.hash && lhs.aRate == rhs.aRate && lhs.pRate == rhs.pRate; + } + + + + /** * */ template - class BijectionCandidates { - std::unordered_map> groupCandidates; - std::unordered_map, std::vector> beCandidates; + struct BijectionCandidates { + std::unordered_map> gateCandidates; + std::unordered_map, std::vector> beCandidates; + std::unordered_map, std::vector> pdepCandidates; + }; + + template + class DFTColouring { + DFT const& dft; + std::unordered_map gateColour; + std::unordered_map> beColour; + std::unordered_map> depColour; + GateGroupToHash gateColourizer; + + public: + DFTColouring(DFT const& ft) : dft(ft) { + for(size_t id = 0; id < dft.nrElements(); ++id ) { + if(dft.isBasicElement(id)) { + colourize(dft.getBasicElement(id)); + } else if(dft.isGate(id)) { + colourize(dft.getGate(id)); + } else { + assert(dft.isDependency(id)); + colourize(dft.getDependency(id)); + } + } + } + + BijectionCandidates colourSubdft(std::vector const& subDftIndices) const { + BijectionCandidates res; + for (size_t index : subDftIndices) { + if(dft.isBasicElement(index)) { + auto it = res.beCandidates.find(beColour.at(index)); + if(it != res.beCandidates.end()) { + it->second.push_back(index); + } else { + res.beCandidates[beColour.at(index)] = std::vector({index}); + } + } else if(dft.isGate(index)) { + auto it = res.gateCandidates.find(gateColour.at(index)); + if(it != res.gateCandidates.end()) { + it->second.push_back(index); + } else { + res.gateCandidates[gateColour.at(index)] = std::vector({index}); + } + } else { + assert(dft.isDependency(index)); + auto it = res.pdepCandidates.find(depColour.at(index)); + if(it != res.pdepCandidates.end()) { + it->second.push_back(index); + } else { + res.pdepCandidates[depColour.at(index)] = std::vector({index}); + } + } + + } + return res; + } + + + protected: + void colourize(std::shared_ptr> const& be) { + beColour[be->id()] = BEColourClass(be->activeFailureRate(), be->passiveFailureRate(), be->nrParents()); + } + + void colourize(std::shared_ptr> const& gate) { + gateColour[gate->id()] = gateColourizer(gate->type(), gate->nrChildren(), gate->nrParents(), 0, gate->rank()); + } + + void colourize(std::shared_ptr> const& dep) { + depColour[dep->id()] = std::pair(dep->probability(), dep->dependentEvent()->activeFailureRate()); + } }; @@ -107,36 +198,61 @@ namespace storage { } protected: - + /** + * Construct the initial bijection. + */ 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); + initializePermutationsAndTreatTrivialGroups(bleft.beCandidates, bright.beCandidates, currentPermutations.beCandidates); + initializePermutationsAndTreatTrivialGroups(bleft.gateCandidates, bright.gateCandidates, currentPermutations.gateCandidates); + initializePermutationsAndTreatTrivialGroups(bleft.pdepCandidates, bright.pdepCandidates, currentPermutations.pdepCandidates); + } + + /** + * Construct the next bijection + * @return true if a next bijection exists. + */ + bool findNextBijection() { + bool foundNext = false; + if(!currentPermutations.beCandidates.empty()) { + auto it = currentPermutations.beCandidates.begin(); + while(!foundNext && it == currentPermutations.beCandidates.end()) { + foundNext = std::next_permutation(it->second.begin(), it->second.end()); + ++it; } } - - for(auto const& colour : bright.groupCandidates) { - if(colour.second.size()>1) { - currentPermutations.groupCandidates.insert(colour); + if(!foundNext && !currentPermutations.gateCandidates.empty()) { + auto it = currentPermutations.gateCandidates.begin(); + while(!foundNext && it == currentPermutations.beCandidates.end()) { + foundNext = std::next_permutation(it->second.begin(), it->second.end()); + ++it; } } - // 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); + if(!foundNext && !currentPermutations.pdepCandidates.empty()) { + auto it = currentPermutations.pdepCandidates.begin(); + while(!foundNext && it == currentPermutations.pdepCandidates.end()) { + foundNext = std::next_permutation(it->second.begin(), it->second.end()); + ++it; + } } - for(auto const& colour : bleft.groupCandidates) { - zipVectorsIntoMap(colour.second, bright.groupCandidates.find(colour.first)->second, bijection); - } + if(foundNext) { + for(auto const& colour : bleft.beCandidates) { + zipVectorsIntoMap(colour.second, currentPermutations.beCandidates.find(colour.first)->second, bijection); + } - } + for(auto const& colour : bleft.gateCandidates) { + zipVectorsIntoMap(colour.second, currentPermutations.gateCandidates.find(colour.first)->second, bijection); + } - bool findNextBijection() { - return false; + for(auto const& colour : bleft.pdepCandidates) { + zipVectorsIntoMap(colour.second, currentPermutations.pdepCandidates.find(colour.first)->second, bijection); + } + } + + return foundNext; } @@ -152,21 +268,21 @@ namespace storage { * Returns true if the colours are compatible. */ bool checkCompatibility() { - if(bleft.groupCandidates.size() != bright.groupCandidates.size()) { + if(bleft.gateCandidates.size() != bright.gateCandidates.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) { + for (auto const &gc : bleft.gateCandidates) { + if (bright.gateCandidates.count(gc.first) == 0) { candidatesCompatible = false; break; } } if(candidatesCompatible) { - for(auto const& bc : bleft.groupCandidates) { + for(auto const& bc : bleft.gateCandidates) { if(bright.beCandidates.count(bc.first) == 0) { candidatesCompatible = false; break; @@ -176,6 +292,26 @@ namespace storage { } } + /** + * + */ + template + void initializePermutationsAndTreatTrivialGroups(std::unordered_map> const& left, + std::unordered_map> const& right, + std::unordered_map>& permutations) { + for(auto const& colour : right) { + if(colour.second.size()>1) { + auto it = permutations.insert(colour); + std::sort(it->second.begin(), it->second.end()); + zipVectorsIntoMap(colour.second, permutations.find(colour.first)->second, bijection); + } else { + assert(colour.second.size() == 1); + assert(bijection.count(left[colour.first].front()) == 0); + bijection[left[colour.first].front()] = colour.second.front(); + } + } + } + /** * Local helper function for the creation of bijections, should be hidden from api. */ @@ -184,7 +320,6 @@ namespace storage { assert(a.size() == b.size()); auto it = b.cbegin(); for(size_t lIndex : a) { - assert(map.count(lIndex) == 0); map[lIndex] = *it; ++it; } @@ -199,3 +334,21 @@ namespace storage { } // namespace storm::dft } // namespace storm + +namespace std { + template + struct hash> { + size_t operator()(storm::storage::BEColourClass const& bcc) const { + std::hash hasher; + return (hasher(bcc.aRate) ^ hasher(bcc.pRate) << 8) | bcc.hash; + } + }; + + template + struct hash> { + size_t operator()(std::pair const& p) const { + std::hash hasher; + return hasher(p.first) ^ hasher(p.second); + } + }; +} \ No newline at end of file diff --git a/src/utility/iota_n.h b/src/utility/iota_n.h new file mode 100644 index 000000000..a7e4ba829 --- /dev/null +++ b/src/utility/iota_n.h @@ -0,0 +1,13 @@ +#pragma once + +namespace storm { + namespace utility { + template + void iota_n(OutputIterator first, Size n, Assignable value) + { + std::generate_n(first, n, [&value]() { + return value++; + }); + } + } +}