diff --git a/src/parser/DFTGalileoParser.cpp b/src/parser/DFTGalileoParser.cpp index d56899d20..262098a68 100644 --- a/src/parser/DFTGalileoParser.cpp +++ b/src/parser/DFTGalileoParser.cpp @@ -54,7 +54,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Exception during file opening on " << filename << "."); return false; } - file.exceptions( 0 ); + file.exceptions( std::ifstream::goodbit ); std::string line; bool generalSuccess = true; @@ -156,4 +156,4 @@ namespace storm { #endif } -} \ No newline at end of file +} diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index 49c92e05a..112a9273b 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -143,6 +143,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 diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h index 7cb5eaf4a..fed33eee3 100644 --- a/src/storage/dft/DFTState.h +++ b/src/storage/dft/DFTState.h @@ -5,6 +5,7 @@ #include "DFTElementState.h" #include +#include namespace storm { namespace storage {