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