Some fixes for approximation

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;
         }
 

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);
             }
 

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;
         }