From 1c95722711e82a46c78a96996eb92f2584dfc8c3 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Sat, 29 Oct 2016 22:46:20 +0200
Subject: [PATCH] Do not skip states if approx = 0.0

Former-commit-id: 37dbb9739c95648dcfc91e5e0f85792f28d14afa
---
 src/builder/ExplicitDFTModelBuilderApprox.cpp | 26 ++++++++++---------
 1 file changed, 14 insertions(+), 12 deletions(-)

diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp
index 93a7b282e..c6c584e86 100644
--- a/src/builder/ExplicitDFTModelBuilderApprox.cpp
+++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp
@@ -143,17 +143,19 @@ namespace storm {
                 initializeNextIteration();
             }
 
-            switch (heuristic) {
-                case storm::builder::ApproximationHeuristic::NONE:
-                    // Do not change anything
-                    approximationThreshold = dft.nrElements()+10;
-                    break;
-                case storm::builder::ApproximationHeuristic::DEPTH:
-                    approximationThreshold = iteration;
-                    break;
-                case storm::builder::ApproximationHeuristic::PROBABILITY:
-                    approximationThreshold = 10 * std::pow(2, iteration);
-                    break;
+            if (approximationThreshold > 0) {
+                switch (heuristic) {
+                    case storm::builder::ApproximationHeuristic::NONE:
+                        // Do not change anything
+                        approximationThreshold = dft.nrElements()+10;
+                        break;
+                    case storm::builder::ApproximationHeuristic::DEPTH:
+                        approximationThreshold = iteration;
+                        break;
+                    case storm::builder::ApproximationHeuristic::PROBABILITY:
+                        approximationThreshold = 10 * std::pow(2, iteration);
+                        break;
+                }
             }
             exploreStateSpace(approximationThreshold);
 
@@ -319,7 +321,7 @@ namespace storm {
                 // Try to explore the next state
                 generator.load(currentState);
 
-                if (nrExpandedStates > approximationThreshold && !currentExplorationHeuristic->isExpand()) {
+                if (approximationThreshold > 0.0 && nrExpandedStates > approximationThreshold && !currentExplorationHeuristic->isExpand()) {
                 //if (currentExplorationHeuristic->isSkip(approximationThreshold)) {
                     // Skip the current state
                     ++nrSkippedStates;