From 3dd0bffef9194492e1a86821ac5317f7296aa417 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 18 Mar 2019 22:02:36 +0100 Subject: [PATCH] Refactored BucketPriorityQueue --- .../builder/ExplicitDFTModelBuilder.cpp | 2 +- src/storm-dft/storage/BucketPriorityQueue.cpp | 86 ++++++++-------- src/storm-dft/storage/BucketPriorityQueue.h | 98 ++++++++++++++----- 3 files changed, 121 insertions(+), 65 deletions(-) diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index 466cba537..3e1436ba7 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -325,7 +325,7 @@ namespace storm { // TODO Matthias: do not empty queue every time but break before while (!explorationQueue.empty()) { // Get the first state in the queue - ExplorationHeuristicPointer currentExplorationHeuristic = explorationQueue.popTop(); + ExplorationHeuristicPointer currentExplorationHeuristic = explorationQueue.pop(); StateType currentId = currentExplorationHeuristic->getId(); auto itFind = statesNotExplored.find(currentId); STORM_LOG_ASSERT(itFind != statesNotExplored.end(), "Id " << currentId << " not found"); diff --git a/src/storm-dft/storage/BucketPriorityQueue.cpp b/src/storm-dft/storage/BucketPriorityQueue.cpp index a591764ac..a0926e70c 100644 --- a/src/storm-dft/storage/BucketPriorityQueue.cpp +++ b/src/storm-dft/storage/BucketPriorityQueue.cpp @@ -7,29 +7,29 @@ namespace storm { namespace storage { - template - 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) { + template + BucketPriorityQueue::BucketPriorityQueue(size_t nrBuckets, double lowerValue, double ratio, bool higher) : buckets(nrBuckets), currentBucket(nrBuckets), nrUnsortedItems(0), lowerValue(lowerValue), higher(higher), logBase(std::log(ratio)), nrBuckets(nrBuckets) { + compare = ([](PriorityTypePointer a, PriorityTypePointer b) { return *a < *b; }); } - template - void BucketPriorityQueue::fix() { + template + void BucketPriorityQueue::fix() { if (currentBucket < nrBuckets && nrUnsortedItems > buckets[currentBucket].size() / 10) { - // Fix current bucket + // Sort current bucket std::make_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare); nrUnsortedItems = 0; } } - template - bool BucketPriorityQueue::empty() const { + template + bool BucketPriorityQueue::empty() const { return currentBucket == nrBuckets && immediateBucket.empty(); } - template - std::size_t BucketPriorityQueue::size() const { + template + size_t BucketPriorityQueue::size() const { size_t size = immediateBucket.size(); for (size_t i = currentBucket; currentBucket < nrBuckets; ++i) { size += buckets[i].size(); @@ -37,8 +37,8 @@ namespace storm { return size; } - template - typename BucketPriorityQueue::HeuristicPointer const& BucketPriorityQueue::top() const { + template + typename BucketPriorityQueue::PriorityTypePointer const& BucketPriorityQueue::top() const { if (!immediateBucket.empty()) { return immediateBucket.back(); } @@ -46,8 +46,8 @@ namespace storm { return buckets[currentBucket].front(); } - template - void BucketPriorityQueue::push(HeuristicPointer const& item) { + template + void BucketPriorityQueue::push(PriorityTypePointer const& item) { if (item->isExpand()) { immediateBucket.push_back(item); return; @@ -59,7 +59,7 @@ namespace storm { } buckets[bucket].push_back(item); if (bucket == currentBucket) { - // Insert in first bucket + // Inserted in first bucket if (AUTOSORT) { std::push_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare); } else { @@ -68,8 +68,8 @@ namespace storm { } } - template - void BucketPriorityQueue::update(HeuristicPointer const& item, double oldPriority) { + template + void BucketPriorityQueue::update(PriorityTypePointer const& item, double oldPriority) { STORM_LOG_ASSERT(!item->isExpand(), "Item is marked for expansion"); size_t newBucket = getBucket(item->getPriority()); size_t oldBucket = getBucket(oldPriority); @@ -95,7 +95,7 @@ namespace storm { // Remove old entry by swap-and-pop if (buckets[oldBucket].size() >= 2) { // Find old index by linear search - // Notice: using a map to rememeber index was not efficient + // Notice: using a map to remember index was not efficient size_t oldIndex = 0; for ( ; oldIndex < buckets[oldBucket].size(); ++oldIndex) { if (buckets[oldBucket][oldIndex]->getId() == item->getId()) { @@ -120,14 +120,16 @@ namespace storm { } - template - void BucketPriorityQueue::pop() { + template + typename BucketPriorityQueue::PriorityTypePointer BucketPriorityQueue::pop() { if (!immediateBucket.empty()) { + PriorityTypePointer item = immediateBucket.back(); immediateBucket.pop_back(); - return; + return item; } STORM_LOG_ASSERT(!empty(), "BucketPriorityQueue is empty"); std::pop_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare); + PriorityTypePointer item = buckets[currentBucket].back(); buckets[currentBucket].pop_back(); if (buckets[currentBucket].empty()) { // Find next bucket with elements @@ -141,17 +143,11 @@ namespace storm { } } } - } - - template - typename BucketPriorityQueue::HeuristicPointer BucketPriorityQueue::popTop() { - HeuristicPointer item = top(); - pop(); return item; } - template - size_t BucketPriorityQueue::getBucket(double priority) const { + template + size_t BucketPriorityQueue::getBucket(double priority) const { STORM_LOG_ASSERT(priority >= lowerValue, "Priority " << priority << " is too low"); // For possible values greater 1 @@ -160,41 +156,39 @@ namespace storm { if (tmpBucket < 0) { tmpBucket = 0; } - size_t newBucket = tmpBucket; + size_t newBucket = static_cast(tmpBucket); // For values ensured to be lower 1 - //size_t newBucket = std::log(priority - lowerValue) / logBase; if (newBucket >= nrBuckets) { newBucket = nrBuckets - 1; } if (!higher) { newBucket = nrBuckets-1 - newBucket; } - //std::cout << "get Bucket: " << priority << ", " << newBucket << std::endl; STORM_LOG_ASSERT(newBucket < nrBuckets, "Priority " << priority << " is too high"); return newBucket; } - template - void BucketPriorityQueue::print(std::ostream& out) const { + template + void BucketPriorityQueue::print(std::ostream& out) const { out << "Bucket priority queue with size " << buckets.size() << ", lower value: " << lowerValue << " and logBase: " << logBase << std::endl; out << "Immediate bucket: "; - for (HeuristicPointer heuristic : immediateBucket) { - out << heuristic->getId() << ", "; + for (auto item : immediateBucket) { + out << item->getId() << ", "; } out << std::endl; out << "Current bucket (" << currentBucket << ") has " << nrUnsortedItems << " unsorted items" << std::endl; for (size_t bucket = 0; bucket < buckets.size(); ++bucket) { if (!buckets[bucket].empty()) { out << "Bucket " << bucket << ":" << std::endl; - for (HeuristicPointer heuristic : buckets[bucket]) { - out << "\t" << heuristic->getId() << ": " << heuristic->getPriority() << std::endl; + for (auto item : buckets[bucket]) { + out << "\t" << item->getId() << ": " << item->getPriority() << std::endl; } } } } - template - void BucketPriorityQueue::printSizes(std::ostream& out) const { + template + void BucketPriorityQueue::printSizes(std::ostream& out) const { out << "Bucket sizes: " << immediateBucket.size() << " | "; for (size_t bucket = 0; bucket < buckets.size(); ++bucket) { out << buckets[bucket].size() << " "; @@ -203,10 +197,18 @@ namespace storm { } // Template instantiations - template class BucketPriorityQueue; + template class BucketPriorityQueue>; + template class BucketPriorityQueue>; + template class BucketPriorityQueue>; + template class BucketPriorityQueue>; + template class BucketPriorityQueue>; #ifdef STORM_HAVE_CARL - template class BucketPriorityQueue; + template class BucketPriorityQueue>; + template class BucketPriorityQueue>; + template class BucketPriorityQueue>; + template class BucketPriorityQueue>; + template class BucketPriorityQueue>; #endif } } diff --git a/src/storm-dft/storage/BucketPriorityQueue.h b/src/storm-dft/storage/BucketPriorityQueue.h index 10c753763..2c0c3cb37 100644 --- a/src/storm-dft/storage/BucketPriorityQueue.h +++ b/src/storm-dft/storage/BucketPriorityQueue.h @@ -10,38 +10,102 @@ namespace storm { namespace storage { - template + /*! + * Priority queue based on buckets. + * Can be used to keep track of states during state space exploration. + * @tparam PriorityType Underlying priority data type + */ + template class BucketPriorityQueue { - using HeuristicPointer = std::shared_ptr>; + using PriorityTypePointer = std::shared_ptr; public: + /*! + * Create new priority queue. + * @param nrBuckets + * @param lowerValue + * @param ratio + * @param higher + */ explicit BucketPriorityQueue(size_t nrBuckets, double lowerValue, double ratio, bool higher); void fix(); + /*! + * Check whether queue is empty. + * @return True iff queue is empty. + */ bool empty() const; + /*! + * Return number of entries. + * @return Size of queue. + */ std::size_t size() const; - HeuristicPointer const& top() const; + /*! + * Get element with highest priority. + * @return Top element. + */ + PriorityTypePointer const& top() const; + + /*! + * Add element. + * @param item Element. + */ + void push(PriorityTypePointer const& item); + + /*! + * Update existing element. + * @param item Element with changes. + * @param oldPriority Old priority. + */ + void update(PriorityTypePointer const& item, double oldPriority); + + /*! + * Get element with highest priority and remove it from the queue. + * @return Top element. + */ + PriorityTypePointer pop(); + + /*! + * Print info about priority queue. + * @param out Output stream. + */ + void print(std::ostream& out) const; - void push(HeuristicPointer const& item); + /*! + * Print sizes of buckets. + * @param out Output stream. + */ + void printSizes(std::ostream& out) const; - void update(HeuristicPointer const& item, double oldPriority); + private: - void pop(); + /*! + * Get bucket for given priority. + * @param priority Priority. + * @return Bucket containing the priority. + */ + size_t getBucket(double priority) const; - HeuristicPointer popTop(); + // List of buckets + std::vector> buckets; - void print(std::ostream& out) const; + // Bucket containing all items which should be considered immediately + std::vector immediateBucket; - void printSizes(std::ostream& out) const; + // Index of first bucket which contains items + size_t currentBucket; - private: + // Number of unsorted items in current bucket + size_t nrUnsortedItems; - size_t getBucket(double priority) const; + // Comparison function for priorities + std::function compare; + // Minimal value const double lowerValue; const bool higher; @@ -50,20 +114,10 @@ namespace storm { const double logBase; + // Number of available buckets 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; };