Browse Source

Propagate dont care to currently not failable BEs

Former-commit-id: 1fcb15f4ec
tempestpy_adaptions
Mavo 8 years ago
parent
commit
20b00e8f1d
  1. 7
      src/storage/dft/DFTState.cpp

7
src/storage/dft/DFTState.cpp

@ -202,6 +202,11 @@ namespace storm {
auto it = std::find(mCurrentlyFailableBE.begin(), mCurrentlyFailableBE.end(), id);
if (it != mCurrentlyFailableBE.end()) {
mCurrentlyFailableBE.erase(it);
} else {
it = std::find(mCurrentlyNotFailableBE.begin(), mCurrentlyNotFailableBE.end(), id);
if (it != mCurrentlyNotFailableBE.end()) {
mCurrentlyNotFailableBE.erase(it);
}
}
}
@ -253,7 +258,7 @@ namespace storm {
ValueType DFTState<ValueType>::getNotFailableBERate(size_t index) const {
STORM_LOG_ASSERT(index < nrNotFailableBEs(), "Index invalid.");
STORM_LOG_ASSERT(storm::utility::isZero<ValueType>(mDft.getBasicElement(mCurrentlyNotFailableBE[index])->activeFailureRate()) ||
(mDft.hasRepresentant(mCurrentlyNotFailableBE[index]) && !isActive(mDft.getRepresentant(mCurrentlyNotFailableBE[index]))), "BE " << mCurrentlyNotFailableBE[index] << " can fail");
(mDft.hasRepresentant(mCurrentlyNotFailableBE[index]) && !isActive(mDft.getRepresentant(mCurrentlyNotFailableBE[index]))), "BE " << mCurrentlyNotFailableBE[index] << " can fail in state: " << mDft.getStateString(mStatus, mStateGenerationInfo, mId));
// Use active failure rate as passive failure rate is 0.
return getBERate(mCurrentlyNotFailableBE[index], false);
}

Loading…
Cancel
Save