Only fix queue when needed

Former-commit-id: 50231c4554

src/builder/DftExplorationHeuristic.cpp

@@ -14,69 +14,34 @@ namespace storm {
             // Intentionally left empty
         }
 
-        template<typename ValueType>
-        void DFTExplorationHeuristic<ValueType>::updateHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) {
-            this->depth = std::min(this->depth, depth);
-            this->rate = std::max(this->rate, rate);
-            this->exitRate = std::max(this->exitRate, exitRate);
-        }
-
-        template<typename ValueType>
-        DFTExplorationHeuristicNone<ValueType>::DFTExplorationHeuristicNone(size_t id) : DFTExplorationHeuristic<ValueType>(id) {
-            // Intentionally left empty
-        }
-
-        template<typename ValueType>
-        bool DFTExplorationHeuristicNone<ValueType>::isSkip(double approximationThreshold) const {
-            return false;
-        }
-
-        template<typename ValueType>
-        bool DFTExplorationHeuristicNone<ValueType>::operator<(DFTExplorationHeuristicNone<ValueType> const& other) const {
-            // Just use memory address for comparing
-            // TODO Matthias: better idea?
-            return this > &other;
-        }
-
-        template<typename ValueType>
-        DFTExplorationHeuristicDepth<ValueType>::DFTExplorationHeuristicDepth(size_t id) : DFTExplorationHeuristic<ValueType>(id) {
-            // Intentionally left empty
-        }
-
-        template<typename ValueType>
-        bool DFTExplorationHeuristicDepth<ValueType>::isSkip(double approximationThreshold) const {
-            return !this->expand && this->depth > approximationThreshold;
-        }
-
-        template<typename ValueType>
-        bool DFTExplorationHeuristicDepth<ValueType>::operator<(DFTExplorationHeuristicDepth<ValueType> const& other) const {
-            return this->depth > other.depth;
+        template<>
+        bool DFTExplorationHeuristicRateRatio<double>::updateHeuristicValues(size_t depth, double rate, double exitRate) {
+            bool update = false;
+            if (this->rate < rate) {
+                this->rate = rate;
+                update = true;
             }
-
-        template<typename ValueType>
-        DFTExplorationHeuristicRateRatio<ValueType>::DFTExplorationHeuristicRateRatio(size_t id) : DFTExplorationHeuristic<ValueType>(id) {
-            // Intentionally left empty
+            if (this->exitRate < exitRate) {
+                this->exitRate = exitRate;
+                update = true;
             }
-
-        template<typename ValueType>
-        bool DFTExplorationHeuristicRateRatio<ValueType>::isSkip(double approximationThreshold) const {
-            return !this->expand && this->getRateRatio() < approximationThreshold;
+            return update;
         }
 
-        template<typename ValueType>
-        bool DFTExplorationHeuristicRateRatio<ValueType>::operator<(DFTExplorationHeuristicRateRatio<ValueType> const& other) const {
-            return this->getRateRatio() < other.getRateRatio();
+        template<>
+        bool DFTExplorationHeuristicRateRatio<storm::RationalFunction>::updateHeuristicValues(size_t depth, storm::RationalFunction rate, storm::RationalFunction exitRate) {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic rate ration does not work for rational functions.");
+            return false;
         }
 
-
         template<>
-        double DFTExplorationHeuristicRateRatio<double>::getRateRatio() const {
+        double DFTExplorationHeuristicRateRatio<double>::getPriority() const {
             return rate/exitRate;
         }
 
         template<>
-        double DFTExplorationHeuristicRateRatio<storm::RationalFunction>::getRateRatio() const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic rate ration does not work.");
+        double DFTExplorationHeuristicRateRatio<storm::RationalFunction>::getPriority() const {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic rate ration does not work for rational functions.");
         }
 
 

src/builder/DftExplorationHeuristic.h

@@ -22,7 +22,9 @@ namespace storm {
         public:
             DFTExplorationHeuristic(size_t id);
 
-            void updateHeuristicValues(size_t depth, ValueType rate, ValueType exitRate);
+            virtual bool updateHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) = 0;
+
+            virtual double getPriority() const = 0;
 
             virtual bool isSkip(double approximationThreshold) const = 0;
 
@@ -50,34 +52,74 @@ namespace storm {
         template<typename ValueType>
         class DFTExplorationHeuristicNone : public DFTExplorationHeuristic<ValueType> {
         public:
-            DFTExplorationHeuristicNone(size_t id);
+            DFTExplorationHeuristicNone(size_t id) : DFTExplorationHeuristic<ValueType>(id) {
+                // Intentionally left empty
+            }
+
+            bool updateHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) override {
+                return false;
+            }
 
-            bool isSkip(double approximationThreshold) const override;
+            double getPriority() const override {
+                return this->id;
+            }
 
-            bool operator<(DFTExplorationHeuristicNone<ValueType> const& other) const;
+            bool isSkip(double approximationThreshold) const override {
+                return false;
+            }
+
+            bool operator<(DFTExplorationHeuristicNone<ValueType> const& other) const {
+                return this->id > other.id;
+            }
         };
 
         template<typename ValueType>
         class DFTExplorationHeuristicDepth : public DFTExplorationHeuristic<ValueType> {
         public:
-            DFTExplorationHeuristicDepth(size_t id);
+            DFTExplorationHeuristicDepth(size_t id) : DFTExplorationHeuristic<ValueType>(id) {
+                // Intentionally left empty
+            }
 
-            bool isSkip(double approximationThreshold) const override;
+            bool updateHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) override {
+                if (depth < this->depth) {
+                    this->depth = depth;
+                    return true;
+                }
+                return false;
+            }
 
-            bool operator<(DFTExplorationHeuristicDepth<ValueType> const& other) const;
+
+            double getPriority() const override {
+                return this->depth;
+            }
+
+            bool isSkip(double approximationThreshold) const override {
+                return !this->expand && this->depth > approximationThreshold;
+            }
+
+            bool operator<(DFTExplorationHeuristicDepth<ValueType> const& other) const {
+                return this->depth > other.depth;
+            }
         };
 
         template<typename ValueType>
         class DFTExplorationHeuristicRateRatio : public DFTExplorationHeuristic<ValueType> {
         public:
-            DFTExplorationHeuristicRateRatio(size_t id);
+            DFTExplorationHeuristicRateRatio(size_t id) : DFTExplorationHeuristic<ValueType>(id) {
+                // Intentionally left empty
+            }
 
-            bool isSkip(double approximationThreshold) const override;
+            bool updateHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) override;
 
-            bool operator<(DFTExplorationHeuristicRateRatio<ValueType> const& other) const;
+            double getPriority() const override;
 
-        private:
-            double getRateRatio() const;
+            bool isSkip(double approximationThreshold) const override {
+                return !this->expand && this->getPriority() < approximationThreshold;
+            }
+
+            bool operator<(DFTExplorationHeuristicRateRatio<ValueType> const& other) const {
+                return this->getPriority() < other.getPriority();
+            }
         };
 
     }

src/builder/ExplicitDFTModelBuilderApprox.cpp

@@ -290,8 +290,7 @@ namespace storm {
                                     // Do not skip absorbing state or if reached by dependencies
                                     iter->second.second->markExpand();
                                 }
-                                iter->second.second->updateHeuristicValues(currentExplorationHeuristic->getDepth() + 1, stateProbabilityPair.second, choice.getTotalMass());
-                                fixQueue = true;
+                                fixQueue = iter->second.second->updateHeuristicValues(currentExplorationHeuristic->getDepth() + 1, stateProbabilityPair.second, choice.getTotalMass());
                             }
                         }
                         matrixBuilder.finishRow();