dft isomorphism

Former-commit-id: 1404390f5a

src/storage/dft/DFT.cpp

@@ -142,6 +142,8 @@ namespace storm {
             return stream.str();
         }
 
+
+
         // Explicitly instantiate the class.
         template class DFT<double>;
 

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]);
             }
@@ -183,6 +191,7 @@ namespace storm {
 
             std::string getStateString(DFTStatePointer const& state) const;
 
+            DFTIsomorphisms detectIsomorphicChildren() const;
         private:
             bool elementIndicesCorrect() const {
                 for(size_t i = 0; i < mElements.size(); ++i) {

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