diff --git a/benchmark_dft.py b/benchmark_dft.py
index b12d4f185..54dadeacc 100644
--- a/benchmark_dft.py
+++ b/benchmark_dft.py
@@ -13,10 +13,17 @@ EXAMPLE_DIR= "/Users/mvolk/develop/storm/examples/dft/"
 benchmarks = [ 
     ("and", False, [3, 1]),
     ("and_param", True, ["(4*x^2+2*x+1)/((x) * (2*x+1))", "1"]),
+    ("cardiac", False, [11378, 1]),
+    ("cas", False, [0.859736, 1]),
     ("cm2", False, [0.256272, 1]),
     #("cm4", False, [0, 1]),
     ("cps", False, ["inf", 0.333333]),
-    #("fdep", False, [0, 1]),
+    ("deathegg", False, [46.667, 1]),
+    ("fdep", False, [0.666667, 1]),
+    ("fdep2", False, [2, 1]),
+    #("ftpp_complex", False, [0, 1]), # Compute
+    #("ftpp_large", False, [0, 1]), # Compute
+    #("ftpp_standard", False, [0, 1]), # Compute
     ("mdcs", False, [2.85414, 1]),
     ("mdcs2", False, [2.85414, 1]),
     ("mp", False, [1.66667, 1]),
@@ -51,7 +58,7 @@ def run_storm_dft(filename, prop, parametric, quiet):
     dft_file = os.path.join(EXAMPLE_DIR, filename + ".dft")
     args = [STORM_PATH,
             dft_file,
-            '--prop', prop]
+            prop]
     if parametric:
         args.append('--parametric')
 
@@ -59,8 +66,7 @@ def run_storm_dft(filename, prop, parametric, quiet):
     # Get result
     match = re.search(r'Result: \[(.*)\]', output)
     if not match:
-        print("No valid result found in: " + output)
-        return
+        return None
     
     result = match.group(1)
     return result
@@ -88,7 +94,7 @@ if __name__ == "__main__":
     args = parser.parse_args()
     count = 0
     correct = 0
-    properties = ["ET=? [F \"failed\"]", "P=? [F \"failed\"]"]
+    properties = ['--expectedtime', '--probability']
     start = time.time()
     for index, prop in enumerate(properties):
         for (benchmark, parametric, result_original) in benchmarks:
@@ -98,6 +104,10 @@ if __name__ == "__main__":
             if args.debuglevel > 0:
                 print("Running '{}' with property '{}'".format(benchmark, prop))
             result = run_storm_dft(benchmark, prop, parametric, args.debuglevel<2)
+            if result is None:
+                print("Error occurred on example '{}' with property '{}'".format(benchmark, prop))
+                continue
+
             if not parametric:
                 # Float
                 result = float(result)
diff --git a/examples/dft/cardiac.dft b/examples/dft/cardiac.dft
new file mode 100644
index 000000000..505f002b1
--- /dev/null
+++ b/examples/dft/cardiac.dft
@@ -0,0 +1,21 @@
+toplevel "SYSTEM";
+"SYSTEM" or "FDEP" "CPU" "MOTOR" "PUMPS";
+"FDEP" fdep "TRIGGER" "P" "B";
+"TRIGGER" or "CS" "SS";
+"CPU" wsp "P" "B";
+"MOTOR" or "SWITCH" "MOTORS";
+"SWITCH" pand "MS" "MA";
+"MOTORS" csp "MA" "MB";
+"PUMPS" and "PUMP1" "PUMP2";
+"PUMP1" csp "PA" "PS";
+"PUMP2" csp "PB" "PS";
+"P" lambda=5.0e-5 dorm=0;
+"B" lambda=5.0e-5 dorm=0.5;
+"CS" lambda=2.0e-5 dorm=0;
+"SS" lambda=2.0e-5 dorm=0;
+"MS" lambda=1.0e-6 dorm=0;
+"MA" lambda=1.0e-4 dorm=0;
+"MB" lambda=1.0e-4 dorm=0;
+"PA" lambda=1.0e-4 dorm=0;
+"PB" lambda=1.0e-4 dorm=0;
+"PS" lambda=1.0e-4 dorm=0;
diff --git a/examples/dft/cas.dft b/examples/dft/cas.dft
new file mode 100644
index 000000000..812a3f30a
--- /dev/null
+++ b/examples/dft/cas.dft
@@ -0,0 +1,24 @@
+toplevel "System";
+"System" or "CPUfdep" "CPUunit" "Motorunit" "Pumpunit";
+
+"CPUfdep" fdep "trigger" "P" "B";
+"trigger" or "CS" "SS";
+"CS" lambda=0.2 dorm=0;
+"SS" lambda=0.2 dorm=0;
+"CPUunit" wsp "P" "B";
+"P" lambda=0.5 dorm=0;
+"B" lambda=0.5 dorm=0.5;
+
+"Motorunit" or "MP" "Motors";
+"MP" pand "MS" "MA";
+"Motors" csp "MA" "MB";
+"MS" lambda=0.01 dorm=0;
+"MA" lambda=1 dorm=0;
+"MB" lambda=1 dorm=0;
+
+"Pumpunit" and "PumpA" "PumpB";
+"PumpA" csp "PA" "PS";
+"PumpB" csp "PB" "PS";
+"PA" lambda=1 dorm=0;
+"PB" lambda=1 dorm=0;
+"PS" lambda=1 dorm=0;
diff --git a/examples/dft/deathegg.dft b/examples/dft/deathegg.dft
new file mode 100644
index 000000000..618684c4e
--- /dev/null
+++ b/examples/dft/deathegg.dft
@@ -0,0 +1,16 @@
+toplevel "DeathEgg";
+"DeathEgg" or "DeathEggProxy" "DeathEggServer" "CampusPowerDependency" "ProxyPowerDependency";
+"DeathEggServer" or "CampusNET" "DES_Disks";
+"DES_Disks" and "DES_Disks_RAID1" "DES_Disks_RAID2";
+"DES_Disks_RAID1" and "DES_Disk_1" "DES_Disk_2";
+"DES_Disks_RAID2" and "DES_Disk_3" "DES_Disk_4";
+"DeathEggProxy" lambda=0.01 dorm=0;
+"DES_Disk_1" lambda=0.01 dorm=0;
+"DES_Disk_2" lambda=0.01 dorm=0;
+"DES_Disk_3" lambda=0.01 dorm=0;
+"DES_Disk_4" lambda=0.01 dorm=0;
+"CampusPowerDependency" fdep "CampusPower" "DeathEggServer";
+"ProxyPowerDependency" fdep "ProxyPower" "DeathEggProxy";
+"CampusPower" lambda=0.01 dorm=0;
+"CampusNET" lambda=0.01 dorm=0;
+"ProxyPower" lambda=0.01 dorm=0;
\ No newline at end of file
diff --git a/examples/dft/fdep.dft b/examples/dft/fdep.dft
new file mode 100644
index 000000000..e597c46ce
--- /dev/null
+++ b/examples/dft/fdep.dft
@@ -0,0 +1,8 @@
+toplevel "System";
+"System" or "Power" "Machine";
+"Power" fdep "B_Power" "P" "B";
+"Machine" or "P" "B";
+
+"B_Power" lambda=0.5 dorm=0;
+"P" lambda=0.5 dorm=0;
+"B" lambda=0.5 dorm=0.5;
diff --git a/examples/dft/fdep2.dft b/examples/dft/fdep2.dft
new file mode 100644
index 000000000..a444ed4be
--- /dev/null
+++ b/examples/dft/fdep2.dft
@@ -0,0 +1,5 @@
+toplevel "A";
+"A" and "B" "C";
+"F" fdep "B" "C";
+"B" lambda=0.5 dorm=0;
+"C" lambda=0.5 dorm=0;
diff --git a/examples/dft/ftpp_complex.dft b/examples/dft/ftpp_complex.dft
new file mode 100644
index 000000000..1b836ee6b
--- /dev/null
+++ b/examples/dft/ftpp_complex.dft
@@ -0,0 +1,129 @@
+toplevel "System";
+"System" or "triadA" "triadB" "triadC" "triadD" "fA" "fB" "fC" "fD";
+
+"triadA" 2of3 "aA" "bA" "cA";
+"aA" csp "TAA" "TAS";
+"bA" csp "TAB" "TAS";
+"cA" csp "TAC" "TAS";
+
+"triadB" 2of3 "aB" "bB" "cB";
+"aB" csp "TBA" "TBS";
+"bB" csp "TBB" "TBS";
+"cB" csp "TBC" "TBS";
+
+"triadC" 2of3 "aC" "bC" "cC";
+"aC" csp "TCA" "TCS";
+"bC" csp "TCB" "TCS";
+"cC" csp "TCC" "TCS";
+
+"triadD" 2of3 "aD" "bD" "cD";
+"aD" csp "TDA" "TDS";
+"bD" csp "TDB" "TDS";
+"cD" csp "TDC" "TDS";
+
+"fA" fdep "NEA" "TAA" "TBA" "TCA" "TDA";
+"fB" fdep "NEB" "TAB" "TBB" "TCB" "TDB";
+"fC" fdep "NEC" "TAC" "TBC" "TCC" "TDC";
+"fD" fdep "NED" "TAS" "TBS" "TCS" "TDS";
+
+
+"NEA" lambda=0.017 dorm=1;
+"NEB" lambda=0.017 dorm=1;
+"NEC" lambda=0.017 dorm=1;
+"NED" lambda=0.017 dorm=1;
+
+"TAA" or "cpuAA" "memAA";
+"memAA" csp "memAA1" "memAA2";
+"cpuAA" lambda=0.11 dorm=0;
+"memAA1" lambda=0.11 dorm=0;
+"memAA2" lambda=0.11 dorm=0;
+
+"TAB" or "cpuAB" "memAB";
+"memAB" csp "memAB1" "memAB2";
+"cpuAB" lambda=0.11 dorm=0;
+"memAB1" lambda=0.11 dorm=0;
+"memAB2" lambda=0.11 dorm=0;
+
+"TAC" or "cpuAC" "memAC";
+"memAC" csp "memAC1" "memAC2";
+"cpuAC" lambda=0.11 dorm=0;
+"memAC1" lambda=0.11 dorm=0;
+"memAC2" lambda=0.11 dorm=0;
+
+"TAS" or "cpuAS" "memAS";
+"memAS" csp "memAS1" "memAS2";
+"cpuAS" lambda=0.11 dorm=0;
+"memAS1" lambda=0.11 dorm=0;
+"memAS2" lambda=0.11 dorm=0;
+
+"TBA" or "cpuBA" "memBA";
+"memBA" csp "memBA1" "memBA2";
+"cpuBA" lambda=0.11 dorm=0;
+"memBA1" lambda=0.11 dorm=0;
+"memBA2" lambda=0.11 dorm=0;
+
+"TBB" or "cpuBB" "memBB";
+"memBB" csp "memBB1" "memBB2";
+"cpuBB" lambda=0.11 dorm=0;
+"memBB1" lambda=0.11 dorm=0;
+"memBB2" lambda=0.11 dorm=0;
+
+"TBC" or "cpuBC" "memBC";
+"memBC" csp "memBC1" "memBC2";
+"cpuBC" lambda=0.11 dorm=0;
+"memBC1" lambda=0.11 dorm=0;
+"memBC2" lambda=0.11 dorm=0;
+
+"TBS" or "cpuBS" "memBS";
+"memBS" csp "memBS1" "memBS2";
+"cpuBS" lambda=0.11 dorm=0;
+"memBS1" lambda=0.11 dorm=0;
+"memBS2" lambda=0.11 dorm=0;
+
+"TCA" or "cpuCA" "memCA";
+"memCA" csp "memCA1" "memCA2";
+"cpuCA" lambda=0.11 dorm=0;
+"memCA1" lambda=0.11 dorm=0;
+"memCA2" lambda=0.11 dorm=0;
+
+"TCB" or "cpuCB" "memCB";
+"memCB" csp "memCB1" "memCB2";
+"cpuCB" lambda=0.11 dorm=0;
+"memCB1" lambda=0.11 dorm=0;
+"memCB2" lambda=0.11 dorm=0;
+
+"TCC" or "cpuCC" "memCC";
+"memCC" csp "memCC1" "memCC2";
+"cpuCC" lambda=0.11 dorm=0;
+"memCC1" lambda=0.11 dorm=0;
+"memCC2" lambda=0.11 dorm=0;
+
+"TCS" or "cpuCS" "memCS";
+"memCS" csp "memCS1" "memCS2";
+"cpuCS" lambda=0.11 dorm=0;
+"memCS1" lambda=0.11 dorm=0;
+"memCS2" lambda=0.11 dorm=0;
+
+"TDA" or "cpuDA" "memDA";
+"memDA" csp "memDA1" "memDA2";
+"cpuDA" lambda=0.11 dorm=0;
+"memDA1" lambda=0.11 dorm=0;
+"memDA2" lambda=0.11 dorm=0;
+
+"TDB" or "cpuDB" "memDB";
+"memDB" csp "memDB1" "memDB2";
+"cpuDB" lambda=0.11 dorm=0;
+"memDB1" lambda=0.11 dorm=0;
+"memDB2" lambda=0.11 dorm=0;
+
+"TDC" or "cpuDC" "memDC";
+"memDC" csp "memDC1" "memDC2";
+"cpuDC" lambda=0.11 dorm=0;
+"memDC1" lambda=0.11 dorm=0;
+"memDC2" lambda=0.11 dorm=0;
+
+"TDS" or "cpuDS" "memDS";
+"memDS" csp "memDS1" "memDS2";
+"cpuDS" lambda=0.11 dorm=0;
+"memDS1" lambda=0.11 dorm=0;
+"memDS2" lambda=0.11 dorm=0;
diff --git a/examples/dft/ftpp_large.dft b/examples/dft/ftpp_large.dft
new file mode 100644
index 000000000..cdc8032e7
--- /dev/null
+++ b/examples/dft/ftpp_large.dft
@@ -0,0 +1,63 @@
+toplevel "System";
+"System" or "triadA" "triadB" "triadC" "triadD" "fA" "fB" "fC" "fD" "fE";
+
+"triadA" 3of4 "aA" "bA" "cA" "dA";
+"aA" csp "TAA" "TAS";
+"bA" csp "TAB" "TAS";
+"cA" csp "TAC" "TAS";
+"dA" csp "TAD" "TAS";
+
+"triadB" 3of4 "aB" "bB" "cB" "dB";
+"aB" csp "TBA" "TBS";
+"bB" csp "TBB" "TBS";
+"cB" csp "TBC" "TBS";
+"dB" csp "TBD" "TBS";
+
+"triadC" 3of4 "aC" "bC" "cC" "dC";
+"aC" csp "TCA" "TCS";
+"bC" csp "TCB" "TCS";
+"cC" csp "TCC" "TCS";
+"dC" csp "TCD" "TCS";
+
+"triadD" 3of4 "aD" "bD" "cD" "dD";
+"aD" csp "TDA" "TDS";
+"bD" csp "TDB" "TDS";
+"cD" csp "TDC" "TDS";
+"dD" csp "TDD" "TDS";
+
+"fA" fdep "NEA" "TAA" "TBA" "TCA" "TDA";
+"fB" fdep "NEB" "TAB" "TBB" "TCB" "TDB";
+"fC" fdep "NEC" "TAC" "TBC" "TCC" "TDC";
+"fD" fdep "NED" "TAD" "TBD" "TCD" "TDD";
+"fE" fdep "NEE" "TAS" "TBS" "TCS" "TDS";
+
+
+"NEA" lambda=0.017 dorm=1;
+"NEB" lambda=0.017 dorm=1;
+"NEC" lambda=0.017 dorm=1;
+"NED" lambda=0.017 dorm=1;
+"NEE" lambda=0.017 dorm=1;
+
+"TAA" lambda=0.11 dorm=0;
+"TAB" lambda=0.11 dorm=0;
+"TAC" lambda=0.11 dorm=0;
+"TAD" lambda=0.11 dorm=0;
+"TAS" lambda=0.11 dorm=0;
+
+"TBA" lambda=0.11 dorm=0;
+"TBB" lambda=0.11 dorm=0;
+"TBC" lambda=0.11 dorm=0;
+"TBD" lambda=0.11 dorm=0;
+"TBS" lambda=0.11 dorm=0;
+
+"TCA" lambda=0.11 dorm=0;
+"TCB" lambda=0.11 dorm=0;
+"TCC" lambda=0.11 dorm=0;
+"TCD" lambda=0.11 dorm=0;
+"TCS" lambda=0.11 dorm=0;
+
+"TDA" lambda=0.11 dorm=0;
+"TDB" lambda=0.11 dorm=0;
+"TDC" lambda=0.11 dorm=0;
+"TDD" lambda=0.11 dorm=0;
+"TDS" lambda=0.11 dorm=0;
diff --git a/examples/dft/ftpp_standard.dft b/examples/dft/ftpp_standard.dft
new file mode 100644
index 000000000..9eaa7720e
--- /dev/null
+++ b/examples/dft/ftpp_standard.dft
@@ -0,0 +1,53 @@
+toplevel "System";
+"System" or "triadA" "triadB" "triadC" "triadD" "fA" "fB" "fC" "fD";
+
+"triadA" 2of3 "aA" "bA" "cA";
+"aA" csp "TAA" "TAS";
+"bA" csp "TAB" "TAS";
+"cA" csp "TAC" "TAS";
+
+"triadB" 2of3 "aB" "bB" "cB";
+"aB" csp "TBA" "TBS";
+"bB" csp "TBB" "TBS";
+"cB" csp "TBC" "TBS";
+
+"triadC" 2of3 "aC" "bC" "cC";
+"aC" csp "TCA" "TCS";
+"bC" csp "TCB" "TCS";
+"cC" csp "TCC" "TCS";
+
+"triadD" 2of3 "aD" "bD" "cD";
+"aD" csp "TDA" "TDS";
+"bD" csp "TDB" "TDS";
+"cD" csp "TDC" "TDS";
+
+"fA" fdep "NEA" "TAA" "TBA" "TCA" "TDA";
+"fB" fdep "NEB" "TAB" "TBB" "TCB" "TDB";
+"fC" fdep "NEC" "TAC" "TBC" "TCC" "TDC";
+"fD" fdep "NED" "TAS" "TBS" "TCS" "TDS";
+
+
+"NEA" lambda=0.017 dorm=1;
+"NEB" lambda=0.017 dorm=1;
+"NEC" lambda=0.017 dorm=1;
+"NED" lambda=0.017 dorm=1;
+
+"TAA" lambda=0.11 dorm=0;
+"TAB" lambda=0.11 dorm=0;
+"TAC" lambda=0.11 dorm=0;
+"TAS" lambda=0.11 dorm=0;
+
+"TBA" lambda=0.11 dorm=0;
+"TBB" lambda=0.11 dorm=0;
+"TBC" lambda=0.11 dorm=0;
+"TBS" lambda=0.11 dorm=0;
+
+"TCA" lambda=0.11 dorm=0;
+"TCB" lambda=0.11 dorm=0;
+"TCC" lambda=0.11 dorm=0;
+"TCS" lambda=0.11 dorm=0;
+
+"TDA" lambda=0.11 dorm=0;
+"TDB" lambda=0.11 dorm=0;
+"TDC" lambda=0.11 dorm=0;
+"TDS" lambda=0.11 dorm=0;
diff --git a/examples/dft/pdep.dft b/examples/dft/pdep.dft
new file mode 100644
index 000000000..f8cb0382b
--- /dev/null
+++ b/examples/dft/pdep.dft
@@ -0,0 +1,12 @@
+// From Junges2015
+// Example 3.19
+
+toplevel "SF";
+"SF" or "A" "B" "PDEP";
+"A" pand "S" "MA";
+"B" and "MA" "MB";
+"PDEP" pdep=0.2 "MA" "S";
+
+"S" lambda=0.5 dorm=0;
+"MA" lambda=0.5 dorm=0;
+"MB" lambda=0.5 dorm=0;
diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp
index 9332044f2..817295346 100644
--- a/src/builder/ExplicitDFTModelBuilder.cpp
+++ b/src/builder/ExplicitDFTModelBuilder.cpp
@@ -1,18 +1,21 @@
 #include "src/builder/ExplicitDFTModelBuilder.h"
-#include <src/models/sparse/Ctmc.h>
+#include <src/models/sparse/MarkovAutomaton.h>
+#include <src/models/sparse/CTMC.h>
 #include <src/utility/constants.h>
+#include <src/utility/vector.h>
+#include <src/exceptions/UnexpectedException.h>
 #include <map>
 
 namespace storm {
     namespace builder {
 
-        template <typename ValueType, typename RewardModelType, typename IndexType>
-        ExplicitDFTModelBuilder<ValueType, RewardModelType, IndexType>::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), rewardModels(), choiceLabeling() {
+        template <typename ValueType>
+        ExplicitDFTModelBuilder<ValueType>::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), markovianStates(), exitRates(), choiceLabeling() {
             // Intentionally left empty.
         }
 
-        template<typename ValueType, typename RewardModelType, typename IndexType>
-        std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> ExplicitDFTModelBuilder<ValueType, RewardModelType, IndexType>::buildCTMC() {
+        template <typename ValueType>
+        std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilder<ValueType>::buildModel() {
             // Initialize
             DFTStatePointer state = std::make_shared<storm::storage::DFTState<ValueType>>(mDft, newIndex++);
             mStates.findOrAdd(state->status(), state);
@@ -20,18 +23,24 @@ namespace storm {
             std::queue<DFTStatePointer> stateQueue;
             stateQueue.push(state);
 
-            bool deterministicModel = true;
+            bool deterministicModel = false;
+            ModelComponents modelComponents;
+            std::vector<uint_fast64_t> tmpMarkovianStates;
             storm::storage::SparseMatrixBuilder<ValueType> transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0);
 
             // Begin model generation
-            exploreStates(stateQueue, transitionMatrixBuilder);
+            bool deterministic = exploreStates(stateQueue, transitionMatrixBuilder, tmpMarkovianStates, modelComponents.exitRates);
             STORM_LOG_DEBUG("Generated " << mStates.size() << " states");
+            STORM_LOG_DEBUG("Model is " << (deterministic ? "deterministic" : "non-deterministic"));
 
-            // Build CTMC
-            ModelComponents modelComponents;
+            // Build Markov Automaton
+            modelComponents.markovianStates = storm::storage::BitVector(mStates.size(), tmpMarkovianStates);
             // Build transition matrix
             modelComponents.transitionMatrix = transitionMatrixBuilder.build();
-            STORM_LOG_DEBUG("TransitionMatrix: " << std::endl << modelComponents.transitionMatrix);
+            STORM_LOG_DEBUG("Transition matrix: " << std::endl << modelComponents.transitionMatrix);
+            STORM_LOG_DEBUG("Exit rates: " << modelComponents.exitRates);
+            STORM_LOG_DEBUG("Markovian states: " << modelComponents.markovianStates);
+            assert(!deterministic || modelComponents.transitionMatrix.getRowCount() == modelComponents.transitionMatrix.getColumnCount());
 
             // Build state labeling
             modelComponents.stateLabeling = storm::models::sparse::StateLabeling(mStates.size());
@@ -63,48 +72,81 @@ namespace storm {
                 }
             }
 
-            std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> model;
-            model = std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>>(new storm::models::sparse::Ctmc<ValueType, RewardModelType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling)));
+            std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
+            if (deterministic) {
+                // Turn the probabilities into rates by multiplying each row with the exit rate of the state.
+                // TODO Matthias: avoid transforming back and forth
+                storm::storage::SparseMatrix<ValueType> rateMatrix(modelComponents.transitionMatrix);
+                for (uint_fast64_t row = 0; row < rateMatrix.getRowCount(); ++row) {
+                    for (auto& entry : rateMatrix.getRow(row)) {
+                        entry.setValue(entry.getValue() * modelComponents.exitRates[row]);
+                    }
+                }
+
+                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));
+
+            }
             model->printModelInformationToStream(std::cout);
             return model;
         }
 
-        template<typename ValueType, typename RewardModelType, typename IndexType>
-        void ExplicitDFTModelBuilder<ValueType, RewardModelType, IndexType>::exploreStates(std::queue<DFTStatePointer>& stateQueue, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder) {
+        template <typename ValueType>
+        bool ExplicitDFTModelBuilder<ValueType>::exploreStates(std::queue<DFTStatePointer>& stateQueue, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<uint_fast64_t>& markovianStates, std::vector<ValueType>& exitRates) {
 
+            assert(exitRates.empty());
+            assert(markovianStates.empty());
+            // TODO Matthias: set Markovian states directly as bitvector?
             std::map<size_t, ValueType> outgoingTransitions;
+            size_t rowOffset = 0; // Captures number of non-deterministic choices
+            bool deterministic = true;
 
             while (!stateQueue.empty()) {
                 // Initialization
                 outgoingTransitions.clear();
+                ValueType exitRate = storm::utility::zero<ValueType>();
 
                 // Consider next state
                 DFTStatePointer state = stateQueue.front();
                 stateQueue.pop();
 
+                bool hasDependencies = state->nrFailableDependencies() > 0;
+                deterministic &= !hasDependencies;
+                size_t failableCount = hasDependencies ? state->nrFailableDependencies() : state->nrFailableBEs();
                 size_t smallest = 0;
 
+                transitionMatrixBuilder.newRowGroup(state->getId() + rowOffset);
+
                 // Add self loop for target states
                 if (mDft.hasFailed(state) || mDft.isFailsafe(state)) {
-                    transitionMatrixBuilder.addNextValue(state->getId(), state->getId(), storm::utility::one<ValueType>());
+                    transitionMatrixBuilder.addNextValue(state->getId() + rowOffset, state->getId(), storm::utility::one<ValueType>());
                     STORM_LOG_TRACE("Added self loop for " << state->getId());
+                    exitRates.push_back(storm::utility::one<ValueType>());
+                    assert(exitRates.size()-1 == state->getId());
+                    markovianStates.push_back(state->getId());
                     // No further exploration required
                     continue;
+                } else {
+                    STORM_LOG_THROW(state->nrFailableBEs() > 0, storm::exceptions::UnexpectedException, "State " << state->getId() << " is no target state but behaves like one");
                 }
 
                 // Let BE fail
-                while (smallest < state->nrFailableBEs()) {
+                while (smallest < failableCount) {
                     STORM_LOG_TRACE("exploring from: " << mDft.getStateString(state));
 
                     // Construct new state as copy from original one
                     DFTStatePointer newState = std::make_shared<storm::storage::DFTState<ValueType>>(*state);
                     std::pair<std::shared_ptr<storm::storage::DFTBE<ValueType>>, bool> nextBEPair = newState->letNextBEFail(smallest++);
                     std::shared_ptr<storm::storage::DFTBE<ValueType>> nextBE = nextBEPair.first;
-                    if (nextBE == nullptr) {
-                        break;
-                    }
+                    assert(nextBE);
+                    assert(nextBEPair.second == hasDependencies);
                     STORM_LOG_TRACE("with the failure of: " << nextBE->name() << " [" << nextBE->id() << "]");
 
+                    // Update failable dependencies
+                    newState->updateFailableDependencies(nextBE->id());
+
+                    // Propagate failures
                     storm::storage::DFTStateSpaceGenerationQueues<ValueType> queues;
 
                     for (DFTGatePointer parent : nextBE->parents()) {
@@ -142,43 +184,61 @@ namespace storm {
                         stateQueue.push(newState);
                     }
 
-                    // Set failure rate according to usage
-                    bool isUsed = true;
-                    if (mDft.hasRepresentant(nextBE->id())) {
-                        DFTElementPointer representant = mDft.getRepresentant(nextBE->id());
-                        // Used must be checked for the state we are coming from as this state is responsible for the
-                        // rate and not the new state we are going to
-                        isUsed = state->isUsed(representant->id());
-                    }
-                    STORM_LOG_TRACE("BE " << nextBE->name() << " is " << (isUsed ? "used" : "not used"));
-                    ValueType rate = isUsed ? nextBE->activeFailureRate() : nextBE->passiveFailureRate();
-                    auto resultFind = outgoingTransitions.find(newState->getId());
-                    if (resultFind != outgoingTransitions.end()) {
-                        // Add to existing transition
-                        resultFind->second += rate;
-                        STORM_LOG_TRACE("Updated transition from " << state->getId() << " to " << resultFind->first << " with " << rate << " to " << resultFind->second);
+                    // Set transitions
+                    if (hasDependencies) {
+                        // Failure is due to dependency -> add non-deterministic choice
+                        transitionMatrixBuilder.addNextValue(state->getId() + rowOffset++, newState->getId(), storm::utility::one<ValueType>());
                     } else {
-                        // Insert new transition
-                        outgoingTransitions.insert(std::make_pair(newState->getId(), rate));
-                        STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << newState->getId() << " with " << rate);
+                        // Set failure rate according to usage
+                        bool isUsed = true;
+                        if (mDft.hasRepresentant(nextBE->id())) {
+                            DFTElementPointer representant = mDft.getRepresentant(nextBE->id());
+                            // Used must be checked for the state we are coming from as this state is responsible for the
+                            // rate and not the new state we are going to
+                            isUsed = state->isUsed(representant->id());
+                        }
+                        STORM_LOG_TRACE("BE " << nextBE->name() << " is " << (isUsed ? "used" : "not used"));
+                        ValueType rate = isUsed ? nextBE->activeFailureRate() : nextBE->passiveFailureRate();
+                        auto resultFind = outgoingTransitions.find(newState->getId());
+                        if (resultFind != outgoingTransitions.end()) {
+                            // Add to existing transition
+                            resultFind->second += rate;
+                            STORM_LOG_TRACE("Updated transition from " << state->getId() << " to " << resultFind->first << " with " << rate << " to " << resultFind->second);
+                        } else {
+                            // Insert new transition
+                            outgoingTransitions.insert(std::make_pair(newState->getId(), rate));
+                            STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << newState->getId() << " with " << rate);
+                        }
+                        exitRate += rate;
                     }
+
                 } // end while failing BE
 
-                // Add all transitions
-                for (auto it = outgoingTransitions.begin(); it != outgoingTransitions.end(); ++it)
-                {
-                    transitionMatrixBuilder.addNextValue(state->getId(), it->first, it->second);
+                if (hasDependencies) {
+                    rowOffset--; // One increment to many
+                } else {
+                    // Add all probability transitions
+                    for (auto it = outgoingTransitions.begin(); it != outgoingTransitions.end(); ++it)
+                    {
+                        ValueType probability = it->second / exitRate; // Transform rate to probability
+                        transitionMatrixBuilder.addNextValue(state->getId() + rowOffset, it->first, probability);
+                    }
+
+                    markovianStates.push_back(state->getId());
                 }
+                exitRates.push_back(exitRate);
+                assert(exitRates.size()-1 == state->getId());
 
             } // end while queue
+            assert(!deterministic || rowOffset == 0);
+            return deterministic;
         }
 
         // Explicitly instantiate the class.
-        template class ExplicitDFTModelBuilder<double, storm::models::sparse::StandardRewardModel<double>, uint32_t>;
+        template class ExplicitDFTModelBuilder<double>;
 
 #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>;
+        template class ExplicitDFTModelBuilder<storm::RationalFunction>;
 #endif
 
     } // namespace builder
diff --git a/src/builder/ExplicitDFTModelBuilder.h b/src/builder/ExplicitDFTModelBuilder.h
index ed02e60d4..6125b6fa1 100644
--- a/src/builder/ExplicitDFTModelBuilder.h
+++ b/src/builder/ExplicitDFTModelBuilder.h
@@ -16,7 +16,7 @@
 namespace storm {
     namespace builder {
 
-        template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename IndexType = uint32_t>
+        template<typename ValueType>
         class ExplicitDFTModelBuilder {
 
             using DFTElementPointer = std::shared_ptr<storm::storage::DFTElement<ValueType>>;
@@ -33,8 +33,11 @@ namespace storm {
                 // The state labeling.
                 storm::models::sparse::StateLabeling stateLabeling;
 
-                // The reward models associated with the model.
-                std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<typename RewardModelType::ValueType>> rewardModels;
+                // The Markovian states.
+                storm::storage::BitVector markovianStates;
+
+                // The exit rates.
+                std::vector<ValueType> exitRates;
 
                 // A vector that stores a labeling for each choice.
                 boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> choiceLabeling;
@@ -50,10 +53,10 @@ namespace storm {
                 // 2^nrBE is upper bound for state space
             }
 
-            std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> buildCTMC();
+            std::shared_ptr<storm::models::sparse::Model<ValueType>> buildModel();
 
         private:
-            void exploreStates(std::queue<DFTStatePointer>& stateQueue, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder);
+            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/parser/DFTGalileoParser.cpp b/src/parser/DFTGalileoParser.cpp
index 163bc1488..c8639ae30 100644
--- a/src/parser/DFTGalileoParser.cpp
+++ b/src/parser/DFTGalileoParser.cpp
@@ -54,7 +54,7 @@ namespace storm {
                 STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Exception during file opening on " << filename << ".");
                 return false;
             }
-            file.exceptions( 0 );
+            file.exceptions( std::ifstream::goodbit );
 
             std::string line;
             bool generalSuccess = true;
@@ -106,8 +106,11 @@ namespace storm {
                         success = builder.addPandElement(name, childNames);
                     } else if (tokens[1] == "wsp" || tokens[1] == "csp") {
                         success = builder.addSpareElement(name, childNames);
-                    } else if (boost::starts_with(tokens[1], "fdep")) {
-                        STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Functional dependencies currently not supported");
+                    } else if (tokens[1] == "fdep") {
+                        success = builder.addDepElement(name, childNames, storm::utility::one<ValueType>());
+                    } else if (boost::starts_with(tokens[1], "pdep=")) {
+                        ValueType probability = parseRationalExpression(tokens[1].substr(5));
+                        success = builder.addDepElement(name, childNames, probability);
                     } else if (boost::starts_with(tokens[1], "lambda=")) {
                         ValueType failureRate = parseRationalExpression(tokens[1].substr(7));
                         ValueType dormancyFactor = parseRationalExpression(tokens[2].substr(5));
@@ -156,4 +159,4 @@ namespace storm {
 #endif
         
     }
-}
\ No newline at end of file
+}
diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp
index b05e57eda..319a08925 100644
--- a/src/storage/dft/DFT.cpp
+++ b/src/storage/dft/DFT.cpp
@@ -13,13 +13,13 @@ namespace storm {
             size_t stateIndex = 0;
             mUsageInfoBits = storm::utility::math::uint64_log2(mElements.size()-1)+1;
 
-            for(auto& elem : mElements) {
+            for (auto& elem : mElements) {
                 mIdToFailureIndex.push_back(stateIndex);
                 stateIndex += 2;
                 if(elem->isBasicElement()) {
                     ++mNrOfBEs;
                 }
-                else if(elem->isSpareGate()) {
+                else if (elem->isSpareGate()) {
                     ++mNrOfSpares;
                     for(auto const& spareReprs : std::static_pointer_cast<DFTSpare<ValueType>>(elem)->children()) {
                         if(mActivationIndex.count(spareReprs->id()) == 0) {
@@ -41,6 +41,8 @@ namespace storm {
                     mUsageIndex.insert(std::make_pair(elem->id(), stateIndex));
                     stateIndex += mUsageInfoBits;
 
+                } else if (elem->isDependency()) {
+                    mDependencies.push_back(elem->id());
                 }
             }
 
@@ -135,10 +137,11 @@ namespace storm {
             for (auto const& elem : mElements) {
                 stream << state->getElementStateInt(elem->id());
                 if(elem->isSpareGate()) {
+                    stream << "[";
                     if(state->isActiveSpare(elem->id())) {
-                        stream << " actively";
+                        stream << "actively ";
                     }
-                    stream << " using " << state->uses(elem->id());
+                    stream << "using " << state->uses(elem->id()) << "]";
                 }
             }
             return stream.str();
diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h
index ec68e1f30..92f1c0531 100644
--- a/src/storage/dft/DFT.h
+++ b/src/storage/dft/DFT.h
@@ -51,6 +51,7 @@ namespace storm {
             size_t mStateSize;
             std::map<size_t, size_t> mActivationIndex;
             std::map<size_t, std::vector<size_t>> mSpareModules;
+            std::vector<size_t> mDependencies;
             std::vector<size_t> mTopModule;
             std::vector<size_t> mIdToFailureIndex;
             std::map<size_t, size_t> mUsageIndex;
@@ -120,6 +121,10 @@ namespace storm {
                 }
             }
             
+            std::vector<size_t> const& getDependencies() const {
+                return mDependencies;
+            }
+
             void propagateActivation(DFTState<ValueType>& state, size_t representativeId) const {
                 state.activate(representativeId);
                 for(size_t id : module(representativeId)) {
diff --git a/src/storage/dft/DFTBuilder.cpp b/src/storage/dft/DFTBuilder.cpp
index f6fff39ff..fffd33946 100644
--- a/src/storage/dft/DFTBuilder.cpp
+++ b/src/storage/dft/DFTBuilder.cpp
@@ -18,11 +18,30 @@ namespace storm {
             for(auto& elem : mChildNames) {
                 DFTGatePointer gate = std::static_pointer_cast<DFTGate<ValueType>>(elem.first);
                 for(auto const& child : elem.second) {
-                    gate->pushBackChild(mElements[child]);
-                    mElements[child]->addParent(gate);
+                    auto itFind = mElements.find(child);
+                    if (itFind != mElements.end()) {
+                        // Child found
+                        DFTElementPointer childElement = itFind->second;
+                        assert(!childElement->isDependency());
+                        gate->pushBackChild(childElement);
+                        childElement->addParent(gate);
+                    } else {
+                        // Child not found -> find first dependent event to assure that child is dependency
+                        auto itFind = mElements.find(child + "_1");
+                        assert(itFind != mElements.end());
+                        assert(itFind->second->isDependency());
+                        STORM_LOG_TRACE("Ignore functional dependency " << child << " in gate " << gate->name());
+                    }
                 }
             }
 
+            // Initialize dependencies
+            for (auto& dependency : mDependencies) {
+                DFTGatePointer triggerEvent = std::static_pointer_cast<DFTGate<ValueType>>(mElements[dependency->nameTrigger()]);
+                std::shared_ptr<DFTBE<ValueType>> dependentEvent = std::static_pointer_cast<DFTBE<ValueType>>(mElements[dependency->nameDependent()]);
+                dependency->initialize(triggerEvent, dependentEvent);
+            }
+
             // Sort elements topologically
             // compute rank
             for (auto& elem : mElements) {
@@ -40,7 +59,7 @@ namespace storm {
         template<typename ValueType>
         unsigned DFTBuilder<ValueType>::computeRank(DFTElementPointer const& elem) {
             if(elem->rank() == -1) {
-                if(elem->nrChildren() == 0) {
+                if(elem->nrChildren() == 0 || elem->isDependency()) {
                     elem->setRank(0);
                 } else {
                     DFTGatePointer gate = std::static_pointer_cast<DFTGate<ValueType>>(elem);
diff --git a/src/storage/dft/DFTBuilder.h b/src/storage/dft/DFTBuilder.h
index 0cb0efab5..ef01369c9 100644
--- a/src/storage/dft/DFTBuilder.h
+++ b/src/storage/dft/DFTBuilder.h
@@ -19,12 +19,14 @@ namespace storm {
             using DFTElementVector = std::vector<DFTElementPointer>;
             using DFTGatePointer = std::shared_ptr<DFTGate<ValueType>>;
             using DFTGateVector = std::vector<DFTGatePointer>;
+            using DFTDependencyPointer = std::shared_ptr<DFTDependency<ValueType>>;
 
         private:
             std::size_t mNextId = 0;
             std::string topLevelIdentifier;
             std::unordered_map<std::string, DFTElementPointer> mElements;
             std::unordered_map<DFTElementPointer, std::vector<std::string>> mChildNames;
+            std::vector<DFTDependencyPointer> mDependencies;
             
         public:
             DFTBuilder() {
@@ -51,6 +53,42 @@ namespace storm {
                 return addStandardGate(name, children, DFTElementType::SPARE);
             }
             
+            bool addDepElement(std::string const& name, std::vector<std::string> const& children, ValueType probability) {
+                assert(children.size() > 1);
+                if(mElements.count(name) != 0) {
+                    // Element with that name already exists.
+                    return false;
+                }
+
+                if (storm::utility::isZero(probability)) {
+                    // Element is superfluous
+                    return true;
+                }
+                std::string trigger = children[0];
+
+                //TODO Matthias: collect constraints for SMT solving
+                //0 <= probability <= 1
+                if (!storm::utility::isOne(probability) && children.size() > 2) {
+                    //TODO Matthias: introduce additional element for probability and then add pdeps with probability 1 to children
+                    std::cerr << "Probability != 1 for more than one child currently not supported." << std::endl;
+                    return false;
+                }
+
+                for (size_t i = 1; i < children.size(); ++i) {
+                    std::string nameDep = name + "_" + std::to_string(i);
+                    if(mElements.count(nameDep) != 0) {
+                        // Element with that name already exists.
+                        std::cerr << "Element with name: " << nameDep << " already exists." << std::endl;
+                        return false;
+                    }
+                    assert(storm::utility::isOne(probability) || children.size() == 2);
+                    DFTDependencyPointer element = std::make_shared<DFTDependency<ValueType>>(mNextId++, nameDep, trigger, children[i], probability);
+                    mElements[element->name()] = element;
+                    mDependencies.push_back(element);
+                }
+                return true;
+            }
+
             bool addVotElement(std::string const& name, unsigned threshold, std::vector<std::string> const& children) {
                 assert(children.size() > 0);
                 if(mElements.count(name) != 0) {
diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h
index fe340a43a..fb5123180 100644
--- a/src/storage/dft/DFTElements.h
+++ b/src/storage/dft/DFTElements.h
@@ -84,7 +84,11 @@ namespace storm {
             virtual bool isSpareGate() const {
                 return false;
             }
-            
+
+            virtual bool isDependency() const {
+                return false;
+            }
+
             virtual void setId(size_t newId) {
                 mId = newId;
             }
@@ -405,6 +409,88 @@ namespace storm {
         };
 
 
+        template<typename ValueType>
+        class DFTDependency : public DFTElement<ValueType> {
+
+            using DFTGatePointer = std::shared_ptr<DFTGate<ValueType>>;
+            using DFTBEPointer = std::shared_ptr<DFTBE<ValueType>>;
+            using DFTBEVector = std::vector<DFTBEPointer>;
+
+        protected:
+            std::string mNameTrigger;
+            std::string mNameDependent;
+            ValueType mProbability;
+            DFTGatePointer mTriggerEvent;
+            DFTBEPointer mDependentEvent;
+
+        public:
+            DFTDependency(size_t id, std::string const& name, std::string const& trigger, std::string const& dependent, ValueType probability) :
+                DFTElement<ValueType>(id, name), mNameTrigger(trigger), mNameDependent(dependent), mProbability(probability)
+            {
+            }
+
+            virtual ~DFTDependency() {}
+
+            void initialize(DFTGatePointer triggerEvent, DFTBEPointer dependentEvent) {
+                assert(triggerEvent->name() == mNameTrigger);
+                assert(dependentEvent->name() == mNameDependent);
+                mTriggerEvent = triggerEvent;
+                mDependentEvent = dependentEvent;
+            }
+
+            std::string nameTrigger() {
+                return mNameTrigger;
+            }
+
+            std::string nameDependent() {
+                return mNameDependent;
+            }
+
+            ValueType probability() {
+                return mProbability;
+            }
+
+            DFTGatePointer const& triggerEvent() const {
+                assert(mTriggerEvent);
+                return mTriggerEvent;
+            }
+
+            DFTBEPointer const& dependentEvent() const {
+                assert(mDependentEvent);
+                return mDependentEvent;
+            }
+
+            virtual size_t nrChildren() const override {
+                return 1;
+            }
+
+            virtual bool isDependency() const override {
+                return true;
+            }
+
+            virtual std::vector<size_t> independentUnit() const override {
+                std::set<size_t> unit = {this->mId};
+                mDependentEvent->extendUnit(unit);
+                if(unit.count(mTriggerEvent->id()) != 0) {
+                    return {};
+                }
+                return std::vector<size_t>(unit.begin(), unit.end());
+            }
+
+            virtual std::string toString() const override {
+                std::stringstream stream;
+                bool fdep = storm::utility::isOne(mProbability);
+                stream << "{" << this->name() << "} " << (fdep ? "FDEP" : "PDEP") << "(" << mTriggerEvent->name() << " => " << mDependentEvent->name() << ")";
+                if (!fdep) {
+                    stream << " with probability " << mProbability;
+                }
+                return stream.str();
+            }
+
+        protected:
+
+        };
+
 
         template<typename ValueType>
         class DFTAnd : public DFTGate<ValueType> {
diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp
index d760129e0..17bb4aee8 100644
--- a/src/storage/dft/DFTState.cpp
+++ b/src/storage/dft/DFTState.cpp
@@ -78,17 +78,41 @@ namespace storm {
             }
         }
 
+        template<typename ValueType>
+        bool DFTState<ValueType>::updateFailableDependencies(size_t id) {
+            assert(hasFailed(id));
+            for (size_t i = 0; i < mDft.getDependencies().size(); ++i) {
+                std::shared_ptr<DFTDependency<ValueType>> dependency = std::static_pointer_cast<DFTDependency<ValueType>>(mDft.getElement(mDft.getDependencies()[i]));
+                if (dependency->triggerEvent()->id() == id) {
+                    if (!hasFailed(dependency->dependentEvent()->id())) {
+                        mFailableDependencies.push_back(dependency->id());
+                        STORM_LOG_TRACE("New dependency failure: " << dependency->toString());
+                    }
+                }
+            }
+            return nrFailableDependencies() > 0;
+        }
+
         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());
-            // TODO set when implementing functional dependencies
-            bool dueToFdep = false;
-            std::pair<std::shared_ptr<DFTBE<ValueType>>,bool> res(mDft.getBasicElement(mIsCurrentlyFailableBE[index]), dueToFdep);
-            mIsCurrentlyFailableBE.erase(mIsCurrentlyFailableBE.begin() + index);
-            setFailed(res.first->id());
-            return res;
+            if (nrFailableDependencies() > 0) {
+                // Consider failure due to dependency
+                assert(index < nrFailableDependencies());
+                std::shared_ptr<DFTDependency<ValueType>> dependency = std::static_pointer_cast<DFTDependency<ValueType>>(mDft.getElement(mFailableDependencies[index]));
+                std::pair<std::shared_ptr<DFTBE<ValueType>>,bool> res(mDft.getBasicElement(dependency->dependentEvent()->id()), true);
+                mFailableDependencies.erase(mFailableDependencies.begin() + index);
+                setFailed(res.first->id());
+                return res;
+            } else {
+                // Consider "normal" failure
+                assert(index < nrFailableBEs());
+                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;
+            }
         }
 
         template<typename ValueType>
diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h
index 7cb5eaf4a..a1bab2583 100644
--- a/src/storage/dft/DFTState.h
+++ b/src/storage/dft/DFTState.h
@@ -5,6 +5,7 @@
 #include "DFTElementState.h"
 
 #include <sstream>
+#include <memory>
 
 namespace storm {
     namespace storage {
@@ -24,6 +25,7 @@ namespace storm {
             size_t mId;
             std::vector<size_t> mInactiveSpares;
             std::vector<size_t> mIsCurrentlyFailableBE;
+            std::vector<size_t> mFailableDependencies;
             std::vector<size_t> mUsedRepresentants;
             bool mValid = true;
             const DFT<ValueType>& mDft;
@@ -109,6 +111,17 @@ namespace storm {
                 return mIsCurrentlyFailableBE.size();
             }
 
+            size_t nrFailableDependencies() const {
+                return mFailableDependencies.size();
+            }
+
+            /**
+             * Sets all failable BEs due to dependencies from newly failed element
+             * @param id Id of the newly failed element
+             * @return true if failable dependent events exist
+             */
+            bool updateFailableDependencies(size_t id);
+
             /**
              * Sets the next BE as failed
              * @param smallestIndex Index in currentlyFailableBE of BE to fail
@@ -118,17 +131,31 @@ namespace storm {
             
             std::string getCurrentlyFailableString() const {
                 std::stringstream stream;
-                auto it = mIsCurrentlyFailableBE.begin();
-                stream << "{";
-                if(it != mIsCurrentlyFailableBE.end()) {
-                    stream << *it;
-                }
-                ++it;
-                while(it != mIsCurrentlyFailableBE.end()) {
-                    stream << ", " << *it;
+                if (nrFailableDependencies() > 0) {
+                    auto it = mFailableDependencies.begin();
+                    stream << "{Dependencies: ";
+                    if (it != mFailableDependencies.end()) {
+                        stream << *it;
+                    }
+                    ++it;
+                    while(it != mFailableDependencies.end()) {
+                        stream << ", " << *it;
+                        ++it;
+                    }
+                    stream << "} ";
+                } else {
+                    auto it = mIsCurrentlyFailableBE.begin();
+                    stream << "{";
+                    if(it != mIsCurrentlyFailableBE.end()) {
+                        stream << *it;
+                    }
                     ++it;
+                    while(it != mIsCurrentlyFailableBE.end()) {
+                        stream << ", " << *it;
+                        ++it;
+                    }
+                    stream << "}";
                 }
-                stream << "}";
                 return stream.str();
             }
 
diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp
index fc113e438..a8122f2bd 100644
--- a/src/storm-dyftee.cpp
+++ b/src/storm-dyftee.cpp
@@ -6,7 +6,7 @@
 #include "utility/storm.h"
 
 /*!
- * Load DFT from filename, build corresponding CTMC and check against given property.
+ * Load DFT from filename, build corresponding Model and check against given property.
  *
  * @param filename Path to DFT file in Galileo format.
  * @param property PCTC formula capturing the property to check.
@@ -19,21 +19,21 @@ void analyzeDFT(std::string filename, std::string property) {
     storm::storage::DFT<ValueType> dft = parser.parseDFT(filename);
     std::cout << "Built data structure" << std::endl;
 
-    // Building CTMC
-    std::cout << "Building CTMC..." << std::endl;
+    // 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.buildCTMC();
-    std::cout << "Built CTMC" << std::endl;
+    std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.buildModel();
+    std::cout << "Built Model" << std::endl;
 
     // Model checking
     std::cout << "Model checking..." << std::endl;
     std::vector<std::shared_ptr<storm::logic::Formula>> formulas = storm::parseFormulasForExplicit(property);
     assert(formulas.size() == 1);
-    std::unique_ptr<storm::modelchecker::CheckResult> resultCtmc(storm::verifySparseModel(model, formulas[0]));
-    assert(resultCtmc);
+    std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, formulas[0]));
+    assert(result);
     std::cout << "Result: ";
-    resultCtmc->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
-    std::cout << *resultCtmc << std::endl;
+    result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
+    std::cout << *result << std::endl;
 }
 
 /*!
@@ -46,7 +46,7 @@ void analyzeDFT(std::string filename, std::string property) {
 int main(int argc, char** argv) {
     if(argc < 2) {
         std::cout << "Storm-DyFTeE should be called with a filename as argument." << std::endl;
-        std::cout << "./storm-dft <filename> <optional pctl-formula> <optional --parametric>" << std::endl;
+        std::cout << "./storm-dft <filename> <--prop pctl-formula> <--parametric>" << std::endl;
         return 1;
     }
 
@@ -54,19 +54,32 @@ int main(int argc, char** argv) {
     bool parametric = false;
     log4cplus::LogLevel level = log4cplus::WARN_LOG_LEVEL;
     std::string filename = argv[1];
-    std::string pctlFormula = "Pmax=?[true U \"failed\"]";
+    std::string pctlFormula = "";
     for (int i = 2; i < argc; ++i) {
         std::string option = argv[i];
         if (option == "--parametric") {
             parametric = true;
+        } else if (option == "--expectedtime") {
+            assert(pctlFormula.empty());
+            pctlFormula = "ET=?[F \"failed\"]";
+        } else if (option == "--probability") {
+            assert(pctlFormula.empty());
+            pctlFormula = "P=? [F \"failed\"]";
         } else if (option == "--trace") {
             level = log4cplus::TRACE_LOG_LEVEL;
         } else if (option == "--debug") {
             level = log4cplus::DEBUG_LOG_LEVEL;
+        } else if (option == "--prop") {
+            assert(pctlFormula.empty());
+            ++i;
+            assert(i < argc);
+            pctlFormula = argv[i];
         } else {
-            pctlFormula = option;
+            std::cout << "Option '" << option << "' not recognized." << std::endl;
+            return 1;
         }
     }
+    assert(!pctlFormula.empty());
 
     storm::utility::setUp();
     logger.setLogLevel(level);
diff --git a/src/utility/vector.cpp b/src/utility/vector.cpp
index e4a1dd05c..20af3c628 100644
--- a/src/utility/vector.cpp
+++ b/src/utility/vector.cpp
@@ -1,7 +1,8 @@
 #include "src/utility/vector.h"
 
-template<typename ValueType>
-std::ostream& operator<<(std::ostream& out, std::vector<ValueType> const& vector) {
+//template<typename ValueType>
+//std::ostream& operator<<(std::ostream& out, std::vector<ValueType> const& vector) {
+std::ostream& operator<<(std::ostream& out, std::vector<double> const& vector) {
     out << "vector (" << vector.size() << ") [ ";
     for (uint_fast64_t i = 0; i < vector.size() - 1; ++i) {
         out << vector[i] << ", ";
@@ -12,5 +13,5 @@ std::ostream& operator<<(std::ostream& out, std::vector<ValueType> const& vector
 }
 
 // Explicitly instantiate functions.
-template std::ostream& operator<<(std::ostream& out, std::vector<double> const& vector);
-template std::ostream& operator<<(std::ostream& out, std::vector<uint_fast64_t> const& vector);
+//template std::ostream& operator<<(std::ostream& out, std::vector<double> const& vector);
+//template std::ostream& operator<<(std::ostream& out, std::vector<uint_fast64_t> const& vector);
\ No newline at end of file
diff --git a/src/utility/vector.h b/src/utility/vector.h
index 665569645..6b09f0467 100644
--- a/src/utility/vector.h
+++ b/src/utility/vector.h
@@ -15,8 +15,10 @@
 #include "src/utility/macros.h"
 #include "src/solver/OptimizationDirection.h"
 
-template<typename ValueType>
-std::ostream& operator<<(std::ostream& out, std::vector<ValueType> const& vector);
+// Template was causing problems as Carl has the same function
+//template<typename ValueType>
+//std::ostream& operator<<(std::ostream& out, std::vector<ValueType> const& vector);
+std::ostream& operator<<(std::ostream& out, std::vector<double> const& vector);
 
 namespace storm {
     namespace utility {