Use custom DynamicPriorityQueue

Former-commit-id: b4b552a84d

src/builder/ExplicitDFTModelBuilderApprox.cpp

@@ -23,14 +23,17 @@ namespace storm {
         }
 
         template<typename ValueType, typename StateType>
-        ExplicitDFTModelBuilderApprox<ValueType, StateType>::ExplicitDFTModelBuilderApprox(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) : dft(dft), stateGenerationInfo(std::make_shared<storm::storage::DFTStateGenerationInfo>(dft.buildStateGenerationInfo(symmetries))), enableDC(enableDC), generator(dft, *stateGenerationInfo, enableDC, mergeFailedStates), matrixBuilder(!generator.isDeterministicModel()), stateStorage(((dft.stateVectorSize() / 64) + 1) * 64) {
+        ExplicitDFTModelBuilderApprox<ValueType, StateType>::ExplicitDFTModelBuilderApprox(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) :
+                dft(dft),
+                stateGenerationInfo(std::make_shared<storm::storage::DFTStateGenerationInfo>(dft.buildStateGenerationInfo(symmetries))),
+                enableDC(enableDC),
+                generator(dft, *stateGenerationInfo, enableDC, mergeFailedStates),
+                matrixBuilder(!generator.isDeterministicModel()),
+                stateStorage(((dft.stateVectorSize() / 64) + 1) * 64),
+                statesToExplore(storm::storage::DynamicPriorityQueue<DFTStatePointer, std::vector<DFTStatePointer>, std::function<bool(DFTStatePointer, DFTStatePointer)>>(&storm::builder::compareDepth<ValueType>))
+        {
             // stateVectorSize is bound for size of bitvector
-
             heuristic = storm::settings::getModule<storm::settings::modules::DFTSettings>().getApproximationHeuristic();
-
-            // Compare states by their distance from the initial state
-            // TODO Matthias: customize
-            statesToExplore = std::priority_queue<DFTStatePointer, std::deque<DFTStatePointer>, std::function<bool(DFTStatePointer, DFTStatePointer)>>(&storm::builder::compareDepth<ValueType>);
         }
 
         template<typename ValueType, typename StateType>
@@ -279,6 +282,9 @@ namespace storm {
                     }
                 }
 
+                // Update priority queue
+                statesToExplore.fix();
+
                 if (statesToExplore.empty()) {
                     explorationFinished = true;
                     // Before ending the exploration check for pseudo states which are not initialized yet

src/builder/ExplicitDFTModelBuilderApprox.h

@@ -10,6 +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 <boost/container/flat_set.hpp>
 #include <boost/optional/optional.hpp>
 #include <stack>
@@ -286,7 +287,7 @@ namespace storm {
             storm::storage::sparse::StateStorage<StateType> stateStorage;
 
             // A pniority queue of states that still need to be explored.
-            std::priority_queue<DFTStatePointer, std::deque<DFTStatePointer>, std::function<bool(DFTStatePointer, DFTStatePointer)>> statesToExplore;
+            storm::storage::DynamicPriorityQueue<DFTStatePointer, std::vector<DFTStatePointer>, std::function<bool(DFTStatePointer, DFTStatePointer)>> statesToExplore;
 
             // Holds all skipped states which were not yet expanded. More concretely it is a mapping from matrix indices
             // to the corresponding skipped states.

src/storage/DynamicPriorityQueue.h

@@ -0,0 +1,67 @@
+#ifndef STORM_STORAGE_DYNAMICPRIORITYQUEUE_H_
+#define STORM_STORAGE_DYNAMICPRIORITYQUEUE_H_
+
+#include <algorithm>
+#include <vector>
+
+namespace storm {
+    namespace storage {
+
+        template<typename T, typename Container = std::vector<T>, typename Compare = std::less<T>>
+        class DynamicPriorityQueue {
+
+        private:
+            Container container;
+            Compare compare;
+
+        public:
+            explicit DynamicPriorityQueue(const Compare& compare) : container(), compare(compare) {
+                // Intentionally left empty
+            }
+
+            explicit DynamicPriorityQueue(Container&& container, const Compare& compare) : container(std::move(container)), compare(compare) {
+                std::make_heap(container.begin(), container.end(), compare);
+            }
+
+            void fix() {
+                std::make_heap(container.begin(), container.end(), compare);
+            }
+
+            bool empty() const {
+                return container.empty();
+            }
+
+            std::size_t size() const {
+                return container.size();
+            }
+
+            const T& top() const {
+                return container.front();
+            }
+
+            void push(const T& item) {
+                container.push_back(item);
+                std::push_heap(container.begin(), container.end(), compare);
+            }
+
+            void push(T&& item) {
+                container.push_back(std::move(item));
+                std::push_heap(container.begin(), container.end(), compare);
+            }
+
+            void pop() {
+                std::pop_heap(container.begin(), container.end(), compare);
+                container.pop_back();
+            }
+
+            T popTop() {
+                T item = top();
+                pop();
+                return item;
+            }
+
+        };
+    }
+}
+
+#endif // STORM_STORAGE_DYNAMICPRIORITYQUEUE_H_