Removed approximation heuristic NONE

src/storm-dft/builder/DftExplorationHeuristic.cpp

@@ -30,14 +30,12 @@ namespace storm {
 
         // Instantiate templates.
         template class DFTExplorationHeuristic<double>;
-        template class DFTExplorationHeuristicNone<double>;
         template class DFTExplorationHeuristicDepth<double>;
         template class DFTExplorationHeuristicProbability<double>;
         template class DFTExplorationHeuristicBoundDifference<double>;
 
 #ifdef STORM_HAVE_CARL
         template class DFTExplorationHeuristic<storm::RationalFunction>;
-        template class DFTExplorationHeuristicNone<storm::RationalFunction>;
         template class DFTExplorationHeuristicDepth<storm::RationalFunction>;
         template class DFTExplorationHeuristicProbability<storm::RationalFunction>;
         template class DFTExplorationHeuristicBoundDifference<storm::RationalFunction>;

src/storm-dft/builder/DftExplorationHeuristic.h

@@ -12,7 +12,7 @@ namespace storm {
         /*!
          * Enum representing the heuristic used for deciding which states to expand.
          */
-        enum class ApproximationHeuristic { NONE, DEPTH, PROBABILITY, BOUNDDIFFERENCE };
+        enum class ApproximationHeuristic { DEPTH, PROBABILITY, BOUNDDIFFERENCE };
 
 
         /*!
@@ -90,30 +90,6 @@ namespace storm {
             ValueType probability;
         };
 
-        template<typename ValueType>
-        class DFTExplorationHeuristicNone : public DFTExplorationHeuristic<ValueType> {
-        public:
-            DFTExplorationHeuristicNone(size_t id) : DFTExplorationHeuristic<ValueType>(id) {
-                // Intentionally left empty
-            }
-
-            DFTExplorationHeuristicNone(size_t id, DFTExplorationHeuristic<ValueType> const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic<ValueType>(id, predecessor, rate, exitRate) {
-                // Intentionally left empty
-            }
-
-            bool updateHeuristicValues(DFTExplorationHeuristic<ValueType> const&, ValueType, ValueType) override {
-                return false;
-            }
-
-            double getPriority() const override {
-                return 0;
-            }
-
-            bool isSkip(double) const override {
-                return false;
-            }
-        };
-
         template<typename ValueType>
         class DFTExplorationHeuristicDepth : public DFTExplorationHeuristic<ValueType> {
         public:

src/storm-dft/builder/ExplicitDFTModelBuilder.cpp

@@ -160,9 +160,6 @@ namespace storm {
                 STORM_LOG_ASSERT(!statesNotExplored.at(initialStateIndex).second, "Heuristic for initial state is already initialized");
                 ExplorationHeuristicPointer heuristic;
                 switch (usedHeuristic) {
-                    case storm::builder::ApproximationHeuristic::NONE:
-                        heuristic = std::make_shared<DFTExplorationHeuristicNone<ValueType>>(initialStateIndex);
-                        break;
                     case storm::builder::ApproximationHeuristic::DEPTH:
                         heuristic = std::make_shared<DFTExplorationHeuristicDepth<ValueType>>(initialStateIndex);
                         break;
@@ -182,10 +179,6 @@ namespace storm {
 
             if (approximationThreshold > 0.0) {
                 switch (usedHeuristic) {
-                    case storm::builder::ApproximationHeuristic::NONE:
-                        // Do not change anything
-                        approximationThreshold = dft.nrElements()+10;
-                        break;
                     case storm::builder::ApproximationHeuristic::DEPTH:
                         approximationThreshold = iteration + 1;
                         break;
@@ -397,9 +390,6 @@ namespace storm {
                                     // Initialize heuristic values
                                     ExplorationHeuristicPointer heuristic;
                                     switch (usedHeuristic) {
-                                        case storm::builder::ApproximationHeuristic::NONE:
-                                            heuristic = std::make_shared<DFTExplorationHeuristicNone<ValueType>>(stateProbabilityPair.first, *currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass());
-                                            break;
                                         case storm::builder::ApproximationHeuristic::DEPTH:
                                             heuristic = std::make_shared<DFTExplorationHeuristicDepth<ValueType>>(stateProbabilityPair.first, *currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass());
                                             break;

src/storm-dft/settings/modules/FaultTreeSettings.cpp

@@ -32,9 +32,9 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, firstDependencyOptionName, false, "Avoid non-determinism by always taking the first possible dependency.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, approximationErrorOptionName, false, "Approximation error allowed.").setShortName(approximationErrorOptionShortName).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("error", "The relative approximation error to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(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 {none, depth, probability, bounddifference}. Default is")
+                    .addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "The name of the heuristic used for approximation.")
                     .setDefaultValueString("depth")
-                    .addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator({"none", "depth", "probability", "bounddifference"})).build()).build());
+                    .addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator({"depth", "probability", "bounddifference"})).build()).build());
 #ifdef STORM_HAVE_Z3
                 this->addOption(storm::settings::OptionBuilder(moduleName, solveWithSmtOptionName, true, "Solve the DFT with SMT.").build());
 #endif
@@ -61,14 +61,8 @@ namespace storm {
             }
 
             storm::builder::ApproximationHeuristic FaultTreeSettings::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 == "none") {
-                    return storm::builder::ApproximationHeuristic::NONE;
-                } else if (heuristicAsString == "depth") {
+                if (heuristicAsString == "depth") {
                     return storm::builder::ApproximationHeuristic::DEPTH;
                 } else if (heuristicAsString == "probability") {
                     return storm::builder::ApproximationHeuristic::PROBABILITY;

src/storm-dft/storage/BucketPriorityQueue.cpp

@@ -198,14 +198,12 @@ namespace storm {
 
         // Template instantiations
         template class BucketPriorityQueue<storm::builder::DFTExplorationHeuristic<double>>;
-        template class BucketPriorityQueue<storm::builder::DFTExplorationHeuristicNone<double>>;
         template class BucketPriorityQueue<storm::builder::DFTExplorationHeuristicDepth<double>>;
         template class BucketPriorityQueue<storm::builder::DFTExplorationHeuristicProbability<double>>;
         template class BucketPriorityQueue<storm::builder::DFTExplorationHeuristicBoundDifference<double>>;
 
 #ifdef STORM_HAVE_CARL
         template class BucketPriorityQueue<storm::builder::DFTExplorationHeuristic<storm::RationalFunction>>;
-        template class BucketPriorityQueue<storm::builder::DFTExplorationHeuristicNone<storm::RationalFunction>>;
         template class BucketPriorityQueue<storm::builder::DFTExplorationHeuristicDepth<storm::RationalFunction>>;
         template class BucketPriorityQueue<storm::builder::DFTExplorationHeuristicProbability<storm::RationalFunction>>;
         template class BucketPriorityQueue<storm::builder::DFTExplorationHeuristicBoundDifference<storm::RationalFunction>>;