Merge branch 'dft-approximation' of https://sselab.de/lab9/private/git/storm into dft-approximation

Former-commit-id: feef06888a

src/builder/DftExplorationHeuristic.cpp

@@ -47,9 +47,29 @@ namespace storm {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic rate ration does not work for rational functions.");
         }
 
+        template<>
+        bool DFTExplorationHeuristicBoundDifference<double>::updateHeuristicValues(DFTExplorationHeuristic<double> const& predecessor, double rate, double exitRate) {
+            STORM_LOG_ASSERT(exitRate > 0, "Exit rate is 0");
+            probability += predecessor.getProbability() * rate/exitRate;
+            return true;
+        }
+
+        template<>
+        bool DFTExplorationHeuristicBoundDifference<storm::RationalFunction>::updateHeuristicValues(DFTExplorationHeuristic<storm::RationalFunction> const& predecessor, 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<typename ValueType>
+        void DFTExplorationHeuristicBoundDifference<ValueType>::setBounds(ValueType lowerBound, ValueType upperBound) {
+            this->lowerBound = lowerBound;
+            this->upperBound = upperBound;
+            difference = (storm::utility::one<ValueType>() / upperBound) - (storm::utility::one<ValueType>() / lowerBound);
+        }
+
         template<>
         double DFTExplorationHeuristicBoundDifference<double>::getPriority() const {
-            return upperBound / lowerBound;
+            return probability * difference;
         }
 
         template<>

src/builder/DftExplorationHeuristic.h

@@ -10,7 +10,7 @@ namespace storm {
         /*!
          * Enum representing the heuristic used for deciding which states to expand.
          */
-        enum class ApproximationHeuristic { NONE, DEPTH, PROBABILITY };
+        enum class ApproximationHeuristic { NONE, DEPTH, PROBABILITY, BOUNDDIFFERENCE };
 
 
         /*!
@@ -165,9 +165,9 @@ namespace storm {
                 // Intentionally left empty
             }
 
-            bool updateHeuristicValues(DFTExplorationHeuristic<ValueType> const& predecessor, ValueType rate, ValueType exitRate) override {
-                return false;
-            }
+            void setBounds(ValueType lowerBound, ValueType upperBound);
+
+            bool updateHeuristicValues(DFTExplorationHeuristic<ValueType> const& predecessor, ValueType rate, ValueType exitRate) override;
 
             double getPriority() const override;
 
@@ -180,8 +180,7 @@ namespace storm {
             }
 
         private:
-            ValueType lowerBound;
-            ValueType upperBound;
+            ValueType difference;
         };
 
 

src/builder/ExplicitDFTModelBuilderApprox.cpp

@@ -28,7 +28,7 @@ namespace storm {
                 dft(dft),
                 stateGenerationInfo(std::make_shared<storm::storage::DFTStateGenerationInfo>(dft.buildStateGenerationInfo(symmetries))),
                 enableDC(enableDC),
-                heuristic(storm::settings::getModule<storm::settings::modules::DFTSettings>().getApproximationHeuristic()),
+                usedHeuristic(storm::settings::getModule<storm::settings::modules::DFTSettings>().getApproximationHeuristic()),
                 generator(dft, *stateGenerationInfo, enableDC, mergeFailedStates),
                 matrixBuilder(!generator.isDeterministicModel()),
                 stateStorage(((dft.stateVectorSize() / 64) + 1) * 64),
@@ -38,7 +38,7 @@ namespace storm {
         {
             // Intentionally left empty.
             // TODO Matthias: remove again
-            heuristic = storm::builder::ApproximationHeuristic::PROBABILITY;
+            usedHeuristic = storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE;
 
             // Compute independent subtrees
             if (dft.topLevelType() == storm::storage::DFTElementType::OR) {
@@ -144,7 +144,7 @@ namespace storm {
             }
 
             if (approximationThreshold > 0) {
-                switch (heuristic) {
+                switch (usedHeuristic) {
                     case storm::builder::ApproximationHeuristic::NONE:
                         // Do not change anything
                         approximationThreshold = dft.nrElements()+10;
@@ -153,6 +153,7 @@ namespace storm {
                         approximationThreshold = iteration;
                         break;
                     case storm::builder::ApproximationHeuristic::PROBABILITY:
+                    case storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE:
                         approximationThreshold = 10 * std::pow(2, iteration);
                         break;
                 }
@@ -360,6 +361,20 @@ namespace storm {
                                         // Do not skip absorbing state or if reached by dependencies
                                         iter->second.second->markExpand();
                                     }
+                                    if (usedHeuristic == storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE) {
+                                        // Compute bounds for heuristic now
+                                        if (state->isPseudoState()) {
+                                            // Create concrete state from pseudo state
+                                            state->construct();
+                                        }
+                                        STORM_LOG_ASSERT(!currentState->isPseudoState(), "State is pseudo state.");
+
+                                        // Initialize bounds
+                                        ValueType lowerBound = getLowerBound(state);
+                                        ValueType upperBound = getUpperBound(state);
+                                        heuristic->setBounds(lowerBound, upperBound);
+                                    }
+
                                     explorationQueue.push(heuristic);
                                 } else if (!iter->second.second->isExpand()) {
                                     double oldPriority = iter->second.second->getPriority();
@@ -567,9 +582,11 @@ namespace storm {
                 for (size_t i = 0; i < rates.size(); ++i) {
                     // Cold BEs cannot fail in the first step
                     if (!coldBEs.get(i) && rateCount[i] > 0) {
+                        std::iter_swap(rates.begin() + i, rates.end() - 1);
                         // Compute AND MTTF of subtree without current rate and scale with current rate
                         upperBound += rates.back() * rateCount[i] * computeMTTFAnd(rates, rates.size() - 1);
-                        // Swap here to avoid swapping back
+                        // Swap back
+                        // TODO try to avoid swapping back
                         std::iter_swap(rates.begin() + i, rates.end() - 1);
                     }
                 }

src/builder/ExplicitDFTModelBuilderApprox.h

@@ -28,7 +28,7 @@ namespace storm {
 
             using DFTStatePointer = std::shared_ptr<storm::storage::DFTState<ValueType>>;
             // TODO Matthias: make choosable
-            using ExplorationHeuristic = DFTExplorationHeuristicProbability<ValueType>;
+            using ExplorationHeuristic = DFTExplorationHeuristicBoundDifference<ValueType>;
             using ExplorationHeuristicPointer = std::shared_ptr<ExplorationHeuristic>;
 
 
@@ -289,7 +289,7 @@ namespace storm {
             const bool mergeFailedStates = true;
 
             // Heuristic used for approximation
-            storm::builder::ApproximationHeuristic heuristic;
+            storm::builder::ApproximationHeuristic usedHeuristic;
 
             // Current id for new state
             size_t newIndex = 0;

src/storage/BucketPriorityQueue.cpp

@@ -153,7 +153,16 @@ namespace storm {
         template<typename ValueType>
         size_t BucketPriorityQueue<ValueType>::getBucket(double priority) const {
             STORM_LOG_ASSERT(priority >= lowerValue, "Priority " << priority << " is too low");
-            size_t newBucket = std::log(priority - lowerValue) / logBase;
+
+            // For possible values greater 1
+            double tmpBucket = std::log(priority - lowerValue) / logBase;
+            tmpBucket += buckets.size() / 2;
+            if (tmpBucket < 0) {
+                tmpBucket = 0;
+            }
+            size_t newBucket = tmpBucket;
+            // For values ensured to be lower 1
+            //size_t newBucket = std::log(priority - lowerValue) / logBase;
             if (newBucket >= nrBuckets) {
                 newBucket = nrBuckets - 1;
             }

src/storage/BucketPriorityQueue.h

@@ -13,7 +13,7 @@ namespace storm {
         template<typename ValueType>
         class BucketPriorityQueue {
 
-            using HeuristicPointer = std::shared_ptr<storm::builder::DFTExplorationHeuristicProbability<ValueType>>;
+            using HeuristicPointer = std::shared_ptr<storm::builder::DFTExplorationHeuristicBoundDifference<ValueType>>;
 
         public:
             explicit BucketPriorityQueue(size_t nrBuckets, double lowerValue, double ratio);