sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Refactored BucketPriorityQueue

main
Matthias Volk 7 years ago
parent
6afcaa291d
commit
e53d946b04
3 changed files with 121 additions and 65 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
  2. 86
      src/storm-dft/storage/BucketPriorityQueue.cpp
  3. 98
      src/storm-dft/storage/BucketPriorityQueue.h

2
src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
View File

@ -325,7 +325,7 @@ namespace storm {
// TODO Matthias: do not empty queue every time but break before // TODO Matthias: do not empty queue every time but break before
while (!explorationQueue.empty()) { while (!explorationQueue.empty()) {
// Get the first state in the queue // Get the first state in the queue
ExplorationHeuristicPointer currentExplorationHeuristic = explorationQueue.popTop();
ExplorationHeuristicPointer currentExplorationHeuristic = explorationQueue.pop();
StateType currentId = currentExplorationHeuristic->getId(); StateType currentId = currentExplorationHeuristic->getId();
auto itFind = statesNotExplored.find(currentId); auto itFind = statesNotExplored.find(currentId);
STORM_LOG_ASSERT(itFind != statesNotExplored.end(), "Id " << currentId << " not found"); STORM_LOG_ASSERT(itFind != statesNotExplored.end(), "Id " << currentId << " not found");

86
src/storm-dft/storage/BucketPriorityQueue.cpp
View File

@ -7,29 +7,29 @@
namespace storm { namespace storm {
namespace storage { namespace storage {
template<typename ValueType>
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) {
template<typename PriorityType>
BucketPriorityQueue<PriorityType>::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; return *a < *b;
}); });
} }
template<typename ValueType>
void BucketPriorityQueue<ValueType>::fix() {
template<typename PriorityType>
void BucketPriorityQueue<PriorityType>::fix() {
if (currentBucket < nrBuckets && nrUnsortedItems > buckets[currentBucket].size() / 10) { if (currentBucket < nrBuckets && nrUnsortedItems > buckets[currentBucket].size() / 10) {
// Fix current bucket
// Sort current bucket
std::make_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare); std::make_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare);
nrUnsortedItems = 0; nrUnsortedItems = 0;
} }
} }
template<typename ValueType>
bool BucketPriorityQueue<ValueType>::empty() const {
template<typename PriorityType>
bool BucketPriorityQueue<PriorityType>::empty() const {
return currentBucket == nrBuckets && immediateBucket.empty(); return currentBucket == nrBuckets && immediateBucket.empty();
} }
template<typename ValueType>
std::size_t BucketPriorityQueue<ValueType>::size() const {
template<typename PriorityType>
size_t BucketPriorityQueue<PriorityType>::size() const {
size_t size = immediateBucket.size(); size_t size = immediateBucket.size();
for (size_t i = currentBucket; currentBucket < nrBuckets; ++i) { for (size_t i = currentBucket; currentBucket < nrBuckets; ++i) {
size += buckets[i].size(); size += buckets[i].size();
@ -37,8 +37,8 @@ namespace storm {
return size; return size;
} }
template<typename ValueType>
typename BucketPriorityQueue<ValueType>::HeuristicPointer const& BucketPriorityQueue<ValueType>::top() const {
template<typename PriorityType>
typename BucketPriorityQueue<PriorityType>::PriorityTypePointer const& BucketPriorityQueue<PriorityType>::top() const {
if (!immediateBucket.empty()) { if (!immediateBucket.empty()) {
return immediateBucket.back(); return immediateBucket.back();
} }
@ -46,8 +46,8 @@ namespace storm {
return buckets[currentBucket].front(); return buckets[currentBucket].front();
} }
template<typename ValueType>
void BucketPriorityQueue<ValueType>::push(HeuristicPointer const& item) {
template<typename PriorityType>
void BucketPriorityQueue<PriorityType>::push(PriorityTypePointer const& item) {
if (item->isExpand()) { if (item->isExpand()) {
immediateBucket.push_back(item); immediateBucket.push_back(item);
return; return;
@ -59,7 +59,7 @@ namespace storm {
} }
buckets[bucket].push_back(item); buckets[bucket].push_back(item);
if (bucket == currentBucket) { if (bucket == currentBucket) {
// Insert in first bucket
// Inserted in first bucket
if (AUTOSORT) { if (AUTOSORT) {
std::push_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare); std::push_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare);
} else { } else {
@ -68,8 +68,8 @@ namespace storm {
} }
} }
template<typename ValueType>
void BucketPriorityQueue<ValueType>::update(HeuristicPointer const& item, double oldPriority) {
template<typename PriorityType>
void BucketPriorityQueue<PriorityType>::update(PriorityTypePointer const& item, double oldPriority) {
STORM_LOG_ASSERT(!item->isExpand(), "Item is marked for expansion"); STORM_LOG_ASSERT(!item->isExpand(), "Item is marked for expansion");
size_t newBucket = getBucket(item->getPriority()); size_t newBucket = getBucket(item->getPriority());
size_t oldBucket = getBucket(oldPriority); size_t oldBucket = getBucket(oldPriority);
@ -95,7 +95,7 @@ namespace storm {
// Remove old entry by swap-and-pop // Remove old entry by swap-and-pop
if (buckets[oldBucket].size() >= 2) { if (buckets[oldBucket].size() >= 2) {
// Find old index by linear search // 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; size_t oldIndex = 0;
for ( ; oldIndex < buckets[oldBucket].size(); ++oldIndex) { for ( ; oldIndex < buckets[oldBucket].size(); ++oldIndex) {
if (buckets[oldBucket][oldIndex]->getId() == item->getId()) { if (buckets[oldBucket][oldIndex]->getId() == item->getId()) {
@ -120,14 +120,16 @@ namespace storm {
} }
template<typename ValueType>
void BucketPriorityQueue<ValueType>::pop() {
template<typename PriorityType>
typename BucketPriorityQueue<PriorityType>::PriorityTypePointer BucketPriorityQueue<PriorityType>::pop() {
if (!immediateBucket.empty()) { if (!immediateBucket.empty()) {
PriorityTypePointer item = immediateBucket.back();
immediateBucket.pop_back(); immediateBucket.pop_back();
return;
return item;
} }
STORM_LOG_ASSERT(!empty(), "BucketPriorityQueue is empty"); STORM_LOG_ASSERT(!empty(), "BucketPriorityQueue is empty");
std::pop_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare); std::pop_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare);
PriorityTypePointer item = buckets[currentBucket].back();
buckets[currentBucket].pop_back(); buckets[currentBucket].pop_back();
if (buckets[currentBucket].empty()) { if (buckets[currentBucket].empty()) {
// Find next bucket with elements // Find next bucket with elements
@ -141,17 +143,11 @@ namespace storm {
} }
} }
} }
}
template<typename ValueType>
typename BucketPriorityQueue<ValueType>::HeuristicPointer BucketPriorityQueue<ValueType>::popTop() {
HeuristicPointer item = top();
pop();
return item; return item;
} }
template<typename ValueType>
size_t BucketPriorityQueue<ValueType>::getBucket(double priority) const {
template<typename PriorityType>
size_t BucketPriorityQueue<PriorityType>::getBucket(double priority) const {
STORM_LOG_ASSERT(priority >= lowerValue, "Priority " << priority << " is too low"); STORM_LOG_ASSERT(priority >= lowerValue, "Priority " << priority << " is too low");
// For possible values greater 1 // For possible values greater 1
@ -160,41 +156,39 @@ namespace storm {
if (tmpBucket < 0) { if (tmpBucket < 0) {
tmpBucket = 0; tmpBucket = 0;
} }
size_t newBucket = tmpBucket;
size_t newBucket = static_cast<size_t>(tmpBucket);
// For values ensured to be lower 1 // For values ensured to be lower 1
//size_t newBucket = std::log(priority - lowerValue) / logBase;
if (newBucket >= nrBuckets) { if (newBucket >= nrBuckets) {
newBucket = nrBuckets - 1; newBucket = nrBuckets - 1;
} }
if (!higher) { if (!higher) {
newBucket = nrBuckets-1 - newBucket; newBucket = nrBuckets-1 - newBucket;
} }
//std::cout << "get Bucket: " << priority << ", " << newBucket << std::endl;
STORM_LOG_ASSERT(newBucket < nrBuckets, "Priority " << priority << " is too high"); STORM_LOG_ASSERT(newBucket < nrBuckets, "Priority " << priority << " is too high");
return newBucket; return newBucket;
} }
template<typename ValueType>
void BucketPriorityQueue<ValueType>::print(std::ostream& out) const {
template<typename PriorityType>
void BucketPriorityQueue<PriorityType>::print(std::ostream& out) const {
out << "Bucket priority queue with size " << buckets.size() << ", lower value: " << lowerValue << " and logBase: " << logBase << std::endl; out << "Bucket priority queue with size " << buckets.size() << ", lower value: " << lowerValue << " and logBase: " << logBase << std::endl;
out << "Immediate bucket: "; out << "Immediate bucket: ";
for (HeuristicPointer heuristic : immediateBucket) {
out << heuristic->getId() << ", ";
for (auto item : immediateBucket) {
out << item->getId() << ", ";
} }
out << std::endl; out << std::endl;
out << "Current bucket (" << currentBucket << ") has " << nrUnsortedItems << " unsorted items" << std::endl; out << "Current bucket (" << currentBucket << ") has " << nrUnsortedItems << " unsorted items" << std::endl;
for (size_t bucket = 0; bucket < buckets.size(); ++bucket) { for (size_t bucket = 0; bucket < buckets.size(); ++bucket) {
if (!buckets[bucket].empty()) { if (!buckets[bucket].empty()) {
out << "Bucket " << bucket << ":" << std::endl; 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<typename ValueType>
void BucketPriorityQueue<ValueType>::printSizes(std::ostream& out) const {
template<typename PriorityType>
void BucketPriorityQueue<PriorityType>::printSizes(std::ostream& out) const {
out << "Bucket sizes: " << immediateBucket.size() << " | "; out << "Bucket sizes: " << immediateBucket.size() << " | ";
for (size_t bucket = 0; bucket < buckets.size(); ++bucket) { for (size_t bucket = 0; bucket < buckets.size(); ++bucket) {
out << buckets[bucket].size() << " "; out << buckets[bucket].size() << " ";
@ -203,10 +197,18 @@ namespace storm {
} }
// Template instantiations // Template instantiations
template class BucketPriorityQueue<double>;
template class BucketPriorityQueue<storm::builder::DFTExplorationHeuristic<double>>;
template class BucketPriorityQueue<storm::builder::DFTExplorationHeuristicNone<double>>;
template class BucketPriorityQueue<storm::builder::DFTExplorationHeuristicDepth<double>>;
template class BucketPriorityQueue<storm::builder::DFTExplorationHeuristicProbability<double>>;
template class BucketPriorityQueue<storm::builder::DFTExplorationHeuristicBoundDifference<double>>;
#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
template class BucketPriorityQueue<storm::RationalFunction>;
template class BucketPriorityQueue<storm::builder::DFTExplorationHeuristic<storm::RationalFunction>>;
template class BucketPriorityQueue<storm::builder::DFTExplorationHeuristicNone<storm::RationalFunction>>;
template class BucketPriorityQueue<storm::builder::DFTExplorationHeuristicDepth<storm::RationalFunction>>;
template class BucketPriorityQueue<storm::builder::DFTExplorationHeuristicProbability<storm::RationalFunction>>;
template class BucketPriorityQueue<storm::builder::DFTExplorationHeuristicBoundDifference<storm::RationalFunction>>;
#endif #endif
} }
} }

98
src/storm-dft/storage/BucketPriorityQueue.h
View File

@ -10,38 +10,102 @@
namespace storm { namespace storm {
namespace storage { namespace storage {
template<typename ValueType>
/*!
* 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 PriorityType>
class BucketPriorityQueue { class BucketPriorityQueue {
using HeuristicPointer = std::shared_ptr<storm::builder::DFTExplorationHeuristicDepth<ValueType>>;
using PriorityTypePointer = std::shared_ptr<PriorityType>;
public: public:
/*!
* Create new priority queue.
* @param nrBuckets
* @param lowerValue
* @param ratio
* @param higher
*/
explicit BucketPriorityQueue(size_t nrBuckets, double lowerValue, double ratio, bool higher); explicit BucketPriorityQueue(size_t nrBuckets, double lowerValue, double ratio, bool higher);
void fix(); void fix();
/*!
* Check whether queue is empty.
* @return True iff queue is empty.
*/
bool empty() const; bool empty() const;
/*!
* Return number of entries.
* @return Size of queue.
*/
std::size_t size() const; 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<std::vector<PriorityTypePointer>> buckets;
void print(std::ostream& out) const;
// Bucket containing all items which should be considered immediately
std::vector<PriorityTypePointer> 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<bool(PriorityTypePointer, PriorityTypePointer)> compare;
// Minimal value
const double lowerValue; const double lowerValue;
const bool higher; const bool higher;
@ -50,20 +114,10 @@ namespace storm {
const double logBase; const double logBase;
// Number of available buckets
const size_t nrBuckets; const size_t nrBuckets;
size_t nrUnsortedItems;
// List of buckets
std::vector<std::vector<HeuristicPointer>> buckets;
// Bucket containing all items which should be considered immediately
std::vector<HeuristicPointer> immediateBucket;
// Index of first bucket which contains items
size_t currentBucket;
std::function<bool(HeuristicPointer, HeuristicPointer)> compare;
}; };

Write Preview
Loading…
Cancel
Save