From ed9ac339e69d73153c31d53a73e3b312165d0490 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Fri, 5 Feb 2016 13:14:48 +0100
Subject: [PATCH 1/3] dft isomorphism

Former-commit-id: 1404390f5a2fbdac56705132a2ed9558085ef7d9
---
 src/storage/dft/DFT.cpp          |  2 ++
 src/storage/dft/DFT.h            | 23 ++++++++++++++++-------
 src/storage/dft/DFTIsomorphism.h | 25 +++++++++++++++++++++++++
 3 files changed, 43 insertions(+), 7 deletions(-)
 create mode 100644 src/storage/dft/DFTIsomorphism.h

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<double>;
 
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 <memory>
 #include <unordered_map>
 #include <list>
 #include <map>
 
+#include <boost/iterator/counting_iterator.hpp>
+
+#include "DFTIsomorphism.h"
+#include "DFTElements.h"
+#include "../BitVector.h"
+
 #include "../../utility/math.h"
 #include "src/utility/macros.h"
-#include <boost/iterator/counting_iterator.hpp>
 
 namespace storm {
     namespace storage {
@@ -28,8 +30,9 @@ namespace storm {
             }
         };
 
-
-
+        /**
+         * Represents a Dynamic Fault Tree
+         */
         template<typename ValueType>
         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<DFTBE<ValueType>> getBasicElement(size_t index) const {
+                assert(index < nrElements());
                 assert(mElements[index]->isBasicElement());
                 return std::static_pointer_cast<DFTBE<ValueType>>(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 <vector>
+
+namespace storm {
+namespace storage {
+    /**
+     * Saves isomorphism between subtrees
+     */
+    class DFTIsomorphism {
+        std::vector<std::vector<size_t>> classes;
+    };
+
+    /**
+     * Saves sets of isomorphic subtrees
+     */
+    class DFTIsomorphisms {
+        std::vector<DFTIsomorphism> isomorphisms;
+
+        void addIsomorphismClass(DFTIsomorphism const &) {
+
+        }
+    };
+} // namespace storm::dft
+} // namespace storm

From 50e37217de2dfc9b09b6e55f4e762817d3a16f63 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Fri, 5 Feb 2016 13:59:21 +0100
Subject: [PATCH 2/3] Fixed compile problem

Former-commit-id: 718456a293ed121ad644718453505dfa01c6233c
---
 src/parser/DFTGalileoParser.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/parser/DFTGalileoParser.cpp b/src/parser/DFTGalileoParser.cpp
index 163bc1488..8bc96ed78 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
+}

From 3b1c695b5d2c4b7f9b4c3b05249addcd24e76dae Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Fri, 5 Feb 2016 16:33:57 +0100
Subject: [PATCH 3/3] Another compile fix

Former-commit-id: 6bb97a0505e07d4952fad582c75e9d04d2f16481
---
 src/storage/dft/DFTState.h | 1 +
 1 file changed, 1 insertion(+)

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 <sstream>
+#include <memory>
 
 namespace storm {
     namespace storage {