From 19a1c99fd3b41bfdbe50854d58a095d4b54df6c9 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Thu, 7 Apr 2016 17:47:38 +0200
Subject: [PATCH] Sort failable BEs according to active failure rate

Former-commit-id: c4622e9dc80ccb921899a016199fc5a705a5a664
---
 src/storage/dft/DFTState.cpp | 15 ++++++++++++++-
 src/storage/dft/DFTState.h   |  5 +++++
 2 files changed, 19 insertions(+), 1 deletion(-)

diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp
index b1c9a4fc1..25edf1d38 100644
--- a/src/storage/dft/DFTState.cpp
+++ b/src/storage/dft/DFTState.cpp
@@ -21,6 +21,7 @@ namespace storm {
 
             std::vector<size_t> alwaysActiveBEs = dft.nonColdBEs();
             mIsCurrentlyFailableBE.insert(mIsCurrentlyFailableBE.end(), alwaysActiveBEs.begin(), alwaysActiveBEs.end());
+            sortFailableBEs();
         }
         
         template<typename ValueType>
@@ -41,6 +42,7 @@ namespace storm {
                     STORM_LOG_TRACE("Spare " << index << " uses " << useId);
                 }
             }
+            sortFailableBEs();
             
             // Initialize failable dependencies
             for (size_t dependencyId : mDft.getDependencies()) {
@@ -208,7 +210,7 @@ namespace storm {
             if (nrFailableDependencies() > 0) {
                 // Consider failure due to dependency
                 assert(index < nrFailableDependencies());
-                std::shared_ptr<DFTDependency<ValueType> const> dependency = mDft.getDependency(getDependencyId(index));
+                std::shared_ptr<DFTDependency<ValueType> const> dependency = mDft.getDependency(mFailableDependencies[index]);
                 std::pair<std::shared_ptr<DFTBE<ValueType> const>,bool> res(mDft.getBasicElement(dependency->dependentEvent()->id()), true);
                 mFailableDependencies.erase(mFailableDependencies.begin() + index);
                 setFailed(res.first->id());
@@ -260,6 +262,7 @@ namespace storm {
                     propagateActivation(uses(elem));
                 }
             }
+            sortFailableBEs();
         }
 
         template<typename ValueType>
@@ -354,6 +357,16 @@ namespace storm {
             }
             return changed;
         }
+        
+        template<typename ValueType>
+        void DFTState<ValueType>::sortFailableBEs() {
+            std::sort( mIsCurrentlyFailableBE.begin( ), mIsCurrentlyFailableBE.end( ), [&](size_t const& lhs, size_t const& rhs) {
+                ValueType leftRate = mDft.getBasicElement(lhs)->activeFailureRate();
+                ValueType rightRate = mDft.getBasicElement(rhs)->activeFailureRate();
+                // Sort decreasing
+                return rightRate < leftRate;
+            });
+        }
 
 
         // Explicitly instantiate the class.
diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h
index 5b68d46ae..f647aae17 100644
--- a/src/storage/dft/DFTState.h
+++ b/src/storage/dft/DFTState.h
@@ -235,6 +235,11 @@ namespace storm {
             
         private:
             void propagateActivation(size_t representativeId);
+            
+            /*!
+             * Sort failable BEs in decreasing order of their active failure rate.
+             */
+            void sortFailableBEs();
 
         };