diff --git a/examples/dft/spare8.dft b/examples/dft/spare8.dft
new file mode 100644
index 000000000..c67eaf022
--- /dev/null
+++ b/examples/dft/spare8.dft
@@ -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;
+
diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp
index cbb9b69d0..4900845a5 100644
--- a/src/builder/ExplicitDFTModelBuilder.cpp
+++ b/src/builder/ExplicitDFTModelBuilder.cpp
@@ -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
diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp
index 519036fff..3fbcd5ee1 100644
--- a/src/storage/dft/DFT.cpp
+++ b/src/storage/dft/DFT.cpp
@@ -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 << "]";
}
}
}
diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h
index 36efe9c2f..db1f0f6cf 100644
--- a/src/storage/dft/DFTElements.h
+++ b/src/storage/dft/DFTElements.h
@@ -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()))
diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp
index 0bad03f78..7f34e03ef 100644
--- a/src/storage/dft/DFTState.cpp
+++ b/src/storage/dft/DFTState.cpp
@@ -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;
}
diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h
index 821aa2fcb..7a26e10ab 100644
--- a/src/storage/dft/DFTState.h
+++ b/src/storage/dft/DFTState.h
@@ -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);
+
};
}