diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index 1b777fb54..9332044f2 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -77,7 +77,6 @@ namespace storm { while (!stateQueue.empty()) { // Initialization outgoingTransitions.clear(); - ValueType sum = storm::utility::zero(); // Consider next state DFTStatePointer state = stateQueue.front(); @@ -147,7 +146,9 @@ namespace storm { bool isUsed = true; if (mDft.hasRepresentant(nextBE->id())) { DFTElementPointer representant = mDft.getRepresentant(nextBE->id()); - isUsed = newState->isUsed(representant->id()); + // Used 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()); } STORM_LOG_TRACE("BE " << nextBE->name() << " is " << (isUsed ? "used" : "not used")); ValueType rate = isUsed ? nextBE->activeFailureRate() : nextBE->passiveFailureRate(); @@ -155,20 +156,18 @@ namespace storm { if (resultFind != outgoingTransitions.end()) { // Add to existing transition resultFind->second += rate; + STORM_LOG_TRACE("Updated transition from " << state->getId() << " to " << resultFind->first << " with " << rate << " to " << resultFind->second); } else { // Insert new transition outgoingTransitions.insert(std::make_pair(newState->getId(), rate)); + STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << newState->getId() << " with " << rate); } - sum += rate; } // end while failing BE // Add all transitions for (auto it = outgoingTransitions.begin(); it != outgoingTransitions.end(); ++it) { - // TODO Matthias: correct? - ValueType rate = it->second;// / sum; - transitionMatrixBuilder.addNextValue(state->getId(), it->first, rate); - STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << it->first << " with " << rate); + transitionMatrixBuilder.addNextValue(state->getId(), it->first, it->second); } } // end while queue diff --git a/src/storage/dft/DFTBuilder.cpp b/src/storage/dft/DFTBuilder.cpp index 870b7f8bf..fd068bf7c 100644 --- a/src/storage/dft/DFTBuilder.cpp +++ b/src/storage/dft/DFTBuilder.cpp @@ -16,15 +16,14 @@ namespace storm { template DFT DFTBuilder::build() { for(auto& elem : mChildNames) { + DFTGatePointer gate = std::static_pointer_cast>(elem.first); for(auto const& child : elem.second) { - DFTGatePointer gate = std::static_pointer_cast>(elem.first); gate->pushBackChild(mElements[child]); mElements[child]->addParent(gate); } } // Sort elements topologically - // compute rank for (auto& elem : mElements) { computeRank(elem.second); diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index daa1d3d54..7f92ebb19 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -657,13 +657,7 @@ namespace storm { if(state.isOperational(this->mId)) { size_t uses = state.extractUses(mUseIndex); if(!state.isOperational(uses)) { - // TODO compute children ids before. - std::vector childrenIds; - for(auto const& child : this->mChildren) { - childrenIds.push_back(child->id()); - } - - bool claimingSuccessful = state.claimNew(this->mId, mUseIndex, uses, childrenIds); + bool claimingSuccessful = state.claimNew(this->mId, mUseIndex, uses, this->mChildren); if(!claimingSuccessful) { this->fail(state, queues); } diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index ebf3c770b..d760129e0 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -134,15 +134,19 @@ namespace storm { } template - bool DFTState::claimNew(size_t spareId, size_t usageIndex, size_t currentlyUses, std::vector const& childIds) { - auto it = find(childIds.begin(), childIds.end(), currentlyUses); - assert(it != childIds.end()); + bool DFTState::claimNew(size_t spareId, size_t usageIndex, size_t currentlyUses, std::vector>> const& children) { + auto it = children.begin(); + while ((*it)->id() != currentlyUses) { + assert(it != children.end()); + ++it; + } ++it; - while(it != childIds.end()) { - if(!hasFailed(*it) && !isUsed(*it)) { - setUsesAtPosition(usageIndex, *it); + while(it != children.end()) { + size_t childId = (*it)->id(); + if(!hasFailed(childId) && !isUsed(childId)) { + setUsesAtPosition(usageIndex, childId); if(isActiveSpare(spareId)) { - mDft.propagateActivation(*this,*it); + mDft.propagateActivation(*this, childId); } return true; } diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h index 4ea11a991..7cb5eaf4a 100644 --- a/src/storage/dft/DFTState.h +++ b/src/storage/dft/DFTState.h @@ -13,6 +13,8 @@ namespace storm { class DFT; template class DFTBE; + template + class DFTElement; template class DFTState { @@ -97,7 +99,7 @@ namespace storm { */ void setUsesAtPosition(size_t usageIndex, size_t child); - bool claimNew(size_t spareId, size_t usageIndex, size_t currentlyUses, std::vector const& childIds); + bool claimNew(size_t spareId, size_t usageIndex, size_t currentlyUses, std::vector>> const& children); bool hasOutgoingEdges() const { return !mIsCurrentlyFailableBE.empty();