diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index ce44a1db9..a5f4be44a 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -57,7 +57,7 @@ namespace storm { using detail::PreviousExplicitResult; template - GameBasedMdpModelChecker::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule().getPrecision() * 2), reuseQualitativeResults(false), reuseQuantitativeResults(false), solveMode(storm::settings::getModule().getSolveMode()) { + GameBasedMdpModelChecker::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule().getPrecision() * 2, storm::settings::getModule().getRelativeTerminationCriterion()), reuseQualitativeResults(false), reuseQuantitativeResults(false), solveMode(storm::settings::getModule().getSolveMode()) { STORM_LOG_WARN_COND(!model.hasUndefinedConstants(), "Model contains undefined constants. Game-based abstraction can treat such models, but you should make sure that you did not simply forget to define these constants. In particular, it may be necessary to constrain the values of the undefined constants."); diff --git a/src/storm/settings/modules/AbstractionSettings.cpp b/src/storm/settings/modules/AbstractionSettings.cpp index fccd65722..08f947a48 100644 --- a/src/storm/settings/modules/AbstractionSettings.cpp +++ b/src/storm/settings/modules/AbstractionSettings.cpp @@ -19,6 +19,7 @@ namespace storm { const std::string AbstractionSettings::addAllGuardsOptionName = "all-guards"; const std::string AbstractionSettings::useInterpolationOptionName = "interpolation"; const std::string AbstractionSettings::precisionOptionName = "precision"; + const std::string AbstractionSettings::relativeOptionName = "relative"; const std::string AbstractionSettings::pivotHeuristicOptionName = "pivot-heuristic"; const std::string AbstractionSettings::reuseResultsOptionName = "reuse"; const std::string AbstractionSettings::restrictToRelevantStatesOptionName = "relevant"; @@ -66,6 +67,11 @@ namespace storm { .build()); this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "The precision used for detecting convergence.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-03).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, relativeOptionName, true, "Sets whether to use a relative termination criterion.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff)) + .setDefaultValueString("off").build()) + .build()); std::vector pivotHeuristic = {"nearest-max-dev", "most-prob-path", "max-weighted-dev"}; this->addOption(storm::settings::OptionBuilder(moduleName, pivotHeuristicOptionName, true, "Sets the pivot selection heuristic.") @@ -148,6 +154,10 @@ namespace storm { return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble(); } + bool AbstractionSettings::getRelativeTerminationCriterion() const { + return this->getOption(relativeOptionName).getArgumentByName("value").getValueAsString() == "on"; + } + AbstractionSettings::PivotSelectionHeuristic AbstractionSettings::getPivotSelectionHeuristic() const { std::string heuristicName = this->getOption(pivotHeuristicOptionName).getArgumentByName("name").getValueAsString(); if (heuristicName == "nearest-max-dev") { diff --git a/src/storm/settings/modules/AbstractionSettings.h b/src/storm/settings/modules/AbstractionSettings.h index 7cd950042..0959f2772 100644 --- a/src/storm/settings/modules/AbstractionSettings.h +++ b/src/storm/settings/modules/AbstractionSettings.h @@ -83,6 +83,11 @@ namespace storm { */ double getPrecision() const; + /*! + * Retrieves whether to use a relative termination criterion for detecting convergence. + */ + bool getRelativeTerminationCriterion() const; + /*! * Retrieves the selected heuristic to select pivot blocks. * @@ -146,6 +151,7 @@ namespace storm { const static std::string addAllGuardsOptionName; const static std::string useInterpolationOptionName; const static std::string precisionOptionName; + const static std::string relativeOptionName; const static std::string pivotHeuristicOptionName; const static std::string reuseResultsOptionName; const static std::string restrictToRelevantStatesOptionName; diff --git a/src/storm/utility/ConstantsComparator.cpp b/src/storm/utility/ConstantsComparator.cpp index 913c79f2d..a4ed2e024 100644 --- a/src/storm/utility/ConstantsComparator.cpp +++ b/src/storm/utility/ConstantsComparator.cpp @@ -72,11 +72,11 @@ namespace storm { return std::abs(value1 - value2) < precision; } - ConstantsComparator::ConstantsComparator() : precision(storm::settings::getModule().getPrecision()) { + ConstantsComparator::ConstantsComparator() : precision(storm::settings::getModule().getPrecision()), relative(false) { // Intentionally left empty. } - ConstantsComparator::ConstantsComparator(double precision) : precision(precision) { + ConstantsComparator::ConstantsComparator(double precision, bool relative) : precision(precision), relative(relative) { // Intentionally left empty. } @@ -93,7 +93,11 @@ namespace storm { } bool ConstantsComparator::isEqual(double const& value1, double const& value2) const { - return std::abs(value1 - value2) <= precision; + if (relative) { + return value1 == value2 || std::abs(value1 - value2)/std::abs(value1 + value2) <= precision; + } else { + return std::abs(value1 - value2) <= precision; + } } bool ConstantsComparator::isConstant(double const&) const { diff --git a/src/storm/utility/ConstantsComparator.h b/src/storm/utility/ConstantsComparator.h index 988d08538..9f32551f3 100644 --- a/src/storm/utility/ConstantsComparator.h +++ b/src/storm/utility/ConstantsComparator.h @@ -56,7 +56,7 @@ namespace storm { public: ConstantsComparator(); - ConstantsComparator(double precision); + ConstantsComparator(double precision, bool relative = false); bool isOne(double const& value) const; @@ -73,6 +73,9 @@ namespace storm { private: // The precision used for comparisons. double precision; + + // Whether to use relative comparison for equality. + bool relative; }; } }