From 8d38358c115dda77d55c001c2f8178c2f52aebbb Mon Sep 17 00:00:00 2001 From: Mavo Date: Mon, 24 Oct 2016 17:28:56 +0200 Subject: [PATCH] Use BucketPriorityQueue instead of DynamicPriorityQueue Former-commit-id: 7a22ef5b1671b4a33319e4cc6c98bff2e473aa77 --- src/builder/DftExplorationHeuristic.cpp | 22 +- src/builder/DftExplorationHeuristic.h | 12 +- src/builder/ExplicitDFTModelBuilderApprox.cpp | 55 +++-- src/builder/ExplicitDFTModelBuilderApprox.h | 9 +- src/storage/BucketPriorityQueue.cpp | 191 ++++++++++++++++++ src/storage/BucketPriorityQueue.h | 70 +++++++ 6 files changed, 320 insertions(+), 39 deletions(-) create mode 100644 src/storage/BucketPriorityQueue.cpp create mode 100644 src/storage/BucketPriorityQueue.h diff --git a/src/builder/DftExplorationHeuristic.cpp b/src/builder/DftExplorationHeuristic.cpp index 3b9c2e110..dbd64088b 100644 --- a/src/builder/DftExplorationHeuristic.cpp +++ b/src/builder/DftExplorationHeuristic.cpp @@ -4,28 +4,20 @@ #include "src/utility/constants.h" #include "src/exceptions/NotImplementedException.h" -#include - namespace storm { namespace builder { template - DFTExplorationHeuristic::DFTExplorationHeuristic(size_t id) : id(id), expand(false), depth(std::numeric_limits::max()), rate(storm::utility::zero()), exitRate(storm::utility::zero()) { - // Intentionally left empty + DFTExplorationHeuristic::DFTExplorationHeuristic(size_t id, size_t depth, ValueType rate, ValueType exitRate) : id(id), expand(false), depth(depth) { + STORM_LOG_ASSERT(storm::utility::zero() < exitRate, "Exit rate is 0"); + rateRatio = rate/exitRate; } template<> bool DFTExplorationHeuristicRateRatio::updateHeuristicValues(size_t depth, double rate, double exitRate) { - bool update = false; - if (this->rate < rate) { - this->rate = rate; - update = true; - } - if (this->exitRate < exitRate) { - this->exitRate = exitRate; - update = true; - } - return update; + STORM_LOG_ASSERT(exitRate > 0, "Exit rate is 0"); + rateRatio += rate/exitRate; + return true; } template<> @@ -36,7 +28,7 @@ namespace storm { template<> double DFTExplorationHeuristicRateRatio::getPriority() const { - return rate/exitRate; + return rateRatio; } template<> diff --git a/src/builder/DftExplorationHeuristic.h b/src/builder/DftExplorationHeuristic.h index 2b4fc5047..d23c673fc 100644 --- a/src/builder/DftExplorationHeuristic.h +++ b/src/builder/DftExplorationHeuristic.h @@ -20,7 +20,7 @@ namespace storm { class DFTExplorationHeuristic { public: - DFTExplorationHeuristic(size_t id); + DFTExplorationHeuristic(size_t id, size_t depth, ValueType rate, ValueType exitRate); virtual bool updateHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) = 0; @@ -44,15 +44,13 @@ namespace storm { size_t id; bool expand; size_t depth; - ValueType rate; - ValueType exitRate; - + ValueType rateRatio; }; template class DFTExplorationHeuristicNone : public DFTExplorationHeuristic { public: - DFTExplorationHeuristicNone(size_t id) : DFTExplorationHeuristic(id) { + DFTExplorationHeuristicNone(size_t id, size_t depth, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, depth, rate, exitRate) { // Intentionally left empty } @@ -76,7 +74,7 @@ namespace storm { template class DFTExplorationHeuristicDepth : public DFTExplorationHeuristic { public: - DFTExplorationHeuristicDepth(size_t id) : DFTExplorationHeuristic(id) { + DFTExplorationHeuristicDepth(size_t id, size_t depth, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, depth, rate, exitRate) { // Intentionally left empty } @@ -105,7 +103,7 @@ namespace storm { template class DFTExplorationHeuristicRateRatio : public DFTExplorationHeuristic { public: - DFTExplorationHeuristicRateRatio(size_t id) : DFTExplorationHeuristic(id) { + DFTExplorationHeuristicRateRatio(size_t id, size_t depth, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, depth, rate, exitRate) { // Intentionally left empty } diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index ed7c1500d..07863bb01 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -31,11 +31,13 @@ namespace storm { generator(dft, *stateGenerationInfo, enableDC, mergeFailedStates), matrixBuilder(!generator.isDeterministicModel()), stateStorage(((dft.stateVectorSize() / 64) + 1) * 64), - explorationQueue([this](ExplorationHeuristicPointer a, ExplorationHeuristicPointer b) { - return *a < *b; - }) + // TODO Matthias: make choosable + //explorationQueue(dft.nrElements(), 0, 1) + explorationQueue(41, 0, 1.0/20) { // Intentionally left empty. + // TODO Matthias: remove again + heuristic = storm::builder::ApproximationHeuristic::RATERATIO; } template @@ -76,7 +78,11 @@ namespace storm { initialStateIndex = stateStorage.initialStateIndices[0]; STORM_LOG_TRACE("Initial state: " << initialStateIndex); // Initialize heuristic values for inital state - statesNotExplored.at(initialStateIndex).second->updateHeuristicValues(0, storm::utility::zero(), storm::utility::zero()); + STORM_LOG_ASSERT(!statesNotExplored.at(initialStateIndex).second, "Heuristic for initial state is already initialized"); + ExplorationHeuristicPointer heuristic = std::make_shared(initialStateIndex, 0, storm::utility::zero(), storm::utility::one()); + heuristic->markExpand(); + statesNotExplored[initialStateIndex].second = heuristic; + explorationQueue.push(heuristic); } else { initializeNextIteration(); } @@ -84,6 +90,7 @@ namespace storm { switch (heuristic) { case storm::builder::ApproximationHeuristic::NONE: // Do not change anything + approximationThreshold = 0; break; case storm::builder::ApproximationHeuristic::DEPTH: approximationThreshold = iteration; @@ -225,8 +232,12 @@ namespace storm { void ExplicitDFTModelBuilderApprox::exploreStateSpace(double approximationThreshold) { size_t nrExpandedStates = 0; size_t nrSkippedStates = 0; + size_t fix = 0; // TODO Matthias: do not empty queue every time but break before while (!explorationQueue.empty()) { + explorationQueue.fix(); + //explorationQueue.print(std::cout); + //printNotExplored(); // Get the first state in the queue ExplorationHeuristicPointer currentExplorationHeuristic = explorationQueue.popTop(); StateType currentId = currentExplorationHeuristic->getId(); @@ -253,7 +264,6 @@ namespace storm { matrixBuilder.newRowGroup(); // Try to explore the next state - bool fixQueue = false; generator.load(currentState); if (currentExplorationHeuristic->isSkip(approximationThreshold)) { @@ -286,22 +296,31 @@ namespace storm { if (iter != statesNotExplored.end()) { // Update heuristic values DFTStatePointer state = iter->second.first; + if (!iter->second.second) { + // Initialize heuristic values + ExplorationHeuristicPointer heuristic = std::make_shared(stateProbabilityPair.first, currentExplorationHeuristic->getDepth() + 1, stateProbabilityPair.second, choice.getTotalMass()); + iter->second.second = heuristic; + explorationQueue.push(heuristic); + } else { + double oldPriority = iter->second.second->getPriority(); + if (iter->second.second->updateHeuristicValues(currentExplorationHeuristic->getDepth() + 1, stateProbabilityPair.second, choice.getTotalMass())) { + // Update priority queue + ++fix; + explorationQueue.update(iter->second.second, oldPriority); + } + } if (state->hasFailed(dft.getTopLevelIndex()) || state->isFailsafe(dft.getTopLevelIndex()) || state->nrFailableDependencies() > 0 || (state->nrFailableDependencies() == 0 && state->nrFailableBEs() == 0)) { // Do not skip absorbing state or if reached by dependencies iter->second.second->markExpand(); + // TODO Matthias give highest priority to ensure expanding before all skipped } - fixQueue = iter->second.second->updateHeuristicValues(currentExplorationHeuristic->getDepth() + 1, stateProbabilityPair.second, choice.getTotalMass()); } } matrixBuilder.finishRow(); } } - - // Update priority queue - if (fixQueue) { - explorationQueue.fix(); - } } // end exploration + std::cout << "Fixed queue " << fix << " times" << std::endl; STORM_LOG_INFO("Expanded " << nrExpandedStates << " states"); STORM_LOG_INFO("Skipped " << nrSkippedStates << " states"); @@ -502,9 +521,8 @@ namespace storm { stateId = stateStorage.stateToId.findOrAdd(state->status(), state->getId()); STORM_LOG_ASSERT(stateId == state->getId(), "Ids do not match."); // Insert state as not yet explored - ExplorationHeuristicPointer heuristic = std::make_shared(stateId); - statesNotExplored[stateId] = std::make_pair(state, heuristic); - explorationQueue.push(heuristic); + ExplorationHeuristicPointer nullHeuristic; + statesNotExplored[stateId] = std::make_pair(state, nullHeuristic); // Reserve one slot for the new state in the remapping matrixBuilder.stateRemapping.push_back(0); STORM_LOG_TRACE("New " << (state->isPseudoState() ? "pseudo" : "concrete") << " state: " << dft.getStateString(state)); @@ -521,6 +539,15 @@ namespace storm { modelComponents.markovianStates.set(matrixBuilder.getCurrentRowGroup() - 1, markovian); } + template + void ExplicitDFTModelBuilderApprox::printNotExplored() const { + std::cout << "states not explored:" << std::endl; + for (auto it : statesNotExplored) { + std::cout << it.first << " -> " << dft.getStateString(it.second.first) << std::endl; + } + } + + // Explicitly instantiate the class. template class ExplicitDFTModelBuilderApprox; diff --git a/src/builder/ExplicitDFTModelBuilderApprox.h b/src/builder/ExplicitDFTModelBuilderApprox.h index 4238194eb..e23a8e819 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.h +++ b/src/builder/ExplicitDFTModelBuilderApprox.h @@ -10,7 +10,7 @@ #include "src/storage/sparse/StateStorage.h" #include "src/storage/dft/DFT.h" #include "src/storage/dft/SymmetricUnits.h" -#include "src/storage/DynamicPriorityQueue.h" +#include "src/storage/BucketPriorityQueue.h" #include #include #include @@ -28,7 +28,7 @@ namespace storm { using DFTStatePointer = std::shared_ptr>; // TODO Matthias: make choosable - using ExplorationHeuristic = DFTExplorationHeuristicNone; + using ExplorationHeuristic = DFTExplorationHeuristicRateRatio; using ExplorationHeuristicPointer = std::shared_ptr; @@ -240,6 +240,8 @@ namespace storm { */ bool isPriorityGreater(StateType idA, StateType idB) const; + void printNotExplored() const; + /*! * Create the model model from the model components. * @@ -293,7 +295,8 @@ namespace storm { storm::storage::sparse::StateStorage stateStorage; // A priority queue of states that still need to be explored. - storm::storage::DynamicPriorityQueue, std::function> explorationQueue; + storm::storage::BucketPriorityQueue explorationQueue; + //storm::storage::DynamicPriorityQueue, std::function> explorationQueue; // A mapping of not yet explored states from the id to the tuple (state object, heuristic values). std::map> statesNotExplored; diff --git a/src/storage/BucketPriorityQueue.cpp b/src/storage/BucketPriorityQueue.cpp new file mode 100644 index 000000000..e87e25506 --- /dev/null +++ b/src/storage/BucketPriorityQueue.cpp @@ -0,0 +1,191 @@ +#include "src/storage/BucketPriorityQueue.h" +#include "src/utility/macros.h" +#include "src/adapters/CarlAdapter.h" + +namespace storm { + namespace storage { + + template + BucketPriorityQueue::BucketPriorityQueue(size_t nrBuckets, double lowerValue, double stepPerBucket) : buckets(nrBuckets), currentBucket(nrBuckets), lowerValue(lowerValue), stepPerBucket(stepPerBucket), nrUnsortedItems(0) { + compare = ([this](HeuristicPointer a, HeuristicPointer b) { + return *a < *b; + }); + } + + template + void BucketPriorityQueue::fix() { + if (currentBucket < buckets.size() && nrUnsortedItems > 0) { + // Fix current bucket + std::make_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare); + nrUnsortedItems = 0; + } + } + + template + bool BucketPriorityQueue::empty() const { + return currentBucket == buckets.size(); + } + + template + std::size_t BucketPriorityQueue::size() const { + size_t size = 0; + for (size_t i = currentBucket; currentBucket < buckets.size(); ++i) { + size += buckets[i].size(); + } + STORM_LOG_ASSERT(size == heuristicMapping.size(), "Sizes to not coincide"); + return size; + } + + template + typename BucketPriorityQueue::HeuristicPointer const& BucketPriorityQueue::top() const { + STORM_LOG_ASSERT(!empty(), "BucketPriorityQueue is empty"); + STORM_LOG_ASSERT(nrUnsortedItems == 0, "First bucket is not sorted"); + return buckets[currentBucket].front(); + } + + template + void BucketPriorityQueue::push(HeuristicPointer const& item) { + size_t bucket = getBucket(item->getPriority()); + if (bucket < currentBucket) { + setMappingBucket(currentBucket); + currentBucket = bucket; + nrUnsortedItems = 0; + } + buckets[bucket].push_back(item); + if (bucket == currentBucket) { + // Insert in first bucket + if (AUTOSORT) { + std::push_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare); + } else { + ++nrUnsortedItems; + } + } + // Set mapping + heuristicMapping[item->getId()] = std::make_pair(bucket, buckets[bucket].size() - 1); + } + + template + void BucketPriorityQueue::update(HeuristicPointer const& item, double oldPriority) { + size_t newBucket = getBucket(item->getPriority()); + size_t oldBucket = getBucket(oldPriority); + + if (oldBucket == newBucket) { + if (currentBucket < newBucket) { + // No change as the bucket is not sorted yet + } else { + if (AUTOSORT) { + // Sort first bucket + fix(); + } else { + ++nrUnsortedItems; + } + } + } else { + // Move to new bucket + STORM_LOG_ASSERT(newBucket < oldBucket, "Will update to higher bucket"); + if (newBucket < currentBucket) { + setMappingBucket(currentBucket); + currentBucket = newBucket; + nrUnsortedItems = 0; + } + // Remove old entry by swap-and-pop + if (buckets[oldBucket].size() >= 2) { + size_t oldIndex = heuristicMapping.at(item->getId()).second; + std::iter_swap(buckets[oldBucket].begin() + oldIndex, buckets[oldBucket].end() - 1); + // Set mapping for swapped item + heuristicMapping[buckets[oldBucket][oldIndex]->getId()] = std::make_pair(oldBucket, oldIndex); + } + buckets[oldBucket].pop_back(); + // Insert new element + buckets[newBucket].push_back(item); + if (newBucket == currentBucket) { + if (AUTOSORT) { + // Sort in first bucket + std::push_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare); + } else { + ++nrUnsortedItems; + } + } + // Set mapping + heuristicMapping[item->getId()] = std::make_pair(newBucket, buckets[newBucket].size() - 1); + } + } + + + template + void BucketPriorityQueue::pop() { + STORM_LOG_ASSERT(!empty(), "BucketPriorityQueue is empty"); + STORM_LOG_ASSERT(nrUnsortedItems == 0, "First bucket is not sorted"); + std::pop_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare); + // Remove from mapping + heuristicMapping.erase(buckets[currentBucket].back()->getId()); + buckets[currentBucket].pop_back(); + if (buckets[currentBucket].empty()) { + // Find next bucket with elements + for ( ; currentBucket < buckets.size(); ++currentBucket) { + if (!buckets[currentBucket].empty()) { + nrUnsortedItems = buckets[currentBucket].size(); + if (AUTOSORT) { + fix(); + } + break; + } + } + } + } + + template + typename BucketPriorityQueue::HeuristicPointer BucketPriorityQueue::popTop() { + HeuristicPointer item = top(); + pop(); + return item; + } + + template + size_t BucketPriorityQueue::getBucket(double priority) const { + STORM_LOG_ASSERT(priority >= lowerValue, "Priority " << priority << " is too low"); + size_t newBucket = (priority - lowerValue) / stepPerBucket; + if (HIGHER) { + newBucket = buckets.size()-1 - newBucket; + } + //std::cout << "get Bucket: " << priority << ", " << newBucket << ", " << ((priority - lowerValue) / stepPerBucket) << std::endl; + STORM_LOG_ASSERT(newBucket < buckets.size(), "Priority " << priority << " is too high"); + return newBucket; + } + + template + void BucketPriorityQueue::setMappingBucket(size_t bucket) { + if (bucket < buckets.size()) { + for (size_t index = 0; index < buckets[bucket].size(); ++index) { + heuristicMapping[buckets[bucket][index]->getId()] = std::make_pair(bucket, index); + } + } + } + + template + void BucketPriorityQueue::print(std::ostream& out) const { + out << "Bucket priority queue with size " << buckets.size() << ", lower value: " << lowerValue << " and step per bucket: " << stepPerBucket << 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 << " (" << (HIGHER ? buckets.size() -1 - bucket * stepPerBucket : bucket * stepPerBucket) << "):" << std::endl; + for (HeuristicPointer heuristic : buckets[bucket]) { + out << "\t" << heuristic->getId() << ": " << heuristic->getPriority() << std::endl; + } + } + } + out << "Mapping:" << std::endl; + for (auto it : heuristicMapping) { + out << it.first << " -> " << it.second.first << ", " << it.second.second << std::endl; + } + } + + + // Template instantiations + template class BucketPriorityQueue; + +#ifdef STORM_HAVE_CARL + template class BucketPriorityQueue; +#endif + } +} diff --git a/src/storage/BucketPriorityQueue.h b/src/storage/BucketPriorityQueue.h new file mode 100644 index 000000000..a08bfbd3b --- /dev/null +++ b/src/storage/BucketPriorityQueue.h @@ -0,0 +1,70 @@ +#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 stepPerBucket); + + 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; + + private: + + size_t getBucket(double priority) const; + + void setMappingBucket(size_t bucket); + + // List of buckets + std::vector> buckets; + + // Index of first bucket which contains items + size_t currentBucket; + + // Mapping from id to (bucket, index in bucket) + std::unordered_map> heuristicMapping; + + std::function compare; + + double lowerValue; + + double stepPerBucket; + + size_t nrUnsortedItems; + + const bool HIGHER = true; + + const bool AUTOSORT = false; + }; + + } +} + +#endif // STORM_STORAGE_BUCKETPRIORITYQUEUE_H_