From 5d8fc7db77750404ee38736f409340db6b4b1d6e Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 19 Mar 2019 11:28:14 +0100 Subject: [PATCH] Removed approximation heuristic NONE --- .../builder/DftExplorationHeuristic.cpp | 2 -- .../builder/DftExplorationHeuristic.h | 26 +------------------ .../builder/ExplicitDFTModelBuilder.cpp | 10 ------- .../settings/modules/FaultTreeSettings.cpp | 12 +++------ src/storm-dft/storage/BucketPriorityQueue.cpp | 2 -- 5 files changed, 4 insertions(+), 48 deletions(-) diff --git a/src/storm-dft/builder/DftExplorationHeuristic.cpp b/src/storm-dft/builder/DftExplorationHeuristic.cpp index 43b3ad96b..dcb031f2a 100644 --- a/src/storm-dft/builder/DftExplorationHeuristic.cpp +++ b/src/storm-dft/builder/DftExplorationHeuristic.cpp @@ -30,14 +30,12 @@ namespace storm { // Instantiate templates. template class DFTExplorationHeuristic; - template class DFTExplorationHeuristicNone; template class DFTExplorationHeuristicDepth; template class DFTExplorationHeuristicProbability; template class DFTExplorationHeuristicBoundDifference; #ifdef STORM_HAVE_CARL template class DFTExplorationHeuristic; - template class DFTExplorationHeuristicNone; template class DFTExplorationHeuristicDepth; template class DFTExplorationHeuristicProbability; template class DFTExplorationHeuristicBoundDifference; diff --git a/src/storm-dft/builder/DftExplorationHeuristic.h b/src/storm-dft/builder/DftExplorationHeuristic.h index de4b5cfc5..b0fd73a66 100644 --- a/src/storm-dft/builder/DftExplorationHeuristic.h +++ b/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 - class DFTExplorationHeuristicNone : public DFTExplorationHeuristic { - public: - DFTExplorationHeuristicNone(size_t id) : DFTExplorationHeuristic(id) { - // Intentionally left empty - } - - DFTExplorationHeuristicNone(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, predecessor, rate, exitRate) { - // Intentionally left empty - } - - bool updateHeuristicValues(DFTExplorationHeuristic const&, ValueType, ValueType) override { - return false; - } - - double getPriority() const override { - return 0; - } - - bool isSkip(double) const override { - return false; - } - }; - template class DFTExplorationHeuristicDepth : public DFTExplorationHeuristic { public: diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index f9e4b54f6..922f680e9 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/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>(initialStateIndex); - break; case storm::builder::ApproximationHeuristic::DEPTH: heuristic = std::make_shared>(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>(stateProbabilityPair.first, *currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass()); - break; case storm::builder::ApproximationHeuristic::DEPTH: heuristic = std::make_shared>(stateProbabilityPair.first, *currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass()); break; diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.cpp b/src/storm-dft/settings/modules/FaultTreeSettings.cpp index a110ea0a7..740c6aa54 100644 --- a/src/storm-dft/settings/modules/FaultTreeSettings.cpp +++ b/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; diff --git a/src/storm-dft/storage/BucketPriorityQueue.cpp b/src/storm-dft/storage/BucketPriorityQueue.cpp index a0926e70c..3ce3659b5 100644 --- a/src/storm-dft/storage/BucketPriorityQueue.cpp +++ b/src/storm-dft/storage/BucketPriorityQueue.cpp @@ -198,14 +198,12 @@ namespace storm { // Template instantiations template class BucketPriorityQueue>; - template class BucketPriorityQueue>; template class BucketPriorityQueue>; template class BucketPriorityQueue>; template class BucketPriorityQueue>; #ifdef STORM_HAVE_CARL template class BucketPriorityQueue>; - template class BucketPriorityQueue>; template class BucketPriorityQueue>; template class BucketPriorityQueue>; template class BucketPriorityQueue>;