From 7bcbbe75faf5ea592b3253cad345517b1b3b8bc8 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Sun, 21 Feb 2016 15:53:14 +0100
Subject: [PATCH] Set dont care for children if parent gate fails

Former-commit-id: c70852b7e85804cea30d6a27090baaa8457e4cb8
---
 src/storage/dft/DFTElements.cpp | 26 ++++++++++++++++----------
 src/storage/dft/DFTElements.h   |  2 ++
 2 files changed, 18 insertions(+), 10 deletions(-)

diff --git a/src/storage/dft/DFTElements.cpp b/src/storage/dft/DFTElements.cpp
index 26f5f9cbe..e06b3fe7d 100644
--- a/src/storage/dft/DFTElements.cpp
+++ b/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>
diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h
index 11fc31948..d5620717f 100644
--- a/src/storage/dft/DFTElements.h
+++ b/src/storage/dft/DFTElements.h
@@ -350,6 +350,7 @@ namespace storm {
                     }
                 }
                 state.setFailed(this->mId);
+                this->childrenDontCare(state, queues);
             }
 
             void failsafe(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
@@ -359,6 +360,7 @@ namespace storm {
                     }
                 }
                 state.setFailsafe(this->mId);
+                this->childrenDontCare(state, queues);
             }
 
             void childrenDontCare(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {