Fix in BucketPriorityQueue

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

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;

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;