From 34edb426be0097c3d7e2e4fa3caaab68d128bc6a Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 13 Mar 2019 14:15:59 +0100 Subject: [PATCH] Fixed arguments for exploration heuristic settings --- src/storm-dft/settings/modules/FaultTreeSettings.cpp | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.cpp b/src/storm-dft/settings/modules/FaultTreeSettings.cpp index 7c9ef14af..a110ea0a7 100644 --- a/src/storm-dft/settings/modules/FaultTreeSettings.cpp +++ b/src/storm-dft/settings/modules/FaultTreeSettings.cpp @@ -31,7 +31,10 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, disableDCOptionName, false, "Disable Dont Care propagation.").build()); 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 {depth, probability}. Default is").setDefaultValueString("depth").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator({"depth", "rateratio"})).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") + .setDefaultValueString("depth") + .addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator({"none", "depth", "probability", "bounddifference"})).build()).build()); #ifdef STORM_HAVE_Z3 this->addOption(storm::settings::OptionBuilder(moduleName, solveWithSmtOptionName, true, "Solve the DFT with SMT.").build()); #endif @@ -63,10 +66,14 @@ namespace storm { return storm::builder::ApproximationHeuristic::NONE; } std::string heuristicAsString = this->getOption(approximationHeuristicOptionName).getArgumentByName("heuristic").getValueAsString(); - if (heuristicAsString == "depth") { + if (heuristicAsString == "none") { + return storm::builder::ApproximationHeuristic::NONE; + } else if (heuristicAsString == "depth") { return storm::builder::ApproximationHeuristic::DEPTH; } else if (heuristicAsString == "probability") { return storm::builder::ApproximationHeuristic::PROBABILITY; + } else if (heuristicAsString == "bounddifference") { + return storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE; } STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal value '" << heuristicAsString << "' set as heuristic for approximation."); }