sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Do not use cold BEs in first step of approximation formula 

Former-commit-id: d204be9633
tempestpy_adaptions
Mavo 8 years ago
parent
02c4195f31
commit
dae1a7eefe
3 changed files with 29 additions and 81 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 32
      src/builder/ExplicitDFTModelBuilderApprox.cpp
  2. 53
      src/storage/dft/DFTState.cpp
  3. 25
      src/storage/dft/DFTState.h

32
src/builder/ExplicitDFTModelBuilderApprox.cpp
View File

@ -522,9 +522,6 @@ namespace storm {
for (size_t index = 0; index < state->nrFailableBEs(); ++index) {
lowerBound += state->getFailableBERate(index);
}
for (size_t index = 0; index < state->nrNotFailableBEs(); ++index) {
lowerBound += state->getNotFailableBERate(index);
}
return lowerBound;
}
@ -538,20 +535,31 @@ namespace storm {
for (std::vector<size_t> const& subtree : subtreeBEs) {
// Get all possible rates
std::vector<ValueType> rates;
for (size_t id : subtree) {
storm::storage::BitVector coldBEs(subtree.size(), false);
for (size_t i = 0; i < subtree.size(); ++i) {
size_t id = subtree[i];
if (state->isOperational(id)) {
// Get BE rate
rates.push_back(state->getBERate(id, true));
rateSum += rates.back();
ValueType rate = state->getBERate(id);
if (storm::utility::isZero<ValueType>(rate)) {
// Get active failure rate for cold BE
rate = dft.getBasicElement(id)->activeFailureRate();
// Mark BE as cold
coldBEs.set(i, true);
}
rates.push_back(rate);
rateSum += rate;
}
}
// We move backwards and start with swapping the last element to itself
// Then we do not need to swap back
for (auto it = rates.rbegin(); it != rates.rend(); ++it) {
// Compute AND MTTF of subtree without current rate and scale with current rate
std::iter_swap(it, rates.end() - 1);
upperBound += rates.back() * computeMTTFAnd(rates, rates.size() - 1);
for (size_t i = 0; i < rates.size(); ++i) {
// Cold BEs cannot fail in the first step
if (!coldBEs.get(i)) {
// Compute AND MTTF of subtree without current rate and scale with current rate
upperBound += rates.back() * computeMTTFAnd(rates, rates.size() - 1);
// Swap here to avoid swapping back
std::iter_swap(rates.begin() + i, rates.end() - 1);
}
}
}

53
src/storage/dft/DFTState.cpp
View File

@ -17,23 +17,11 @@ namespace storm {
this->setUses(spareId, elem->children()[0]->id());
}
for (auto elem : mDft.getBasicElements()) {
if (!storm::utility::isZero(elem->activeFailureRate())) {
mCurrentlyNotFailableBE.push_back(elem->id());
}
}
// Initialize activation
propagateActivation(mDft.getTopLevelIndex());
std::vector<size_t> alwaysActiveBEs = mDft.nonColdBEs();
mCurrentlyFailableBE.insert(mCurrentlyFailableBE.end(), alwaysActiveBEs.begin(), alwaysActiveBEs.end());
// Remove always active BEs from currently not failable BEs
for (size_t id : alwaysActiveBEs) {
auto it = std::find(mCurrentlyNotFailableBE.begin(), mCurrentlyNotFailableBE.end(), id);
STORM_LOG_ASSERT(it != mCurrentlyNotFailableBE.end(), "Id not found.");
mCurrentlyNotFailableBE.erase(it);
}
}
template<typename ValueType>
@ -46,7 +34,6 @@ namespace storm {
STORM_LOG_TRACE("Construct concrete state from pseudo state " << mDft.getStateString(mStatus, mStateGenerationInfo, mId));
// Clear information from pseudo state
mCurrentlyFailableBE.clear();
mCurrentlyNotFailableBE.clear();
mFailableDependencies.clear();
mUsedRepresentants.clear();
STORM_LOG_ASSERT(mPseudoState, "Only pseudo states can be constructed.");
@ -57,10 +44,6 @@ namespace storm {
if ((!be->isColdBasicElement() && be->canFail()) || !mDft.hasRepresentant(index) || isActive(mDft.getRepresentant(index))) {
mCurrentlyFailableBE.push_back(index);
STORM_LOG_TRACE("Currently failable: " << mDft.getBasicElement(index)->toString());
} else {
// BE currently is not failable
mCurrentlyNotFailableBE.push_back(index);
STORM_LOG_TRACE("Currently not failable: " << mDft.getBasicElement(index)->toString());
}
} else if (mDft.getElement(index)->isSpareGate()) {
// Initialize used representants
@ -204,11 +187,6 @@ 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);
}
}
}
@ -241,35 +219,22 @@ namespace storm {
}
template<typename ValueType>
ValueType DFTState<ValueType>::getBERate(size_t id, bool avoidCold) const {
ValueType DFTState<ValueType>::getBERate(size_t id) const {
STORM_LOG_ASSERT(mDft.isBasicElement(id), "Element is no BE.");
if (mDft.hasRepresentant(id) && !isActive(mDft.getRepresentant(id))) {
if (avoidCold && mDft.getBasicElement(id)->isColdBasicElement()) {
// Return active failure rate instead of 0.
return mDft.getBasicElement(id)->activeFailureRate();
} else {
// Return passive failure rate
return mDft.getBasicElement(id)->passiveFailureRate();
}
// Return passive failure rate
return mDft.getBasicElement(id)->passiveFailureRate();
} else {
// Return active failure rate
return mDft.getBasicElement(id)->activeFailureRate();
}
// Return active failure rate
return mDft.getBasicElement(id)->activeFailureRate();
}
template<typename ValueType>
ValueType DFTState<ValueType>::getFailableBERate(size_t index) const {
STORM_LOG_ASSERT(index < nrFailableBEs(), "Index invalid.");
return getBERate(mCurrentlyFailableBE[index], false);
}
template<typename ValueType>
ValueType DFTState<ValueType>::getNotFailableBERate(size_t index) const {
STORM_LOG_ASSERT(index < nrNotFailableBEs(), "Index invalid.");
STORM_LOG_ASSERT(isPseudoState() || storm::utility::isZero<ValueType>(mDft.getBasicElement(mCurrentlyNotFailableBE[index])->activeFailureRate()) ||
(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], true);
return getBERate(mCurrentlyFailableBE[index]);
}
template<typename ValueType>
@ -326,10 +291,6 @@ namespace storm {
if (be->isColdBasicElement() && be->canFail()) {
// Add to failable BEs
mCurrentlyFailableBE.push_back(elem);
// Remove from not failable BEs
auto it = std::find(mCurrentlyNotFailableBE.begin(), mCurrentlyNotFailableBE.end(), elem);
STORM_LOG_ASSERT(it != mCurrentlyNotFailableBE.end(), "Element " << elem << " not found.");
mCurrentlyNotFailableBE.erase(it);
}
} else if (mDft.getElement(elem)->isSpareGate() && !isActive(uses(elem))) {
propagateActivation(uses(elem));

25
src/storage/dft/DFTState.h
View File

@ -27,7 +27,6 @@ namespace storm {
storm::storage::BitVector mStatus;
size_t mId;
std::vector<size_t> mCurrentlyFailableBE;
std::vector<size_t> mCurrentlyNotFailableBE;
std::vector<size_t> mFailableDependencies;
std::vector<size_t> mUsedRepresentants;
bool mPseudoState;
@ -181,15 +180,6 @@ namespace storm {
return mCurrentlyFailableBE.size();
}
/**
* Get number of currently not failable BEs. These are cold BE which can fail in the future.
*
* @return Number of not failable BEs.
*/
size_t nrNotFailableBEs() const {
return mCurrentlyNotFailableBE.size();
}
/**
* Get the failure rate of the currently failable BE on the given index.
*
@ -200,24 +190,13 @@ namespace storm {
ValueType getFailableBERate(size_t index) const;
/**
* Get the failure rate of the currently not failable BE on the given index.
*
* @param index Index of BE in list of currently not failable BEs.
*
* @return Failure rate of the BE.
*/
ValueType getNotFailableBERate(size_t index) const;
/**
* Get the failure rate of the given BE.
* Get the current failure rate of the given BE.
*
* @param id Id of BE.
* @param avoidCold Flag indicating if a cold passive failure rate should be avoided by giving
* the active failure rate instead.
*
* @return Failure rate of the BE.
*/
ValueType getBERate(size_t id, bool avoidCold) const;
ValueType getBERate(size_t id) const;
/** Get number of currently failable dependencies.
*

Write Preview
Loading…
Cancel
Save