Browse Source

Fixed activation for failed nested SPAREs.

If a nested (passive) SPARE is already failed and it becomes activated (through claiming), it will not activate its children.
tempestpy_adaptions
Matthias Volk 4 years ago
parent
commit
868c9fb0fd
No known key found for this signature in database GPG Key ID: 83A57678F739FCD3
  1. 9
      src/storm-dft/storage/dft/DFTState.cpp

9
src/storm-dft/storage/dft/DFTState.cpp

@ -387,8 +387,13 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "BE type '" << be->type() << "' is not supported."); STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "BE type '" << be->type() << "' is not supported.");
} }
} }
} else if (mDft.getElement(elem)->isSpareGate() && !isActive(uses(elem))) {
propagateActivation(uses(elem));
} else if (mDft.getElement(elem)->isSpareGate()){
if (isOperational(elem)) {
// We do not activate children if the SPARE is already failed
if (!isActive(uses(elem))) {
propagateActivation(uses(elem));
}
}
} }
} }
} }

Loading…
Cancel
Save