Merge branch 'master' into prismlang-sim

4 years ago · 4514ed76d6
24 changed files with 462 additions and 133 deletions
--- a/.github/workflows/buildtest.yml
+++ b/.github/workflows/buildtest.yml
@ -1,6 +1,6 @@
 name: Build Test
-# Builds and tests storm on varius platforms
-# also deploys images to dockerhub
+# Builds and tests storm on various platforms
+# also deploys images to Dockerhub

 on:
  schedule:
@ -8,6 +8,7 @@ on:
      - cron: '0 6 * * *'
  # needed to trigger the workflow manually
  workflow_dispatch:
+  pull_request:

 env:
  CARL_BRANCH: "master14"
@ -120,7 +121,7 @@ jobs:
      - name: Build storm
        run: sudo docker exec storm bash -c "cd /opt/storm/build; make -j ${NR_JOBS}"

-        # A bit hacky... but its usefullnes has been proven in production
+        # A bit hacky... but its usefulness has been proven in production
      - name: Check release makeflags
        if: matrix.debugOrRelease == 'release'
        run: |
@ -134,6 +135,8 @@ jobs:
        run: sudo docker exec storm bash -c "cd /opt/storm/build; ctest test --output-on-failure"

      - name: Deploy storm
+        # Only deploy if using master (and not for pull requests)
+        if: github.ref == 'refs/heads/master'
        run: |
          sudo docker commit storm movesrwth/storm:ci-${{ matrix.debugOrRelease }}
          sudo docker push movesrwth/storm:ci-${{ matrix.debugOrRelease }}
--- a/doc/merge_pull_requests.md
+++ b/doc/merge_pull_requests.md
@ -0,0 +1,39 @@
+The following steps should be performed to integrate pull requests from Github.
+
+0. After a pull request is opened, some automatic build checks should be performed by Github Actions.
+   Failures of these checks should be fixed.
+
+1. Manually review the pull request on Github and suggest improvements if necessary.
+   In particular make sure:
+   * No unnecessary files were committed (for example build artefacts, etc.)
+   * No remains from the development are present (for example debug output, hackish workarounds, etc.)
+   * ...
+
+2. Integrate the pull request via Github, preferably by *rebase and merge*.
+
+3. Optional (if not done already): add the Github repository as another remote for your local copy of the internal repository:
+   ```console
+   git remote add github https://github.com/moves-rwth/storm.git
+   ```
+   
+4. Fetch the current Github master:
+   ```console
+   git fetch github
+   ```
+
+5. Make sure to be on the (internal) master:
+   ```console
+   git checkout master
+   ```
+
+6. Rebase the changes of Github onto the (internal) master:
+   ```console
+   git rebase github/master
+   ```
+
+7. Check that Storm builds successfully and everything works as expected.
+
+8. Push the changes into the internal repository:
+   ```console
+   git push origin
+   ```
--- a/resources/examples/testfiles/dft/fdep6.dft
+++ b/resources/examples/testfiles/dft/fdep6.dft
@ -0,0 +1,11 @@
+toplevel "A";
+"A" and "B" "C";
+"B" lambda=1;
+"C" lambda=1;
+"F1" fdep "O" "B";
+"F2" fdep "O" "C";
+"O" or "S" "T";
+"S" or "T" "D";
+"T" or "E";
+"D" lambda=2;
+"E" lambda=4;
--- a/src/storm-dft-cli/storm-dft.cpp
+++ b/src/storm-dft-cli/storm-dft.cpp
@ -171,7 +171,7 @@ void processOptions() {
        // All events are relevant
        additionalRelevantEventNames = {"all"};
    }
-    storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents<ValueType>(*dft, props, additionalRelevantEventNames, faultTreeSettings.isAllowDCForRelevantEvents());
+    storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents<ValueType>(*dft, props, additionalRelevantEventNames);


    // Analyze DFT
@ -183,7 +183,7 @@ void processOptions() {
        if (faultTreeSettings.isApproximationErrorSet()) {
            approximationError = faultTreeSettings.getApproximationError();
        }
-        storm::api::analyzeDFT<ValueType>(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), relevantEvents, approximationError, faultTreeSettings.getApproximationHeuristic(), transformationSettings.isChainEliminationSet(), transformationSettings.getLabelBehavior(), true);
+        storm::api::analyzeDFT<ValueType>(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), relevantEvents, faultTreeSettings.isAllowDCForRelevantEvents(), approximationError, faultTreeSettings.getApproximationHeuristic(), transformationSettings.isChainEliminationSet(), transformationSettings.getLabelBehavior(), true);
    }
 }

--- a/src/storm-dft/api/storm-dft.h
+++ b/src/storm-dft/api/storm-dft.h
@ -125,12 +125,11 @@ namespace storm {
         * @param dft DFT.
         * @param properties List of properties. All events occurring in a property are relevant.
         * @param additionalRelevantEventNames List of names of additional relevant events.
-         * @param allowDCForRelevant Whether to allow Don't Care propagation for relevant events.
         * @return Relevant events.
         */
        template<typename ValueType>
-        storm::utility::RelevantEvents computeRelevantEvents(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, std::vector<std::string> const& additionalRelevantEventNames, bool allowDCForRelevant) {
-            storm::utility::RelevantEvents events(additionalRelevantEventNames, allowDCForRelevant);
+        storm::utility::RelevantEvents computeRelevantEvents(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, std::vector<std::string> const& additionalRelevantEventNames) {
+            storm::utility::RelevantEvents events(additionalRelevantEventNames);
            events.addNamesFromProperty(properties);
            return events;
        }
@ -144,6 +143,7 @@ namespace storm {
         * @param symred Flag whether symmetry reduction should be used.
         * @param allowModularisation Flag whether modularisation should be applied if possible.
         * @param relevantEvents Relevant events which should be observed.
+         * @param allowDCForRelevant Whether to allow Don't Care propagation for relevant events
         * @param approximationError Allowed approximation error.  Value 0 indicates no approximation.
         * @param approximationHeuristic Heuristic used for state space exploration.
         * @param eliminateChains If true, chains of non-Markovian states are eliminated from the resulting MA.
@ -153,11 +153,11 @@ namespace storm {
         */
        template<typename ValueType>
        typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results
-        analyzeDFT(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred = true, bool allowModularisation = true, storm::utility::RelevantEvents const& relevantEvents = storm::utility::RelevantEvents(),
+        analyzeDFT(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred = true, bool allowModularisation = true, storm::utility::RelevantEvents const& relevantEvents = storm::utility::RelevantEvents(), bool allowDCForRelevant = false,
                   double approximationError = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, bool eliminateChains = false,
                   storm::transformer::EliminationLabelBehavior labelBehavior = storm::transformer::EliminationLabelBehavior::KeepLabels, bool printOutput = false) {
            storm::modelchecker::DFTModelChecker<ValueType> modelChecker(printOutput);
-            typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, relevantEvents, approximationError, approximationHeuristic, eliminateChains, labelBehavior);
+            typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, relevantEvents, allowDCForRelevant, approximationError, approximationHeuristic, eliminateChains, labelBehavior);
            if (printOutput) {
                modelChecker.printTimings();
                modelChecker.printResults(results);
--- a/src/storm-dft/generator/DftNextStateGenerator.cpp
+++ b/src/storm-dft/generator/DftNextStateGenerator.cpp
@ -159,14 +159,13 @@ namespace storm {
                // Set transitions
                if (exploreDependencies) {
                    // Failure is due to dependency -> add non-deterministic choice if necessary
-                    ValueType probability = mDft.getDependency(*iterFailable)->probability();
+                    ValueType probability = dependency->probability();
                    choice.addProbability(newStateId, probability);
                    STORM_LOG_TRACE("Added transition to " << newStateId << " with probability " << probability);

                    if (!storm::utility::isOne(probability)) {
                        // Add transition to state where dependency was unsuccessful
-                        DFTStatePointer unsuccessfulState = state->copy();
-                        unsuccessfulState->letDependencyBeUnsuccessful(*iterFailable);
+                        DFTStatePointer unsuccessfulState = createSuccessorState(state, nextBE, dependency, false);
                        // Add state
                        StateType unsuccessfulStateId = stateToIdCallback(unsuccessfulState);
                        ValueType remainingProbability = storm::utility::one<ValueType>() - probability;
@ -221,10 +220,20 @@ namespace storm {
        }

        template<typename ValueType, typename StateType>
-        typename DftNextStateGenerator<ValueType, StateType>::DFTStatePointer DftNextStateGenerator<ValueType, StateType>::createSuccessorState(DFTStatePointer const state, std::shared_ptr<storm::storage::DFTBE<ValueType> const>& failedBE, std::shared_ptr<storm::storage::DFTDependency<ValueType> const>& triggeringDependency) const {
+        typename DftNextStateGenerator<ValueType, StateType>::DFTStatePointer DftNextStateGenerator<ValueType, StateType>::createSuccessorState(DFTStatePointer const state, std::shared_ptr<storm::storage::DFTBE<ValueType> const>& failedBE, std::shared_ptr<storm::storage::DFTDependency<ValueType> const>& triggeringDependency, bool dependencySuccessful) const {
            // Construct new state as copy from original one
            DFTStatePointer newState = state->copy();
-            STORM_LOG_TRACE("With the failure of: " << failedBE->name() << " [" << failedBE->id() << "]" << (triggeringDependency != nullptr ? " (through dependency " + triggeringDependency->name() + " [" + std::to_string(triggeringDependency->id()) + ")]" : "") << " in " << mDft.getStateString(state));
+
+            if (!dependencySuccessful) {
+                // Dependency was unsuccessful -> no BE fails
+                STORM_LOG_ASSERT(triggeringDependency != nullptr, "Dependency is not given");
+                STORM_LOG_TRACE("With the unsuccessful triggering of PDEP " << triggeringDependency->name() << " [" << triggeringDependency->id() << "]" << " in " << mDft.getStateString(state));
+                newState->letDependencyBeUnsuccessful(triggeringDependency);
+                return newState;
+            }
+
+
+            STORM_LOG_TRACE("With the failure of " << failedBE->name() << " [" << failedBE->id() << "]" << (triggeringDependency != nullptr ? " (through dependency " + triggeringDependency->name() + " [" + std::to_string(triggeringDependency->id()) + ")]" : "") << " in " << mDft.getStateString(state));

            newState->letBEFail(failedBE, triggeringDependency);

--- a/src/storm-dft/generator/DftNextStateGenerator.h
+++ b/src/storm-dft/generator/DftNextStateGenerator.h
@ -61,10 +61,12 @@ namespace storm {
             * @param state Current state.
             * @param failedBE BE which fails next.
             * @param triggeringDependency Dependency which triggered the failure (or nullptr if BE failed on its own).
+             * @param dependencySuccessful Whether the triggering dependency was successful.
+             *              If the dependency is unsuccessful, failedBE does not fail and only the depedendy is marked as failed.
             * 
             * @return Successor state.
             */
-            DFTStatePointer createSuccessorState(DFTStatePointer const state, std::shared_ptr<storm::storage::DFTBE<ValueType> const> &failedBE, std::shared_ptr<storm::storage::DFTDependency<ValueType> const> &triggeringDependency) const;
+            DFTStatePointer createSuccessorState(DFTStatePointer const state, std::shared_ptr<storm::storage::DFTBE<ValueType> const> &failedBE, std::shared_ptr<storm::storage::DFTDependency<ValueType> const> &triggeringDependency, bool dependencySuccessful = true) const;

            /**
             * Propagate the failures in a given state if the given BE fails
--- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
@ -22,7 +22,7 @@ namespace storm {

        template<typename ValueType>
        typename DFTModelChecker<ValueType>::dft_results DFTModelChecker<ValueType>::check(storm::storage::DFT<ValueType> const& origDft, std::vector<std::shared_ptr<const storm::logic::Formula>> const& properties,
-                                                                                           bool symred, bool allowModularisation, storm::utility::RelevantEvents const& relevantEvents,
+                                                                                           bool symred, bool allowModularisation, storm::utility::RelevantEvents const& relevantEvents, bool allowDCForRelevant,
                                                                                           double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic,
                                                                                           bool eliminateChains, storm::transformer::EliminationLabelBehavior labelBehavior) {
            totalTimer.start();
@ -44,14 +44,14 @@ namespace storm {
            // TODO: distinguish for all properties, not only for first one
            if (properties[0]->isTimeOperatorFormula() && allowModularisation) {
                // Use parallel composition as modularisation approach for expected time
-                std::shared_ptr<storm::models::sparse::Model<ValueType>> model = buildModelViaComposition(dft, properties, symred, true, relevantEvents);
+                std::shared_ptr<storm::models::sparse::Model<ValueType>> model = buildModelViaComposition(dft, properties, symred, true, relevantEvents, allowDCForRelevant);
                // Model checking
                std::vector<ValueType> resultsValue = checkModel(model, properties);
                for (ValueType result : resultsValue) {
                    results.push_back(result);
                }
            } else {
-                results = checkHelper(dft, properties, symred, allowModularisation, relevantEvents, approximationError, approximationHeuristic, eliminateChains, labelBehavior);
+                results = checkHelper(dft, properties, symred, allowModularisation, relevantEvents, allowDCForRelevant, approximationError, approximationHeuristic, eliminateChains, labelBehavior);
            }
            totalTimer.stop();
            return results;
@ -59,7 +59,7 @@ namespace storm {

        template<typename ValueType>
        typename DFTModelChecker<ValueType>::dft_results DFTModelChecker<ValueType>::checkHelper(storm::storage::DFT<ValueType> const& dft, property_vector const& properties,
-                                                                                                 bool symred, bool allowModularisation, storm::utility::RelevantEvents const& relevantEvents,
+                                                                                                 bool symred, bool allowModularisation, storm::utility::RelevantEvents const& relevantEvents, bool allowDCForRelevant,
                                                                                                 double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic,
                                                                                                 bool eliminateChains, storm::transformer::EliminationLabelBehavior labelBehavior) {
            STORM_LOG_TRACE("Check helper called");
@ -114,7 +114,7 @@ namespace storm {
                        std::vector<ValueType> res;
                        for (auto const ft : dfts) {
                            // TODO: allow approximation in modularisation
-                            dft_results ftResults = checkHelper(ft, {property}, symred, true, relevantEvents, 0.0);
+                            dft_results ftResults = checkHelper(ft, {property}, symred, true, relevantEvents, allowDCForRelevant, 0.0);
                            STORM_LOG_ASSERT(ftResults.size() == 1, "Wrong number of results");
                            res.push_back(boost::get<ValueType>(ftResults[0]));
                        }
@ -152,13 +152,13 @@ namespace storm {
                return results;
            } else {
                // No modularisation was possible
-                return checkDFT(dft, properties, symred, relevantEvents, approximationError, approximationHeuristic, eliminateChains, labelBehavior);
+                return checkDFT(dft, properties, symred, relevantEvents, allowDCForRelevant, approximationError, approximationHeuristic, eliminateChains, labelBehavior);
            }
        }

        template<typename ValueType>
        std::shared_ptr<storm::models::sparse::Ctmc<ValueType>>
-        DFTModelChecker<ValueType>::buildModelViaComposition(storm::storage::DFT<ValueType> const &dft, property_vector const &properties, bool symred, bool allowModularisation, storm::utility::RelevantEvents const& relevantEvents) {
+        DFTModelChecker<ValueType>::buildModelViaComposition(storm::storage::DFT<ValueType> const &dft, property_vector const &properties, bool symred, bool allowModularisation, storm::utility::RelevantEvents const& relevantEvents, bool allowDCForRelevant) {
            // TODO: use approximation?
            STORM_LOG_TRACE("Build model via composition");
            std::vector<storm::storage::DFT<ValueType>> dfts;
@ -197,7 +197,7 @@ namespace storm {
                    STORM_LOG_DEBUG("Building Model via parallel composition...");
                    explorationTimer.start();

-                    ft.setRelevantEvents(relevantEvents);
+                    ft.setRelevantEvents(relevantEvents, allowDCForRelevant);
                    // Find symmetries
                    std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;
                    storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry);
@ -259,7 +259,7 @@ namespace storm {
                // No composition was possible
                explorationTimer.start();

-                dft.setRelevantEvents(relevantEvents);
+                dft.setRelevantEvents(relevantEvents, allowDCForRelevant);

                // Find symmetries
                std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;
@ -289,13 +289,13 @@ namespace storm {

        template<typename ValueType>
        typename DFTModelChecker<ValueType>::dft_results
-        DFTModelChecker<ValueType>::checkDFT(storm::storage::DFT<ValueType> const &dft, property_vector const &properties, bool symred, storm::utility::RelevantEvents const& relevantEvents,
+        DFTModelChecker<ValueType>::checkDFT(storm::storage::DFT<ValueType> const &dft, property_vector const &properties, bool symred, storm::utility::RelevantEvents const& relevantEvents, bool allowDCForRelevant,
                                             double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic, bool eliminateChains, storm::transformer::EliminationLabelBehavior labelBehavior) {
            explorationTimer.start();
            auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
            auto dftIOSettings = storm::settings::getModule<storm::settings::modules::DftIOSettings>();

-            dft.setRelevantEvents(relevantEvents);
+            dft.setRelevantEvents(relevantEvents, allowDCForRelevant);

            // Find symmetries
            std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;
--- a/src/storm-dft/modelchecker/dft/DFTModelChecker.h
+++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.h
@ -48,13 +48,15 @@ namespace storm {
             * @param symred Flag whether symmetry reduction should be used.
             * @param allowModularisation Flag indicating if modularisation is allowed.
             * @param relevantEvents Relevant events which should be observed.
+             * @param allowDCForRelevant Whether to allow Don't Care propagation for relevant events
             * @param approximationError Error allowed for approximation. Value 0 indicates no approximation.
             * @param approximationHeuristic Heuristic used for state space exploration.
             * @param eliminateChains If true, chains of non-Markovian states are elimianted from the resulting MA
             * @param labelBehavior Behavior of labels of eliminated states
             * @return Model checking results for the given properties..
             */
-            dft_results check(storm::storage::DFT<ValueType> const& origDft, property_vector const& properties, bool symred = true, bool allowModularisation = true, storm::utility::RelevantEvents const& relevantEvents = storm::utility::RelevantEvents(),
+            dft_results check(storm::storage::DFT<ValueType> const& origDft, property_vector const& properties, bool symred = true, bool allowModularisation = true,
+                              storm::utility::RelevantEvents const& relevantEvents = storm::utility::RelevantEvents(), bool allowDCForRelevant = false,
                              double approximationError = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH,
                              bool eliminateChains = false, storm::transformer::EliminationLabelBehavior labelBehavior = storm::transformer::EliminationLabelBehavior::KeepLabels);

@ -92,13 +94,15 @@ namespace storm {
             * @param symred Flag indicating if symmetry reduction should be used.
             * @param allowModularisation Flag indicating if modularisation is allowed.
             * @param relevantEvents Relevant events which should be observed.
+             * @param allowDCForRelevant Whether to allow Don't Care propagation for relevant events
             * @param approximationError Error allowed for approximation. Value 0 indicates no approximation.
             * @param approximationHeuristic Heuristic used for approximation.
             * @param eliminateChains If true, chains of non-Markovian states are elimianted from the resulting MA
             * @param labelBehavior Behavior of labels of eliminated states
             * @return Model checking results (or in case of approximation two results for lower and upper bound)
             */
-            dft_results checkHelper(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, bool allowModularisation, storm::utility::RelevantEvents const& relevantEvents,
+            dft_results checkHelper(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, bool allowModularisation,
+                                    storm::utility::RelevantEvents const& relevantEvents, bool allowDCForRelevant = false,
                                    double approximationError = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH,
                                    bool eliminateChains = false, storm::transformer::EliminationLabelBehavior labelBehavior = storm::transformer::EliminationLabelBehavior::KeepLabels);

@ -109,10 +113,16 @@ namespace storm {
             * @param properties Properties to check for.
             * @param symred Flag indicating if symmetry reduction should be used.
             * @param allowModularisation Flag indicating if modularisation is allowed.
-             * @param relevantEvents List with ids of relevant events which should be observed.
+             * @param relevantEvents Relevant events which should be observed.
+             * @param allowDCForRelevant Whether to allow Don't Care propagation for relevant events
             * @return CTMC representing the DFT
             */
-            std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> buildModelViaComposition(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, bool allowModularisation, storm::utility::RelevantEvents const& relevantEvents);
+            std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> buildModelViaComposition(storm::storage::DFT<ValueType> const& dft,
+                    property_vector const& properties,
+                    bool symred,
+                    bool allowModularisation,
+                    storm::utility::RelevantEvents const& relevantEvents,
+                    bool allowDCForRelevant);

            /*!
             * Check model generated from DFT.
@ -120,7 +130,8 @@ namespace storm {
             * @param dft The DFT.
             * @param properties Properties to check for.
             * @param symred Flag indicating if symmetry reduction should be used.
-             * @param relevantEvents List with ids of relevant events which should be observed.
+             * @param relevantEvents Relevant events which should be observed.
+             * @param allowDCForRelevant Whether to allow Don't Care propagation for relevant events
             * @param approximationError Error allowed for approximation. Value 0 indicates no approximation.
             * @param approximationHeuristic Heuristic used for approximation.
             * @param eliminateChains If true, chains of non-Markovian states are elimianted from the resulting MA
@ -128,7 +139,7 @@ namespace storm {
             *
             * @return Model checking result
             */
-            dft_results checkDFT(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, storm::utility::RelevantEvents const& relevantEvents,
+            dft_results checkDFT(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, storm::utility::RelevantEvents const& relevantEvents, bool allowDCForRelevant,
                                 double approximationError = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH,
                                 bool eliminateChains = false, storm::transformer::EliminationLabelBehavior labelBehavior = storm::transformer::EliminationLabelBehavior::KeepLabels);

--- a/src/storm-dft/simulator/DFTTraceSimulator.cpp
+++ b/src/storm-dft/simulator/DFTTraceSimulator.cpp
@ -26,7 +26,7 @@ namespace storm {
            }

            template<typename ValueType>
-            double DFTTraceSimulator<ValueType>::randomStep() {
+            std::tuple<storm::dft::storage::FailableElements::const_iterator, double, bool> DFTTraceSimulator<ValueType>::randomNextFailure() {
                auto iterFailable = state->getFailableElements().begin();

                // Check for absorbing state:
@ -34,18 +34,25 @@ namespace storm {
                // - no BE can fail
                if (!state->hasOperationalRelevantEvent() || iterFailable == state->getFailableElements().end()) {
                    STORM_LOG_TRACE("No sucessor states available for " << state->getId());
-                    return -1;
+                    return std::make_tuple(iterFailable, -1, true);
                }

                // Get all failable elements
                if (iterFailable.isFailureDueToDependency()) {
                    if (iterFailable.isConflictingDependency()) {
-                        // We take the first dependeny to resolve the non-determinism
+                        // We take the first dependency to resolve the non-determinism
                        STORM_LOG_WARN("Non-determinism present! We take the dependency with the lowest id");
                    }
-                    STORM_LOG_TRACE("Let dependency " << *iterFailable.getFailBE(dft).second << " fail");
-                    bool res = step(iterFailable);
-                    return res ? 0 : -1;
+
+                    auto dependency = iterFailable.getFailBE(dft).second;
+                    if (!dependency->isFDEP()) {
+                        // Flip a coin whether the PDEP is successful
+                        storm::utility::BernoulliDistributionGenerator probGenerator(dependency->probability());
+                        bool successful = probGenerator.random(randomGenerator);
+                        return std::make_tuple(iterFailable, 0, successful);
+                    }
+                    STORM_LOG_TRACE("Let dependency " << *dependency << " fail");
+                    return std::make_tuple(iterFailable, 0, true);
                } else {
                    // Consider all "normal" BE failures
                    // Initialize with first BE
@ -67,58 +74,114 @@ namespace storm {
                            smallestTimebound = timebound;
                        }
                    }
-                    STORM_LOG_TRACE("Let BE " << *nextFail.getFailBE(dft).first << "fail after time " << smallestTimebound);
-                    bool res = step(nextFail);
-                    return res ? smallestTimebound : -1;
+                    STORM_LOG_TRACE("Let BE " << *nextFail.getFailBE(dft).first << " fail after time " << smallestTimebound);
+                    return std::make_tuple(nextFail, smallestTimebound, true);
                }
            }

+            template<>
+            std::tuple<storm::dft::storage::FailableElements::const_iterator, double, bool> DFTTraceSimulator<storm::RationalFunction>::randomNextFailure() {
+                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Simulation not support for parametric DFTs.");
+            }
+
            template<typename ValueType>
-            bool DFTTraceSimulator<ValueType>::step(storm::dft::storage::FailableElements::const_iterator nextFailElement) {
+            std::pair<SimulationResult, double> DFTTraceSimulator<ValueType>::randomStep() {
+                auto retTuple = this->randomNextFailure();
+                storm::dft::storage::FailableElements::const_iterator nextFailable = std::get<0>(retTuple);
+                double time = std::get<1>(retTuple);
+                bool successful = std::get<2>(retTuple);
+                if (time < 0) {
+                    return std::make_pair(SimulationResult::UNSUCCESSFUL, -1);
+                } else {
+                    // Apply next failure
+                    return std::make_pair(step(nextFailable, successful), time);
+                }
+            }
+
+            template<typename ValueType>
+            SimulationResult DFTTraceSimulator<ValueType>::step(storm::dft::storage::FailableElements::const_iterator nextFailElement, bool dependencySuccessful) {
                if (nextFailElement == state->getFailableElements().end()) {
-                    return false;
+                    // No next failure possible
+                    return SimulationResult::UNSUCCESSFUL;
                }

                auto nextBEPair = nextFailElement.getFailBE(dft);
-                auto newState = generator.createSuccessorState(state, nextBEPair.first, nextBEPair.second);
-
-                // TODO handle PDEP
+                auto newState = generator.createSuccessorState(state, nextBEPair.first, nextBEPair.second, dependencySuccessful);
                
                if(newState->isInvalid() || newState->isTransient()) {
                    STORM_LOG_TRACE("Step is invalid because new state " << (newState->isInvalid() ? "it is invalid" : "the transient fault is ignored"));
-                    return false;
+                    return SimulationResult::INVALID;
                }

                state = newState;
-                return true;
+                return SimulationResult::SUCCESSFUL;
            }

            template<typename ValueType>
-            bool DFTTraceSimulator<ValueType>::simulateCompleteTrace(double timebound) {
+            SimulationResult DFTTraceSimulator<ValueType>::simulateCompleteTrace(double timebound) {
                resetToInitial();
+
+                // Check whether DFT is initially already failed.
+                if (state->hasFailed(dft.getTopLevelIndex())) {
+                    STORM_LOG_TRACE("DFT is initially failed");
+                    return SimulationResult::SUCCESSFUL;
+                }
+
                double time = 0;
                while (time <= timebound) {
-                    // Check whether DFT failed within timebound
-                    if (state->hasFailed(dft.getTopLevelIndex())) {
-                        STORM_LOG_TRACE("DFT has failed after " << time);
-                        return true;
+                    // Generate next failure
+                    auto retTuple = randomNextFailure();
+                    storm::dft::storage::FailableElements::const_iterator nextFailable = std::get<0>(retTuple);
+                    double addTime = std::get<1>(retTuple);
+                    bool successfulDependency = std::get<2>(retTuple);
+                    if (addTime < 0) {
+                        // No next state can be reached, because no element can fail anymore.
+                        STORM_LOG_TRACE("No next state possible in state " << dft.getStateString(state) << " because no element can fail anymore");
+                        return SimulationResult::UNSUCCESSFUL;
                    }

-                    // Generate next state
-                    double res = randomStep();
+                    // TODO: exit if time would be up after this failure
+                    // This is only correct if no invalid states are possible! (no restrictors and no transient failures)
+
+                    // Apply next failure
+                    auto stepResult = step(nextFailable, successfulDependency);
                    STORM_LOG_TRACE("Current state: " << dft.getStateString(state));
-                    if (res < 0) {
-                        // No next state can be reached
-                        STORM_LOG_TRACE("No next state possible in state " << dft.getStateString(state));
-                        return false;
+
+                    // Check whether state is invalid
+                    if (stepResult != SimulationResult::SUCCESSFUL) {
+                        STORM_LOG_ASSERT(stepResult == SimulationResult::INVALID, "Result of simulation step should be invalid.");
+                        // No next state can be reached, because the state is invalid.
+                        STORM_LOG_TRACE("No next state possible in state " << dft.getStateString(state) << " because simulation was invalid");
+                        STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Handling of invalid states is not supported for simulation");
+                        return SimulationResult::INVALID;
+                    }
+
+                    // Check whether time is up
+                    // Checking whether the time is up must be performed after checking if a state is invalid.
+                    // Otherwise we would erroneously mark invalid traces as unsucessful.
+                    time += addTime;
+                    if (time > timebound) {
+                        STORM_LOG_TRACE("Time limit" << timebound << " exceeded: " << time);
+                        return SimulationResult::UNSUCCESSFUL;
+                    }
+
+                    // Check whether DFT is failed
+                    if (state->hasFailed(dft.getTopLevelIndex())) {
+                        STORM_LOG_TRACE("DFT has failed after " << time);
+                        return SimulationResult::SUCCESSFUL;
                    }
-                    time += res;
                }
-                // Time is up
-                return false;
+                STORM_LOG_ASSERT(false, "Should not be reachable");
+                return SimulationResult::UNSUCCESSFUL;
+            }
+
+            template<>
+            SimulationResult DFTTraceSimulator<storm::RationalFunction>::simulateCompleteTrace(double timebound) {
+                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Simulation not support for parametric DFTs.");
            } 

            template class DFTTraceSimulator<double>;
+            template class DFTTraceSimulator<storm::RationalFunction>;
        }
    }
 }
--- a/src/storm-dft/simulator/DFTTraceSimulator.h
+++ b/src/storm-dft/simulator/DFTTraceSimulator.h
@ -10,6 +10,12 @@ namespace storm {
    namespace dft {
        namespace simulator {

+            /*!
+             * Simulation result.
+             *
+             */
+            enum class SimulationResult { SUCCESSFUL, UNSUCCESSFUL, INVALID };
+
            /*!
             * Simulator for DFTs.
             * A step in the simulation corresponds to the failure of one BE (either on its own or triggered by a dependency)
@ -19,6 +25,7 @@ namespace storm {
            template<typename ValueType>
            class DFTTraceSimulator {
                using DFTStatePointer = std::shared_ptr<storm::storage::DFTState<ValueType>>;
+
            public:
                /*!
                 * Constructor.
@ -52,27 +59,40 @@ namespace storm {
                 * Perform one simulation step by letting the next element fail.
                 * 
                 * @param nextFailElement Iterator giving the next element which should fail.
-                 * @return True iff step could be performed successfully.
+                 * @param dependencySuccessful Whether the triggering dependency was successful.
+                 *              If the dependency is unsuccessful, no BE fails and only the depedendy is marked as failed.
+                 * @return Successful if step could be performed, unsuccesful if no element can fail or invalid if the next state is invalid (due to a restrictor).
+                 */
+                SimulationResult step(storm::dft::storage::FailableElements::const_iterator nextFailElement, bool dependencySuccessful = true);
+
+                /*!
+                 * Randomly pick an element which fails next (either a BE or a dependency which triggers a BE) and the time after which it fails.
+                 * The time is 0 for a dependency and -1 if no failure can take place.
+                 * In the latter case, the next failable element is not defined.
+                 *
+                 * @return Tuple of next failable element, time after which is fails and whether a possible failure through the dependency is successful.
                 */
-                bool step(storm::dft::storage::FailableElements::const_iterator nextFailElement);
+                std::tuple<storm::dft::storage::FailableElements::const_iterator, double, bool> randomNextFailure();

                /*!
                 * Perform a random step by using the random number generator.
                 * 
-                 * @return double The time which progessed between the last step and this step.
-                 *      Returns -1 if no next step could be created.
+                 * @return Pair of the simulation result (successful, unsuccesful, invalid) and the time which progessed between the last step and this step.
                 */
-                double randomStep();
+                std::pair<SimulationResult, double> randomStep();

                /*!
                 * Perform a complete simulation of a failure trace by using the random number generator.
                 * The simulation starts in the initial state and tries to reach a state where the top-level event of the DFT has failed.
                 * If this target state can be reached within the given timebound, the simulation was successful.
+                 * If an invalid state (due to a restrictor) was reached, the simulated trace is invalid.
                 * 
                 * @param timebound Time bound in which the system failure should occur.
-                 * @return True iff a system failure occurred for the generated trace within the time bound.
+                 * @return Simulation result is (1) successful if a system failure occurred for the generated trace within the time bound,
+                 *                              (2) unsuccesfull, if no system failure occurred within the time bound, or
+                 *                              (3) invalid, if an invalid state (due to a restrictor) was reached during the trace generation.
                 */
-                bool simulateCompleteTrace(double timebound);
+                SimulationResult simulateCompleteTrace(double timebound);

            protected:

@ -83,7 +103,7 @@ namespace storm {
                storm::storage::DFTStateGenerationInfo const& stateGenerationInfo;

                // Generator for creating next state in DFT
-                storm::generator::DftNextStateGenerator<double> generator;
+                storm::generator::DftNextStateGenerator<ValueType> generator;

                // Current state
                DFTStatePointer state;
--- a/src/storm-dft/storage/dft/DFT.cpp
+++ b/src/storm-dft/storage/dft/DFT.cpp
@ -10,6 +10,7 @@

 #include "storm-dft/builder/DFTBuilder.h"
 #include "storm-dft/storage/dft/DFTIsomorphism.h"
+#include "storm-dft/utility/RelevantEvents.h"


 namespace storm {
@ -1038,7 +1039,7 @@ namespace storm {
        }

        template<typename ValueType>
-        void DFT<ValueType>::setRelevantEvents(storm::utility::RelevantEvents const& relevantEvents) const {
+        void DFT<ValueType>::setRelevantEvents(storm::utility::RelevantEvents const& relevantEvents, bool const allowDCForRelevant) const {
            mRelevantEvents.clear();
            STORM_LOG_THROW(relevantEvents.checkRelevantNames(*this), storm::exceptions::InvalidArgumentException, "One of the relevant elements does not exist.");
            // Top level element is first element
@ -1046,7 +1047,7 @@ namespace storm {
            for (auto& elem : mElements) {
                if (relevantEvents.isRelevant(elem->name()) || elem->id() == this->getTopLevelIndex()) {
                    elem->setRelevance(true);
-                    elem->setAllowDC(relevantEvents.isAllowDC());
+                    elem->setAllowDC(allowDCForRelevant);
                    if (elem->id() != this->getTopLevelIndex()) {
                        // Top level element was already added
                        mRelevantEvents.push_back(elem->id());
--- a/src/storm-dft/storage/dft/DFT.h
+++ b/src/storm-dft/storage/dft/DFT.h
@ -17,13 +17,15 @@
 #include "storm-dft/storage/dft/SymmetricUnits.h"
 #include "storm-dft/storage/dft/DFTStateGenerationInfo.h"
 #include "storm-dft/storage/dft/DFTLayoutInfo.h"
-#include "storm-dft/utility/RelevantEvents.h"

 namespace storm {
+    // Forward declarations
    namespace builder {
-        // Forward declaration
        template<typename T> class DFTBuilder;
    }
+    namespace utility {
+        class RelevantEvents;
+    }

    namespace storage {

@ -376,8 +378,9 @@ namespace storm {
            /*!
             * Set the relevance flag for all elements according to the given relevant events.
             * @param relevantEvents All elements which should be to relevant. All elements not occurring are set to irrelevant.
+             * @param allowDCForRelevant Whether to allow Don't Care propagation for relevant events
             */
-            void setRelevantEvents(storm::utility::RelevantEvents const& relevantEvents) const;
+            void setRelevantEvents(storm::utility::RelevantEvents const& relevantEvents, bool const allowDCForRelevant) const;

            /*!
             * Get a string containing the list of all relevant events.
--- a/src/storm-dft/storage/dft/DFTState.cpp
+++ b/src/storm-dft/storage/dft/DFTState.cpp
@ -343,10 +343,10 @@ namespace storm {
        }
 
        template<typename ValueType>
-        void DFTState<ValueType>::letDependencyBeUnsuccessful(size_t id) {
+        void DFTState<ValueType>::letDependencyBeUnsuccessful(std::shared_ptr<storm::storage::DFTDependency<ValueType> const> dependency) {
            STORM_LOG_ASSERT(failableElements.hasDependencies(), "Index invalid.");
-            std::shared_ptr<DFTDependency<ValueType> const> dependency = mDft.getDependency(id);
-            failableElements.removeDependency(id);
+            STORM_LOG_ASSERT(!dependency->isFDEP(), "Dependency is not a PDEP.");
+            failableElements.removeDependency(dependency->id());
            setDependencyUnsuccessful(dependency->id());
        }

--- a/src/storm-dft/storage/dft/DFTState.h
+++ b/src/storm-dft/storage/dft/DFTState.h
@ -247,9 +247,9 @@ namespace storm {
            
            /**
             * Sets the dependency as unsuccesful meaning no BE will fail.
-             * @param index Index of dependency to fail.
+             * @param dependency Dependency.
             */
-            void letDependencyBeUnsuccessful(size_t index = 0);
+            void letDependencyBeUnsuccessful(std::shared_ptr<storm::storage::DFTDependency<ValueType> const> dependency);
            
            /**
             * Order the state in decreasing order using the symmetries.
--- a/src/storm-dft/transformations/DftTransformator.cpp
+++ b/src/storm-dft/transformations/DftTransformator.cpp
@ -150,7 +150,7 @@ namespace storm {
                        }
                        case storm::storage::DFTElementType::POR: {
                            auto por = std::static_pointer_cast<storm::storage::DFTPor<ValueType> const>(element);
-                            builder.addPandElement(por->name(), getChildrenVector(por), por->isInclusive());
+                            builder.addPorElement(por->name(), getChildrenVector(por), por->isInclusive());
                            break;
                        }
                        case storm::storage::DFTElementType::SPARE:
--- a/src/storm-dft/utility/RelevantEvents.h
+++ b/src/storm-dft/utility/RelevantEvents.h
@ -19,20 +19,25 @@ namespace storm {
             * If name 'all' occurs, all elements are stored as relevant.
             *
             * @param relevantEvents List of relevant event names.
-             * @param allowDCForRelevant Whether to allow Don't Care propagation for relevant events.
             */
-            RelevantEvents(std::vector<std::string> const& relevantEvents = {}, bool allowDCForRelevant = false) : names(), allRelevant(false), allowDC(allowDCForRelevant) {
-                for (auto const& name: relevantEvents) {
-                    if (name == "all") {
-                        this->allRelevant = true;
-                        this->names.clear();
-                        break;
-                    } else {
-                        this->addEvent(name);
-                    }
+            RelevantEvents(std::vector<std::string> const& relevantEvents = {}) {
+                // check if the name "all" occurs
+                if (std::any_of(relevantEvents.begin(), relevantEvents.end(),
+                                [](auto const& name) { return name == "all"; })) {
+                    this->allRelevant = true;
+                } else {
+                    this->names.insert(relevantEvents.begin(), relevantEvents.end());
                }
            }

+            bool operator==(RelevantEvents const& rhs) {
+                return this->allRelevant == rhs.allRelevant || this->names == rhs.names;
+            }
+
+            bool operator!=(RelevantEvents const& rhs) {
+                return !(*this == rhs);
+            }
+
            /*!
             * Add relevant event names required by the labels in properties.
             *
@ -57,8 +62,10 @@ namespace storm {
                    } else {
                        // Get name of event
                        if (boost::ends_with(label, "_failed")) {
+                            // length of "_failed" = 7
                            this->addEvent(label.substr(0, label.size() - 7));
                        } else if (boost::ends_with(label, "_dc")) {
+                            // length of "_dc" = 3
                            this->addEvent(label.substr(0, label.size() - 3));
                        } else if (label.find("_claimed_") != std::string::npos) {
                            STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::FaultTreeSettings>().isAddLabelsClaiming(), storm::exceptions::InvalidArgumentException, "Claiming labels will not be exported but are required for label '" << label << "'. Try setting --labels-claiming.");
@ -73,7 +80,7 @@ namespace storm {
             * Check that the relevant names correspond to existing elements in the DFT.
             *
             * @param dft DFT.
-             * @return True iff relevant names are consistent with DFT elements.
+             * @return True iff the relevant names are consistent with the given DFT.
             */
            template <typename ValueType>
            bool checkRelevantNames(storm::storage::DFT<ValueType> const& dft) const {
@ -85,6 +92,9 @@ namespace storm {
                return true;
            }

+            /*!
+             * @return True iff the given name is the name of a relevant Event
+             */
            bool isRelevant(std::string const& name) const {
                if (this->allRelevant) {
                    return true;
@ -93,10 +103,6 @@ namespace storm {
                }
            }

-            bool isAllowDC() const {
-                return this->allowDC;
-            }
-
        private:

            /*!
@ -109,13 +115,10 @@ namespace storm {
            }

            // Names of relevant events.
-            std::set<std::string> names;
+            std::set<std::string> names{};

            // Whether all elements are relevant.
-            bool allRelevant;
-
-            // Whether to allow Don't Care propagation for relevant events.
-            bool allowDC;
+            bool allRelevant{false};
        };

    } // namespace utility
--- a/src/storm/utility/random.cpp
+++ b/src/storm/utility/random.cpp
@ -37,6 +37,13 @@ namespace storm {
        }


+        BernoulliDistributionGenerator::BernoulliDistributionGenerator(double prob) : distribution(prob) {
+        }
+
+        bool BernoulliDistributionGenerator::random(boost::mt19937& engine) {
+            return distribution(engine);
+        }
+
        ExponentialDistributionGenerator::ExponentialDistributionGenerator(double rate) : distribution(rate) {
        }

--- a/src/storm/utility/random.h
+++ b/src/storm/utility/random.h
@ -44,6 +44,14 @@ namespace storm {
        };


+        class BernoulliDistributionGenerator {
+        public:
+            BernoulliDistributionGenerator(double prob);
+            bool random(boost::mt19937& engine);
+        private:
+            boost::random::bernoulli_distribution<> distribution;
+        };
+
        class ExponentialDistributionGenerator {
        public:
            ExponentialDistributionGenerator(double rate);
--- a/src/test/storm-dft/api/DftApproximationTest.cpp
+++ b/src/test/storm-dft/api/DftApproximationTest.cpp
@ -57,7 +57,7 @@ namespace {
            EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
            std::string property = "T=? [F \"failed\"]";
            std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
-            typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, false, storm::utility::RelevantEvents(), errorBound, config.heuristic, false);
+            typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, false, storm::utility::RelevantEvents(), false, errorBound, config.heuristic, false);
            return boost::get<storm::modelchecker::DFTModelChecker<double>::approximation_result>(results[0]);
        }

@ -67,7 +67,7 @@ namespace {
            std::stringstream propertyStream;
            propertyStream << "P=? [F<=" << timeBound << " \"failed\"]";
            std::vector <std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(propertyStream.str()));
-            typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, false, storm::utility::RelevantEvents(), errorBound, config.heuristic, false);
+            typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, false, storm::utility::RelevantEvents(), false, errorBound, config.heuristic, false);
            return boost::get<storm::modelchecker::DFTModelChecker<double>::approximation_result>(results[0]);
        }

--- a/src/test/storm-dft/api/DftModelBuildingTest.cpp
+++ b/src/test/storm-dft/api/DftModelBuildingTest.cpp
@ -18,8 +18,8 @@ namespace {
        storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry);

        // Set relevant events (none)
-        storm::utility::RelevantEvents relevantEvents({}, false);
-        dft->setRelevantEvents(relevantEvents);
+        storm::utility::RelevantEvents relevantEvents{};
+        dft->setRelevantEvents(relevantEvents, false);
        // Build model
        storm::builder::ExplicitDFTModelBuilder<double> builder(*dft, symmetries);
        builder.buildModel(0, 0.0);
@ -28,8 +28,8 @@ namespace {
        EXPECT_EQ(13ul, model->getNumberOfTransitions());

        // Set relevant events (all)
-        relevantEvents = storm::utility::RelevantEvents({"all"}, false);
-        dft->setRelevantEvents(relevantEvents);
+        relevantEvents = storm::utility::RelevantEvents({"all"});
+        dft->setRelevantEvents(relevantEvents, false);
        // Build model
        storm::builder::ExplicitDFTModelBuilder<double> builder2(*dft, symmetries);
        builder2.buildModel(0, 0.0);
@ -38,8 +38,8 @@ namespace {
        EXPECT_EQ(2305ul, model->getNumberOfTransitions());

        // Set relevant events (H)
-        relevantEvents = storm::utility::RelevantEvents({"H"}, false);
-        dft->setRelevantEvents(relevantEvents);
+        relevantEvents = storm::utility::RelevantEvents({"H"});
+        dft->setRelevantEvents(relevantEvents, false);
        // Build model
        storm::builder::ExplicitDFTModelBuilder<double> builder3(*dft, symmetries);
        builder3.buildModel(0, 0.0);
@ -49,8 +49,8 @@ namespace {


        // Set relevant events (H, I)
-        relevantEvents = storm::utility::RelevantEvents({"H", "I"}, false);
-        dft->setRelevantEvents(relevantEvents);
+        relevantEvents = storm::utility::RelevantEvents({"H", "I"});
+        dft->setRelevantEvents(relevantEvents, false);
        // Build model
        storm::builder::ExplicitDFTModelBuilder<double> builder4(*dft, symmetries);
        builder4.buildModel(0, 0.0);
@ -59,8 +59,8 @@ namespace {
        EXPECT_EQ(33ul, model->getNumberOfTransitions());

        // Set relevant events (none)
-        relevantEvents = storm::utility::RelevantEvents({}, true);
-        dft->setRelevantEvents(relevantEvents);
+        relevantEvents = storm::utility::RelevantEvents{};
+        dft->setRelevantEvents(relevantEvents, true);
        // Build model
        storm::builder::ExplicitDFTModelBuilder<double> builder5(*dft, symmetries);
        builder5.buildModel(0, 0.0);
@ -69,8 +69,8 @@ namespace {
        EXPECT_EQ(13ul, model->getNumberOfTransitions());

        // Set relevant events (all)
-        relevantEvents = storm::utility::RelevantEvents({"all"}, true);
-        dft->setRelevantEvents(relevantEvents);
+        relevantEvents = storm::utility::RelevantEvents({"all"});
+        dft->setRelevantEvents(relevantEvents, true);
        // Build model
        storm::builder::ExplicitDFTModelBuilder<double> builder6(*dft, symmetries);
        builder6.buildModel(0, 0.0);
@ -80,8 +80,8 @@ namespace {


        // Set relevant events (H, I)
-        relevantEvents = storm::utility::RelevantEvents({"H", "I"}, true);
-        dft->setRelevantEvents(relevantEvents);
+        relevantEvents = storm::utility::RelevantEvents({"H", "I"});
+        dft->setRelevantEvents(relevantEvents, true);
        // Build model
        storm::builder::ExplicitDFTModelBuilder<double> builder7(*dft, symmetries);
        builder7.buildModel(0, 0.0);
--- a/src/test/storm-dft/api/DftModelCheckerTest.cpp
+++ b/src/test/storm-dft/api/DftModelCheckerTest.cpp
@ -86,10 +86,10 @@ namespace {
            if (!config.useDC) {
                relevantNames.push_back("all");
            }
-            storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents<ValueType>(*dft, properties, relevantNames, false);
+            storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents<ValueType>(*dft, properties, relevantNames);

            // Perform model checking
-            typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, config.useMod, relevantEvents);
+            typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, config.useMod, relevantEvents, false);
            return boost::get<double>(results[0]);
        }

--- a/src/test/storm-dft/simulator/DftSimulatorTest.cpp
+++ b/src/test/storm-dft/simulator/DftSimulatorTest.cpp
@ -10,16 +10,16 @@

 namespace {

-    // Helper function
-    double simulateDft(std::string const& file, double timebound, size_t noRuns) {
+    // Helper functions
+    std::pair<double, double> simulateDft(std::string const& file, double timebound, size_t noRuns) {
        // Load, build and prepare DFT
        storm::transformations::dft::DftTransformator<double> dftTransformator = storm::transformations::dft::DftTransformator<double>();
        std::shared_ptr<storm::storage::DFT<double>> dft = dftTransformator.transformBinaryFDEPs(*(storm::api::loadDFTGalileoFile<double>(file)));
        EXPECT_TRUE(storm::api::isWellFormed(*dft).first);

        // Set relevant events
-        storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents<double>(*dft, {}, {}, false);
-        dft->setRelevantEvents(relevantEvents);
+        storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents<double>(*dft, {}, {});
+        dft->setRelevantEvents(relevantEvents, false);

        // Find symmetries
        std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;
@ -27,23 +27,168 @@ namespace {
        storm::storage::DFTStateGenerationInfo stateGenerationInfo(dft->buildStateGenerationInfo(symmetries));
        
        // Init random number generator
+        //storm::utility::setLogLevel(l3pp::LogLevel::TRACE);
        boost::mt19937 gen(5u);
        storm::dft::simulator::DFTTraceSimulator<double> simulator(*dft, stateGenerationInfo, gen);
        
-        size_t count = 0;;
-        bool res;
+        size_t count = 0;
+        size_t invalid = 0;
+        storm::dft::simulator::SimulationResult res;
        for (size_t i=0; i<noRuns; ++i) {
            res = simulator.simulateCompleteTrace(timebound);
-            if (res) {
+            if (res == storm::dft::simulator::SimulationResult::SUCCESSFUL) {
                ++count;
+            } else if (res == storm::dft::simulator::SimulationResult::INVALID) {
+                // Discard invalid traces
+                ++invalid;
            }
        }
+        return std::make_pair(count, invalid);
+    }
+
+    double simulateDftProb(std::string const& file, double timebound, size_t noRuns) {
+        size_t count;
+        size_t invalid;
+        std::tie(count, invalid) = simulateDft(file, timebound, noRuns);
+        EXPECT_EQ(invalid, 0ul);
        return (double) count / noRuns;
    }

-    TEST(DftSimulatorTest, And) {
-        double result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/and.dft", 2, 10000);
+    TEST(DftSimulatorTest, AndUnreliability) {
+        double result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/and.dft", 2, 10000);
        EXPECT_NEAR(result, 0.3995764009, 0.01);
    }

+    TEST(DftSimulatorTest, OrUnreliability) {
+        double result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/or.dft", 1, 10000);
+        EXPECT_NEAR(result, 0.6321205588, 0.01);
+    }
+
+    TEST(DftSimulatorTest, VotingUnreliability) {
+        double result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/voting.dft", 1, 10000);
+        EXPECT_NEAR(result, 0.4511883639, 0.01);
+        result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/voting2.dft", 1, 10000);
+        EXPECT_NEAR(result, 0.8173164759, 0.01);
+        result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/voting3.dft", 1, 10000);
+        EXPECT_NEAR(result, 0.3496529873, 0.01);
+        result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/voting4.dft", 1, 10000);
+#if BOOST_VERSION > 106400
+        EXPECT_NEAR(result, 0.693568287, 0.01);
+#else
+        // Older Boost versions yield different value
+        EXPECT_NEAR(result, 0.693568287, 0.015);
+#endif
+    }
+
+    TEST(DftSimulatorTest, PandUnreliability) {
+        double result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/pand.dft", 1, 10000);
+        EXPECT_NEAR(result, 0.03087312562, 0.01);
+    }
+
+    TEST(DftSimulatorTest, PorUnreliability) {
+        double result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/por.dft", 1, 10000);
+        EXPECT_NEAR(result, 0.2753355179, 0.01);
+    }
+
+    TEST(DftSimulatorTest, FdepUnreliability) {
+        double result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/fdep.dft", 1, 10000);
+        EXPECT_NEAR(result, 0.7768698399, 0.01);
+        result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/fdep2.dft", 1, 10000);
+        EXPECT_NEAR(result, 0.3934693403, 0.01);
+        result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/fdep3.dft", 1, 10000);
+        EXPECT_NEAR(result, 0.329679954, 0.01);
+        result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/fdep4.dft", 1, 10000);
+        EXPECT_NEAR(result, 0.601280086, 0.01);
+        result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/fdep5.dft", 1, 10000);
+        EXPECT_NEAR(result, 0.1548181217, 0.01);
+        result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/fdep6.dft", 1, 10000);
+        EXPECT_NEAR(result, 0.9985116987, 0.01);
+    }
+
+    TEST(DftSimulatorTest, PdepUnreliability) {
+        double result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/pdep.dft", 1, 10000);
+        EXPECT_NEAR(result, 0.2017690905, 0.01);
+        result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/pdep2.dft", 1, 10000);
+        EXPECT_NEAR(result, 0.2401091405, 0.01);
+        result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/pdep3.dft", 1, 10000);
+        EXPECT_NEAR(result, 0.2259856274, 0.01);
+        // Example pdep4 contains non-determinism which is not handled in simulation
+        //result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/pdep4.dft", 1, 10000);
+        //EXPECT_NEAR(result, 0.008122157897, 0.01);
+    }
+
+    TEST(DftSimulatorTest, SpareUnreliability) {
+        double result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/spare.dft", 1, 10000);
+        EXPECT_NEAR(result, 0.1118530638, 0.01);
+        result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/spare2.dft", 1, 10000);
+        EXPECT_NEAR(result, 0.2905027469, 0.01);
+        result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/spare3.dft", 1, 10000);
+        EXPECT_NEAR(result, 0.4660673246, 0.01);
+        result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/spare4.dft", 1, 10000);
+        EXPECT_NEAR(result, 0.01273070783, 0.01);
+        result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/spare5.dft", 1, 10000);
+        EXPECT_NEAR(result, 0.2017690905, 0.01);
+        result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/spare6.dft", 1, 10000);
+        EXPECT_NEAR(result, 0.4693712702, 0.01);
+        result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/spare7.dft", 1, 10000);
+        EXPECT_NEAR(result, 0.06108774525, 0.01);
+        result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/spare8.dft", 1, 10000);
+        EXPECT_NEAR(result, 0.02686144489, 0.01);
+    }
+
+    TEST(DftSimulatorTest, SeqUnreliability) {
+        size_t count;
+        size_t invalid;
+        std::tie(count, invalid) = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/seq.dft", 1, 10000);
+        EXPECT_EQ(invalid, 0ul);
+        double result = (double) count / 10000;
+        EXPECT_NEAR(result, 0.09020401043, 0.01);
+        std::tie(count, invalid) = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/seq2.dft", 1, 10000);
+        EXPECT_EQ(invalid, 0ul);
+        result = (double) count / 10000;
+        EXPECT_NEAR(result, 0.01438767797, 0.01);
+        std::tie(count, invalid) = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/seq3.dft", 1, 10000);
+        EXPECT_EQ(invalid, 0ul);
+        result = (double) count / 10000;
+        EXPECT_NEAR(result, 0.01438767797, 0.01);
+        std::tie(count, invalid) = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/seq4.dft", 1, 10000);
+        EXPECT_EQ(invalid, 0ul);
+        result = (double) count / 10000;
+        EXPECT_NEAR(result, 0.01438767797, 0.01);
+        std::tie(count, invalid) = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/seq5.dft", 1, 10000);
+        EXPECT_EQ(invalid, 0ul);
+        result = (double) count / 10000;
+        EXPECT_FLOAT_EQ(result, 0);
+        std::tie(count, invalid) = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/seq6.dft", 1, 10000);
+        EXPECT_EQ(invalid, 0ul);
+        result = (double) count / 10000;
+        EXPECT_NEAR(result, 2.499875004e-09, 0.01);
+    }
+
+    TEST(DftSimulatorTest, MutexUnreliability) {
+        size_t count;
+        size_t invalid;
+        // Invalid states are currently not supported
+        EXPECT_THROW(simulateDft(STORM_TEST_RESOURCES_DIR "/dft/mutex.dft", 1, 10000), storm::exceptions::NotSupportedException);
+        //EXPECT_GE(invalid, 0);
+        //double result = (double) count / (10000 - invalid);
+        //EXPECT_NEAR(result, 0.8646647168, 0.01);
+        EXPECT_THROW(simulateDft(STORM_TEST_RESOURCES_DIR "/dft/mutex2.dft", 1, 10000), storm::exceptions::NotSupportedException);
+        //EXPECT_EQ(invalid, 10000);
+        //EXPECT_EQ(count, 0);
+        std::tie(count, invalid) = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/mutex3.dft", 1, 10000);
+        EXPECT_EQ(invalid, 0ul);
+        EXPECT_EQ(count, 0ul);
+    }
+
+    TEST(DftSimulatorTest, SymmetryUnreliability) {
+        double result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/symmetry6.dft", 1, 10000);
+        EXPECT_NEAR(result, 0.3421934224, 0.01);
+    }
+
+    TEST(DftSimulatorTest, HecsUnreliability) {
+        double result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/hecs_2_2.dft", 1, 10000);
+        EXPECT_NEAR(result, 0.00021997582, 0.001);
+    }
+
 }
--- a/src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp
+++ b/src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp
@ -78,8 +78,8 @@ namespace {
            if (!config.useDC) {
                relevantNames.push_back("all");
            }
-            storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents<double>(*dft, {}, relevantNames, false);
-            dft->setRelevantEvents(relevantEvents);
+            storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents<double>(*dft, {}, relevantNames);
+            dft->setRelevantEvents(relevantEvents, false);

            // Find symmetries
            std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;
@ -173,8 +173,11 @@ namespace {
        auto state = simulator.getCurrentState();
        EXPECT_FALSE(state->hasFailed(dft->getTopLevelIndex()));
   
+        storm::dft::simulator::SimulationResult res;
+        double timebound;
        // First random step
-        double timebound = simulator.randomStep();
+        std::tie(res, timebound) = simulator.randomStep();
+        EXPECT_EQ(res, storm::dft::simulator::SimulationResult::SUCCESSFUL);
 #if BOOST_VERSION > 106400
        // Older Boost versions yield different value
        EXPECT_FLOAT_EQ(timebound, 0.522079);
@ -182,7 +185,8 @@ namespace {
        state = simulator.getCurrentState();
        EXPECT_FALSE(state->hasFailed(dft->getTopLevelIndex()));

-        timebound = simulator.randomStep();
+        std::tie(res, timebound) = simulator.randomStep();
+        EXPECT_EQ(res, storm::dft::simulator::SimulationResult::SUCCESSFUL);
 #if BOOST_VERSION > 106400
        // Older Boost versions yield different value
        EXPECT_FLOAT_EQ(timebound, 0.9497214);