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 <limits>
-
namespace storm {
namespace builder {
template<typename ValueType>
- DFTExplorationHeuristic<ValueType>::DFTExplorationHeuristic(size_t id) : id(id), expand(false), depth(std::numeric_limits<std::size_t>::max()), rate(storm::utility::zero<ValueType>()), exitRate(storm::utility::zero<ValueType>()) {
- // Intentionally left empty
+ DFTExplorationHeuristic<ValueType>::DFTExplorationHeuristic(size_t id, size_t depth, ValueType rate, ValueType exitRate) : id(id), expand(false), depth(depth) {
+ STORM_LOG_ASSERT(storm::utility::zero<ValueType>() < exitRate, "Exit rate is 0");
+ rateRatio = rate/exitRate;
}
template<>
bool DFTExplorationHeuristicRateRatio<double>::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<double>::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<typename ValueType>
class DFTExplorationHeuristicNone : public DFTExplorationHeuristic<ValueType> {
public:
- DFTExplorationHeuristicNone(size_t id) : DFTExplorationHeuristic<ValueType>(id) {
+ DFTExplorationHeuristicNone(size_t id, size_t depth, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic<ValueType>(id, depth, rate, exitRate) {
// Intentionally left empty
}
@@ -76,7 +74,7 @@ namespace storm {
template<typename ValueType>
class DFTExplorationHeuristicDepth : public DFTExplorationHeuristic<ValueType> {
public:
- DFTExplorationHeuristicDepth(size_t id) : DFTExplorationHeuristic<ValueType>(id) {
+ DFTExplorationHeuristicDepth(size_t id, size_t depth, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic<ValueType>(id, depth, rate, exitRate) {
// Intentionally left empty
}
@@ -105,7 +103,7 @@ namespace storm {
template<typename ValueType>
class DFTExplorationHeuristicRateRatio : public DFTExplorationHeuristic<ValueType> {
public:
- DFTExplorationHeuristicRateRatio(size_t id) : DFTExplorationHeuristic<ValueType>(id) {
+ DFTExplorationHeuristicRateRatio(size_t id, size_t depth, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic<ValueType>(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<typename ValueType, typename StateType>
@@ -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<ValueType>(), storm::utility::zero<ValueType>());
+ STORM_LOG_ASSERT(!statesNotExplored.at(initialStateIndex).second, "Heuristic for initial state is already initialized");
+ ExplorationHeuristicPointer heuristic = std::make_shared<ExplorationHeuristic>(initialStateIndex, 0, storm::utility::zero<ValueType>(), storm::utility::one<ValueType>());
+ 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<ValueType, StateType>::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<ExplorationHeuristic>(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<ExplorationHeuristic>(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<typename ValueType, typename StateType>
+ void ExplicitDFTModelBuilderApprox<ValueType, StateType>::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<double>;
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 <boost/container/flat_set.hpp>
#include <boost/optional/optional.hpp>
#include <stack>
@@ -28,7 +28,7 @@ namespace storm {
using DFTStatePointer = std::shared_ptr<storm::storage::DFTState<ValueType>>;
// TODO Matthias: make choosable
- using ExplorationHeuristic = DFTExplorationHeuristicNone<ValueType>;
+ using ExplorationHeuristic = DFTExplorationHeuristicRateRatio<ValueType>;
using ExplorationHeuristicPointer = std::shared_ptr<ExplorationHeuristic>;
@@ -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<StateType> stateStorage;
// A priority queue of states that still need to be explored.
- storm::storage::DynamicPriorityQueue<ExplorationHeuristicPointer, std::vector<ExplorationHeuristicPointer>, std::function<bool(ExplorationHeuristicPointer, ExplorationHeuristicPointer)>> explorationQueue;
+ storm::storage::BucketPriorityQueue<ValueType> explorationQueue;
+ //storm::storage::DynamicPriorityQueue<ExplorationHeuristicPointer, std::vector<ExplorationHeuristicPointer>, std::function<bool(ExplorationHeuristicPointer, ExplorationHeuristicPointer)>> explorationQueue;
// A mapping of not yet explored states from the id to the tuple (state object, heuristic values).
std::map<StateType, std::pair<DFTStatePointer, ExplorationHeuristicPointer>> 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<typename ValueType>
+ BucketPriorityQueue<ValueType>::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<typename ValueType>
+ void BucketPriorityQueue<ValueType>::fix() {
+ if (currentBucket < buckets.size() && nrUnsortedItems > 0) {
+ // Fix current bucket
+ std::make_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare);
+ nrUnsortedItems = 0;
+ }
+ }
+
+ template<typename ValueType>
+ bool BucketPriorityQueue<ValueType>::empty() const {
+ return currentBucket == buckets.size();
+ }
+
+ template<typename ValueType>
+ std::size_t BucketPriorityQueue<ValueType>::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 ValueType>
+ typename BucketPriorityQueue<ValueType>::HeuristicPointer const& BucketPriorityQueue<ValueType>::top() const {
+ STORM_LOG_ASSERT(!empty(), "BucketPriorityQueue is empty");
+ STORM_LOG_ASSERT(nrUnsortedItems == 0, "First bucket is not sorted");
+ return buckets[currentBucket].front();
+ }
+
+ template<typename ValueType>
+ void BucketPriorityQueue<ValueType>::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<typename ValueType>
+ void BucketPriorityQueue<ValueType>::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<typename ValueType>
+ void BucketPriorityQueue<ValueType>::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 ValueType>
+ typename BucketPriorityQueue<ValueType>::HeuristicPointer BucketPriorityQueue<ValueType>::popTop() {
+ HeuristicPointer item = top();
+ pop();
+ return item;
+ }
+
+ template<typename ValueType>
+ size_t BucketPriorityQueue<ValueType>::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<typename ValueType>
+ void BucketPriorityQueue<ValueType>::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<typename ValueType>
+ void BucketPriorityQueue<ValueType>::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<double>;
+
+#ifdef STORM_HAVE_CARL
+ template class BucketPriorityQueue<storm::RationalFunction>;
+#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 <algorithm>
+#include <functional>
+#include <unordered_map>
+#include <vector>
+
+namespace storm {
+ namespace storage {
+
+ template<typename ValueType>
+ class BucketPriorityQueue {
+
+ using HeuristicPointer = std::shared_ptr<storm::builder::DFTExplorationHeuristicRateRatio<ValueType>>;
+
+ 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<std::vector<HeuristicPointer>> buckets;
+
+ // Index of first bucket which contains items
+ size_t currentBucket;
+
+ // Mapping from id to (bucket, index in bucket)
+ std::unordered_map<size_t, std::pair<size_t, size_t>> heuristicMapping;
+
+ std::function<bool(HeuristicPointer, HeuristicPointer)> compare;
+
+ double lowerValue;
+
+ double stepPerBucket;
+
+ size_t nrUnsortedItems;
+
+ const bool HIGHER = true;
+
+ const bool AUTOSORT = false;
+ };
+
+ }
+}
+
+#endif // STORM_STORAGE_BUCKETPRIORITYQUEUE_H_