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 bool DFTElement::checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& 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 diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index 66e8b3e8a..36efe9c2f 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -370,6 +370,7 @@ namespace storm { } } state.setFailed(this->mId); + this->childrenDontCare(state, queues); } void failsafe(DFTState& state, DFTStateSpaceGenerationQueues& queues) const { @@ -379,6 +380,7 @@ namespace storm { } } state.setFailsafe(this->mId); + this->childrenDontCare(state, queues); } void childrenDontCare(DFTState& state, DFTStateSpaceGenerationQueues& queues) const {