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 - BucketPriorityQueue::BucketPriorityQueue(size_t nrBuckets, double lowerValue, double ratio) : lowerValue(lowerValue), logBase(std::log(ratio)), nrBuckets(nrBuckets), nrUnsortedItems(0), buckets(nrBuckets), currentBucket(nrBuckets) { + BucketPriorityQueue::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>; 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;