From 945447e7e01b176f8eab01e41ae961a1ed8e449e Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Mon, 24 Oct 2016 18:41:07 +0200
Subject: [PATCH] Use DFS as default

Former-commit-id: 34f9e80d1bd25c18085ca6f89beb5c163644ccdd
---
 src/builder/ExplicitDFTModelBuilderApprox.cpp | 8 ++++----
 src/builder/ExplicitDFTModelBuilderApprox.h   | 2 +-
 src/storage/BucketPriorityQueue.cpp           | 2 +-
 src/storage/BucketPriorityQueue.h             | 2 +-
 4 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp
index 07863bb01..78272238c 100644
--- a/src/builder/ExplicitDFTModelBuilderApprox.cpp
+++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp
@@ -32,12 +32,12 @@ namespace storm {
                 matrixBuilder(!generator.isDeterministicModel()),
                 stateStorage(((dft.stateVectorSize() / 64) + 1) * 64),
                 // TODO Matthias: make choosable
-                //explorationQueue(dft.nrElements(), 0, 1)
-                explorationQueue(41, 0, 1.0/20)
+                explorationQueue(dft.nrElements()+1, 0, 1)
+                //explorationQueue(141, 0, 0.02)
         {
             // Intentionally left empty.
             // TODO Matthias: remove again
-            heuristic = storm::builder::ApproximationHeuristic::RATERATIO;
+            heuristic = storm::builder::ApproximationHeuristic::NONE;
         }
 
         template<typename ValueType, typename StateType>
@@ -90,7 +90,7 @@ namespace storm {
             switch (heuristic) {
                 case storm::builder::ApproximationHeuristic::NONE:
                     // Do not change anything
-                    approximationThreshold = 0;
+                    approximationThreshold = dft.nrElements()+10;
                     break;
                 case storm::builder::ApproximationHeuristic::DEPTH:
                     approximationThreshold = iteration;
diff --git a/src/builder/ExplicitDFTModelBuilderApprox.h b/src/builder/ExplicitDFTModelBuilderApprox.h
index e23a8e819..1f779e44f 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 = DFTExplorationHeuristicRateRatio<ValueType>;
+            using ExplorationHeuristic = DFTExplorationHeuristicDepth<ValueType>;
             using ExplorationHeuristicPointer = std::shared_ptr<ExplorationHeuristic>;
 
 
diff --git a/src/storage/BucketPriorityQueue.cpp b/src/storage/BucketPriorityQueue.cpp
index bc3ca8780..fe1ca95b5 100644
--- a/src/storage/BucketPriorityQueue.cpp
+++ b/src/storage/BucketPriorityQueue.cpp
@@ -16,7 +16,7 @@ namespace storm {
         void BucketPriorityQueue<ValueType>::fix() {
             if (currentBucket < buckets.size() && nrUnsortedItems > 0) {
                 // Fix current bucket
-                std::make_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare);
+                //std::make_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare);
                 nrUnsortedItems = 0;
             }
         }
diff --git a/src/storage/BucketPriorityQueue.h b/src/storage/BucketPriorityQueue.h
index 2e36e3cb6..3d3c2d35d 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::DFTExplorationHeuristicRateRatio<ValueType>>;
+            using HeuristicPointer = std::shared_ptr<storm::builder::DFTExplorationHeuristicDepth<ValueType>>;
 
         public:
             explicit BucketPriorityQueue(size_t nrBuckets, double lowerValue, double stepPerBucket);