Merge branch 'monolithic-dft' of https://sselab.de/lab9/private/git/storm into monolithic-dft

Former-commit-id: 2ed40386ae

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
         
     }
-}
+}

src/storage/dft/DFT.cpp

@@ -143,6 +143,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]);
             }
@@ -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) {

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

src/storage/dft/DFTState.h

@@ -5,6 +5,7 @@
 #include "DFTElementState.h"
 
 #include <sstream>
+#include <memory>
 
 namespace storm {
     namespace storage {