From 11f01cdf5273136f0718a170b83ea4202c657431 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Thu, 18 Feb 2016 21:09:12 +0100
Subject: [PATCH] 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<size_t> handledWithinClass;
+ std::set<size_t> foundEqClassFor;
for(auto it1 = colourClass.second.cbegin(); it1 != colourClass.second.cend(); ++it1) {
+ std::vector<std::vector<size_t>> symClass;
+ if(foundEqClassFor.count(*it1) > 0) {
+ continue;
+ }
if(!getGate(*it1)->hasOnlyStaticParents()) {
continue;
}
@@ -200,20 +204,38 @@ namespace storm {
}
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;
bool isSymmetry = false;
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;
- auto LHS = colouring.colourSubdft(isubdft1);
- auto RHS = colouring.colourSubdft(isubdft2);
- auto IsoCheck = DFTIsomorphismCheck<ValueType>(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<ValueType>(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<size_t>({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<typename ValueType>
void DFTElement<ValueType>::extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> 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<size_t> 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<std::pair<size_t, size_t>> getIsomorphism() const {
-
+ std::map<size_t, size_t> const& getIsomorphism() const {
+ return bijection;
}
/**