adding relative precision to comparator and game-based abstraction

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -57,7 +57,7 @@ namespace storm {
         using detail::PreviousExplicitResult;
 
         template<storm::dd::DdType Type, typename ModelType>
-        GameBasedMdpModelChecker<Type, ModelType>::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getPrecision() * 2), reuseQualitativeResults(false), reuseQuantitativeResults(false), solveMode(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getSolveMode()) {
+        GameBasedMdpModelChecker<Type, ModelType>::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getPrecision() * 2, storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getRelativeTerminationCriterion()), reuseQualitativeResults(false), reuseQuantitativeResults(false), solveMode(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().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.");
             

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<std::string> 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") {

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;

src/storm/utility/ConstantsComparator.cpp

@@ -72,11 +72,11 @@ namespace storm {
             return std::abs(value1 - value2) < precision;
         }
         
-        ConstantsComparator<double>::ConstantsComparator() : precision(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()) {
+        ConstantsComparator<double>::ConstantsComparator() : precision(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()), relative(false) {
             // Intentionally left empty.
         }
         
-        ConstantsComparator<double>::ConstantsComparator(double precision) : precision(precision) {
+        ConstantsComparator<double>::ConstantsComparator(double precision, bool relative) : precision(precision), relative(relative) {
             // Intentionally left empty.
         }
         
@@ -93,7 +93,11 @@ namespace storm {
         }
         
         bool ConstantsComparator<double>::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<double>::isConstant(double const&) const {

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;
         };
     }
 }