diff --git a/src/modelchecker/dft/DFTModelChecker.cpp b/src/modelchecker/dft/DFTModelChecker.cpp index 26f2033d6..717ace4c3 100644 --- a/src/modelchecker/dft/DFTModelChecker.cpp +++ b/src/modelchecker/dft/DFTModelChecker.cpp @@ -254,7 +254,7 @@ namespace storm { template<> bool DFTModelChecker::isApproximationSufficient(double lowerBound, double upperBound, double approximationError) { - return upperBound - lowerBound <= approximationError; + return upperBound - lowerBound <= approximationError * (lowerBound + upperBound) / 2; } template diff --git a/src/modelchecker/dft/DFTModelChecker.h b/src/modelchecker/dft/DFTModelChecker.h index 62bb5afe4..83df59bfa 100644 --- a/src/modelchecker/dft/DFTModelChecker.h +++ b/src/modelchecker/dft/DFTModelChecker.h @@ -106,7 +106,8 @@ namespace storm { std::unique_ptr checkModel(std::shared_ptr>& model, std::shared_ptr const& formula); /*! - * Checks if the computed approximation is sufficient, i.e. upperBound - lowerBound <= approximationError. + * Checks if the computed approximation is sufficient, i.e. + * upperBound - lowerBound <= approximationError * mean(upperBound, lowerBound). * * @param lowerBound The lower bound on the result. * @param upperBound The upper bound on the result. diff --git a/src/settings/modules/DFTSettings.cpp b/src/settings/modules/DFTSettings.cpp index 1b3f0bae2..0dcb49f1d 100644 --- a/src/settings/modules/DFTSettings.cpp +++ b/src/settings/modules/DFTSettings.cpp @@ -39,7 +39,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, symmetryReductionOptionName, false, "Exploit symmetric structure of model.").setShortName(symmetryReductionOptionShortName).build()); 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, approximationErrorOptionName, false, "Approximation error allowed.").setShortName(approximationErrorOptionShortName).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("error", "The relative 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()); diff --git a/src/settings/modules/DFTSettings.h b/src/settings/modules/DFTSettings.h index 2aa418538..e580a5d05 100644 --- a/src/settings/modules/DFTSettings.h +++ b/src/settings/modules/DFTSettings.h @@ -63,7 +63,7 @@ namespace storm { bool isApproximationErrorSet() const; /*! - * Retrieves the error allowed for approximation the model checking result. + * Retrieves the relative error allowed for approximating the model checking result. * * @return The allowed errorbound. */