diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp
index fb1c5cd33..e039b389f 100644
--- a/src/builder/ExplicitDFTModelBuilder.cpp
+++ b/src/builder/ExplicitDFTModelBuilder.cpp
@@ -13,10 +13,10 @@ namespace storm {
         template<typename ValueType, typename RewardModelType, typename IndexType>
         std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> ExplicitDFTModelBuilder<ValueType, RewardModelType, IndexType>::buildCTMC() {
             // Initialize
-            storm::storage::DFTState state(mDft, newIndex++);
+            storm::storage::DFTState<ValueType> state(mDft, newIndex++);
             mStates.insert(state);
 
-            std::queue<storm::storage::DFTState> stateQueue;
+            std::queue<storm::storage::DFTState<ValueType>> stateQueue;
             stateQueue.push(state);
 
             bool deterministicModel = true;
@@ -46,7 +46,7 @@ namespace storm {
                 modelComponents.stateLabeling.addLabel(elem->name() + "_fail");
             }
 
-            for (storm::storage::DFTState state : mStates) {
+            for (storm::storage::DFTState<ValueType> state : mStates) {
                 if (mDft.hasFailed(state)) {
                     modelComponents.stateLabeling.addLabelToState("failed", state.getId());
                 }
@@ -72,7 +72,7 @@ namespace storm {
         }
 
         template<typename ValueType, typename RewardModelType, typename IndexType>
-        void ExplicitDFTModelBuilder<ValueType, RewardModelType, IndexType>::exploreStates(std::queue<storm::storage::DFTState>& stateQueue, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder) {
+        void ExplicitDFTModelBuilder<ValueType, RewardModelType, IndexType>::exploreStates(std::queue<storm::storage::DFTState<ValueType>>& stateQueue, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder) {
 
             std::vector<std::pair<size_t, ValueType>> outgoingTransitions;
 
@@ -82,7 +82,7 @@ namespace storm {
                 ValueType sum = 0;
 
                 // Consider next state
-                storm::storage::DFTState state = stateQueue.front();
+                storm::storage::DFTState<ValueType> state = stateQueue.front();
                 stateQueue.pop();
 
                 size_t smallest = 0;
@@ -99,7 +99,7 @@ namespace storm {
                 while (smallest < state.nrFailableBEs()) {
                     STORM_LOG_TRACE("exploring from: " << mDft.getStateString(state));
 
-                    storm::storage::DFTState newState(state);
+                    storm::storage::DFTState<ValueType> newState(state);
                     std::pair<std::shared_ptr<storm::storage::DFTBE<ValueType>>, bool> nextBE = newState.letNextBEFail(smallest++);
                     if (nextBE.first == nullptr) {
                         std::cout << "break" << std::endl;
@@ -108,26 +108,26 @@ namespace storm {
                     }
                     STORM_LOG_TRACE("with the failure of: " << nextBE.first->name() << " [" << nextBE.first->id() << "]");
 
-                    storm::storage::DFTStateSpaceGenerationQueues queues;
+                    storm::storage::DFTStateSpaceGenerationQueues<ValueType> queues;
 
-                    for (std::shared_ptr<storm::storage::DFTGate> parent : nextBE.first->parents()) {
+                    for (DFTGatePointer parent : nextBE.first->parents()) {
                         if (newState.isOperational(parent->id())) {
                             queues.propagateFailure(parent);
                         }
                     }
 
                     while (!queues.failurePropagationDone()) {
-                        std::shared_ptr<storm::storage::DFTGate> next = queues.nextFailurePropagation();
+                        DFTGatePointer next = queues.nextFailurePropagation();
                         next->checkFails(newState, queues);
                     }
 
                     while (!queues.failsafePropagationDone()) {
-                        std::shared_ptr<storm::storage::DFTGate> next = queues.nextFailsafePropagation();
+                        DFTGatePointer next = queues.nextFailsafePropagation();
                         next->checkFailsafe(newState, queues);
                     }
 
                     while (!queues.dontCarePropagationDone()) {
-                        std::shared_ptr<storm::storage::DFTElement> next = queues.nextDontCarePropagation();
+                        DFTElementPointer next = queues.nextDontCarePropagation();
                         next->checkDontCareAnymore(newState, queues);
                     }
 
diff --git a/src/builder/ExplicitDFTModelBuilder.h b/src/builder/ExplicitDFTModelBuilder.h
index de3a94293..8148559c3 100644
--- a/src/builder/ExplicitDFTModelBuilder.h
+++ b/src/builder/ExplicitDFTModelBuilder.h
@@ -18,6 +18,9 @@ namespace storm {
         template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename IndexType = uint32_t>
         class ExplicitDFTModelBuilder {
 
+            using DFTElementPointer = std::shared_ptr<storm::storage::DFTElement<ValueType>>;
+            using DFTGatePointer = std::shared_ptr<storm::storage::DFTGate<ValueType>>;
+
             // A structure holding the individual components of a model.
             struct ModelComponents {
                 ModelComponents();
@@ -36,7 +39,7 @@ namespace storm {
             };
 
             storm::storage::DFT<ValueType> const &mDft;
-            std::unordered_set<storm::storage::DFTState> mStates;
+            std::unordered_set<storm::storage::DFTState<ValueType>> mStates;
             size_t newIndex = 0;
 
         public:
@@ -47,7 +50,7 @@ namespace storm {
             std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> buildCTMC();
 
         private:
-            void exploreStates(std::queue<storm::storage::DFTState>& stateQueue, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder);
+            void exploreStates(std::queue<storm::storage::DFTState<ValueType>>& stateQueue, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder);
 
         };
     }
diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp
index 719c59e26..0b8c99685 100644
--- a/src/storage/dft/DFT.cpp
+++ b/src/storage/dft/DFT.cpp
@@ -4,7 +4,7 @@ namespace storm {
     namespace storage {
 
         template<typename ValueType>
-        DFT<ValueType>::DFT(std::vector<std::shared_ptr<DFTElement>> const& elements, std::shared_ptr<DFTElement> const& tle) : mElements(elements), mNrOfBEs(0), mNrOfSpares(0)
+        DFT<ValueType>::DFT(DFTElementVector const& elements, DFTElementPointer const& tle) : mElements(elements), mNrOfBEs(0), mNrOfSpares(0)
         {
             assert(elementIndicesCorrect());
 
@@ -19,7 +19,7 @@ namespace storm {
                 }
                 else if(elem->isSpareGate()) {
                     ++mNrOfSpares;
-                    for(auto const& spareReprs : std::static_pointer_cast<DFTSpare>(elem)->children()) {
+                    for(auto const& spareReprs : std::static_pointer_cast<DFTSpare<ValueType>>(elem)->children()) {
                         if(mActivationIndex.count(spareReprs->id()) == 0) {
                             mActivationIndex[spareReprs->id()] =  stateIndex++;
                         }
@@ -34,7 +34,7 @@ namespace storm {
                         mSpareModules.insert(std::make_pair(spareReprs->id(), sparesAndBes));
 
                     }
-                    std::static_pointer_cast<DFTSpare>(elem)->setUseIndex(stateIndex);
+                    std::static_pointer_cast<DFTSpare<ValueType>>(elem)->setUseIndex(stateIndex);
                     mUsageIndex.insert(std::make_pair(elem->id(), stateIndex));
                     stateIndex += mUsageInfoBits;
 
@@ -108,7 +108,7 @@ namespace storm {
         }
 
         template<typename ValueType>
-        std::string DFT<ValueType>::getElementsWithStateString(DFTState const& state) const{
+        std::string DFT<ValueType>::getElementsWithStateString(DFTState<ValueType> const& state) const{
             std::stringstream stream;
             for (auto const& elem : mElements) {
                 stream << "[" << elem->id() << "]";
@@ -126,7 +126,7 @@ namespace storm {
         }
 
         template<typename ValueType>
-        std::string DFT<ValueType>::getStateString(DFTState const& state) const{
+        std::string DFT<ValueType>::getStateString(DFTState<ValueType> const& state) const{
             std::stringstream stream;
             stream << "(" << state.getId() << ") ";
             for (auto const& elem : mElements) {
diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h
index 068ea4ef1..0f39e3ddc 100644
--- a/src/storage/dft/DFT.h
+++ b/src/storage/dft/DFT.h
@@ -17,8 +17,9 @@
 namespace storm {
     namespace storage {
 
+        template<typename ValueType>
         struct DFTElementSort {
-            bool operator()(std::shared_ptr<DFTElement> const& a, std::shared_ptr<DFTElement> const& b)  const {
+            bool operator()(std::shared_ptr<DFTElement<ValueType>> const& a, std::shared_ptr<DFTElement<ValueType>> const& b)  const {
                 if (a->rank() == 0 && b->rank() == 0) {
                     return a->isConstant();
                 } else {
@@ -27,11 +28,18 @@ namespace storm {
             }
         };
 
+
+
         template<typename ValueType>
         class DFT {
 
+            using DFTElementPointer = std::shared_ptr<DFTElement<ValueType>>;
+            using DFTElementVector = std::vector<DFTElementPointer>;
+            using DFTGatePointer = std::shared_ptr<DFTGate<ValueType>>;
+            using DFTGateVector = std::vector<DFTGatePointer>;
+
         private:
-            std::vector<std::shared_ptr<DFTElement>> mElements;
+            DFTElementVector mElements;
             size_t mNrOfBEs;
             size_t mNrOfSpares;
             size_t mTopLevelIndex;
@@ -44,9 +52,8 @@ namespace storm {
             std::map<size_t, size_t> mUsageIndex;
             
         public:
-            DFT(std::vector<std::shared_ptr<DFTElement>> const& elements, std::shared_ptr<DFTElement> const& tle);
-            
-            
+            DFT(DFTElementVector const& elements, DFTElementPointer const& tle);
+
             size_t stateSize() const {
                 return mStateSize;
             }
@@ -72,15 +79,15 @@ namespace storm {
                 return mIdToFailureIndex[id];
             }
             
-            void initializeUses(DFTState& state) const {
+            void initializeUses(DFTState<ValueType>& state) const {
                 for(auto const& elem : mElements) {
                     if(elem->isSpareGate()) {
-                        std::static_pointer_cast<DFTSpare>(elem)->initializeUses(state);
+                        std::static_pointer_cast<DFTSpare<ValueType>>(elem)->initializeUses(state);
                     }
                 }
             }
             
-            void initializeActivation(DFTState& state) const {
+            void initializeActivation(DFTState<ValueType>& state) const {
                 state.activate(mTopLevelIndex);
                 for(auto const& elem : mTopModule) {
                     if(mElements[elem]->isSpareGate()) {
@@ -108,8 +115,7 @@ namespace storm {
                 }
             }
             
-            
-            void propagateActivation(DFTState& state, size_t representativeId) const {
+            void propagateActivation(DFTState<ValueType>& state, size_t representativeId) const {
                 state.activate(representativeId);
                 for(size_t id : module(representativeId)) {
                     if(mElements[id]->isSpareGate()) {
@@ -120,15 +126,15 @@ namespace storm {
             
             std::vector<size_t> nonColdBEs() const {
                 std::vector<size_t> result;
-                for(std::shared_ptr<DFTElement> elem : mElements) {
+                for(DFTElementPointer elem : mElements) {
                     if(elem->isBasicElement() && !elem->isColdBasicElement()) {
                         result.push_back(elem->id());
                     }
                 }
                 return result;
             }
-            
-            std::shared_ptr<DFTElement> const& getElement(size_t index) const {
+
+            DFTElementPointer const& getElement(size_t index) const {
                 assert(index < nrElements());
                 return mElements[index];
             }
@@ -140,7 +146,7 @@ namespace storm {
 
             std::vector<std::shared_ptr<DFTBE<ValueType>>> getBasicElements() const {
                 std::vector<std::shared_ptr<DFTBE<ValueType>>> elements;
-                for (std::shared_ptr<storm::storage::DFTElement> elem : mElements) {
+                for (DFTElementPointer elem : mElements) {
                     if (elem->isBasicElement()) {
                         elements.push_back(std::static_pointer_cast<DFTBE<ValueType>>(elem));
                     }
@@ -149,11 +155,11 @@ namespace storm {
             }
 
 
-            bool hasFailed(DFTState const& state) const {
+            bool hasFailed(DFTState<ValueType> const& state) const {
                 return state.hasFailed(mTopLevelIndex);
             }
             
-            bool isFailsafe(DFTState const& state) const {
+            bool isFailsafe(DFTState<ValueType> const& state) const {
                 return state.isFailsafe(mTopLevelIndex);
             }
             
@@ -163,9 +169,9 @@ namespace storm {
 
             std::string getSpareModulesString() const;
 
-            std::string getElementsWithStateString(DFTState const& state) const;
+            std::string getElementsWithStateString(DFTState<ValueType> const& state) const;
 
-            std::string getStateString(DFTState const& state) const;
+            std::string getStateString(DFTState<ValueType> const& state) const;
             
         private:
             bool elementIndicesCorrect() const {
diff --git a/src/storage/dft/DFTBuilder.cpp b/src/storage/dft/DFTBuilder.cpp
index ee7676449..870b7f8bf 100644
--- a/src/storage/dft/DFTBuilder.cpp
+++ b/src/storage/dft/DFTBuilder.cpp
@@ -17,7 +17,7 @@ namespace storm {
         DFT<ValueType> DFTBuilder<ValueType>::build() {
             for(auto& elem : mChildNames) {
                 for(auto const& child : elem.second) {
-                    std::shared_ptr<DFTGate> gate = std::static_pointer_cast<DFTGate>(elem.first);
+                    DFTGatePointer gate = std::static_pointer_cast<DFTGate<ValueType>>(elem.first);
                     gate->pushBackChild(mElements[child]);
                     mElements[child]->addParent(gate);
                 }
@@ -30,25 +30,25 @@ namespace storm {
                 computeRank(elem.second);
             }
 
-            std::vector<std::shared_ptr<DFTElement>> elems = topoSort();
+            DFTElementVector elems = topoSort();
             size_t id = 0;
-            for(std::shared_ptr<DFTElement> e : elems) {
+            for(DFTElementPointer e : elems) {
                 e->setId(id++);
             }
             return DFT<ValueType>(elems, mElements[topLevelIdentifier]);
         }
 
         template<typename ValueType>
-        unsigned DFTBuilder<ValueType>::computeRank(std::shared_ptr<DFTElement> const& elem) {
+        unsigned DFTBuilder<ValueType>::computeRank(DFTElementPointer const& elem) {
             if(elem->rank() == -1) {
                 if(elem->nrChildren() == 0) {
                     elem->setRank(0);
                 } else {
-                    std::shared_ptr<DFTGate> gate = std::static_pointer_cast<DFTGate>(elem);
+                    DFTGatePointer gate = std::static_pointer_cast<DFTGate<ValueType>>(elem);
                     unsigned maxrnk = 0;
                     unsigned newrnk = 0;
 
-                    for (std::shared_ptr<DFTElement> const &child : gate->children()) {
+                    for (DFTElementPointer const &child : gate->children()) {
                         newrnk = computeRank(child);
                         if (newrnk > maxrnk) {
                             maxrnk = newrnk;
@@ -68,22 +68,22 @@ namespace storm {
                 // Element with that name already exists.
                 return false;
             }
-            std::shared_ptr<DFTElement> element;
+            DFTElementPointer element;
             switch(tp) {
                 case DFTElementTypes::AND:
-                    element = std::make_shared<DFTAnd>(mNextId++, name);
+                    element = std::make_shared<DFTAnd<ValueType>>(mNextId++, name);
                     break;
                 case DFTElementTypes::OR:
-                    element = std::make_shared<DFTOr>(mNextId++, name);
+                    element = std::make_shared<DFTOr<ValueType>>(mNextId++, name);
                     break;
                 case DFTElementTypes::PAND:
-                    element = std::make_shared<DFTPand>(mNextId++, name);
+                    element = std::make_shared<DFTPand<ValueType>>(mNextId++, name);
                     break;
                 case DFTElementTypes::POR:
-                    element = std::make_shared<DFTPor>(mNextId++, name);
+                    element = std::make_shared<DFTPor<ValueType>>(mNextId++, name);
                     break;
                 case DFTElementTypes::SPARE:
-                   element = std::make_shared<DFTSpare>(mNextId++, name);
+                   element = std::make_shared<DFTSpare<ValueType>>(mNextId++, name);
                    break;
                 case DFTElementTypes::BE:
                 case DFTElementTypes::VOT:
@@ -102,13 +102,13 @@ namespace storm {
         }
 
         template<typename ValueType>
-        void DFTBuilder<ValueType>::topoVisit(std::shared_ptr<DFTElement> const& n, std::map<std::shared_ptr<DFTElement>, topoSortColour>& visited, std::vector<std::shared_ptr<DFTElement>>& L) {
+        void DFTBuilder<ValueType>::topoVisit(DFTElementPointer const& n, std::map<DFTElementPointer, topoSortColour>& visited, DFTElementVector& L) {
             if(visited[n] == topoSortColour::GREY) {
                 throw storm::exceptions::WrongFormatException("DFT is cyclic");
             } else if(visited[n] == topoSortColour::WHITE) {
                 if(n->isGate()) {
                     visited[n] = topoSortColour::GREY;
-                    for(std::shared_ptr<DFTElement> const& c : std::static_pointer_cast<DFTGate>(n)->children()) {
+                    for(DFTElementPointer const& c : std::static_pointer_cast<DFTGate<ValueType>>(n)->children()) {
                         topoVisit(c, visited, L);
                     }
                 }
@@ -117,14 +117,15 @@ namespace storm {
             }
         }
 
+        // TODO Matthias: use typedefs
         template<typename ValueType>
-        std::vector<std::shared_ptr<DFTElement>> DFTBuilder<ValueType>::topoSort() {
-            std::map<std::shared_ptr<DFTElement>, topoSortColour> visited;
+        std::vector<std::shared_ptr<DFTElement<ValueType>>> DFTBuilder<ValueType>::topoSort() {
+            std::map<std::shared_ptr<DFTElement<ValueType>>, topoSortColour> visited;
             for(auto const& e : mElements) {
                 visited.insert(std::make_pair(e.second, topoSortColour::WHITE)); 
             }
 
-            std::vector<std::shared_ptr<DFTElement>> L;
+            std::vector<std::shared_ptr<DFTElement<ValueType>>> L;
             for(auto const& e : visited) {
                 topoVisit(e.first, visited, L);
             }
diff --git a/src/storage/dft/DFTBuilder.h b/src/storage/dft/DFTBuilder.h
index f129afc0b..88fdc6ef0 100644
--- a/src/storage/dft/DFTBuilder.h
+++ b/src/storage/dft/DFTBuilder.h
@@ -14,11 +14,17 @@ namespace storm {
 
         template<typename ValueType>
         class DFTBuilder {
-            
+
+            using DFTElementPointer = std::shared_ptr<DFTElement<ValueType>>;
+            using DFTElementVector = std::vector<DFTElementPointer>;
+            using DFTGatePointer = std::shared_ptr<DFTGate<ValueType>>;
+            using DFTGateVector = std::vector<DFTGatePointer>;
+
+        private:
             std::size_t mNextId = 0;
             std::string topLevelIdentifier;
-            std::unordered_map<std::string, std::shared_ptr<DFTElement>> mElements;
-            std::unordered_map<std::shared_ptr<DFTElement>, std::vector<std::string>> mChildNames;
+            std::unordered_map<std::string, DFTElementPointer> mElements;
+            std::unordered_map<DFTElementPointer, std::vector<std::string>> mChildNames;
             
         public:
             DFTBuilder() {
@@ -64,7 +70,7 @@ namespace storm {
                     std::cerr << "Voting gates with threshold higher than the number of children is not supported." << std::endl;
                     return false;
                 }
-                std::shared_ptr<DFTElement> element = std::make_shared<DFTVot>(mNextId++, name, threshold);
+                DFTElementPointer element = std::make_shared<DFTVot<ValueType>>(mNextId++, name, threshold);
                 
                 mElements[name] = element;
                 mChildNames[element] = children;
@@ -96,15 +102,15 @@ namespace storm {
          
         private:
             
-            unsigned computeRank(std::shared_ptr<DFTElement> const& elem);
+            unsigned computeRank(DFTElementPointer const& elem);
             
             bool addStandardGate(std::string const& name, std::vector<std::string> const& children, DFTElementTypes tp);
             
             enum class topoSortColour {WHITE, BLACK, GREY}; 
             
-            void topoVisit(std::shared_ptr<DFTElement> const& n, std::map<std::shared_ptr<DFTElement>, topoSortColour>& visited, std::vector<std::shared_ptr<DFTElement>>& L);
+            void topoVisit(DFTElementPointer const& n, std::map<DFTElementPointer, topoSortColour>& visited, DFTElementVector& L);
 
-            std::vector<std::shared_ptr<DFTElement>> topoSort();
+            DFTElementVector topoSort();
             
         };
     }
diff --git a/src/storage/dft/DFTElements.cpp b/src/storage/dft/DFTElements.cpp
index a9040eab0..0c18e3be6 100644
--- a/src/storage/dft/DFTElements.cpp
+++ b/src/storage/dft/DFTElements.cpp
@@ -1,11 +1,15 @@
+#include <src/exceptions/NotImplementedException.h>
+#include <src/utility/macros.h>
 #include "DFTElements.h"
 
 namespace storm {
     namespace storage {
-        bool DFTElement::checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
+
+        template<typename ValueType>
+        bool DFTElement<ValueType>::checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
             if(!state.dontCare(mId))
             {
-                for(std::shared_ptr<DFTGate> const& parent : mParents) {
+                for(DFTGatePointer const& parent : mParents) {
                     if(state.isOperational(parent->id())) {
                         return false;
                     }
@@ -16,8 +20,9 @@ namespace storm {
             }
             return false;
         }
-        
-        void DFTElement::extendSpareModule(std::set<size_t>& elementsInModule) const {
+
+        template<typename ValueType>
+        void DFTElement<ValueType>::extendSpareModule(std::set<size_t>& elementsInModule) const {
             for(auto const& parent : mParents) {
                 if(elementsInModule.count(parent->id()) == 0 && !parent->isSpareGate()) {
                     elementsInModule.insert(parent->id());
@@ -25,8 +30,9 @@ namespace storm {
                 }
             }
         }
-        
-        void DFTElement::extendUnit(std::set<size_t>& unit) const {
+
+        template<typename ValueType>
+        void DFTElement<ValueType>::extendUnit(std::set<size_t>& unit) const {
             unit.insert(mId);
             for(auto const& parent : mParents) {
                 if(unit.count(parent->id()) != 0) {
@@ -34,20 +40,23 @@ namespace storm {
                 }
             }
         }
-        
-        void DFTElement::checkForSymmetricChildren() const {
-            
+
+        template<typename ValueType>
+        void DFTElement<ValueType>::checkForSymmetricChildren() const {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not implemented.");
+            assert(false);
         }
 
         template<typename ValueType>
-        bool DFTBE<ValueType>::checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
-            if(DFTElement::checkDontCareAnymore(state, queues)) {
-                state.beNoLongerFailable(mId);
+        bool DFTBE<ValueType>::checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
+            if(DFTElement<ValueType>::checkDontCareAnymore(state, queues)) {
+                state.beNoLongerFailable(this->mId);
                 return true;
             }
             return false;
         }
 
+
         // Explicitly instantiate the class.
         template class DFTBE<double>;
 
diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h
index 7d3c6110c..6296a176f 100644
--- a/src/storage/dft/DFTElements.h
+++ b/src/storage/dft/DFTElements.h
@@ -16,21 +16,28 @@ using std::size_t;
 
 namespace storm {
     namespace storage {
+
+        template<typename ValueType>
         class DFTGate;
-        
+
+        template<typename ValueType>
         class DFTElement {
+
+            using DFTGatePointer = std::shared_ptr<DFTGate<ValueType>>;
+            using DFTGateVector = std::vector<DFTGatePointer>;
+
+
         protected:
             size_t mId;
             std::string mName;
             size_t mRank = -1;
-            std::vector<std::shared_ptr<DFTGate>> mParents;
-            
-
-            
+            DFTGateVector mParents;
 
         public:
-            DFTElement(size_t id, std::string const& name) : mId(id), mName(name)
+            DFTElement(size_t id, std::string const& name) :
+                    mId(id), mName(name)
             {}
+
             virtual ~DFTElement() {}
 
             
@@ -74,7 +81,7 @@ namespace storm {
                 return mName;
             }
             
-            bool addParent(std::shared_ptr<DFTGate> const& e) {
+            bool addParent(DFTGatePointer const& e) {
                 if(std::find(mParents.begin(), mParents.end(), e) != mParents.end()) {
                     return false;
                 }
@@ -89,20 +96,21 @@ namespace storm {
                 return !mParents.empty();
             }
             
-            std::vector<std::shared_ptr<DFTGate>> const& parents() const {
+            DFTGateVector const& parents() const {
                 return mParents;
             }
             
             virtual void extendSpareModule(std::set<size_t>& elementsInModule) const;
             
             virtual size_t nrChildren() const = 0;
+
             virtual std::string toString() const = 0;
 
-            virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const;
+            virtual bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const;
             
             virtual std::vector<size_t> independentUnit() const = 0;
         
-            virtual void  extendUnit(std::set<size_t>& unit) const;
+            virtual void extendUnit(std::set<size_t>& unit) const;
 
             void checkForSymmetricChildren() const;
         };
@@ -130,26 +138,34 @@ namespace storm {
                     assert(false);
             }
         }
-        
-        class DFTGate : public DFTElement {
+
+
+
+        template<typename ValueType>
+        class DFTGate : public DFTElement<ValueType> {
+
+            using DFTElementPointer = std::shared_ptr<DFTElement<ValueType>>;
+            using DFTElementVector = std::vector<DFTElementPointer>;
+
         protected:
-            std::vector<std::shared_ptr<DFTElement>> mChildren;
+            DFTElementVector mChildren;
+
         public:
-            DFTGate(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement>> const& children) :
-            DFTElement(id, name), mChildren(children)
+            DFTGate(size_t id, std::string const& name, DFTElementVector const& children) :
+                    DFTElement<ValueType>(id, name), mChildren(children)
             {}
             
             virtual ~DFTGate() {}
             
-            void pushBackChild(std::shared_ptr<DFTElement> elem) {
+            void pushBackChild(DFTElementPointer elem) {
                 return mChildren.push_back(elem);
             }
 
             size_t nrChildren() const override {
                 return mChildren.size();
             }
-            
-            std::vector<std::shared_ptr<DFTElement>> const& children() const {
+
+            DFTElementVector const& children() const {
                 return mChildren;
             }
             
@@ -159,11 +175,13 @@ namespace storm {
             
             
             virtual std::string typestring() const = 0;
-            virtual void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const = 0;
-            virtual void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const = 0;
+
+            virtual void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const = 0;
+
+            virtual void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const = 0;
             
             virtual void extendSpareModule(std::set<size_t>& elementsInSpareModule) const override {
-                DFTElement::extendSpareModule(elementsInSpareModule);
+                DFTElement<ValueType>::extendSpareModule(elementsInSpareModule);
                 for(auto const& child : mChildren) {
                     if(elementsInSpareModule.count(child->id()) == 0) {
                         elementsInSpareModule.insert(child->id());
@@ -173,24 +191,22 @@ namespace storm {
             }
             
             virtual std::vector<size_t> independentUnit() const override {
-                std::set<size_t> unit = {mId};
+                std::set<size_t> unit = {this->mId};
                 for(auto const& child : mChildren) {
                     child->extendUnit(unit);
                 }
-                for(auto const& parent : mParents) {
+                for(auto const& parent : this->mParents) {
                     if(unit.count(parent->id()) != 0) {
                         return {};
                     } 
                 }
-                return std::vector<size_t>(unit.begin(), unit.end()); 
-           }
-
-            
+                return std::vector<size_t>(unit.begin(), unit.end());
+            }
             
             virtual std::string toString() const override {
                 std::stringstream stream;
-                stream << "{" << name() << "} " << typestring() << "( ";
-                std::vector<std::shared_ptr<DFTElement>>::const_iterator it = mChildren.begin();
+                stream << "{" << this->name() << "} " << typestring() << "( ";
+                typename DFTElementVector::const_iterator it = mChildren.begin();
                 stream << (*it)->name();
                 ++it;
                 while(it != mChildren.end()) {
@@ -199,10 +215,10 @@ namespace storm {
                 }
                 stream << ")";
                 return stream.str();
-            }    
-            
-            virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override {
-                if(DFTElement::checkDontCareAnymore(state, queues)) {
+            }
+
+            virtual bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+                if(DFTElement<ValueType>::checkDontCareAnymore(state, queues)) {
                     childrenDontCare(state, queues);
                     return true;
                 }
@@ -210,37 +226,37 @@ namespace storm {
             }
             
             virtual void extendUnit(std::set<size_t>& unit) const override {
-                DFTElement::extendUnit(unit);
+                DFTElement<ValueType>::extendUnit(unit);
                 for(auto const& child : mChildren) {
                     child->extendUnit(unit);
                 }
             }
             
         protected:
-            
-            void fail(DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
-                for(std::shared_ptr<DFTGate> parent : mParents) {
+
+            void fail(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
+                for(std::shared_ptr<DFTGate> parent : this->mParents) {
                     if(state.isOperational(parent->id())) {
                         queues.propagateFailure(parent);
                     }
                 }
-                state.setFailed(mId);        
+                state.setFailed(this->mId);
             }
-            
-            void failsafe(DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
-                for(std::shared_ptr<DFTGate> parent : mParents) {
+
+            void failsafe(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
+                for(std::shared_ptr<DFTGate> parent : this->mParents) {
                     if(state.isOperational(parent->id())) {
                         queues.propagateFailsafe(parent);
                     }
                 }
-                state.setFailsafe(mId);
+                state.setFailsafe(this->mId);
             }
-            
-            void childrenDontCare(DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
+
+            void childrenDontCare(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
                 queues.propagateDontCare(mChildren);
             }
-            
-            bool hasFailsafeChild(DFTState& state) const {
+
+            bool hasFailsafeChild(DFTState<ValueType>& state) const {
                 for(auto const& child : mChildren) {
                     if(state.isFailsafe(child->id()))
                     {
@@ -249,9 +265,8 @@ namespace storm {
                 }
                 return false;
             }
-            
-            
-            bool hasFailedChild(DFTState& state) const {
+
+            bool hasFailedChild(DFTState<ValueType>& state) const {
                 for(auto const& child : mChildren) {
                     if(state.hasFailed(child->id())) {
                         return true;
@@ -265,17 +280,15 @@ namespace storm {
        
 
         template<typename ValueType>
-        class DFTBE : public DFTElement {
-
+        class DFTBE : public DFTElement<ValueType> {
 
             ValueType mActiveFailureRate;
             ValueType mPassiveFailureRate;
+
         public:
             DFTBE(size_t id, std::string const& name, ValueType failureRate, ValueType dormancyFactor) :
-            DFTElement(id, name), mActiveFailureRate(failureRate), mPassiveFailureRate(dormancyFactor * failureRate)
-            {
-                
-            }
+                    DFTElement<ValueType>(id, name), mActiveFailureRate(failureRate), mPassiveFailureRate(dormancyFactor * failureRate)
+            {}
                         
             virtual size_t nrChildren() const {
                 return 0;
@@ -304,9 +317,10 @@ namespace storm {
             }
             
             virtual std::vector<size_t> independentUnit() const {
-                return {mId};
+                return {this->mId};
             }
-            virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const;
+
+            virtual bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const;
         };
 
         template<typename ValueType>
@@ -314,16 +328,17 @@ namespace storm {
             return os << "{" << be.name() << "} BE(" << be.activeFailureRate() << ", " << be.passiveFailureRate() << ")";
         }
 
-        
-        
 
-        class DFTConst : public DFTElement {
+
+        template<typename ValueType>
+        class DFTConst : public DFTElement<ValueType> {
+
             bool mFailed;
+
         public:
-            DFTConst(size_t id, std::string const& name, bool failed) : DFTElement(id, name), mFailed(failed) 
-            {
-                
-            }
+            DFTConst(size_t id, std::string const& name, bool failed) :
+                    DFTElement<ValueType>(id, name), mFailed(failed)
+            {}
             
             bool failed() const {
                 return mFailed;
@@ -339,96 +354,96 @@ namespace storm {
             
         };
 
-        class DFTAnd : public DFTGate {
+
+
+        template<typename ValueType>
+        class DFTAnd : public DFTGate<ValueType> {
             
         public:
-            DFTAnd(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement>> const& children = {}) :
-            DFTGate(id, name, children) 
+            DFTAnd(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
+                    DFTGate<ValueType>(id, name, children)
             {}
-            
-            void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
-                
-                if(state.isOperational(mId)) {
-                    for(auto const& child : mChildren)
+
+            void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
+                if(state.isOperational(this->mId)) {
+                    for(auto const& child : this->mChildren)
                     {
                         if(!state.hasFailed(child->id())) {
-                            return;// false;
+                            return;
                         }
                     }
-                    fail(state, queues);
-                    //return true;
-                } 
-                //return false;
+                    this->fail(state, queues);
+                }
             }
-            
-            void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{
-                assert(hasFailsafeChild(state));
-                if(state.isOperational(mId)) {
-                    failsafe(state, queues);
-                    childrenDontCare(state, queues);
-                    //return true;
+
+            void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const{
+                assert(this->hasFailsafeChild(state));
+                if(state.isOperational(this->mId)) {
+                    this->failsafe(state, queues);
+                    this->childrenDontCare(state, queues);
                 }
-                //return false;
             }
             
             std::string typestring() const {
                 return "AND";
             }
         };
-        
-        inline std::ostream& operator<<(std::ostream& os, DFTAnd const& gate) {
+
+        template<typename ValueType>
+        inline std::ostream& operator<<(std::ostream& os, DFTAnd<ValueType> const& gate) {
             return os << gate.toString();
         }
-       
+
         
 
-        class DFTOr : public DFTGate {
+        template<typename ValueType>
+        class DFTOr : public DFTGate<ValueType> {
+
         public:
-            DFTOr(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement>> const& children = {}) :
-            DFTGate(id, name, children) 
+            DFTOr(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
+                    DFTGate<ValueType>(id, name, children)
             {}
-            
-             void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
-                 assert(hasFailedChild(state));
-                if(state.isOperational(mId)) {
-                    fail(state, queues);
-                    //return true;
-                } 
-                // return false;
+
+            void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
+                assert(this->hasFailedChild(state));
+                if(state.isOperational(this->mId)) {
+                    this->fail(state, queues);
+                }
             }
-             
-            void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{
-                 for(auto const& child : mChildren) {
+
+            void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const{
+                 for(auto const& child : this->mChildren) {
                      if(!state.isFailsafe(child->id())) {
-                         return;// false;
+                         return;
                      }
                  }
-                 failsafe(state, queues);
-                 //return true;
+                 this->failsafe(state, queues);
             }
             
             std::string typestring() const {
                 return "OR";
             }
-        private:
-            //static const std::string typestring = "or";
         };
-        
-         inline std::ostream& operator<<(std::ostream& os, DFTOr const& gate) {
+
+        template<typename ValueType>
+        inline std::ostream& operator<<(std::ostream& os, DFTOr<ValueType> const& gate) {
             return os << gate.toString();
         }
 
-        class DFTSeqAnd : public DFTGate {
+
+
+        template<typename ValueType>
+        class DFTSeqAnd : public DFTGate<ValueType> {
+
         public:
-            DFTSeqAnd(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement>> const& children = {}) :
-            DFTGate(id, name, children) 
+            DFTSeqAnd(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
+                    DFTGate<ValueType>(id, name, children)
             {}
-            
-            void checkFails(storm::storage::DFTState& state,  DFTStateSpaceGenerationQueues& queues) const {
-                
-                if(!state.hasFailed(mId)) {
+
+            void checkFails(storm::storage::DFTState<ValueType>& state,  DFTStateSpaceGenerationQueues<ValueType>& queues) const {
+                if(!state.hasFailed(this->mId)) {
                     bool childOperationalBefore = false;
-                    for(auto const& child : mChildren)
+                    for(auto const& child : this->mChildren)
                     {
                         if(!state.hasFailed(child->id())) {
                             childOperationalBefore = true;
@@ -436,22 +451,20 @@ namespace storm {
                         else {
                             if(childOperationalBefore) {
                                 state.markAsInvalid();
-                                return; //false;
+                                return;
                             }
                         }
                     }
                     if(!childOperationalBefore) {
                        fail(state, queues);
-                       //return true;
                     }
                   
                 } 
-                //return false;
             }
-            
-            void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{
+
+            void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const{
                 assert(hasFailsafeChild(state));
-                if(state.isOperational(mId)) {
+                if(state.isOperational(this->mId)) {
                     failsafe(state, queues);
                     //return true;
                 }
@@ -461,71 +474,74 @@ namespace storm {
             std::string  typestring() const {
                 return "SEQAND";
             }
-        private:
-            //static const std::string typestring = "seqand"; 
         };
-        
-         inline std::ostream& operator<<(std::ostream& os, DFTSeqAnd const& gate) {
+
+        template<typename ValueType>
+        inline std::ostream& operator<<(std::ostream& os, DFTSeqAnd<ValueType> const& gate) {
              return os << gate.toString();
         }
-        
-        class DFTPand : public DFTGate {
+
+
+
+        template<typename ValueType>
+        class DFTPand : public DFTGate<ValueType> {
+
         public:
-            DFTPand(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement>> const& children = {}) :
-            DFTGate(id, name, children) 
+            DFTPand(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
+                    DFTGate<ValueType>(id, name, children)
             {}
-            
-            void checkFails(storm::storage::DFTState& state,  DFTStateSpaceGenerationQueues& queues) const {
-                if(state.isOperational(mId)) {
+
+            void checkFails(storm::storage::DFTState<ValueType>& state,  DFTStateSpaceGenerationQueues<ValueType>& queues) const {
+                if(state.isOperational(this->mId)) {
                     bool childOperationalBefore = false;
-                    for(auto const& child : mChildren)
+                    for(auto const& child : this->mChildren)
                     {
                         if(!state.hasFailed(child->id())) {
                             childOperationalBefore = true;
                         } else if(childOperationalBefore && state.hasFailed(child->id())){
-                            failsafe(state, queues);
-                            childrenDontCare(state, queues);
-                            return; //false;
+                            this->failsafe(state, queues);
+                            this->childrenDontCare(state, queues);
+                            return;
                         }
                     }
                     if(!childOperationalBefore) {
-                        fail(state, queues);
-                        //return true;
+                        this->fail(state, queues);
                     }
                 }
-                // return false;
             }
-             
-            void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{
-                assert(hasFailsafeChild(state));
-                if(state.isOperational(mId)) {
-                    failsafe(state, queues);
-                    childrenDontCare(state, queues);
-                    //return true;
+
+            void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const{
+                assert(this->hasFailsafeChild(state));
+                if(state.isOperational(this->mId)) {
+                    this->failsafe(state, queues);
+                    this->childrenDontCare(state, queues);
                 }
-                //return false;
-            } 
+            }
             
             std::string typestring() const {
                 return "PAND";
             }
         };
         
-         inline std::ostream& operator<<(std::ostream& os, DFTPand const& gate) {
+        template<typename ValueType>
+        inline std::ostream& operator<<(std::ostream& os, DFTPand<ValueType> const& gate) {
              return os << gate.toString();
         }
-        
-        class DFTPor : public DFTGate {
+
+
+
+        template<typename ValueType>
+        class DFTPor : public DFTGate<ValueType> {
         public:
-            DFTPor(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement>> const& children = {}) :
-            DFTGate(id, name, children) 
+            DFTPor(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
+                    DFTGate<ValueType>(id, name, children)
             {}
-            
-            void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
+
+            void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
                  assert(false);
             }
-             
-            void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{
+
+            void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const{
                 assert(false);
             }
             
@@ -533,58 +549,60 @@ namespace storm {
                 return "POR";
             }
         };
-        
-         inline std::ostream& operator<<(std::ostream& os, DFTPor const& gate) {
+
+        template<typename ValueType>
+        inline std::ostream& operator<<(std::ostream& os, DFTPor<ValueType> const& gate) {
              return os << gate.toString();
         }
 
-        class DFTVot : public DFTGate {
+
+
+        template<typename ValueType>
+        class DFTVot : public DFTGate<ValueType> {
+
         private:
             unsigned mThreshold;
+
         public:
-            DFTVot(size_t id, std::string const& name, unsigned threshold, std::vector<std::shared_ptr<DFTElement>> const& children = {}) :
-            DFTGate(id, name, children), mThreshold(threshold)
+            DFTVot(size_t id, std::string const& name, unsigned threshold, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
+                    DFTGate<ValueType>(id, name, children), mThreshold(threshold)
             {}
-            
-            void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
-                
-                if(state.isOperational(mId)) {
+
+            void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
+                if(state.isOperational(this->mId)) {
                     unsigned nrFailedChildren = 0;
-                    for(auto const& child : mChildren)
+                    for(auto const& child : this->mChildren)
                     {
                         if(state.hasFailed(child->id())) {
                             ++nrFailedChildren;
                             if(nrFailedChildren >= mThreshold) 
                             {
-                                fail(state, queues);
-                                return;// true;
+                                this->fail(state, queues);
+                                return;
                             }
                         }
                     }
                   
                 } 
-                //    return false;
-               
             }
-            
-            void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{
-                assert(hasFailsafeChild(state));
-                if(state.isOperational(mId)) {
+
+            void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const{
+                assert(this->hasFailsafeChild(state));
+                if(state.isOperational(this->mId)) {
                     unsigned nrFailsafeChildren = 0;
-                    for(auto const& child : mChildren)
+                    for(auto const& child : this->mChildren)
                     {
                         if(state.isFailsafe(child->id())) {
                             ++nrFailsafeChildren;
-                            if(nrFailsafeChildren > nrChildren() - mThreshold) 
+                            if(nrFailsafeChildren > this->nrChildren() - mThreshold)
                             {
-                                failsafe(state, queues);
-                                childrenDontCare(state, queues);
-                                return;// true;
+                                this->failsafe(state, queues);
+                                this->childrenDontCare(state, queues);
+                                return;
                             }
                         }
                     }
                 }
-                //return false;
             }
             
             std::string typestring() const {
@@ -593,21 +611,24 @@ namespace storm {
 
         };
 
-        inline std::ostream& operator<<(std::ostream& os, DFTVot const& gate) {
+        template<typename ValueType>
+        inline std::ostream& operator<<(std::ostream& os, DFTVot<ValueType> const& gate) {
             return os << gate.toString();
-        }        
-        
-        class DFTSpare : public DFTGate {
+        }
+
+
+
+        template<typename ValueType>
+        class DFTSpare : public DFTGate<ValueType> {
+
+        private:
             size_t mUseIndex;
             size_t mActiveIndex;
             
         public:
-            DFTSpare(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement>> const& children = {}) :
-            DFTGate(id, name, children)
-            {
-                
-            }
-            
+            DFTSpare(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
+                    DFTGate<ValueType>(id, name, children)
+            {}
             
             std::string typestring() const {
                 return "SPARE";
@@ -624,39 +645,40 @@ namespace storm {
             void setActiveIndex(size_t activeIndex) {
                 mActiveIndex = activeIndex;
             }
-            
-            void initializeUses(storm::storage::DFTState& state) {
-                assert(mChildren.size() > 0);
-                state.setUsesAtPosition(mUseIndex, mChildren[0]->id());
+
+            void initializeUses(storm::storage::DFTState<ValueType>& state) {
+                assert(this->mChildren.size() > 0);
+                state.setUsesAtPosition(mUseIndex, this->mChildren[0]->id());
             }
-            
-            void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
-                if(state.isOperational(mId)) {
+
+            void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
+                if(state.isOperational(this->mId)) {
                     size_t uses = state.extractUses(mUseIndex);
                     if(!state.isOperational(uses)) {
                         // TODO compute children ids before.
                         std::vector<size_t> childrenIds;
-                        for(auto const& child : mChildren) {
+                        for(auto const& child : this->mChildren) {
                             childrenIds.push_back(child->id());
                         }
                         
-                        bool claimingSuccessful = state.claimNew(mId, mUseIndex, uses, childrenIds);
+                        bool claimingSuccessful = state.claimNew(this->mId, mUseIndex, uses, childrenIds);
                         if(!claimingSuccessful) {
-                            fail(state, queues);
+                            this->fail(state, queues);
                         }
                     }                  
                 } 
             }
-            
-            void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
-                if(state.isOperational(mId)) {
+
+            void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
+                if(state.isOperational(this->mId)) {
                     if(state.isFailsafe(state.extractUses((mUseIndex)))) {
-                        failsafe(state, queues);
-                        childrenDontCare(state, queues);
+                        this->failsafe(state, queues);
+                        this->childrenDontCare(state, queues);
                     }
                 }
             }
         };
+
     }
 }
 
diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp
index 87838b9a2..98cada93a 100644
--- a/src/storage/dft/DFTState.cpp
+++ b/src/storage/dft/DFTState.cpp
@@ -5,8 +5,8 @@
 namespace storm {
     namespace storage {
 
-        // TODO Matthias: template
-        DFTState::DFTState(DFT<double> const& dft, size_t id) : mStatus(dft.stateSize()), mId(id), mDft(dft)  {
+        template<typename ValueType>
+        DFTState<ValueType>::DFTState(DFT<ValueType> const& dft, size_t id) : mStatus(dft.stateSize()), mId(id), mDft(dft)  {
             mInactiveSpares = dft.getSpareIndices();
             dft.initializeUses(*this);
             dft.initializeActivation(*this);
@@ -14,70 +14,83 @@ namespace storm {
             mIsCurrentlyFailableBE.insert(mIsCurrentlyFailableBE.end(), alwaysActiveBEs.begin(), alwaysActiveBEs.end());
             
         }
-        
-        DFTElementState DFTState::getElementState(size_t id) const {
+
+        template<typename ValueType>
+        DFTElementState DFTState<ValueType>::getElementState(size_t id) const {
             return static_cast<DFTElementState>(getElementStateInt(id));
         }
 
-        int DFTState::getElementStateInt(size_t id) const {
+        template<typename ValueType>
+        int DFTState<ValueType>::getElementStateInt(size_t id) const {
             return mStatus.getAsInt(mDft.failureIndex(id), 2);
         }
 
-        size_t DFTState::getId() const {
+        template<typename ValueType>
+        size_t DFTState<ValueType>::getId() const {
             return mId;
         }
 
-        void DFTState::setId(size_t id) {
+        template<typename ValueType>
+        void DFTState<ValueType>::setId(size_t id) {
             mId = id;
         }
 
-        bool DFTState::isOperational(size_t id) const {
+        template<typename ValueType>
+        bool DFTState<ValueType>::isOperational(size_t id) const {
             return getElementState(id) == DFTElementState::Operational;
         }
 
-        bool DFTState::hasFailed(size_t id) const {
+        template<typename ValueType>
+        bool DFTState<ValueType>::hasFailed(size_t id) const {
             return mStatus[mDft.failureIndex(id)];
         }
 
-        bool DFTState::isFailsafe(size_t id) const {
+        template<typename ValueType>
+        bool DFTState<ValueType>::isFailsafe(size_t id) const {
             return mStatus[mDft.failureIndex(id)+1];
         }
 
-        bool DFTState::dontCare(size_t id) const {
+        template<typename ValueType>
+        bool DFTState<ValueType>::dontCare(size_t id) const {
             return getElementState(id) == DFTElementState::DontCare;
         }
 
-        void DFTState::setFailed(size_t id) {
+        template<typename ValueType>
+        void DFTState<ValueType>::setFailed(size_t id) {
             mStatus.set(mDft.failureIndex(id));
         }
 
-        void DFTState::setFailsafe(size_t id) {
+        template<typename ValueType>
+        void DFTState<ValueType>::setFailsafe(size_t id) {
             mStatus.set(mDft.failureIndex(id)+1);
         }
 
-        void DFTState::setDontCare(size_t id) {
+        template<typename ValueType>
+        void DFTState<ValueType>::setDontCare(size_t id) {
             mStatus.setFromInt(mDft.failureIndex(id), 2, static_cast<uint_fast64_t>(DFTElementState::DontCare) );
         }
-        
-        void DFTState::beNoLongerFailable(size_t id) {
+
+        template<typename ValueType>
+        void DFTState<ValueType>::beNoLongerFailable(size_t id) {
             auto it = std::find(mIsCurrentlyFailableBE.begin(), mIsCurrentlyFailableBE.end(), id);
             if(it != mIsCurrentlyFailableBE.end()) {
                 mIsCurrentlyFailableBE.erase(it);
             }
         }
 
-        // TODO Matthias: template
-        std::pair<std::shared_ptr<DFTBE<double>>, bool> DFTState::letNextBEFail(size_t index)
+        template<typename ValueType>
+        std::pair<std::shared_ptr<DFTBE<ValueType>>, bool> DFTState<ValueType>::letNextBEFail(size_t index)
         {
             assert(index < mIsCurrentlyFailableBE.size());
             STORM_LOG_TRACE("currently failable: " << getCurrentlyFailableString());
-            std::pair<std::shared_ptr<DFTBE<double>>,bool> res(mDft.getBasicElement(mIsCurrentlyFailableBE[index]), false);
+            std::pair<std::shared_ptr<DFTBE<ValueType>>,bool> res(mDft.getBasicElement(mIsCurrentlyFailableBE[index]), false);
             mIsCurrentlyFailableBE.erase(mIsCurrentlyFailableBE.begin() + index);
             setFailed(res.first->id());
             return res;
         }
-        
-        void DFTState::activate(size_t repr) {
+
+        template<typename ValueType>
+        void DFTState<ValueType>::activate(size_t repr) {
             std::vector<size_t>  const& module = mDft.module(repr);
             for(size_t elem : module) {
                 if(mDft.getElement(elem)->isColdBasicElement() && isOperational(elem)) {
@@ -89,33 +102,37 @@ namespace storm {
                 }
             }
         }
-        
-        
-        bool DFTState::isActiveSpare(size_t id) const {
+
+        template<typename ValueType>
+        bool DFTState<ValueType>::isActiveSpare(size_t id) const {
             assert(mDft.getElement(id)->isSpareGate());
             return (std::find(mInactiveSpares.begin(), mInactiveSpares.end(), id) == mInactiveSpares.end());
         }
-        
-        uint_fast64_t DFTState::uses(size_t id) const {
+
+        template<typename ValueType>
+        uint_fast64_t DFTState<ValueType>::uses(size_t id) const {
             return extractUses(mDft.usageIndex(id));
         }
-        
-        uint_fast64_t DFTState::extractUses(size_t from) const {
+
+        template<typename ValueType>
+        uint_fast64_t DFTState<ValueType>::extractUses(size_t from) const {
             assert(mDft.usageInfoBits() < 64);
             return mStatus.getAsInt(from, mDft.usageInfoBits());
         }
-        
-        bool DFTState::isUsed(size_t child) {
+
+        template<typename ValueType>
+        bool DFTState<ValueType>::isUsed(size_t child) {
             return (std::find(mUsedRepresentants.begin(), mUsedRepresentants.end(), child) != mUsedRepresentants.end());
-            
         }
-        
-        void DFTState::setUsesAtPosition(size_t usageIndex, size_t child) {
+
+        template<typename ValueType>
+        void DFTState<ValueType>::setUsesAtPosition(size_t usageIndex, size_t child) {
             mStatus.setFromInt(usageIndex, mDft.usageInfoBits(), child);
             mUsedRepresentants.push_back(child);
         }
-        
-        bool DFTState::claimNew(size_t spareId, size_t usageIndex, size_t currentlyUses, std::vector<size_t> const& childIds) {
+
+        template<typename ValueType>
+        bool DFTState<ValueType>::claimNew(size_t spareId, size_t usageIndex, size_t currentlyUses, std::vector<size_t> const& childIds) {
             auto it = find(childIds.begin(), childIds.end(), currentlyUses);
             assert(it != childIds.end());
             ++it;
@@ -132,5 +149,12 @@ namespace storm {
             return false;
         }
 
+        // Explicitly instantiate the class.
+        template class DFTState<double>;
+
+#ifdef STORM_HAVE_CARL
+        template class DFTState<RationalFunction>;
+#endif
+
     }
-}
+}
\ No newline at end of file
diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h
index 1e8f8cb01..4f25550b0 100644
--- a/src/storage/dft/DFTState.h
+++ b/src/storage/dft/DFTState.h
@@ -14,7 +14,7 @@ namespace storm {
         template<typename ValueType>
         class DFTBE;
 
-
+        template<typename ValueType>
         class DFTState {
             friend struct std::hash<DFTState>;
         private:
@@ -24,12 +24,10 @@ namespace storm {
             std::vector<size_t> mIsCurrentlyFailableBE;
             std::vector<size_t> mUsedRepresentants;
             bool mValid = true;
-            // TODO Matthias: template
-            const DFT<double>& mDft;
+            const DFT<ValueType>& mDft;
             
         public:
-            // TODO Matthias: template
-            DFTState(DFT<double> const& dft, size_t id);
+            DFTState(DFT<ValueType> const& dft, size_t id);
             
             DFTElementState getElementState(size_t id) const;
 
@@ -109,8 +107,7 @@ namespace storm {
                 return mIsCurrentlyFailableBE.size();
             }
 
-            // TODO Matthias: template
-            std::pair<std::shared_ptr<DFTBE<double>>, bool> letNextBEFail(size_t smallestIndex = 0);
+            std::pair<std::shared_ptr<DFTBE<ValueType>>, bool> letNextBEFail(size_t smallestIndex = 0);
             
             std::string getCurrentlyFailableString() {
                 std::stringstream stream;
@@ -137,9 +134,9 @@ namespace storm {
 }
 
 namespace std {
-    template<>
-    struct hash<storm::storage::DFTState> {
-        size_t operator()(storm::storage::DFTState const& s) const {
+    template<typename ValueType>
+    struct hash<storm::storage::DFTState<ValueType>> {
+        size_t operator()(storm::storage::DFTState<ValueType> const& s) const {
             return hash<storm::storage::BitVector>()(s.mStatus);
         }
     };
diff --git a/src/storage/dft/DFTStateSpaceGenerationQueues.h b/src/storage/dft/DFTStateSpaceGenerationQueues.h
index ec0879d52..b881a220b 100644
--- a/src/storage/dft/DFTStateSpaceGenerationQueues.h
+++ b/src/storage/dft/DFTStateSpaceGenerationQueues.h
@@ -10,19 +10,28 @@
 
 namespace storm {
     namespace storage {
+
+        template<typename ValueType>
         class DFTGate;
+        template<typename ValueType>
         class DFTElement;
-        
-    
-        
+
+
+        template<typename ValueType>
         class DFTStateSpaceGenerationQueues {
-            std::priority_queue<std::shared_ptr<DFTGate>, std::vector<std::shared_ptr<DFTGate>>, OrderElementsByRank> failurePropagation;
-            std::vector<std::shared_ptr<DFTGate>> failsafePropagation;
-            std::vector<std::shared_ptr<DFTElement>> dontcarePropagation;
-            std::vector<std::shared_ptr<DFTElement>> activatePropagation;
+
+            using DFTElementPointer = std::shared_ptr<DFTElement<ValueType>>;
+            using DFTElementVector = std::vector<DFTElementPointer>;
+            using DFTGatePointer = std::shared_ptr<DFTGate<ValueType>>;
+            using DFTGateVector = std::vector<DFTGatePointer>;
+
+            std::priority_queue<DFTGatePointer, DFTGateVector, OrderElementsByRank<ValueType>> failurePropagation;
+            DFTGateVector failsafePropagation;
+            DFTElementVector dontcarePropagation;
+            DFTElementVector activatePropagation;
 
         public:
-            void propagateFailure(std::shared_ptr<DFTGate> const& elem) {
+            void propagateFailure(DFTGatePointer const& elem) {
                 failurePropagation.push(elem);
             }
 
@@ -30,8 +39,8 @@ namespace storm {
                 return failurePropagation.empty();
             }
 
-            std::shared_ptr<DFTGate> nextFailurePropagation() {
-                std::shared_ptr<DFTGate> next = failurePropagation.top();
+            DFTGatePointer nextFailurePropagation() {
+                DFTGatePointer next = failurePropagation.top();
                 failurePropagation.pop();
                 return next;
             }
@@ -40,12 +49,12 @@ namespace storm {
                 return failsafePropagation.empty();
             }
             
-            void propagateFailsafe(std::shared_ptr<DFTGate> const& gate) {
+            void propagateFailsafe(DFTGatePointer const& gate) {
                 failsafePropagation.push_back(gate);
             }
-            
-            std::shared_ptr<DFTGate> nextFailsafePropagation() {
-                std::shared_ptr<DFTGate> next = failsafePropagation.back();
+
+            DFTGatePointer nextFailsafePropagation() {
+                DFTGatePointer next = failsafePropagation.back();
                 failsafePropagation.pop_back();
                 return next;
             }
@@ -54,25 +63,23 @@ namespace storm {
                 return dontcarePropagation.empty();
             }
             
-            void propagateDontCare(std::shared_ptr<DFTElement> const& elem) {
+            void propagateDontCare(DFTElementPointer const& elem) {
                 dontcarePropagation.push_back(elem);
             }
             
-            void propagateDontCare(std::vector<std::shared_ptr<DFTElement>> const& elems) {
+            void propagateDontCare(DFTElementVector const& elems) {
                 dontcarePropagation.insert(dontcarePropagation.end(), elems.begin(), elems.end());
             }
             
-            std::shared_ptr<DFTElement> nextDontCarePropagation() {
-                std::shared_ptr<DFTElement> next = dontcarePropagation.back();
+            DFTElementPointer nextDontCarePropagation() {
+                DFTElementPointer next = dontcarePropagation.back();
                 dontcarePropagation.pop_back();
                 return next;
             }
         };
+
     }
-    
 }
 
-
-
 #endif	/* DFTSTATESPACEGENERATIONQUEUES_H */
 
diff --git a/src/storage/dft/OrderDFTElementsById.cpp b/src/storage/dft/OrderDFTElementsById.cpp
index 017969848..6c9493bee 100644
--- a/src/storage/dft/OrderDFTElementsById.cpp
+++ b/src/storage/dft/OrderDFTElementsById.cpp
@@ -3,16 +3,31 @@
 
 namespace storm {
     namespace storage {
-        bool OrderElementsById::operator()(std::shared_ptr<DFTGate> const& a , std::shared_ptr<DFTGate> const& b) const {
+
+        template<typename ValueType>
+        bool OrderElementsById<ValueType>::operator()(std::shared_ptr<DFTGate<ValueType>> const& a , std::shared_ptr<DFTGate<ValueType>> const& b) const {
             return a->id() < b->id();
         }
-        bool OrderElementsById::operator ()(const std::shared_ptr<DFTElement>& a, const std::shared_ptr<DFTElement>& b) const {
+
+        template<typename ValueType>
+        bool OrderElementsById<ValueType>::operator ()(const std::shared_ptr<DFTElement<ValueType>>& a, const std::shared_ptr<DFTElement<ValueType>>& b) const {
             return a->id() < b->id();
         }
-        
-        
-        bool OrderElementsByRank::operator ()(const std::shared_ptr<DFTGate>& a, const std::shared_ptr<DFTGate>& b) const {
+
+
+        template<typename ValueType>
+        bool OrderElementsByRank<ValueType>::operator ()(const std::shared_ptr<DFTGate<ValueType>>& a, const std::shared_ptr<DFTGate<ValueType>>& b) const {
             return a->rank() < b->rank();
         }
+
+
+        // Explicitly instantiate the class.
+        template class OrderElementsById<double>;
+        template class OrderElementsByRank<double>;
+
+#ifdef STORM_HAVE_CARL
+        template class OrderElementsById<RationalFunction>;
+        template class OrderElementsByRank<RationalFunction>;
+#endif
     }
 }
diff --git a/src/storage/dft/OrderDFTElementsById.h b/src/storage/dft/OrderDFTElementsById.h
index 8dfc22da0..821a2de45 100644
--- a/src/storage/dft/OrderDFTElementsById.h
+++ b/src/storage/dft/OrderDFTElementsById.h
@@ -5,16 +5,22 @@
 
 namespace storm {
     namespace storage {
+
+        template<typename ValueType>
         class DFTGate;
+        template<typename ValueType>
         class DFTElement;
-        
+
+        template<typename ValueType>
         struct OrderElementsById {
-            bool operator()(std::shared_ptr<DFTGate> const& a , std::shared_ptr<DFTGate> const& b) const;
-            bool operator()(std::shared_ptr<DFTElement> const& a, std::shared_ptr<DFTElement> const& b) const;
+            bool operator()(std::shared_ptr<DFTGate<ValueType>> const& a , std::shared_ptr<DFTGate<ValueType>> const& b) const;
+
+            bool operator()(std::shared_ptr<DFTElement<ValueType>> const& a, std::shared_ptr<DFTElement<ValueType>> const& b) const;
         };
-        
+
+        template<typename ValueType>
         struct OrderElementsByRank {
-            bool operator()(std::shared_ptr<DFTGate> const& a, std::shared_ptr<DFTGate> const& b) const;
+            bool operator()(std::shared_ptr<DFTGate<ValueType>> const& a, std::shared_ptr<DFTGate<ValueType>> const& b) const;
         };
 
     }