#ifndef STORM_STORAGE_BUCKETPRIORITYQUEUE_H_ #define STORM_STORAGE_BUCKETPRIORITYQUEUE_H_ #include "src/builder/DftExplorationHeuristic.h" #include #include #include #include namespace storm { namespace storage { template class BucketPriorityQueue { using HeuristicPointer = std::shared_ptr>; public: explicit BucketPriorityQueue(size_t nrBuckets, double lowerValue, double ratio); void fix(); bool empty() const; std::size_t size() const; HeuristicPointer const& top() const; void push(HeuristicPointer const& item); void update(HeuristicPointer const& item, double oldPriority); void pop(); HeuristicPointer popTop(); void print(std::ostream& out) const; void printSizes(std::ostream& out) const; private: size_t getBucket(double priority) const; const double lowerValue; const bool HIGHER = true; const bool AUTOSORT = false; const double logBase; const size_t nrBuckets; size_t nrUnsortedItems; // List of buckets std::vector> buckets; // Bucket containing all items which should be considered immediately std::vector immediateBucket; // Index of first bucket which contains items size_t currentBucket; std::function compare; }; } } #endif // STORM_STORAGE_BUCKETPRIORITYQUEUE_H_