diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index 1d04e5210..93a7b282e 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -549,11 +549,24 @@ namespace storm { } } + STORM_LOG_ASSERT(rates.size() > 0, "No rates failable"); + + // Sort rates + std::sort(rates.begin(), rates.end()); + std::vector rateCount(rates.size(), 0); + size_t lastIndex = 0; + for (size_t i = 0; i < rates.size(); ++i) { + if (rates[lastIndex] != rates[i]) { + lastIndex = i; + } + ++rateCount[lastIndex]; + } + for (size_t i = 0; i < rates.size(); ++i) { // Cold BEs cannot fail in the first step - if (!coldBEs.get(i)) { + if (!coldBEs.get(i) && rateCount[i] > 0) { // Compute AND MTTF of subtree without current rate and scale with current rate - upperBound += rates.back() * computeMTTFAnd(rates, rates.size() - 1); + upperBound += rates.back() * rateCount[i] * computeMTTFAnd(rates, rates.size() - 1); // Swap here to avoid swapping back std::iter_swap(rates.begin() + i, rates.end() - 1); } @@ -567,7 +580,7 @@ namespace storm { } template - ValueType ExplicitDFTModelBuilderApprox::computeMTTFAnd(std::vector rates, size_t size) const { + ValueType ExplicitDFTModelBuilderApprox::computeMTTFAnd(std::vector const& rates, size_t size) const { ValueType result = storm::utility::zero(); if (size == 0) { return result; diff --git a/src/builder/ExplicitDFTModelBuilderApprox.h b/src/builder/ExplicitDFTModelBuilderApprox.h index 8cc53a176..933cd3277 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.h +++ b/src/builder/ExplicitDFTModelBuilderApprox.h @@ -246,7 +246,7 @@ namespace storm { * @param size Only indices < size are considered in the vector. * @return MTTF. */ - ValueType computeMTTFAnd(std::vector rates, size_t size) const; + ValueType computeMTTFAnd(std::vector const& rates, size_t size) const; /*! * Compares the priority of two states.