diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index 70ff18122..0b2ff7ee8 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -32,8 +32,6 @@ namespace storm { STORM_LOG_ASSERT(it != mCurrentlyNotFailableBE.end(), "Id not found."); mCurrentlyNotFailableBE.erase(it); } - - sortFailableBEs(); } template @@ -69,8 +67,7 @@ namespace storm { STORM_LOG_TRACE("Spare " << index << " uses " << useId); } } - sortFailableBEs(); - + // Initialize failable dependencies for (size_t dependencyId : mDft.getDependencies()) { std::shared_ptr const> dependency = mDft.getDependency(dependencyId); @@ -324,7 +321,6 @@ namespace storm { propagateActivation(uses(elem)); } } - sortFailableBEs(); } template @@ -422,14 +418,6 @@ namespace storm { } return changed; } - - template - void DFTState::sortFailableBEs() { - std::sort(mCurrentlyFailableBE.begin( ), mCurrentlyFailableBE.end( ), [&](size_t const& lhs, size_t const& rhs) { - // Sort decreasing - return getBERate(rhs, true) < getBERate(lhs, true); - }); - } // Explicitly instantiate the class. diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h index 207eecac3..4ff36d1ab 100644 --- a/src/storage/dft/DFTState.h +++ b/src/storage/dft/DFTState.h @@ -313,11 +313,6 @@ namespace storm { */ ValueType getBERate(size_t id, bool considerPassive) const; - /*! - * Sort failable BEs in decreasing order of their active failure rate. - */ - void sortFailableBEs(); - }; }