From 37d0b66e730953dc3c7c358c3fd6c0048ce076df Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Tue, 19 Mar 2019 11:14:27 +0100
Subject: [PATCH] Some fixes for approximation

---
 src/storm-dft/builder/DftExplorationHeuristic.cpp | 3 ++-
 src/storm-dft/builder/DftExplorationHeuristic.h   | 2 +-
 src/storm-dft/builder/ExplicitDFTModelBuilder.cpp | 6 ++++--
 3 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/src/storm-dft/builder/DftExplorationHeuristic.cpp b/src/storm-dft/builder/DftExplorationHeuristic.cpp
index d46736268..43b3ad96b 100644
--- a/src/storm-dft/builder/DftExplorationHeuristic.cpp
+++ b/src/storm-dft/builder/DftExplorationHeuristic.cpp
@@ -18,7 +18,8 @@ namespace storm {
 
         template<>
         double DFTExplorationHeuristicBoundDifference<double>::getPriority() const {
-            double difference = (storm::utility::one<double>() / upperBound) - (storm::utility::one<double>() / lowerBound);
+            double difference = lowerBound - upperBound; // Lower bound is larger than upper bound
+            difference = 2 * difference / (upperBound + lowerBound);
             return probability * difference;
         }
 
diff --git a/src/storm-dft/builder/DftExplorationHeuristic.h b/src/storm-dft/builder/DftExplorationHeuristic.h
index f49f5925a..de4b5cfc5 100644
--- a/src/storm-dft/builder/DftExplorationHeuristic.h
+++ b/src/storm-dft/builder/DftExplorationHeuristic.h
@@ -26,7 +26,7 @@ namespace storm {
                 // Intentionally left empty
             }
 
-            DFTExplorationHeuristic(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) : id(id), expand(false), lowerBound(storm::utility::zero<ValueType>()), upperBound(storm::utility::zero<ValueType>()), depth(predecessor.depth + 1), probability(storm::utility::one<ValueType>()) {
+            DFTExplorationHeuristic(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) : id(id), expand(false), lowerBound(storm::utility::zero<ValueType>()), upperBound(storm::utility::infinity<ValueType>()), depth(predecessor.depth + 1), probability(storm::utility::zero<ValueType>()) {
                 this->updateHeuristicValues(predecessor, rate, exitRate);
             }
 
diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
index 13647880e..f9e4b54f6 100644
--- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
+++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
@@ -191,7 +191,8 @@ namespace storm {
                         break;
                     case storm::builder::ApproximationHeuristic::PROBABILITY:
                     case storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE:
-                        approximationThreshold = 10 * std::pow(2, iteration);
+                        double exponent = iteration; // Need conversion to avoid overflow when negating
+                        approximationThreshold = std::pow(2, -exponent);
                         break;
                 }
             }
@@ -646,7 +647,7 @@ namespace storm {
                 STORM_LOG_ASSERT(!it->second.first->isPseudoState(), "State is still pseudo state.");
 
                 ExplorationHeuristicPointer heuristic = it->second.second;
-                if (storm::utility::isZero(heuristic->getUpperBound())) {
+                if (storm::utility::isInfinity(heuristic->getUpperBound())) {
                     // Initialize bounds
                     ValueType lowerBound = getLowerBound(it->second.first);
                     ValueType upperBound = getUpperBound(it->second.first);
@@ -669,6 +670,7 @@ namespace storm {
             for (state->getFailableElements().init(false); !state->getFailableElements().isEnd(); state->getFailableElements().next()) {
                 lowerBound += state->getBERate(state->getFailableElements().get());
             }
+            STORM_LOG_TRACE("Lower bound is " << lowerBound << " for state " << state->getId());
             return lowerBound;
         }