From a302ec9cfcb0e1cc2cf69dca03a5b1f429085e48 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Fri, 23 Nov 2018 13:09:36 +0100
Subject: [PATCH] Fix in BucketPriorityQueue

---
 src/storm-dft/builder/ExplicitDFTModelBuilder.cpp | 2 +-
 src/storm-dft/storage/BucketPriorityQueue.cpp     | 4 ++--
 src/storm-dft/storage/BucketPriorityQueue.h       | 4 ++--
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
index 695fd7c55..87cec9ce8 100644
--- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
+++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
@@ -62,7 +62,7 @@ namespace storm {
                 stateStorage(dft.stateBitVectorSize()),
                 // TODO Matthias: make choosable
                 //explorationQueue(dft.nrElements()+1, 0, 1)
-                explorationQueue(200, 0, 0.9)
+                explorationQueue(200, 0, 0.9, false)
         {
             // Intentionally left empty.
             // TODO Matthias: remove again
diff --git a/src/storm-dft/storage/BucketPriorityQueue.cpp b/src/storm-dft/storage/BucketPriorityQueue.cpp
index c9b2adf24..a591764ac 100644
--- a/src/storm-dft/storage/BucketPriorityQueue.cpp
+++ b/src/storm-dft/storage/BucketPriorityQueue.cpp
@@ -8,7 +8,7 @@ namespace storm {
     namespace storage {
 
         template<typename ValueType>
-        BucketPriorityQueue<ValueType>::BucketPriorityQueue(size_t nrBuckets, double lowerValue, double ratio) : lowerValue(lowerValue), logBase(std::log(ratio)), nrBuckets(nrBuckets), nrUnsortedItems(0), buckets(nrBuckets), currentBucket(nrBuckets) {
+        BucketPriorityQueue<ValueType>::BucketPriorityQueue(size_t nrBuckets, double lowerValue, double ratio, bool higher) : lowerValue(lowerValue), higher(higher), logBase(std::log(ratio)), nrBuckets(nrBuckets), nrUnsortedItems(0), buckets(nrBuckets), currentBucket(nrBuckets) {
             compare = ([](HeuristicPointer a, HeuristicPointer b) {
                 return *a < *b;
             });
@@ -166,7 +166,7 @@ namespace storm {
             if (newBucket >= nrBuckets) {
                 newBucket = nrBuckets - 1;
             }
-            if (!HIGHER) {
+            if (!higher) {
                 newBucket = nrBuckets-1 - newBucket;
             }
             //std::cout << "get Bucket: " << priority << ", " << newBucket << std::endl;
diff --git a/src/storm-dft/storage/BucketPriorityQueue.h b/src/storm-dft/storage/BucketPriorityQueue.h
index 004469f9a..10c753763 100644
--- a/src/storm-dft/storage/BucketPriorityQueue.h
+++ b/src/storm-dft/storage/BucketPriorityQueue.h
@@ -16,7 +16,7 @@ namespace storm {
             using HeuristicPointer = std::shared_ptr<storm::builder::DFTExplorationHeuristicDepth<ValueType>>;
 
         public:
-            explicit BucketPriorityQueue(size_t nrBuckets, double lowerValue, double ratio);
+            explicit BucketPriorityQueue(size_t nrBuckets, double lowerValue, double ratio, bool higher);
 
             void fix();
 
@@ -44,7 +44,7 @@ namespace storm {
 
             const double lowerValue;
 
-            const bool HIGHER = true;
+            const bool higher;
 
             const bool AUTOSORT = false;