From cc92085a15de67a6c7a3bc942183429214088f71 Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 18 Feb 2016 16:40:44 +0100 Subject: [PATCH 01/10] bijection check for homomorphism Former-commit-id: bf7f2f40662f11c6fbb1772bdc216eb17253ad12 --- src/storage/dft/DFT.cpp | 17 +++++++++++-- src/storage/dft/DFTIsomorphism.h | 43 ++++++++++++++++++++++++++------ 2 files changed, 51 insertions(+), 9 deletions(-) diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index 5735af2a7..e231c7c8d 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -180,20 +180,29 @@ namespace storm { std::vector> DFT::findSymmetries(DFTColouring const& colouring) const { std::vector vec; vec.reserve(nrElements()); - storm::utility::iota_n(std::back_inserter(vec), 14, 0); + storm::utility::iota_n(std::back_inserter(vec), nrElements(), 0); BijectionCandidates completeCategories = colouring.colourSubdft(vec); std::vector> res; + for(auto const& colourClass : completeCategories.gateCandidates) { if(colourClass.second.size() > 1) { + std::vector handledWithinClass; for(auto it1 = colourClass.second.cbegin(); it1 != colourClass.second.cend(); ++it1) { + if(!getGate(*it1)->hasOnlyStaticParents()) { + continue; + } std::vector sortedParent1Ids = getGate(*it1)->parentIds(); std::sort(sortedParent1Ids.begin(), sortedParent1Ids.end()); auto it2 = it1; for(++it2; it2 != colourClass.second.cend(); ++it2) { + if(!getGate(*it2)->hasOnlyStaticParents()) { + continue; + } 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; + bool isSymmetry = false; std::vector isubdft1 = getGate(*it1)->independentSubDft(); std::vector isubdft2 = getGate(*it2)->independentSubDft(); if(!isubdft1.empty() && !isubdft2.empty() && isubdft1.size() == isubdft2.size()) { @@ -201,7 +210,11 @@ namespace storm { auto LHS = colouring.colourSubdft(isubdft1); auto RHS = colouring.colourSubdft(isubdft2); auto IsoCheck = DFTIsomorphismCheck(LHS, RHS, *this); - IsoCheck.findIsomorphism(); + isSymmetry = IsoCheck.findIsomorphism(); + } + if(isSymmetry) { + std::cout << "subdfts are symmetric" << std::endl; + } } } diff --git a/src/storage/dft/DFTIsomorphism.h b/src/storage/dft/DFTIsomorphism.h index 6c4a44ad6..182a2b01c 100644 --- a/src/storage/dft/DFTIsomorphism.h +++ b/src/storage/dft/DFTIsomorphism.h @@ -261,11 +261,42 @@ namespace storage { */ bool check() { // We can skip BEs, as they are identified by they're homomorphic if they are in the same class - for(auto const& index : bijection) { - // As they are in the same group, the types are fine already. We just have to check the children. - + for(auto const& indexpair : bijection) { + // Check type first. Colouring takes care of a lot, but not necesarily everything (e.g. voting thresholds) + equalType(*dft.getElement(indexpair.first), *dft.getElement(indexpair.second)); + if(dft.isGate(indexpair.first)) { + assert(dft.isGate(indexpair.second)); + auto const& lGate = dft.getGate(indexpair.first); + std::set childrenLeftMapped; + for(auto const& child : lGate->children() ) { + childrenLeftMapped.insert(bijection.at(child->id())); + } + auto const& rGate = dft.getGate(indexpair.second); + std::set childrenRight; + for(auto const& child : rGate->children() ) { + childrenRight.insert(child->id()); + } + if(childrenLeftMapped != childrenRight) { + return false; + } + } else if(dft.isDependency(indexpair.first)) { + assert(dft.isDependency(indexpair.second)); + auto const& lDep = dft.getDependency(indexpair.first); + auto const& rDep = dft.getDependency(indexpair.second); + if(bijection.at(lDep->triggerEvent()->id()) != rDep->triggerEvent()->id()) { + return false; + } + if(bijection.at(lDep->dependentEvent()->id()) != rDep->dependentEvent()->id()) { + return false; + } + } + else { + assert(dft.isBasicElement(indexpair.first)); + assert(dft.isBasicElement(indexpair.second)); + // No operations required. + } } - return false; + return true; } private: @@ -341,9 +372,7 @@ namespace storage { } - //std::vector> computeNextCandidate(){ - - //} + }; From 7bf6dbbaab21ac16a4d2333e45ab0ba25252a450 Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 18 Feb 2016 16:45:45 +0100 Subject: [PATCH 02/10] outgoingDependencies in c++ style :) Former-commit-id: 51af1f47ba499719d5c22cb29b97a6da138a7533 --- src/storage/dft/DFTElements.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index 36075d005..d69b73f3b 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -168,7 +168,7 @@ namespace storm { return mOutgoingDependencies.size(); } - DFTDependencyVector const& getOutgoingDependencies() const { + DFTDependencyVector const& outgoingDependencies() const { return mOutgoingDependencies; } From ca77078a9c866cc0aee16908333ec37c138557de Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 18 Feb 2016 18:03:57 +0100 Subject: [PATCH 03/10] Deterministic Building for DFTs Former-commit-id: bb669a034e24494ae3c88a6a353931651c0c945a --- src/storage/dft/DFTBuilder.cpp | 4 ++-- src/storage/dft/DFTBuilder.h | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/storage/dft/DFTBuilder.cpp b/src/storage/dft/DFTBuilder.cpp index f0d1db5ac..1979aea3b 100644 --- a/src/storage/dft/DFTBuilder.cpp +++ b/src/storage/dft/DFTBuilder.cpp @@ -123,7 +123,7 @@ namespace storm { } template - void DFTBuilder::topoVisit(DFTElementPointer const& n, std::map& visited, DFTElementVector& L) { + void DFTBuilder::topoVisit(DFTElementPointer const& n, std::map>& visited, DFTElementVector& L) { if(visited[n] == topoSortColour::GREY) { throw storm::exceptions::WrongFormatException("DFT is cyclic"); } else if(visited[n] == topoSortColour::WHITE) { @@ -141,7 +141,7 @@ namespace storm { // TODO Matthias: use typedefs template std::vector>> DFTBuilder::topoSort() { - std::map visited; + std::map> visited; for(auto const& e : mElements) { visited.insert(std::make_pair(e.second, topoSortColour::WHITE)); } diff --git a/src/storage/dft/DFTBuilder.h b/src/storage/dft/DFTBuilder.h index 37c3c4eaa..17a16cb49 100644 --- a/src/storage/dft/DFTBuilder.h +++ b/src/storage/dft/DFTBuilder.h @@ -141,7 +141,7 @@ namespace storm { enum class topoSortColour {WHITE, BLACK, GREY}; - void topoVisit(DFTElementPointer const& n, std::map& visited, DFTElementVector& L); + void topoVisit(DFTElementPointer const& n, std::map>& visited, DFTElementVector& L); DFTElementVector topoSort(); From 7663c29c5d5a00fdde84ac892f7e3bca87958368 Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 18 Feb 2016 18:13:10 +0100 Subject: [PATCH 04/10] Fix in SubDFT computation. Former-commit-id: aec3f5d0de949aa07c35222dfe1f8e320713bf81 --- src/storage/dft/DFTElements.cpp | 26 ++++++++++++----- src/storage/dft/DFTElements.h | 51 +++++++++++++++++++++++++++++---- 2 files changed, 65 insertions(+), 12 deletions(-) diff --git a/src/storage/dft/DFTElements.cpp b/src/storage/dft/DFTElements.cpp index c7fc1d960..d59ec8f41 100644 --- a/src/storage/dft/DFTElements.cpp +++ b/src/storage/dft/DFTElements.cpp @@ -46,14 +46,20 @@ namespace storm { template std::vector DFTElement::independentSubDft() const { + std::cout << "INDEPENDENT SUBTREE CALL " << this->id() << std::endl; std::vector res; res.push_back(this->id()); - // Extend for pdeps. return res; } template - void DFTElement::extendSubDft(std::set elemsInSubtree, std::vector const& parentsOfSubRoot) const { + void DFTElement::extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot) const { + if(elemsInSubtree.count(this->id()) > 0) return; + std::cout << "ID " << this->id() << "PREL elems "; + for(auto const& i : elemsInSubtree) { + std::cout << i << " "; + } + std::cout << "in subtree." << std::endl; if(std::find(parentsOfSubRoot.begin(), parentsOfSubRoot.end(), mId) != parentsOfSubRoot.end()) { // This is a parent of the suspected root, thus it is not a subdft. elemsInSubtree.clear(); @@ -61,13 +67,19 @@ namespace storm { } elemsInSubtree.insert(mId); for(auto const& parent : mParents) { - if(elemsInSubtree.count(parent->id()) != 0) { - parent->extendUnit(elemsInSubtree); - if(elemsInSubtree.empty()) { - return; - } + + parent->extendSubDft(elemsInSubtree, parentsOfSubRoot); + if(elemsInSubtree.empty()) { + return; } } + for(auto const& dep : mOutgoingDependencies) { + dep->extendSubDft(elemsInSubtree, parentsOfSubRoot); + if(elemsInSubtree.empty()) { + return; + } + + } } diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index d69b73f3b..81b8ce303 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -202,7 +202,7 @@ namespace storm { * Helper to the independent subtree computation * @see independentSubDft */ - virtual void extendSubDft(std::set elemsInSubtree, std::vector const& parentsOfSubRoot) const; + virtual void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot) const; virtual bool isTypeEqualTo(DFTElement const& other) const { return type() == other.type(); @@ -291,6 +291,11 @@ namespace storm { std::vector pids = this->parentIds(); for(auto const& child : mChildren) { child->extendSubDft(unit, pids); + std::cout << "int sub "; + for(auto const& i : unit) { + std::cout << i << " "; + } + std::cout << std::endl; if(unit.empty()) { // Parent in the subdft, ie it is *not* a subdft break; @@ -299,9 +304,10 @@ namespace storm { return std::vector(unit.begin(), unit.end()); } - virtual void extendSubDft(std::set elemsInSubtree, std::vector const& parentsOfSubRoot) const override { + virtual void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot) const override { + if(elemsInSubtree.count(this->id()) > 0) return; DFTElement::extendSubDft(elemsInSubtree, parentsOfSubRoot); - if(!elemsInSubtree.empty()) { + if(elemsInSubtree.empty()) { // Parent in the subdft, ie it is *not* a subdft return; } @@ -309,7 +315,7 @@ namespace storm { child->extendSubDft(elemsInSubtree, parentsOfSubRoot); if(elemsInSubtree.empty()) { // Parent in the subdft, ie it is *not* a subdft - break; + return; } } } @@ -437,7 +443,7 @@ namespace storm { return mIngoingDependencies.size(); } - DFTDependencyVector const& getIngoingDependencies() const { + DFTDependencyVector const& ingoingDependencies() const { return mIngoingDependencies; } @@ -455,6 +461,22 @@ namespace storm { return storm::utility::isZero(mPassiveFailureRate); } + virtual void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot) const override { + if(elemsInSubtree.count(this->id())) return; + DFTElement::extendSubDft(elemsInSubtree, parentsOfSubRoot); + if(elemsInSubtree.empty()) { + // Parent in the subdft, ie it is *not* a subdft + return; + } + for(auto const& incDep : mIngoingDependencies) { + incDep->extendSubDft(elemsInSubtree, parentsOfSubRoot); + if(elemsInSubtree.empty()) { + // Parent in the subdft, ie it is *not* a subdft + return; + } + } + } + bool isTypeEqualTo(DFTElement const& other) const override { if(!DFTElement::isTypeEqualTo(other)) return false; DFTBE const& otherBE = static_cast const&>(other); @@ -502,6 +524,8 @@ namespace storm { return 0; } + + bool isTypeEqualTo(DFTElement const& other) const override { if(!DFTElement::isTypeEqualTo(other)) return false; DFTConst const& otherCNST = static_cast const&>(other); @@ -589,6 +613,23 @@ namespace storm { return std::vector(unit.begin(), unit.end()); } + virtual void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot) const override { + if(elemsInSubtree.count(this->id())) return; + DFTElement::extendSubDft(elemsInSubtree, parentsOfSubRoot); + if(elemsInSubtree.empty()) { + // Parent in the subdft, ie it is *not* a subdft + return; + } + mDependentEvent->extendSubDft(elemsInSubtree, parentsOfSubRoot); + if(elemsInSubtree.empty()) { + // Parent in the subdft, ie it is *not* a subdft + return; + } + mTriggerEvent->extendSubDft(elemsInSubtree, parentsOfSubRoot); + + + } + virtual std::string toString() const override { std::stringstream stream; bool fdep = storm::utility::isOne(mProbability); From 30df7c0bda435a825d92b6a952009386c46a05f8 Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 18 Feb 2016 18:44:26 +0100 Subject: [PATCH 05/10] Convenience info about bijectioncandidates Former-commit-id: c2af2c957ae465303b18e07dbc43b7a19a0c46ae --- src/storage/dft/DFTIsomorphism.h | 86 ++++++++++++++++++++++++++++++++ 1 file changed, 86 insertions(+) diff --git a/src/storage/dft/DFTIsomorphism.h b/src/storage/dft/DFTIsomorphism.h index 182a2b01c..6ce267e87 100644 --- a/src/storage/dft/DFTIsomorphism.h +++ b/src/storage/dft/DFTIsomorphism.h @@ -63,6 +63,87 @@ namespace storage { std::unordered_map> gateCandidates; std::unordered_map, std::vector> beCandidates; std::unordered_map, std::vector> pdepCandidates; + + size_t nrGroups() const { + return gateCandidates.size() + beCandidates.size() + pdepCandidates.size(); + } + + size_t size() const { + return nrGates() + nrBEs() + nrDeps(); + } + + size_t nrGates() const { + size_t res = 0; + for(auto const& x : gateCandidates) { + res += x.second.size(); + } + return res; + } + + size_t nrBEs() const { + size_t res = 0; + for(auto const& x : beCandidates) { + res += x.second.size(); + } + return res; + } + + size_t nrDeps() const { + size_t res = 0; + for(auto const& x : pdepCandidates) { + res += x.second.size(); + } + return res; + } + + bool hasGate(size_t index) { + for(auto const& x : gateCandidates) { + for( auto const& ind : x.second) { + if(index == ind) return true; + } + } + return false; + } + + bool hasBE(size_t index) { + for(auto const& x : beCandidates) { + for(auto const& ind : x.second) { + if(index == ind) return true; + } + } + return false; + } + + bool hasDep(size_t index) { + for(auto const& x : pdepCandidates) { + for(auto const& ind : x.second) { + if(index == ind) return true; + } + } + return false; + } + + bool has(size_t index) { + return hasGate(index) || hasBE(index) || hasDep(index); + } + + + + size_t trivialGateGroups() const { + size_t res = 0; + for(auto const& x : gateCandidates) { + if(x.second.size() == 1) ++res; + } + return res; + } + + size_t trivialBEGroups() const { + size_t res = 0; + for(auto const& x : beCandidates) { + if(x.second.size() == 1) ++res; + } + return res; + } }; template @@ -207,6 +288,9 @@ namespace storage { initializePermutationsAndTreatTrivialGroups(bleft.beCandidates, bright.beCandidates, currentPermutations.beCandidates); initializePermutationsAndTreatTrivialGroups(bleft.gateCandidates, bright.gateCandidates, currentPermutations.gateCandidates); initializePermutationsAndTreatTrivialGroups(bleft.pdepCandidates, bright.pdepCandidates, currentPermutations.pdepCandidates); + std::cout << bijection.size() << " vs. " << bleft.size() << " vs. " << bright.size() << std::endl; + assert(bijection.size() == bleft.size()); + } /** @@ -214,6 +298,7 @@ namespace storage { * @return true if a next bijection exists. */ bool findNextBijection() { + assert(candidatesCompatible); bool foundNext = false; if(!currentPermutations.beCandidates.empty()) { auto it = currentPermutations.beCandidates.begin(); @@ -260,6 +345,7 @@ namespace storage { * */ bool check() { + assert(bijection.size() == bleft.size()); // We can skip BEs, as they are identified by they're homomorphic if they are in the same class for(auto const& indexpair : bijection) { // Check type first. Colouring takes care of a lot, but not necesarily everything (e.g. voting thresholds) From aaec1fd3bd9b5ff0db8b474ad606100ce0b0837b Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 18 Feb 2016 18:56:36 +0100 Subject: [PATCH 06/10] isomorphism runs through first tests :) Former-commit-id: c83157ba7ad6da368062e7f13e626d0733a14949 --- src/storage/dft/DFTIsomorphism.h | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/src/storage/dft/DFTIsomorphism.h b/src/storage/dft/DFTIsomorphism.h index 6ce267e87..5aec35714 100644 --- a/src/storage/dft/DFTIsomorphism.h +++ b/src/storage/dft/DFTIsomorphism.h @@ -96,7 +96,7 @@ namespace storage { return res; } - bool hasGate(size_t index) { + bool hasGate(size_t index) const { for(auto const& x : gateCandidates) { for( auto const& ind : x.second) { if(index == ind) return true; @@ -105,7 +105,7 @@ namespace storage { return false; } - bool hasBE(size_t index) { + bool hasBE(size_t index) const { for(auto const& x : beCandidates) { for(auto const& ind : x.second) { if(index == ind) return true; @@ -114,7 +114,7 @@ namespace storage { return false; } - bool hasDep(size_t index) { + bool hasDep(size_t index) const { for(auto const& x : pdepCandidates) { for(auto const& ind : x.second) { if(index == ind) return true; @@ -123,7 +123,7 @@ namespace storage { return false; } - bool has(size_t index) { + bool has(size_t index) const { return hasGate(index) || hasBE(index) || hasDep(index); } @@ -355,11 +355,13 @@ namespace storage { auto const& lGate = dft.getGate(indexpair.first); std::set childrenLeftMapped; for(auto const& child : lGate->children() ) { + assert(bleft.has(child->id())); childrenLeftMapped.insert(bijection.at(child->id())); } auto const& rGate = dft.getGate(indexpair.second); std::set childrenRight; for(auto const& child : rGate->children() ) { + assert(bright.has(child->id())); childrenRight.insert(child->id()); } if(childrenLeftMapped != childrenRight) { @@ -435,7 +437,7 @@ namespace storage { auto it = permutations.insert(colour); assert(it.second); std::sort(it.first->second.begin(), it.first->second.end()); - zipVectorsIntoMap(colour.second, permutations.find(colour.first)->second, bijection); + zipVectorsIntoMap(left.at(colour.first), it.first->second, bijection); } else { assert(colour.second.size() == 1); assert(bijection.count(left.at(colour.first).front()) == 0); From 2dbcd260e4127672119fb96474a36014e35fef88 Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 18 Feb 2016 19:00:37 +0100 Subject: [PATCH 07/10] symred is now an option Former-commit-id: 572599165612efed2c499668622425b05902927a --- src/storm-dyftee.cpp | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 deletions(-) diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp index a8122f2bd..f0da80f0f 100644 --- a/src/storm-dyftee.cpp +++ b/src/storm-dyftee.cpp @@ -4,6 +4,7 @@ #include "builder/ExplicitDFTModelBuilder.h" #include "modelchecker/results/CheckResult.h" #include "utility/storm.h" +#include "storage/dft/DFTIsomorphism.h" /*! * Load DFT from filename, build corresponding Model and check against given property. @@ -12,13 +13,19 @@ * @param property PCTC formula capturing the property to check. */ template -void analyzeDFT(std::string filename, std::string property) { +void analyzeDFT(std::string filename, std::string property, bool symred = false) { // Parsing DFT std::cout << "Parsing DFT file..." << std::endl; storm::parser::DFTGalileoParser parser; storm::storage::DFT dft = parser.parseDFT(filename); std::cout << "Built data structure" << std::endl; - + + if(symred) { + std::cout << dft.getElementsString() << std::endl; + auto colouring = dft.colourDFT(); + dft.findSymmetries(colouring); + } + // Building Markov Automaton std::cout << "Building Model..." << std::endl; storm::builder::ExplicitDFTModelBuilder builder(dft); @@ -52,6 +59,7 @@ int main(int argc, char** argv) { // Parse cli arguments bool parametric = false; + bool symred = false; log4cplus::LogLevel level = log4cplus::WARN_LOG_LEVEL; std::string filename = argv[1]; std::string pctlFormula = ""; @@ -74,6 +82,8 @@ int main(int argc, char** argv) { ++i; assert(i < argc); pctlFormula = argv[i]; + } else if (option == "--symred") { + symred = true; } else { std::cout << "Option '" << option << "' not recognized." << std::endl; return 1; @@ -88,8 +98,8 @@ int main(int argc, char** argv) { std::cout << "Running " << (parametric ? "parametric " : "") << "DFT analysis on file " << filename << " with property " << pctlFormula << std::endl; if (parametric) { - analyzeDFT(filename, pctlFormula); + analyzeDFT(filename, pctlFormula, symred); } else { - analyzeDFT(filename, pctlFormula); + analyzeDFT(filename, pctlFormula, symred); } } From 11f01cdf5273136f0718a170b83ea4202c657431 Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 18 Feb 2016 21:09:12 +0100 Subject: [PATCH 08/10] towards using symred for counting abstr Former-commit-id: 51bad8ba1e6b711cc45c82f69240c79dcf8b03cb --- src/storage/dft/DFT.cpp | 36 +++++++++++++++++++++++++------- src/storage/dft/DFTElements.cpp | 5 ----- src/storage/dft/DFTElements.h | 5 ----- src/storage/dft/DFTIsomorphism.h | 4 ++-- 4 files changed, 31 insertions(+), 19 deletions(-) diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index e231c7c8d..1ce4618cf 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -186,8 +186,12 @@ namespace storm { for(auto const& colourClass : completeCategories.gateCandidates) { if(colourClass.second.size() > 1) { - std::vector handledWithinClass; + std::set foundEqClassFor; for(auto it1 = colourClass.second.cbegin(); it1 != colourClass.second.cend(); ++it1) { + std::vector> symClass; + if(foundEqClassFor.count(*it1) > 0) { + continue; + } if(!getGate(*it1)->hasOnlyStaticParents()) { continue; } @@ -200,20 +204,38 @@ namespace storm { } 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; bool isSymmetry = false; 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; - auto LHS = colouring.colourSubdft(isubdft1); - auto RHS = colouring.colourSubdft(isubdft2); - auto IsoCheck = DFTIsomorphismCheck(LHS, RHS, *this); - isSymmetry = IsoCheck.findIsomorphism(); + if(isubdft1.empty() || isubdft2.empty() || isubdft1.size() != isubdft2.size()) { + continue; } + std::cout << "Checking subdfts from " << *it1 << ", " << *it2 << " for isomorphism." << std::endl; + auto LHS = colouring.colourSubdft(isubdft1); + auto RHS = colouring.colourSubdft(isubdft2); + auto IsoCheck = DFTIsomorphismCheck(LHS, RHS, *this); + isSymmetry = IsoCheck.findIsomorphism(); if(isSymmetry) { std::cout << "subdfts are symmetric" << std::endl; + foundEqClassFor.insert(*it2); + if(symClass.empty()) { + for(auto const& i : isubdft1) { + symClass.push_back(std::vector({i})); + } + } + auto symClassIt = symClass.begin(); + for(auto const& i : isubdft1) { + symClassIt->emplace_back(IsoCheck.getIsomorphism().at(i)); + for(auto const& v : *symClassIt) { + std::cout << v << " "; + } + std::cout << std::endl; + ++symClassIt; + + } } } diff --git a/src/storage/dft/DFTElements.cpp b/src/storage/dft/DFTElements.cpp index d59ec8f41..26f5f9cbe 100644 --- a/src/storage/dft/DFTElements.cpp +++ b/src/storage/dft/DFTElements.cpp @@ -55,11 +55,6 @@ namespace storm { template void DFTElement::extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot) const { if(elemsInSubtree.count(this->id()) > 0) return; - std::cout << "ID " << this->id() << "PREL elems "; - for(auto const& i : elemsInSubtree) { - std::cout << i << " "; - } - std::cout << "in subtree." << std::endl; if(std::find(parentsOfSubRoot.begin(), parentsOfSubRoot.end(), mId) != parentsOfSubRoot.end()) { // This is a parent of the suspected root, thus it is not a subdft. elemsInSubtree.clear(); diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index 81b8ce303..c352bd38e 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -291,11 +291,6 @@ namespace storm { std::vector pids = this->parentIds(); for(auto const& child : mChildren) { child->extendSubDft(unit, pids); - std::cout << "int sub "; - for(auto const& i : unit) { - std::cout << i << " "; - } - std::cout << std::endl; if(unit.empty()) { // Parent in the subdft, ie it is *not* a subdft break; diff --git a/src/storage/dft/DFTIsomorphism.h b/src/storage/dft/DFTIsomorphism.h index 5aec35714..0d5590d3d 100644 --- a/src/storage/dft/DFTIsomorphism.h +++ b/src/storage/dft/DFTIsomorphism.h @@ -256,8 +256,8 @@ namespace storage { * Can only be called after the findIsomorphism procedure returned that an isomorphism has found. * @see findIsomorphism */ - std::vector> getIsomorphism() const { - + std::map const& getIsomorphism() const { + return bijection; } /** From 130fa1328ab30f297c79122273c100273472767f Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 18 Feb 2016 21:39:43 +0100 Subject: [PATCH 09/10] function returns independent symmetries Former-commit-id: 674f0bcff263b0d52d928a37cfdac50d69066d47 --- src/storage/dft/DFT.cpp | 15 ++++++++------- src/storage/dft/DFT.h | 4 ++-- src/storage/dft/SymmetricUnits.h | 33 ++++++++++++++++++++++++++------ src/storm-dyftee.cpp | 3 ++- 4 files changed, 39 insertions(+), 16 deletions(-) diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index 1ce4618cf..0a90f1513 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -1,5 +1,6 @@ #include +#include #include "DFT.h" #include "src/exceptions/NotSupportedException.h" @@ -177,12 +178,12 @@ namespace storm { } template - std::vector> DFT::findSymmetries(DFTColouring const& colouring) const { + DFTIndependentSymmetries DFT::findSymmetries(DFTColouring const& colouring) const { std::vector vec; vec.reserve(nrElements()); storm::utility::iota_n(std::back_inserter(vec), nrElements(), 0); BijectionCandidates completeCategories = colouring.colourSubdft(vec); - std::vector> res; + std::map>> res; for(auto const& colourClass : completeCategories.gateCandidates) { if(colourClass.second.size() > 1) { @@ -229,10 +230,6 @@ namespace storm { auto symClassIt = symClass.begin(); for(auto const& i : isubdft1) { symClassIt->emplace_back(IsoCheck.getIsomorphism().at(i)); - for(auto const& v : *symClassIt) { - std::cout << v << " "; - } - std::cout << std::endl; ++symClassIt; } @@ -240,10 +237,14 @@ namespace storm { } } } + if(!symClass.empty()) { + res.emplace(*it1, symClass); + } } + } } - return res; + return DFTIndependentSymmetries(res); } diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h index f2036e7d7..57bfee16d 100644 --- a/src/storage/dft/DFT.h +++ b/src/storage/dft/DFT.h @@ -11,7 +11,7 @@ #include "DFTElements.h" #include "../BitVector.h" - +#include "SymmetricUnits.h" #include "../../utility/math.h" #include "src/utility/macros.h" @@ -230,7 +230,7 @@ namespace storm { DFTColouring colourDFT() const; - std::vector> findSymmetries(DFTColouring const& colouring) const; + DFTIndependentSymmetries findSymmetries(DFTColouring const& colouring) const; private: bool elementIndicesCorrect() const { diff --git a/src/storage/dft/SymmetricUnits.h b/src/storage/dft/SymmetricUnits.h index 3959593a1..6521ee8d2 100644 --- a/src/storage/dft/SymmetricUnits.h +++ b/src/storage/dft/SymmetricUnits.h @@ -1,7 +1,28 @@ -#ifndef SYMMETRICUNITS_H -#define SYMMETRICUNITS_H - - - -#endif /* SYMMETRICUNITS_H */ +#pragma once +namespace storm { + namespace storage { + struct DFTIndependentSymmetries { + std::map>> groups; + + DFTIndependentSymmetries(std::map>> groups) : groups(groups) { + + } + }; + + inline std::ostream& operator<<(std::ostream& os, DFTIndependentSymmetries const& s) { + for(auto const& cl : s.groups) { + std::cout << "SYM GROUP FOR " << cl.first << std::endl; + for(auto const& eqClass : cl.second) { + for(auto const& i : eqClass) { + std::cout << i << " "; + } + std::cout << std::endl; + } + } + + + return os; + } + } +} \ No newline at end of file diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp index f0da80f0f..49b573f33 100644 --- a/src/storm-dyftee.cpp +++ b/src/storm-dyftee.cpp @@ -23,7 +23,8 @@ void analyzeDFT(std::string filename, std::string property, bool symred = false) if(symred) { std::cout << dft.getElementsString() << std::endl; auto colouring = dft.colourDFT(); - dft.findSymmetries(colouring); + auto res = dft.findSymmetries(colouring); + std::cout << res; } // Building Markov Automaton From 2ab4417ed4ff6ad07fcfcc242c0075acd64e657f Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 18 Feb 2016 21:52:05 +0100 Subject: [PATCH 10/10] symmetry also check deps for roots now Former-commit-id: a1141250c2dee120e442dc72e42417c19053b055 --- src/storage/dft/DFT.cpp | 18 +++++++++++++++--- src/storage/dft/DFT.h | 2 ++ 2 files changed, 17 insertions(+), 3 deletions(-) diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index 0a90f1513..d56166f60 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -196,8 +196,8 @@ namespace storm { if(!getGate(*it1)->hasOnlyStaticParents()) { continue; } - std::vector sortedParent1Ids = getGate(*it1)->parentIds(); - std::sort(sortedParent1Ids.begin(), sortedParent1Ids.end()); + + std::pair, std::vector> influencedElem1Ids = getSortedParentAndOutDepIds(*it1); auto it2 = it1; for(++it2; it2 != colourClass.second.cend(); ++it2) { if(!getGate(*it2)->hasOnlyStaticParents()) { @@ -206,7 +206,7 @@ namespace storm { std::vector sortedParent2Ids = getGate(*it2)->parentIds(); std::sort(sortedParent2Ids.begin(), sortedParent2Ids.end()); - if(sortedParent1Ids == sortedParent2Ids) { + if(influencedElem1Ids == getSortedParentAndOutDepIds(*it2)) { std::cout << "Considering ids " << *it1 << ", " << *it2 << " for isomorphism." << std::endl; bool isSymmetry = false; std::vector isubdft1 = getGate(*it1)->independentSubDft(); @@ -247,6 +247,18 @@ namespace storm { return DFTIndependentSymmetries(res); } + template + std::pair, std::vector> DFT::getSortedParentAndOutDepIds(size_t index) const { + std::pair, std::vector> res; + res.first = getElement(index)->parentIds(); + std::sort(res.first.begin(), res.first.end()); + for(auto const& dep : getElement(index)->outgoingDependencies()) { + res.second.push_back(dep->id()); + } + std::sort(res.second.begin(), res.second.end()); + return res; + } + // Explicitly instantiate the class. template class DFT; diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h index 57bfee16d..1583cc8d5 100644 --- a/src/storage/dft/DFT.h +++ b/src/storage/dft/DFT.h @@ -233,6 +233,8 @@ namespace storm { DFTIndependentSymmetries findSymmetries(DFTColouring const& colouring) const; private: + std::pair, std::vector> getSortedParentAndOutDepIds(size_t index) const; + bool elementIndicesCorrect() const { for(size_t i = 0; i < mElements.size(); ++i) { if(mElements[i]->id() != i) return false;