diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp
index 2d466dec8..c6d59d6cb 100644
--- a/src/builder/ExplicitDFTModelBuilder.cpp
+++ b/src/builder/ExplicitDFTModelBuilder.cpp
@@ -55,7 +55,7 @@ namespace storm {
 
 
         template <typename ValueType>
-        std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilder<ValueType>::buildModel() {
+        std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilder<ValueType>::buildModel(LabelOptions const& labelOpts) {
             // Initialize
             DFTStatePointer state = std::make_shared<storm::storage::DFTState<ValueType>>(mDft, *mStateGenerationInfo, newIndex++);
             mStates.findOrAdd(state->status(), state->getId());
@@ -88,26 +88,33 @@ namespace storm {
             modelComponents.stateLabeling.addLabel("init");
             modelComponents.stateLabeling.addLabelToState("init", 0);
             // Label all states corresponding to their status (failed, failsafe, failed BE)
-            modelComponents.stateLabeling.addLabel("failed");
-            modelComponents.stateLabeling.addLabel("failsafe");
+            if(labelOpts.buildFailLabel) {
+                modelComponents.stateLabeling.addLabel("failed");
+            } 
+            if(labelOpts.buildFailSafeLabel) {
+                modelComponents.stateLabeling.addLabel("failsafe");
+            }
+            
             // Collect labels for all BE
             std::vector<std::shared_ptr<storage::DFTBE<ValueType>>> basicElements = mDft.getBasicElements();
             for (std::shared_ptr<storage::DFTBE<ValueType>> elem : basicElements) {
-                modelComponents.stateLabeling.addLabel(elem->name() + "_fail");
+                if(labelOpts.beLabels.count(elem->name()) > 0) {
+                    modelComponents.stateLabeling.addLabel(elem->name() + "_fail");
+                }
             }
 
             for (auto const& stateIdPair : mStates) {
                 storm::storage::BitVector state = stateIdPair.first;
                 size_t stateId = stateIdPair.second;
-                if (mDft.hasFailed(state, *mStateGenerationInfo)) {
+                if (labelOpts.buildFailLabel && mDft.hasFailed(state, *mStateGenerationInfo)) {
                     modelComponents.stateLabeling.addLabelToState("failed", stateId);
                 }
-                if (mDft.isFailsafe(state, *mStateGenerationInfo)) {
+                if (labelOpts.buildFailSafeLabel && mDft.isFailsafe(state, *mStateGenerationInfo)) {
                     modelComponents.stateLabeling.addLabelToState("failsafe", stateId);
                 };
                 // Set fail status for each BE
                 for (std::shared_ptr<storage::DFTBE<ValueType>> elem : basicElements) {
-                    if (storm::storage::DFTState<ValueType>::hasFailed(state, mStateGenerationInfo->getStateIndex(elem->id()))) {
+                    if (labelOpts.beLabels.count(elem->name()) > 0 && storm::storage::DFTState<ValueType>::hasFailed(state, mStateGenerationInfo->getStateIndex(elem->id())) ) {
                         modelComponents.stateLabeling.addLabelToState(elem->name() + "_fail", stateId);
                     }
                 }
@@ -129,7 +136,13 @@ namespace storm {
                 }
                 model = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(std::move(rateMatrix), std::move(modelComponents.stateLabeling));
             } else {
-                model = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates), true);
+                std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates), true);
+                if (ma->hasOnlyTrivialNondeterminism()) {
+                 // Markov automaton can be converted into CTMC
+                    model = ma->convertToCTMC();
+                } else {
+                    model = ma;
+                }
             }
             
             model->printModelInformationToStream(std::cout);
diff --git a/src/builder/ExplicitDFTModelBuilder.h b/src/builder/ExplicitDFTModelBuilder.h
index 322790aa4..522f2375c 100644
--- a/src/builder/ExplicitDFTModelBuilder.h
+++ b/src/builder/ExplicitDFTModelBuilder.h
@@ -46,15 +46,23 @@ namespace storm {
             
             const size_t INITIAL_BUCKETSIZE = 20000;
 
+          
+            
             storm::storage::DFT<ValueType> const& mDft;
             std::shared_ptr<storm::storage::DFTStateGenerationInfo> mStateGenerationInfo;
             storm::storage::BitVectorHashMap<size_t> mStates;
             size_t newIndex = 0;
 
         public:
+              struct LabelOptions {
+                bool buildFailLabel = true;
+                bool buildFailSafeLabel = false;
+                std::set<std::string> beLabels = {};
+            };
+            
             ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft);
 
-            std::shared_ptr<storm::models::sparse::Model<ValueType>> buildModel();
+            std::shared_ptr<storm::models::sparse::Model<ValueType>> buildModel(LabelOptions const& labelOpts);
 
         private:
             bool exploreStates(std::queue<DFTStatePointer>& stateQueue, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<uint_fast64_t>& markovianStates, std::vector<ValueType>& exitRates);
diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp
index c75d96a6c..519036fff 100644
--- a/src/storage/dft/DFT.cpp
+++ b/src/storage/dft/DFT.cpp
@@ -237,11 +237,21 @@ namespace storm {
             return ISD;
         }
 
+        template<typename ValueType>
+        std::vector<size_t> DFT<ValueType>::immediateFailureCauses(size_t index) const {
+            if(isGate(index)) {
+
+            } else {
+                return {index};
+            }
+        }
+
         template<typename ValueType>
         DFTColouring<ValueType> DFT<ValueType>::colourDFT() const {
             return DFTColouring<ValueType>(*this);
         }
 
+
         template<typename ValueType>
         DFTIndependentSymmetries DFT<ValueType>::findSymmetries(DFTColouring<ValueType> const& colouring) const {
             std::vector<size_t> vec;
diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h
index 3beacf8d9..a0059d81b 100644
--- a/src/storage/dft/DFT.h
+++ b/src/storage/dft/DFT.h
@@ -274,6 +274,7 @@ namespace storm {
 
             DFTIndependentSymmetries findSymmetries(DFTColouring<ValueType> const& colouring) const;
 
+            std::vector<size_t> immediateFailureCauses(size_t index) const;
         private:
             std::pair<std::vector<size_t>, std::vector<size_t>> getSortedParentAndOutDepIds(size_t index) const;
             
diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h
index 081a7bf5c..11fc31948 100644
--- a/src/storage/dft/DFTElements.h
+++ b/src/storage/dft/DFTElements.h
@@ -173,6 +173,8 @@ namespace storm {
             }
             
             virtual void extendSpareModule(std::set<size_t>& elementsInModule) const;
+
+           // virtual void extendImmediateFailureCausePathEvents(std::set<size_t>& ) const;
             
             virtual size_t nrChildren() const = 0;
 
diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp
index 7b7cea029..805ef7570 100644
--- a/src/storm-dyftee.cpp
+++ b/src/storm-dyftee.cpp
@@ -32,7 +32,8 @@ void analyzeDFT(std::string filename, std::string property, bool symred = false)
     // Building Markov Automaton
     std::cout << "Building Model..." << std::endl;
     storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft);
-    std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.buildModel();
+    typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
+    std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.buildModel(labeloptions);
     std::cout << "Built Model" << std::endl;
 
     // Model checking
diff --git a/src/utility/storm.h b/src/utility/storm.h
index f737b318e..5d02405fa 100644
--- a/src/utility/storm.h
+++ b/src/utility/storm.h
@@ -196,6 +196,15 @@ namespace storm {
     
     template<typename ModelType>
     std::shared_ptr<storm::models::ModelBase> preprocessModel(std::shared_ptr<storm::models::ModelBase> model, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) {
+        if(model->getType() == storm::models::ModelType::MarkovAutomaton && model->isSparseModel()) {
+            std::shared_ptr<storm::models::sparse::MarkovAutomaton<typename ModelType::ValueType>> ma = model->template as<storm::models::sparse::MarkovAutomaton<typename ModelType::ValueType>>();
+            if (ma->hasOnlyTrivialNondeterminism()) {
+                // Markov automaton can be converted into CTMC
+                model = ma->convertToCTMC();
+                
+            } 
+        }
+        
         if (model->isSparseModel() && storm::settings::generalSettings().isBisimulationSet()) {
             storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong;
             if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) {
@@ -205,6 +214,7 @@ namespace storm {
             STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for sparse models.");
             return performBisimulationMinimization<ModelType>(model->template as<storm::models::sparse::Model<typename ModelType::ValueType>>(), formulas, bisimType);
         }
+        
         return model;
     }
     
@@ -302,15 +312,8 @@ namespace storm {
             result = modelchecker.check(task);
         } else if (model->getType() == storm::models::ModelType::MarkovAutomaton) {
             std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = model->template as<storm::models::sparse::MarkovAutomaton<ValueType>>();
-            if (ma->hasOnlyTrivialNondeterminism()) {
-                // Markov automaton can be converted into CTMC
-                std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> ctmc = ma->convertToCTMC();
-                storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<ValueType>> modelchecker(*ctmc);
-                result = modelchecker.check(task);
-            } else {
-                storm::modelchecker::SparseMarkovAutomatonCslModelChecker<storm::models::sparse::MarkovAutomaton<ValueType>> modelchecker(*ma);
-                result = modelchecker.check(task);
-            }
+            storm::modelchecker::SparseMarkovAutomatonCslModelChecker<storm::models::sparse::MarkovAutomaton<ValueType>> modelchecker(*ma);
+            result = modelchecker.check(task);
         } else {
             STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type " << model->getType() << " is not supported.");
         }