diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index c36f0a9e0..29f97d77c 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -142,6 +142,8 @@ namespace storm { return stream.str(); } + + // Explicitly instantiate the class. template class DFT; diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h index 81cfdf99b..2cfbf6422 100644 --- a/src/storage/dft/DFT.h +++ b/src/storage/dft/DFT.h @@ -2,17 +2,19 @@ #ifndef DFT_H #define DFT_H - -#include "DFTElements.h" -#include "../BitVector.h" #include #include #include #include +#include + +#include "DFTIsomorphism.h" +#include "DFTElements.h" +#include "../BitVector.h" + #include "../../utility/math.h" #include "src/utility/macros.h" -#include namespace storm { namespace storage { @@ -28,8 +30,9 @@ namespace storm { } }; - - + /** + * Represents a Dynamic Fault Tree + */ template class DFT { @@ -136,12 +139,17 @@ namespace storm { return result; } + /** + * Get a pointer to an element in the DFT + * @param index The id of the element + */ DFTElementPointer const& getElement(size_t index) const { assert(index < nrElements()); return mElements[index]; } std::shared_ptr> getBasicElement(size_t index) const { + assert(index < nrElements()); assert(mElements[index]->isBasicElement()); return std::static_pointer_cast>(mElements[index]); } @@ -182,7 +190,8 @@ namespace storm { std::string getElementsWithStateString(DFTStatePointer const& state) const; std::string getStateString(DFTStatePointer const& state) const; - + + DFTIsomorphisms detectIsomorphicChildren() 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 new file mode 100644 index 000000000..2b6016ca4 --- /dev/null +++ b/src/storage/dft/DFTIsomorphism.h @@ -0,0 +1,25 @@ +#pragma once + +#include + +namespace storm { +namespace storage { + /** + * Saves isomorphism between subtrees + */ + class DFTIsomorphism { + std::vector> classes; + }; + + /** + * Saves sets of isomorphic subtrees + */ + class DFTIsomorphisms { + std::vector isomorphisms; + + void addIsomorphismClass(DFTIsomorphism const &) { + + } + }; +} // namespace storm::dft +} // namespace storm