Approximation error is relative to mean of lower and upper bound

Former-commit-id: f01c027a3a

src/modelchecker/dft/DFTModelChecker.cpp

@@ -254,7 +254,7 @@ namespace storm {
 
         template<>
         bool DFTModelChecker<double>::isApproximationSufficient(double lowerBound, double upperBound, double approximationError) {
-            return upperBound - lowerBound <= approximationError;
+            return upperBound - lowerBound <= approximationError * (lowerBound + upperBound) / 2;
         }
 
         template<typename ValueType>

src/modelchecker/dft/DFTModelChecker.h

@@ -106,7 +106,8 @@ namespace storm {
             std::unique_ptr<storm::modelchecker::CheckResult> checkModel(std::shared_ptr<storm::models::sparse::Model<ValueType>>& model, std::shared_ptr<const storm::logic::Formula> 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.

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());

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.
                  */