diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index cd2704dc6..723d75920 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -187,7 +187,9 @@ namespace storm { // Set transitions if (hasDependencies) { // Failure is due to dependency -> add non-deterministic choice - transitionMatrixBuilder.addNextValue(state->getId() + rowOffset++, newState->getId(), storm::utility::one()); + std::shared_ptr const> dependency = mDft.getDependency(state->getDependencyId(smallest-1)); + transitionMatrixBuilder.addNextValue(state->getId() + rowOffset++, newState->getId(), dependency->probability()); + STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << newState->getId() << " with probability " << dependency->probability()); } else { // Set failure rate according to usage bool isUsed = true; @@ -203,11 +205,11 @@ 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); + STORM_LOG_TRACE("Updated transition from " << state->getId() << " to " << resultFind->first << " with rate " << rate << " to new rate " << 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); + STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << newState->getId() << " with rate " << rate); } exitRate += rate; } diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index 672ca14a7..8714f0130 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -99,8 +99,7 @@ namespace storm { STORM_LOG_TRACE("currently failable: " << getCurrentlyFailableString()); if (nrFailableDependencies() > 0) { // Consider failure due to dependency - assert(index < nrFailableDependencies()); - std::shared_ptr const> dependency = mDft.getDependency(mFailableDependencies[index]); + std::shared_ptr const> dependency = mDft.getDependency(getDependencyId(index)); std::pair const>,bool> res(mDft.getBasicElement(dependency->dependentEvent()->id()), true); mFailableDependencies.erase(mFailableDependencies.begin() + index); setFailed(res.first->id()); diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h index 17a9c2d3b..520587a42 100644 --- a/src/storage/dft/DFTState.h +++ b/src/storage/dft/DFTState.h @@ -6,6 +6,7 @@ #include #include +#include namespace storm { namespace storage { @@ -114,6 +115,16 @@ namespace storm { size_t nrFailableDependencies() const { return mFailableDependencies.size(); } + + /** + * Gets the id of the dependency at index in the list of failable dependencies. + * @param index Index in list of failable dependencies. + * @return Id of the dependency + */ + size_t getDependencyId(size_t index) const { + assert(index < nrFailableDependencies()); + return mFailableDependencies[index]; + } /** * Sets all failable BEs due to dependencies from newly failed element