Choose different approximation heuristics

Former-commit-id: e9ddae066b

src/builder/DftExplorationHeuristic.cpp

@@ -15,6 +15,13 @@ namespace storm {
             // Intentionally left empty
         }
 
+        template<typename ValueType>
+        void DFTExplorationHeuristic<ValueType>::setHeuristicValues(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>
         bool DFTExplorationHeuristic<ValueType>::isSkip(double approximationThreshold, ApproximationHeuristic heuristic) const {
             if (!skip) {
@@ -26,8 +33,9 @@ namespace storm {
                 case ApproximationHeuristic::DEPTH:
                     return depth > approximationThreshold;
                 case ApproximationHeuristic::RATERATIO:
-                    // TODO Matthias: implement
-                    STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic rate ration does not work.");
+                    return getRateRatio() < approximationThreshold;
+                default:
+                    STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic not known.");
             }
         }
 
@@ -36,52 +44,41 @@ namespace storm {
             skip = false;
         }
 
-
         template<typename ValueType>
         size_t DFTExplorationHeuristic<ValueType>::getDepth() const {
             return depth;
         }
 
         template<typename ValueType>
-        void DFTExplorationHeuristic<ValueType>::setHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) {
-            this->depth = depth;
-            this->rate = rate;
-            this->exitRate = exitRate;
-        }
-
-        template<typename ValueType>
-        double DFTExplorationHeuristic<ValueType>::getPriority() const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Approximation works only for double.");
+        bool DFTExplorationHeuristic<ValueType>::compare(DFTExplorationHeuristic<ValueType> other, ApproximationHeuristic heuristic) {
+            switch (heuristic) {
+                case ApproximationHeuristic::NONE:
+                    // Just use memory address for comparing
+                    // TODO Matthias: better idea?
+                    return this > &other;
+                case ApproximationHeuristic::DEPTH:
+                    return this->depth > other.depth;
+                case ApproximationHeuristic::RATERATIO:
+                    return this->getRateRatio() < other.getRateRatio();
+                default:
+                    STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic not known.");
+            }
         }
 
         template<>
-        double DFTExplorationHeuristic<double>::getPriority() const {
-            // TODO Matthias: change according to heuristic
-            //return rate/exitRate;
-            return depth;
+        double DFTExplorationHeuristic<double>::getRateRatio() const {
+            return rate/exitRate;
         }
 
         template<>
-        double DFTExplorationHeuristic<storm::RationalFunction>::getPriority() const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Approximation works only for double.");
-            /*std::cout << (rate / exitRate) << " < " << threshold << ": " << (number < threshold) << std::endl;
-             std::map<storm::Variable, storm::RationalNumber> mapping;
-             storm::RationalFunction eval(number.evaluate(mapping));
-             std::cout << "Evaluated: " << eval << std::endl;
-             return eval < threshold;*/
-        }
-
-        template<typename ValueType>
-        bool compareDepth(std::shared_ptr<storm::storage::DFTState<ValueType>> stateA, std::shared_ptr<storm::storage::DFTState<ValueType>> stateB) {
-            return stateA->getPriority() > stateB->getPriority();
+        double DFTExplorationHeuristic<storm::RationalFunction>::getRateRatio() const {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic rate ration does not work.");
         }
 
         template class DFTExplorationHeuristic<double>;
-        template bool compareDepth(std::shared_ptr<storm::storage::DFTState<double>>, std::shared_ptr<storm::storage::DFTState<double>>);
 
 #ifdef STORM_HAVE_CARL
         template class DFTExplorationHeuristic<storm::RationalFunction>;
-        template bool compareDepth(std::shared_ptr<storm::storage::DFTState<storm::RationalFunction>>, std::shared_ptr<storm::storage::DFTState<storm::RationalFunction>>);
 #endif
     }
 }

src/builder/DftExplorationHeuristic.h

@@ -33,19 +33,18 @@ namespace storm {
 
             size_t getDepth() const;
 
-            double getPriority() const;
-            
+            bool compare(DFTExplorationHeuristic<ValueType> other, ApproximationHeuristic heuristic);
+
         private:
 
+            double getRateRatio() const;
+
             bool skip;
             size_t depth;
             ValueType rate;
             ValueType exitRate;
 
         };
-
-        template<typename ValueType>
-        bool compareDepth(std::shared_ptr<storm::storage::DFTState<ValueType>> stateA, std::shared_ptr<storm::storage::DFTState<ValueType>> stateB);
     }
 }
 

src/builder/ExplicitDFTModelBuilderApprox.cpp

@@ -39,10 +39,10 @@ namespace storm {
         }
 
         template<typename ValueType, typename StateType>
-        void ExplicitDFTModelBuilderApprox<ValueType, StateType>::buildModel(LabelOptions const& labelOpts, bool firstTime, double approximationThreshold) {
+        void ExplicitDFTModelBuilderApprox<ValueType, StateType>::buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold) {
             STORM_LOG_TRACE("Generating DFT state space");
 
-            if (firstTime) {
+            if (iteration < 1) {
                 // Initialize
                 modelComponents.markovianStates = storm::storage::BitVector(INITIAL_BITVECTOR_SIZE);
 
@@ -80,6 +80,14 @@ namespace storm {
                 initializeNextIteration();
             }
 
+            switch (heuristic) {
+                case storm::builder::ApproximationHeuristic::DEPTH:
+                    approximationThreshold = iteration;
+                    break;
+                case storm::builder::ApproximationHeuristic::RATERATIO:
+                    approximationThreshold = std::pow(0.1, iteration) * approximationThreshold;
+                    break;
+            }
             exploreStateSpace(approximationThreshold);
 
             size_t stateSize = stateStorage.getNumberOfStates() + (mergeFailedStates ? 1 : 0);
@@ -486,8 +494,7 @@ namespace storm {
 
         template<typename ValueType, typename StateType>
         bool ExplicitDFTModelBuilderApprox<ValueType, StateType>::isPriorityGreater(StateType idA, StateType idB) const {
-            // TODO Matthias: compare directly and according to heuristic
-            return storm::builder::compareDepth(statesNotExplored.at(idA), statesNotExplored.at(idB));
+            return statesNotExplored.at(idA)->comparePriority(statesNotExplored.at(idB), heuristic);
         }
 
 

src/builder/ExplicitDFTModelBuilderApprox.h

@@ -159,10 +159,10 @@ namespace storm {
              * Build model from DFT.
              *
              * @param labelOpts              Options for labeling.
-             * @param firstTime              Flag indicating if the model is built for the first time or rebuilt.
+             * @param iteration              Current number of iteration.
              * @param approximationThreshold Threshold determining when to skip exploring states.
              */
-            void buildModel(LabelOptions const& labelOpts, bool firstTime, double approximationThreshold = 0.0);
+            void buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold = 0.0);
 
             /*!
              * Get the built model.

src/modelchecker/dft/DFTModelChecker.cpp

@@ -150,7 +150,6 @@ namespace storm {
                 // Comparator for checking the error of the approximation
                 storm::utility::ConstantsComparator<ValueType> comparator;
                 // Build approximate Markov Automata for lower and upper bound
-                double currentApproximationError = approximationError;
                 approximation_result approxResult = std::make_pair(storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>());
                 std::chrono::high_resolution_clock::time_point explorationStart;
                 std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
@@ -163,8 +162,7 @@ namespace storm {
                     explorationStart = std::chrono::high_resolution_clock::now();
                     STORM_LOG_INFO("Building model...");
                     // TODO Matthias refine model using existing model and MC results
-                    currentApproximationError = pow(0.1, iteration) * approximationError;
-                    builder.buildModel(labeloptions, iteration < 1, iteration);
+                    builder.buildModel(labeloptions, iteration, approximationError);
 
                     // TODO Matthias: possible to do bisimulation on approximated model and not on concrete one?
 

src/storage/dft/DFTState.h

@@ -139,10 +139,10 @@ namespace storm {
                 return exploreHeuristic.isSkip(approximationThreshold, heuristic);
             }
 
-            double getPriority() const {
-                return exploreHeuristic.getPriority();
+            bool comparePriority(std::shared_ptr<DFTState> const& other, storm::builder::ApproximationHeuristic heuristic) {
+                return this->exploreHeuristic.compare(other->exploreHeuristic, heuristic);
             }
-            
+
             storm::storage::BitVector const& status() const {
                 return mStatus;
             }