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

Merge branch 'monolithic-dft' of https://sselab.de/lab9/private/git/storm into monolithic-dft 

Former-commit-id: 939c3b5ac5
main
sjunges 10 years ago
parent
615882c6b3 371ba87f1c
commit
16c8945eb5
6 changed files with 79 additions and 64 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. 7
      examples/dft/spare8.dft
  2. 15
      src/builder/ExplicitDFTModelBuilder.cpp
  3. 40
      src/storage/dft/DFT.cpp
  4. 32
      src/storage/dft/DFTElements.h
  5. 40
      src/storage/dft/DFTState.cpp
  6. 9
      src/storage/dft/DFTState.h

7
examples/dft/spare8.dft
View File

@ -0,0 +1,7 @@
toplevel "A";
"A" wsp "I" "B";
"B" wsp "J" "K";
"I" lambda=0.5 dorm=0.3;
"J" lambda=0.5 dorm=0.3;
"K" lambda=0.5 dorm=0.3;

15
src/builder/ExplicitDFTModelBuilder.cpp
View File

@ -256,7 +256,7 @@ namespace storm {
if (mStates.contains(unsuccessfulState->status())) {
// Unsuccessful state already exists
unsuccessfulStateId = mStates.getValue(unsuccessfulState->status());
STORM_LOG_TRACE("State " << mDft.getStateString(unsuccessfulState) << " already exists");
STORM_LOG_TRACE("State " << mDft.getStateString(unsuccessfulState) << " with id " << unsuccessfulStateId << " already exists");
} else {
// New unsuccessful state
unsuccessfulState->setId(newIndex++);
@ -277,16 +277,15 @@ namespace storm {
++rowOffset;
} else {
// Set failure rate according to usage
bool isUsed = true;
// Set failure rate according to activation
bool isActive = true;
if (mDft.hasRepresentant(nextBE->id())) {
DFTElementCPointer representant = mDft.getRepresentant(nextBE->id());
// Used must be checked for the state we are coming from as this state is responsible for the
// Active must be checked for the state we are coming from as this state is responsible for the
// rate and not the new state we are going to
isUsed = state->isUsed(representant->id());
isActive = state->isActive(mDft.getRepresentant(nextBE->id())->id());
}
STORM_LOG_TRACE("BE " << nextBE->name() << " is " << (isUsed ? "used" : "not used"));
ValueType rate = isUsed ? nextBE->activeFailureRate() : nextBE->passiveFailureRate();
STORM_LOG_TRACE("BE " << nextBE->name() << " is " << (isActive ? "active" : "not active"));
ValueType rate = isActive ? nextBE->activeFailureRate() : nextBE->passiveFailureRate();
auto resultFind = outgoingTransitions.find(newStateId);
if (resultFind != outgoingTransitions.end()) {
// Add to existing transition

40
src/storage/dft/DFT.cpp
View File

@ -80,23 +80,17 @@ namespace storm {
std::queue<size_t> visitQueue;
std::set<size_t> visited;
visitQueue.push(subTreeRoots[0]);
bool consideredDependencies = false;
while (true) {
if (consideredDependencies) {
break;
}
stateIndex = performStateGenerationInfoDFS(generationInfo, visitQueue, visited, stateIndex);
// Consider dependencies
for (size_t idDependency : getDependencies()) {
std::shared_ptr<DFTDependency<ValueType> const> dependency = getDependency(idDependency);
visitQueue.push(dependency->id());
visitQueue.push(dependency->triggerEvent()->id());
visitQueue.push(dependency->dependentEvent()->id());
}
consideredDependencies = true;
stateIndex = performStateGenerationInfoDFS(generationInfo, visitQueue, visited, stateIndex);
// Consider dependencies
for (size_t idDependency : getDependencies()) {
std::shared_ptr<DFTDependency<ValueType> const> dependency = getDependency(idDependency);
visitQueue.push(dependency->id());
visitQueue.push(dependency->triggerEvent()->id());
visitQueue.push(dependency->dependentEvent()->id());
}
stateIndex = performStateGenerationInfoDFS(generationInfo, visitQueue, visited, stateIndex);
assert(stateIndex = mStateVectorSize);
STORM_LOG_TRACE(generationInfo);
@ -197,10 +191,11 @@ namespace storm {
} else {
stream << "\t** " << storm::storage::toChar(state->getElementState(elem->id()));
if(elem->isSpareGate()) {
if(state->isActiveSpare(elem->id())) {
stream << " actively";
size_t useId = state->uses(elem->id());
if(state->isActive(useId)) {
stream << " actively ";
}
stream << " using " << state->uses(elem->id());
stream << " using " << useId;
}
}
stream << std::endl;
@ -220,10 +215,11 @@ namespace storm {
stream << storm::storage::toChar(state->getElementState(elem->id()));
if(elem->isSpareGate()) {
stream << "[";
if(state->isActiveSpare(elem->id())) {
stream << "actively ";
size_t useId = state->uses(elem->id());
if(state->isActive(useId)) {
stream << " actively ";
}
stream << "using " << state->uses(elem->id()) << "]";
stream << "using " << useId << "]";
}
}
}

32
src/storage/dft/DFTElements.h
View File

@ -279,11 +279,13 @@ namespace storm {
virtual void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const = 0;
virtual void extendSpareModule(std::set<size_t>& elementsInSpareModule) const override {
DFTElement<ValueType>::extendSpareModule(elementsInSpareModule);
for(auto const& child : mChildren) {
if(elementsInSpareModule.count(child->id()) == 0) {
elementsInSpareModule.insert(child->id());
child->extendSpareModule(elementsInSpareModule);
if (!this->isSpareGate()) {
DFTElement<ValueType>::extendSpareModule(elementsInSpareModule);
for( auto const& child : mChildren) {
if(elementsInSpareModule.count(child->id()) == 0) {
elementsInSpareModule.insert(child->id());
child->extendSpareModule(elementsInSpareModule);
}
}
}
}
@ -370,6 +372,9 @@ namespace storm {
}
}
state.setFailed(this->mId);
if (this->isSpareGate()) {
this->finalizeSpare(state);
}
this->childrenDontCare(state, queues);
}
@ -380,6 +385,9 @@ namespace storm {
}
}
state.setFailsafe(this->mId);
if (this->isSpareGate()) {
this->finalizeSpare(state);
}
this->childrenDontCare(state, queues);
}
@ -387,6 +395,20 @@ namespace storm {
queues.propagateDontCare(mChildren);
}
/**
* Finish failed/failsafe spare gate by activating the children and setting the useIndex to zero.
* This prevents multiple fail states with different usages or activations.
* @param state The current state.
*/
void finalizeSpare(DFTState<ValueType>& state) const {
state.setUses(this->mId, 0);
for (auto child : this->children()) {
if (!state.isActive(child->id())) {
state.activate(child->id());
}
}
}
bool hasFailsafeChild(DFTState<ValueType>& state) const {
for(auto const& child : mChildren) {
if(state.isFailsafe(child->id()))

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

@ -7,7 +7,6 @@ namespace storm {
template<typename ValueType>
DFTState<ValueType>::DFTState(DFT<ValueType> const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(dft.stateVectorSize()), mId(id), mDft(dft), mStateGenerationInfo(stateGenerationInfo) {
mInactiveSpares = dft.getSpareIndices();
// Initialize uses
for(size_t id : mDft.getSpareIndices()) {
@ -18,12 +17,7 @@ namespace storm {
}
// Initialize activation
this->activate(mDft.getTopLevelIndex());
for(auto const& id : mDft.module(mDft.getTopLevelIndex())) {
if(mDft.getElement(id)->isSpareGate()) {
propagateActivation(uses(id));
}
}
propagateActivation(mDft.getTopLevelIndex());
std::vector<size_t> alwaysActiveBEs = dft.nonColdBEs();
mIsCurrentlyFailableBE.insert(mIsCurrentlyFailableBE.end(), alwaysActiveBEs.begin(), alwaysActiveBEs.end());
@ -182,29 +176,25 @@ namespace storm {
template<typename ValueType>
void DFTState<ValueType>::activate(size_t repr) {
for(size_t elem : mDft.module(repr)) {
if(mDft.getElement(elem)->isColdBasicElement() && isOperational(elem)) {
mIsCurrentlyFailableBE.push_back(elem);
}
else if(mDft.getElement(elem)->isSpareGate()) {
assert(std::find(mInactiveSpares.begin(), mInactiveSpares.end(), elem) != mInactiveSpares.end());
mInactiveSpares.erase(std::find(mInactiveSpares.begin(), mInactiveSpares.end(), elem));
}
}
size_t activationIndex = mStateGenerationInfo.getSpareActivationIndex(repr);
assert(!mStatus[activationIndex]);
mStatus.set(activationIndex);
propagateActivation(repr);
}
template<typename ValueType>
bool DFTState<ValueType>::isActiveSpare(size_t id) const {
assert(mDft.getElement(id)->isSpareGate());
return (std::find(mInactiveSpares.begin(), mInactiveSpares.end(), id) == mInactiveSpares.end());
bool DFTState<ValueType>::isActive(size_t id) const {
assert(mDft.isRepresentative(id));
return mStatus[mStateGenerationInfo.getSpareActivationIndex(id)];
}
template<typename ValueType>
void DFTState<ValueType>::propagateActivation(size_t representativeId) {
activate(representativeId);
for(size_t id : mDft.module(representativeId)) {
if(mDft.getElement(id)->isSpareGate()) {
propagateActivation(uses(id));
for(size_t elem : mDft.module(representativeId)) {
if(mDft.getElement(elem)->isColdBasicElement() && isOperational(elem)) {
mIsCurrentlyFailableBE.push_back(elem);
} else if (mDft.getElement(elem)->isSpareGate() && !isActive(uses(elem))) {
activate(uses(elem));
}
}
}
@ -243,8 +233,8 @@ namespace storm {
size_t childId = (*it)->id();
if(!hasFailed(childId) && !isUsed(childId)) {
setUses(spareId, childId);
if(isActiveSpare(spareId)) {
propagateActivation(childId);
if(isActive(currentlyUses)) {
activate(childId);
}
return true;
}

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

@ -26,7 +26,6 @@ namespace storm {
// Status is bitvector where each element has two bits with the meaning according to DFTElementState
storm::storage::BitVector mStatus;
size_t mId;
std::vector<size_t> mInactiveSpares;
std::vector<size_t> mIsCurrentlyFailableBE;
std::vector<size_t> mFailableDependencies;
std::vector<size_t> mUsedRepresentants;
@ -79,9 +78,7 @@ namespace storm {
void activate(size_t repr);
bool isActiveSpare(size_t id) const;
void propagateActivation(size_t representativeId);
bool isActive(size_t id) const;
void markAsInvalid() {
mValid = false;
@ -200,6 +197,10 @@ namespace storm {
friend bool operator==(DFTState const& a, DFTState const& b) {
return a.mStatus == b.mStatus;
}
private:
void propagateActivation(size_t representativeId);
};
}

Write Preview
Loading…
Cancel
Save