Merge branch 'monolithic-dft' of https://sselab.de/lab9/private/git/storm into monolithic-dft

Former-commit-id: 8c00fd8bac

src/storage/dft/DFTElements.cpp

@@ -7,18 +7,24 @@ namespace storm {
 
         template<typename ValueType>
         bool DFTElement<ValueType>::checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
-            if(!state.dontCare(mId) && !hasOutgoingDependencies())
-            {
-                for(DFTGatePointer const& parent : mParents) {
-                    if(state.isOperational(parent->id())) {
-                        return false;
-                    }
+            if (state.dontCare(mId)) {
+                return false;
+            }
+            // Check that no outgoing dependencies can be triggered anymore
+            for (DFTDependencyPointer dependency : mOutgoingDependencies) {
+                if (state.isOperational(dependency->dependentEvent()->id()) && state.isOperational(dependency->triggerEvent()->id())) {
+                    return false;
                 }
-                state.setDontCare(mId);
-                return true;
-
             }
-            return false;
+            // Check that no parent can fail anymore
+            for(DFTGatePointer const& parent : mParents) {
+                if(state.isOperational(parent->id())) {
+                    return false;
+                }
+            }
+
+            state.setDontCare(mId);
+            return true;
         }
 
         template<typename ValueType>

src/storage/dft/DFTElements.h

@@ -370,6 +370,7 @@ namespace storm {
                     }
                 }
                 state.setFailed(this->mId);
+                this->childrenDontCare(state, queues);
             }
 
             void failsafe(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
@@ -379,6 +380,7 @@ namespace storm {
                     }
                 }
                 state.setFailsafe(this->mId);
+                this->childrenDontCare(state, queues);
             }
 
             void childrenDontCare(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {