diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp
index 8683dd57e..788c5a0fa 100644
--- a/src/builder/ExplicitDFTModelBuilder.cpp
+++ b/src/builder/ExplicitDFTModelBuilder.cpp
@@ -3,69 +3,132 @@
 namespace storm {
     namespace builder {
 
-        void ExplicitDFTModelBuilder::exploreStateSuccessors(storm::storage::DFTState const &state) {
-            size_t smallest = 0;
+        template<typename ValueType, typename RewardModelType, typename IndexType>
+        void ExplicitDFTModelBuilder<ValueType, RewardModelType, IndexType>::buildCTMC() {
+            // Initialize
+            storm::storage::DFTState state(mDft, newIndex++);
+            mStates.insert(state);
 
-            while(smallest < state.nrFailableBEs()) {
-                //std::cout << "exploring from: " << mDft.getStateString(state) << std::endl;
+            std::queue<storm::storage::DFTState> stateQueue;
+            stateQueue.push(state);
 
-                storm::storage::DFTState newState(state);
-                std::pair<std::shared_ptr<storm::storage::DFTBE<double>>, bool> nextBE = newState.letNextBEFail(smallest++);
-                if(nextBE.first == nullptr) {
-                    //std::cout << "break" << std::endl;
-                    break;
+            bool deterministicModel = true;
+            storm::storage::SparseMatrixBuilder<ValueType> transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0);
 
-                }
-                //std::cout << "with the failure of: " << nextBE.first->name() << " [" << nextBE.first->id() << "]" << std::endl;
+            // Begin model generation
+            exploreStates(stateQueue, transitionMatrixBuilder);
+            //std::cout << "Generated " << mStates.size() << " states" << std::endl;
+
+            // Build CTMC
+            transitionMatrix = transitionMatrixBuilder.build();
+            //std::cout << "TransitionMatrix: " << std::endl;
+            //std::cout << transitionMatrix << std::endl;
+            // TODO Matthias: build CTMC
+        }
+
+        template<typename ValueType, typename RewardModelType, typename IndexType>
+        void ExplicitDFTModelBuilder<ValueType, RewardModelType, IndexType>::exploreStates(std::queue<storm::storage::DFTState>& stateQueue, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder) {
+
+            std::vector<std::pair<size_t, ValueType>> outgoingTransitions;
+
+            while (!stateQueue.empty()) {
+                // Initialization
+                outgoingTransitions.clear();
+                ValueType sum = 0;
+
+                // Consider next state
+                storm::storage::DFTState state = stateQueue.front();
+                stateQueue.pop();
 
-                storm::storage::DFTStateSpaceGenerationQueues queues;
+                size_t smallest = 0;
+
+                // Let BE fail
+                while (smallest < state.nrFailableBEs()) {
+                    //std::cout << "exploring from: " << mDft.getStateString(state) << std::endl;
+
+                    storm::storage::DFTState 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;
+                        break;
 
-                for(std::shared_ptr<storm::storage::DFTGate> parent : nextBE.first->parents()) {
-                    if(newState.isOperational(parent->id())) {
-                        queues.propagateFailure(parent);
                     }
-                }
+                    //std::cout << "with the failure of: " << nextBE.first->name() << " [" << nextBE.first->id() << "]" << std::endl;
 
-                while(!queues.failurePropagationDone()) {
-                    std::shared_ptr<storm::storage::DFTGate> next = queues.nextFailurePropagation();
-                    next->checkFails(newState, queues);
-                }
+                    storm::storage::DFTStateSpaceGenerationQueues queues;
 
-                while(!queues.failsafePropagationDone()) {
-                    std::shared_ptr<storm::storage::DFTGate> next = queues.nextFailsafePropagation();
-                    next->checkFailsafe(newState, queues);
-                }
+                    for (std::shared_ptr<storm::storage::DFTGate> parent : nextBE.first->parents()) {
+                        if (newState.isOperational(parent->id())) {
+                            queues.propagateFailure(parent);
+                        }
+                    }
 
-                while(!queues.dontCarePropagationDone()) {
-                    std::shared_ptr<storm::storage::DFTElement> next = queues.nextDontCarePropagation();
-                    next->checkDontCareAnymore(newState, queues);
-                }
+                    while (!queues.failurePropagationDone()) {
+                        std::shared_ptr<storm::storage::DFTGate> next = queues.nextFailurePropagation();
+                        next->checkFails(newState, queues);
+                    }
 
-                auto it = mStates.find(newState);
-                if (it == mStates.end()) {
-                    // New state
-                    newState.setId(newIndex++);
-                    mStates.insert(newState);
-                    //std::cout << "New state " << mDft.getStateString(newState) << std::endl;
+                    while (!queues.failsafePropagationDone()) {
+                        std::shared_ptr<storm::storage::DFTGate> next = queues.nextFailsafePropagation();
+                        next->checkFailsafe(newState, queues);
+                    }
 
-                    // Recursive call
-                    if(!mDft.hasFailed(newState) && !mDft.isFailsafe(newState)) {
-                        exploreStateSuccessors(newState);
-                    } else {
-                        if (mDft.hasFailed(newState)) {
-                            //std::cout << "Failed " << mDft.getStateString(newState) << std::endl;
+                    while (!queues.dontCarePropagationDone()) {
+                        std::shared_ptr<storm::storage::DFTElement> next = queues.nextDontCarePropagation();
+                        next->checkDontCareAnymore(newState, queues);
+                    }
+
+                    auto it = mStates.find(newState);
+                    if (it == mStates.end()) {
+                        // New state
+                        newState.setId(newIndex++);
+                        auto itInsert = mStates.insert(newState);
+                        assert(itInsert.second);
+                        it = itInsert.first;
+                        //std::cout << "New state " << mDft.getStateString(newState) << std::endl;
+
+                        // Recursive call
+                        if (!mDft.hasFailed(newState) && !mDft.isFailsafe(newState)) {
+                            stateQueue.push(newState);
                         } else {
-                            assert(mDft.isFailsafe(newState));
-                            //std::cout << "Failsafe" << mDft.getStateString(newState) << std::endl;
+                            if (mDft.hasFailed(newState)) {
+                                //std::cout << "Failed " << mDft.getStateString(newState) << std::endl;
+                            } else {
+                                assert(mDft.isFailsafe(newState));
+                                //std::cout << "Failsafe" << mDft.getStateString(newState) << std::endl;
+                            }
                         }
+                    } else {
+                        // State already exists
+                        //std::cout << "State " << mDft.getStateString(*it) << " already exists" << std::endl;
                     }
-                } else {
-                    // State already exists
-                    //std::cout << "State " << mDft.getStateString(*it) << " already exists" << std::endl;
+
+                    // Set transition
+                    ValueType prob = nextBE.first->activeFailureRate();
+                    outgoingTransitions.push_back(std::make_pair(it->getId(), prob));
+                    sum += prob;
+                } // end while failing BE
+
+                // Add all transitions
+                for (auto it = outgoingTransitions.begin(); it != outgoingTransitions.end(); ++it)
+                {
+                    ValueType rate = it->second / sum;
+                    transitionMatrixBuilder.addNextValue(state.getId(), it->first, rate);
+                    //std::cout << "Added transition from " << state.getId() << " to " << it->first << " with " << rate << std::endl;
                 }
-            }
+
+            } // end while queue
         }
 
+        // Explicitly instantiate the class.
+        template
+        class ExplicitDFTModelBuilder<double, storm::models::sparse::StandardRewardModel<double>, uint32_t>;
+
+#ifdef STORM_HAVE_CARL
+        template class ExplicitDFTModelBuilder<double, storm::models::sparse::StandardRewardModel<storm::Interval>, uint32_t>;
+        template class ExplicitDFTModelBuilder<RationalFunction, storm::models::sparse::StandardRewardModel<RationalFunction>, uint32_t>;
+#endif
+
     } // namespace builder
 } // namespace storm
 
diff --git a/src/builder/ExplicitDFTModelBuilder.h b/src/builder/ExplicitDFTModelBuilder.h
index 7009c4896..8938e690f 100644
--- a/src/builder/ExplicitDFTModelBuilder.h
+++ b/src/builder/ExplicitDFTModelBuilder.h
@@ -3,32 +3,42 @@
 
 #include "../storage/dft/DFT.h"
 
+#include <src/models/sparse/StateLabeling.h>
+#include <src/models/sparse/StandardRewardModel.h>
+#include <src/storage/SparseMatrix.h>
+#include <boost/container/flat_set.hpp>
+#include <boost/optional/optional.hpp>
+#include <stack>
 #include <unordered_set>
 
 namespace storm {
     namespace builder {
+
+        template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename IndexType = uint32_t>
         class ExplicitDFTModelBuilder {
             storm::storage::DFT const &mDft;
             std::unordered_set<storm::storage::DFTState> mStates;
             size_t newIndex = 0;
-            //std::stack<std::shared_ptr<storm::storage::DFTState>> mStack;
+
+            // The transition matrix.
+            storm::storage::SparseMatrix<ValueType> transitionMatrix;
+
+            // The state labeling.
+            storm::models::sparse::StateLabeling stateLabeling;
+
+            // A vector that stores a labeling for each choice.
+            boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> choiceLabeling;
 
         public:
             ExplicitDFTModelBuilder(storm::storage::DFT const &dft) : mDft(dft) {
 
             }
 
-            void buildCTMC() {
-                // Construct starting start
-                storm::storage::DFTState state(mDft, newIndex++);
-                mStates.insert(state);
-                // Begin model generation
-                exploreStateSuccessors(state);
-                std::cout << "Generated " << mStates.size() << " states" << std::endl;
-            }
+            void buildCTMC();
 
         private:
-            void exploreStateSuccessors(storm::storage::DFTState const &state);
+            void exploreStates(std::queue<storm::storage::DFTState>& stateQueue, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder);
+
         };
     }
 }
diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h
index d223387e8..9479293d2 100644
--- a/src/storage/dft/DFTElements.h
+++ b/src/storage/dft/DFTElements.h
@@ -262,14 +262,14 @@ namespace storm {
         
        
 
-        template<typename FailureRateType>
+        template<typename ValueType>
         class DFTBE : public DFTElement {
 
-            
-            FailureRateType mActiveFailureRate;
-            FailureRateType mPassiveFailureRate;
+
+            ValueType mActiveFailureRate;
+            ValueType mPassiveFailureRate;
         public:
-            DFTBE(size_t id, std::string const& name, FailureRateType failureRate, FailureRateType dormancyFactor) :
+            DFTBE(size_t id, std::string const& name, ValueType failureRate, ValueType dormancyFactor) :
             DFTElement(id, name), mActiveFailureRate(failureRate), mPassiveFailureRate(dormancyFactor * failureRate)
             {
                 
@@ -278,12 +278,12 @@ namespace storm {
             virtual size_t nrChildren() const {
                 return 0;
             }
-            
-            FailureRateType const& activeFailureRate() const {
+
+            ValueType const& activeFailureRate() const {
                 return mActiveFailureRate;
             }
-            
-            FailureRateType const& passiveFailureRate() const {
+
+            ValueType const& passiveFailureRate() const {
                 return mPassiveFailureRate;
             }
         
diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp
index b86781460..75f329ccb 100644
--- a/src/storm-dyftee.cpp
+++ b/src/storm-dyftee.cpp
@@ -21,7 +21,7 @@ int main(int argc, char** argv) {
     dft.printSpareModules();
 
     std::cout << "Building CTMC..." << std::endl;
-    storm::builder::ExplicitDFTModelBuilder builder(dft);
+    storm::builder::ExplicitDFTModelBuilder<double> builder(dft);
     builder.buildCTMC();
     std::cout << "Built CTMC" << std::endl;
 
@@ -29,4 +29,3 @@ int main(int argc, char** argv) {
     //TODO check CTMC
     //std::cout << "Checked model" << std::endl;
 }
-