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<typename ValueType>
+ DFTColouring<ValueType> DFT<ValueType>::colourDFT() const {
+ return DFTColouring<ValueType>(*this);
+ }
+
+ template<typename ValueType>
+ std::vector<std::vector<size_t>> DFT<ValueType>::findSymmetries(DFTColouring<ValueType> const& colouring) const {
+ std::vector<size_t> vec;
+ vec.reserve(nrElements());
+ storm::utility::iota_n(std::back_inserter(vec), 14, 0);
+ BijectionCandidates<ValueType> completeCategories = colouring.colourSubdft(vec);
+ std::vector<std::vector<size_t>> 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<size_t> sortedParent1Ids = getGate(*it1)->parentIds();
+ std::sort(sortedParent1Ids.begin(), sortedParent1Ids.end());
+ auto it2 = it1;
+ for(++it2; it2 != colourClass.second.cend(); ++it2) {
+ std::vector<size_t> 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<size_t> isubdft1 = getGate(*it1)->independentSubDft();
+ std::vector<size_t> 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<double>;
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<typename T> class DFTColouring;
+
+
/**
* Represents a Dynamic Fault Tree
*/
@@ -222,6 +227,11 @@ namespace storm {
std::string getStateString(DFTStatePointer const& state) const;
std::vector<size_t> getIndependentSubDftRoots(size_t index) const;
+
+ DFTColouring<ValueType> colourDFT() const;
+
+ std::vector<std::vector<size_t>> findSymmetries(DFTColouring<ValueType> 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 <cassert>
#include <vector>
#include <unordered_map>
+#include <utility>
#include "DFTElementType.h"
#include "DFTElements.h"
+#include "DFT.h"
namespace storm {
namespace storage {
@@ -34,14 +37,102 @@ namespace storage {
};
+
+ template<typename ValueType>
+ 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<typename ValueType>
+ bool operator==(BEColourClass<ValueType> const& lhs, BEColourClass<ValueType> const& rhs) {
+ return lhs.hash == rhs.hash && lhs.aRate == rhs.aRate && lhs.pRate == rhs.pRate;
+ }
+
+
+
+
/**
*
*/
template<typename ValueType>
- class BijectionCandidates {
- std::unordered_map<size_t, std::vector<size_t>> groupCandidates;
- std::unordered_map<std::pair<ValueType, ValueType>, std::vector<size_t>> beCandidates;
+ struct BijectionCandidates {
+ std::unordered_map<size_t, std::vector<size_t>> gateCandidates;
+ std::unordered_map<BEColourClass<ValueType>, std::vector<size_t>> beCandidates;
+ std::unordered_map<std::pair<ValueType, ValueType>, std::vector<size_t>> pdepCandidates;
+ };
+
+ template<typename ValueType>
+ class DFTColouring {
+ DFT<ValueType> const& dft;
+ std::unordered_map<size_t, size_t> gateColour;
+ std::unordered_map<size_t, BEColourClass<ValueType>> beColour;
+ std::unordered_map<size_t, std::pair<ValueType, ValueType>> depColour;
+ GateGroupToHash gateColourizer;
+
+ public:
+ DFTColouring(DFT<ValueType> 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<ValueType> colourSubdft(std::vector<size_t> const& subDftIndices) const {
+ BijectionCandidates<ValueType> 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<size_t>({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<size_t>({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<size_t>({index});
+ }
+ }
+
+ }
+ return res;
+ }
+
+
+ protected:
+ void colourize(std::shared_ptr<const DFTBE<ValueType>> const& be) {
+ beColour[be->id()] = BEColourClass<ValueType>(be->activeFailureRate(), be->passiveFailureRate(), be->nrParents());
+ }
+
+ void colourize(std::shared_ptr<const DFTGate<ValueType>> const& gate) {
+ gateColour[gate->id()] = gateColourizer(gate->type(), gate->nrChildren(), gate->nrParents(), 0, gate->rank());
+ }
+
+ void colourize(std::shared_ptr<const DFTDependency<ValueType>> const& dep) {
+ depColour[dep->id()] = std::pair<ValueType, ValueType>(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<typename ColourType>
+ void initializePermutationsAndTreatTrivialGroups(std::unordered_map<ColourType, std::vector<size_t>> const& left,
+ std::unordered_map<ColourType, std::vector<size_t>> const& right,
+ std::unordered_map<ColourType, std::vector<size_t>>& 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<typename ValueType>
+ struct hash<storm::storage::BEColourClass<ValueType>> {
+ size_t operator()(storm::storage::BEColourClass<ValueType> const& bcc) const {
+ std::hash<ValueType> hasher;
+ return (hasher(bcc.aRate) ^ hasher(bcc.pRate) << 8) | bcc.hash;
+ }
+ };
+
+ template<typename ValueType>
+ struct hash<std::pair<ValueType, ValueType>> {
+ size_t operator()(std::pair<ValueType, ValueType> const& p) const {
+ std::hash<ValueType> 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<class OutputIterator, class Size, class Assignable>
+ void iota_n(OutputIterator first, Size n, Assignable value)
+ {
+ std::generate_n(first, n, [&value]() {
+ return value++;
+ });
+ }
+ }
+}