Use DFS as default

Former-commit-id: 34f9e80d1b

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;

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

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

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