Use BucketPriorityQueue instead of DynamicPriorityQueue

Former-commit-id: 7a22ef5b16

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<>

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
             }
 

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>;
 

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;

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
+    }
+}

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_