diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index c17bad0b6..558192678 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -123,16 +123,28 @@ namespace storm { template void DFTState::setFailed(size_t id) { + if (mDft.isRepresentative(id)) { + // Activate failed element + activate(id); + } mStatus.set(mStateGenerationInfo.getStateIndex(id)); } template void DFTState::setFailsafe(size_t id) { + if (mDft.isRepresentative(id)) { + // Activate failed element + activate(id); + } mStatus.set(mStateGenerationInfo.getStateIndex(id)+1); } template void DFTState::setDontCare(size_t id) { + if (mDft.isRepresentative(id)) { + // Activate failed element + activate(id); + } mStatus.setFromInt(mStateGenerationInfo.getStateIndex(id), 2, static_cast(DFTElementState::DontCare) ); } @@ -207,7 +219,6 @@ namespace storm { template void DFTState::activate(size_t repr) { size_t activationIndex = mStateGenerationInfo.getSpareActivationIndex(repr); - assert(!mStatus[activationIndex]); mStatus.set(activationIndex); } diff --git a/src/storage/dft/elements/DFTElement.cpp b/src/storage/dft/elements/DFTElement.cpp index 803199508..1f0ab892d 100644 --- a/src/storage/dft/elements/DFTElement.cpp +++ b/src/storage/dft/elements/DFTElement.cpp @@ -37,7 +37,7 @@ namespace storm { } state.setDontCare(mId); - if (hasParentSpare && !state.isActive(mId)) { + if (hasParentSpare) { // Activate child for consistency in failed spares state.activate(mId); }