From 386d4c7f056b3ce475c76f574bf0f56c49d8f75f Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Wed, 26 Oct 2016 23:14:21 +0200
Subject: [PATCH] Use heuristic NONE to explore complete state space

Former-commit-id: 25990b5ddaa23c00702940d75ac03879df11aeae
---
 src/builder/ExplicitDFTModelBuilderApprox.cpp | 10 +++++-----
 src/builder/ExplicitDFTModelBuilderApprox.h   |  2 +-
 src/storage/BucketPriorityQueue.h             |  2 +-
 src/storage/dft/DFTState.cpp                  |  2 +-
 4 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp
index 432636161..5a3e65585 100644
--- a/src/builder/ExplicitDFTModelBuilderApprox.cpp
+++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp
@@ -33,12 +33,12 @@ namespace storm {
                 matrixBuilder(!generator.isDeterministicModel()),
                 stateStorage(((dft.stateVectorSize() / 64) + 1) * 64),
                 // TODO Matthias: make choosable
-                //explorationQueue(dft.nrElements()+1, 0, 1)
-                explorationQueue(1001, 0, 0.001)
+                explorationQueue(dft.nrElements()+1, 0, 1)
+                //explorationQueue(1001, 0, 0.001)
         {
             // Intentionally left empty.
             // TODO Matthias: remove again
-            heuristic = storm::builder::ApproximationHeuristic::PROBABILITY;
+            heuristic = storm::builder::ApproximationHeuristic::NONE;
         }
 
         template<typename ValueType, typename StateType>
@@ -266,8 +266,8 @@ namespace storm {
                 // Try to explore the next state
                 generator.load(currentState);
 
-                if (nrExpandedStates > approximationThreshold && !currentExplorationHeuristic->isExpand()) {
-                //if (currentExplorationHeuristic->isSkip(approximationThreshold)) {
+                //if (nrExpandedStates > approximationThreshold && !currentExplorationHeuristic->isExpand()) {
+                if (currentExplorationHeuristic->isSkip(approximationThreshold)) {
                     // Skip the current state
                     ++nrSkippedStates;
                     STORM_LOG_TRACE("Skip expansion of state: " << dft.getStateString(currentState));
diff --git a/src/builder/ExplicitDFTModelBuilderApprox.h b/src/builder/ExplicitDFTModelBuilderApprox.h
index 446bed6ad..c3ffe4467 100644
--- a/src/builder/ExplicitDFTModelBuilderApprox.h
+++ b/src/builder/ExplicitDFTModelBuilderApprox.h
@@ -28,7 +28,7 @@ namespace storm {
 
             using DFTStatePointer = std::shared_ptr<storm::storage::DFTState<ValueType>>;
             // TODO Matthias: make choosable
-            using ExplorationHeuristic = DFTExplorationHeuristicProbability<ValueType>;
+            using ExplorationHeuristic = DFTExplorationHeuristicNone<ValueType>;
             using ExplorationHeuristicPointer = std::shared_ptr<ExplorationHeuristic>;
 
 
diff --git a/src/storage/BucketPriorityQueue.h b/src/storage/BucketPriorityQueue.h
index 253b34e19..1aa18689d 100644
--- a/src/storage/BucketPriorityQueue.h
+++ b/src/storage/BucketPriorityQueue.h
@@ -13,7 +13,7 @@ namespace storm {
         template<typename ValueType>
         class BucketPriorityQueue {
 
-            using HeuristicPointer = std::shared_ptr<storm::builder::DFTExplorationHeuristicProbability<ValueType>>;
+            using HeuristicPointer = std::shared_ptr<storm::builder::DFTExplorationHeuristicNone<ValueType>>;
 
         public:
             explicit BucketPriorityQueue(size_t nrBuckets, double lowerValue, double stepPerBucket);
diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp
index b9381598f..aaad9367f 100644
--- a/src/storage/dft/DFTState.cpp
+++ b/src/storage/dft/DFTState.cpp
@@ -323,7 +323,7 @@ namespace storm {
                         mCurrentlyFailableBE.push_back(elem);
                         // Remove from not failable BEs
                         auto it = std::find(mCurrentlyNotFailableBE.begin(), mCurrentlyNotFailableBE.end(), elem);
-                        STORM_LOG_ASSERT(it != mCurrentlyNotFailableBE.end(), "Element not found.");
+                        STORM_LOG_ASSERT(it != mCurrentlyNotFailableBE.end(), "Element " << elem << " not found.");
                         mCurrentlyNotFailableBE.erase(it);
                     }
                 } else if (mDft.getElement(elem)->isSpareGate() && !isActive(uses(elem))) {