Added settings for approximation heuristic

Former-commit-id: 40267add31

src/builder/DftExplorationHeuristic.cpp

@@ -16,10 +16,27 @@ namespace storm {
         }
 
         template<typename ValueType>
-        bool DFTExplorationHeuristic<ValueType>::isSkip() const {
-            return skip;
+        bool DFTExplorationHeuristic<ValueType>::isSkip(double approximationThreshold, ApproximationHeuristic heuristic) const {
+            if (!skip) {
+                return false;
+            }
+            switch (heuristic) {
+                case ApproximationHeuristic::NONE:
+                    return false;
+                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.");
+            }
         }
 
+        template<typename ValueType>
+        void DFTExplorationHeuristic<ValueType>::setNotSkip() {
+            skip = false;
+        }
+
+
         template<typename ValueType>
         size_t DFTExplorationHeuristic<ValueType>::getDepth() const {
             return depth;
@@ -42,10 +59,6 @@ namespace storm {
         template<>
         double DFTExplorationHeuristic<double>::getPriority() const {
             // TODO Matthias: change according to heuristic
-            if (!skip) {
-                // TODO Matthias: change to non-magic number
-                return 0;
-            }
             //return rate/exitRate;
             return depth;
         }

src/builder/DftExplorationHeuristic.h

@@ -14,6 +14,11 @@ namespace storm {
 
     namespace builder {
 
+        /*!
+         * Enum representing the heuristic used for deciding which states to expand.
+         */
+        enum class ApproximationHeuristic { NONE, DEPTH, RATERATIO };
+
         template<typename ValueType>
         class DFTExplorationHeuristic {
 
@@ -22,13 +27,16 @@ namespace storm {
 
             void setHeuristicValues(size_t depth, ValueType rate, ValueType exitRate);
 
-            bool isSkip() const;
+            bool isSkip(double approximationThreshold, ApproximationHeuristic heuristic) const;
+
+            void setNotSkip();
 
             size_t getDepth() const;
 
             double getPriority() const;
             
         private:
+
             bool skip;
             size_t depth;
             ValueType rate;

src/builder/ExplicitDFTModelBuilderApprox.cpp

@@ -26,6 +26,8 @@ namespace storm {
         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) {
             // 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>);
@@ -229,8 +231,7 @@ namespace storm {
                 // Try to explore the next state
                 generator.load(currentState);
 
-                STORM_LOG_TRACE("Priority of state " <<currentState->getId() << ": " << currentState->getPriority());
-                if (currentState->getPriority() > approximationThreshold) {
+                if (currentState->isSkip(approximationThreshold, heuristic)) {
                     // Skip the current state
                     STORM_LOG_TRACE("Skip expansion of state: " << dft.getStateString(currentState));
                     setMarkovian(true);

src/builder/ExplicitDFTModelBuilderApprox.h

@@ -258,6 +258,9 @@ namespace storm {
             //TODO Matthias: make changeable
             const bool mergeFailedStates = true;
 
+            // Heuristic used for approximation
+            storm::builder::ApproximationHeuristic heuristic;
+
             // Current id for new state
             size_t newIndex = 0;
 

src/settings/modules/DFTSettings.cpp

@@ -9,7 +9,6 @@
 
 #include "src/exceptions/InvalidSettingsException.h"
 
-
 namespace storm {
     namespace settings {
         namespace modules {
@@ -23,6 +22,7 @@ namespace storm {
             const std::string DFTSettings::disableDCOptionName = "disabledc";
             const std::string DFTSettings::approximationErrorOptionName = "approximation";
             const std::string DFTSettings::approximationErrorOptionShortName = "approx";
+            const std::string DFTSettings::approximationHeuristicOptionName = "approximationheuristic";
             const std::string DFTSettings::propExpectedTimeOptionName = "expectedtime";
             const std::string DFTSettings::propExpectedTimeOptionShortName = "mttf";
             const std::string DFTSettings::propProbabilityOptionName = "probability";
@@ -40,6 +40,7 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, modularisationOptionName, false, "Use modularisation (not applicable for expected time).").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, disableDCOptionName, false, "Disable Dont Care propagation.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, approximationErrorOptionName, false, "Approximation error allowed.").setShortName(approximationErrorOptionShortName).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("error", "The approximation error to use.").addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleGreaterValidatorIncluding(0.0)).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, approximationHeuristicOptionName, false, "Set the heuristic used for approximation.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "Sets which heuristic is used for approximation. Must be in {depth, rateratio}. Default is").setDefaultValueString("depth").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator({"depth", "rateratio"})).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, propExpectedTimeOptionName, false, "Compute expected time of system failure.").setShortName(propExpectedTimeOptionShortName).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, propProbabilityOptionName, false, "Compute probability of system failure.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, propTimeBoundOptionName, false, "Compute probability of system failure up to given timebound.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("time", "The timebound to use.").addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleGreaterValidatorExcluding(0.0)).build()).build());
@@ -78,6 +79,20 @@ namespace storm {
                 return this->getOption(approximationErrorOptionName).getArgumentByName("error").getValueAsDouble();
             }
 
+            storm::builder::ApproximationHeuristic DFTSettings::getApproximationHeuristic() const {
+                if (!isApproximationErrorSet() || getApproximationError() == 0.0) {
+                    // No approximation is done
+                    return storm::builder::ApproximationHeuristic::NONE;
+                }
+                std::string heuristicAsString = this->getOption(approximationHeuristicOptionName).getArgumentByName("heuristic").getValueAsString();
+                if (heuristicAsString == "depth") {
+                    return storm::builder::ApproximationHeuristic::DEPTH;
+                } else if (heuristicAsString == "rateratio") {
+                    return storm::builder::ApproximationHeuristic::RATERATIO;
+                }
+                STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal value '" << heuristicAsString << "' set as heuristic for approximation.");
+            }
+
             bool DFTSettings::usePropExpectedTime() const {
                 return this->getOption(propExpectedTimeOptionName).getHasOptionBeenSet();
             }
@@ -109,7 +124,6 @@ namespace storm {
 #endif
             
             void DFTSettings::finalize() {
-                
             }
 
             bool DFTSettings::check() const {

src/settings/modules/DFTSettings.h

@@ -3,6 +3,7 @@
 
 #include "storm-config.h"
 #include "src/settings/modules/ModuleSettings.h"
+#include "src/builder/DftExplorationHeuristic.h"
 
 namespace storm {
     namespace settings {
@@ -68,6 +69,13 @@ namespace storm {
                  */
                 double getApproximationError() const;
 
+                /*!
+                 * Retrieves the heuristic used for approximation.
+                 *
+                 * @return The heuristic to use.
+                 */
+                storm::builder::ApproximationHeuristic getApproximationHeuristic() const;
+
                 /*!
                  * Retrieves whether the property expected time should be used.
                  *
@@ -135,6 +143,7 @@ namespace storm {
                 static const std::string disableDCOptionName;
                 static const std::string approximationErrorOptionName;
                 static const std::string approximationErrorOptionShortName;
+                static const std::string approximationHeuristicOptionName;
                 static const std::string propExpectedTimeOptionName;
                 static const std::string propExpectedTimeOptionShortName;
                 static const std::string propProbabilityOptionName;

src/storage/dft/DFTState.h

@@ -112,6 +112,10 @@ namespace storm {
                 exploreHeuristic.setHeuristicValues(oldState->exploreHeuristic.getDepth() + 1, rate, exitRate);
             }
 
+            bool isSkip(double approximationThreshold, storm::builder::ApproximationHeuristic heuristic) {
+                return exploreHeuristic.isSkip(approximationThreshold, heuristic);
+            }
+
             double getPriority() const {
                 return exploreHeuristic.getPriority();
             }