From d95bb71f75a4febcd93abf7b075261671fe070a5 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Sat, 29 Oct 2016 00:02:20 +0200
Subject: [PATCH] Tried to gain more performance

Former-commit-id: 9af2ab7ce0cc6fc311bd5f45c8b2ea79f29c989c
---
 src/builder/ExplicitDFTModelBuilderApprox.cpp | 19 ++++++++++++++++---
 src/builder/ExplicitDFTModelBuilderApprox.h   |  2 +-
 2 files changed, 17 insertions(+), 4 deletions(-)

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<size_t> 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<typename ValueType, typename StateType>
-        ValueType ExplicitDFTModelBuilderApprox<ValueType, StateType>::computeMTTFAnd(std::vector<ValueType> rates, size_t size) const {
+        ValueType ExplicitDFTModelBuilderApprox<ValueType, StateType>::computeMTTFAnd(std::vector<ValueType> const& rates, size_t size) const {
             ValueType result = storm::utility::zero<ValueType>();
             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<ValueType> rates, size_t size) const;
+            ValueType computeMTTFAnd(std::vector<ValueType> const& rates, size_t size) const;
 
             /*!
              * Compares the priority of two states.