Added new CLI settings for GridApproximation

src/storm-pomdp-cli/settings/PomdpSettings.cpp

@@ -31,6 +31,7 @@
 #include "storm/settings/modules/HintSettings.h"
 
 #include "storm-pomdp-cli/settings/modules/POMDPSettings.h"
+#include "storm-pomdp-cli/settings/modules/GridApproximationSettings.h"
 
 namespace storm {
     namespace settings {
@@ -44,6 +45,7 @@ namespace storm {
             storm::settings::addModule<storm::settings::modules::BuildSettings>();
         
             storm::settings::addModule<storm::settings::modules::POMDPSettings>();
+            storm::settings::addModule<storm::settings::modules::GridApproximationSettings>();
         
             storm::settings::addModule<storm::settings::modules::TransformationSettings>();
             storm::settings::addModule<storm::settings::modules::GmmxxEquationSolverSettings>();

src/storm-pomdp-cli/settings/modules/GridApproximationSettings.cpp

@@ -0,0 +1,63 @@
+#include "storm-pomdp-cli/settings/modules/GridApproximationSettings.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/SettingMemento.h"
+#include "storm/settings/Option.h"
+#include "storm/settings/OptionBuilder.h"
+#include "storm/settings/ArgumentBuilder.h"
+
+#include "storm/exceptions/InvalidArgumentException.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            const std::string GridApproximationSettings::moduleName = "grid";
+            
+            const std::string refineOption = "refine";
+            const std::string resolutionOption = "resolution";
+            const std::string limitBeliefExplorationOption = "limit-exploration";
+            const std::string numericPrecisionOption = "numeric-precision";
+
+            GridApproximationSettings::GridApproximationSettings() : ModuleSettings(moduleName) {
+                
+                this->addOption(storm::settings::OptionBuilder(moduleName, refineOption, false,"Enables automatic refinement of the grid until the goal precision is reached").addArgument(
+                        storm::settings::ArgumentBuilder::createDoubleArgument("precision","Allowed difference between upper and lower bound of the result.").setDefaultValueDouble(1e-6).makeOptional().addValidatorDouble(storm::settings::ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0)).build()).build());
+                
+                this->addOption(storm::settings::OptionBuilder(moduleName, resolutionOption, false,"Sets the (initial-) resolution of the grid (higher means more precise results)").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value","the resolution").setDefaultValueUnsignedInteger(10).addValidatorUnsignedInteger(storm::settings::ArgumentValidatorFactory::createUnsignedGreaterValidator(0)).build()).build());
+                
+                this->addOption(storm::settings::OptionBuilder(moduleName, limitBeliefExplorationOption, false,"Sets whether the belief space exploration is stopped if upper and lower bound are close").addArgument(
+                        storm::settings::ArgumentBuilder::createDoubleArgument("threshold","the difference between upper and lower bound when to stop").setDefaultValueDouble(0.0).addValidatorDouble(storm::settings::ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0)).build()).build());
+                
+                this->addOption(storm::settings::OptionBuilder(moduleName, numericPrecisionOption, false,"Sets the precision used to determine whether two belief-states are equal.").addArgument(
+                        storm::settings::ArgumentBuilder::createDoubleArgument("value","the precision").setDefaultValueDouble(1e-9).makeOptional().addValidatorDouble(storm::settings::ArgumentValidatorFactory::createDoubleRangeValidatorIncluding(0, 1)).build()).build());
+                
+            }
+
+            bool GridApproximationSettings::isRefineSet() const {
+                return this->getOption(refineOption).getHasOptionBeenSet();
+            }
+            
+            double GridApproximationSettings::getRefinementPrecision() const {
+                return this->getOption(refineOption).getArgumentByName("precision").getValueAsDouble();
+            }
+            
+            uint64_t GridApproximationSettings::getGridResolution() const {
+                return this->getOption(resolutionOption).getArgumentByName("value").getValueAsUnsignedInteger();
+            }
+            
+            double GridApproximationSettings::getExplorationThreshold() const {
+                return this->getOption(limitBeliefExplorationOption).getArgumentByName("threshold").getValueAsDouble();
+            }
+            
+            bool GridApproximationSettings::isNumericPrecisionSetFromDefault() const {
+                return !this->getOption(numericPrecisionOption).getHasOptionBeenSet() || this->getOption(numericPrecisionOption).getArgumentByName("value").wasSetFromDefaultValue();
+            }
+            
+            double GridApproximationSettings::getNumericPrecision() const {
+                return this->getOption(numericPrecisionOption).getArgumentByName("value").getValueAsDouble();
+            }
+            
+        } // namespace modules
+    } // namespace settings
+} // namespace storm

src/storm-pomdp-cli/settings/modules/GridApproximationSettings.h

@@ -0,0 +1,40 @@
+#pragma once
+
+#include "storm-config.h"
+#include "storm/settings/modules/ModuleSettings.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+
+            /*!
+             * This class represents the settings for POMDP model checking.
+             */
+            class GridApproximationSettings : public ModuleSettings {
+            public:
+
+                /*!
+                 * Creates a new set of POMDP settings.
+                 */
+                GridApproximationSettings();
+
+                virtual ~GridApproximationSettings() = default;
+                
+                bool isRefineSet() const;
+                double getRefinementPrecision() const;
+                uint64_t getGridResolution() const;
+                double getExplorationThreshold() const;
+                bool isNumericPrecisionSetFromDefault() const;
+                double getNumericPrecision() const;
+                
+                // The name of the module.
+                static const std::string moduleName;
+
+            private:
+
+                
+            };
+
+        } // namespace modules
+    } // namespace settings
+} // namespace storm

src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp

@@ -15,7 +15,6 @@ namespace storm {
             const std::string POMDPSettings::moduleName = "pomdp";
             const std::string exportAsParametricModelOption = "parametric-drn";
             const std::string gridApproximationOption = "gridapproximation";
-            const std::string limitBeliefExplorationOption = "limit-exploration";
             const std::string qualitativeReductionOption = "qualitativereduction";
             const std::string analyzeUniqueObservationsOption = "uniqueobservations";
             const std::string mecReductionOption = "mecreduction";
@@ -42,9 +41,7 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, fscmode, false, "Sets the way the pMC is obtained").addArgument(storm::settings::ArgumentBuilder::createStringArgument("type", "type name").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(fscModes)).setDefaultValueString("standard").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, transformBinaryOption, false, "Transforms the pomdp to a binary pomdp.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, transformSimpleOption, false, "Transforms the pomdp to a binary and simple pomdp.").build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, gridApproximationOption, false,"Analyze the POMDP using grid approximation.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("resolution","the resolution of the grid").setDefaultValueUnsignedInteger(10).makeOptional().addValidatorUnsignedInteger(storm::settings::ArgumentValidatorFactory::createUnsignedGreaterValidator(0)).build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, limitBeliefExplorationOption, false,"Sets whether the belief space exploration is stopped if upper and lower bound are close").addArgument(
-                        storm::settings::ArgumentBuilder::createDoubleArgument("threshold","the difference between upper and lower bound when to stop").setDefaultValueDouble(0.0).addValidatorDouble(storm::settings::ArgumentValidatorFactory::createDoubleRangeValidatorIncluding(0,1)).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, gridApproximationOption, false,"Analyze the POMDP using grid approximation.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, memlessSearchOption, false, "Search for a qualitative memoryless scheuler").addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "method name").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(memlessSearchMethods)).setDefaultValueString("none").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, checkFullyObservableOption, false, "Performs standard model checking on the underlying MDP").build());
 
@@ -78,10 +75,6 @@ namespace storm {
                 return this->getOption(gridApproximationOption).getHasOptionBeenSet();
             }
 
-            uint64_t POMDPSettings::getGridResolution() const {
-                return this->getOption(gridApproximationOption).getArgumentByName("resolution").getValueAsUnsignedInteger();
-            }
-
             bool POMDPSettings::isMemlessSearchSet() const {
                 return this->getOption(memlessSearchOption).getHasOptionBeenSet();
             }
@@ -94,14 +87,6 @@ namespace storm {
                 return this->getOption(memlessSearchOption).getArgumentByName("method").getValueAsString();
             }
 
-            bool POMDPSettings::isLimitExplorationSet() const {
-                return this->getOption(limitBeliefExplorationOption).getHasOptionBeenSet();
-            }
-
-            double POMDPSettings::getExplorationThreshold() const {
-                return this->getOption(limitBeliefExplorationOption).getArgumentByName("threshold").getValueAsDouble();
-            }
-
             uint64_t POMDPSettings::getMemoryBound() const {
                 return this->getOption(memoryBoundOption).getArgumentByName("bound").getValueAsUnsignedInteger();
             }

src/storm-pomdp-cli/settings/modules/POMDPSettings.h

@@ -27,7 +27,6 @@ namespace storm {
                 bool isQualitativeReductionSet() const;
 
                 bool isGridApproximationSet() const;
-                bool isLimitExplorationSet() const;
                 bool isAnalyzeUniqueObservationsSet() const;
                 bool isMecReductionSet() const;
                 bool isSelfloopReductionSet() const;
@@ -39,8 +38,6 @@ namespace storm {
                 std::string getFscApplicationTypeString() const;
                 uint64_t getMemoryBound() const;
 
-                uint64_t getGridResolution() const;
-                double getExplorationThreshold() const;
                 storm::storage::PomdpMemoryPattern getMemoryPattern() const;
                 
                 bool check() const override;

src/storm-pomdp-cli/storm-pomdp.cpp

@@ -5,6 +5,7 @@
 #include "storm/settings/modules/GeneralSettings.h"
 #include "storm/settings/modules/DebugSettings.h"
 #include "storm-pomdp-cli/settings/modules/POMDPSettings.h"
+#include "storm-pomdp-cli/settings/modules/GridApproximationSettings.h"
 #include "storm-pomdp-cli/settings/PomdpSettings.h"
 
 #include "storm/analysis/GraphConditions.h"
@@ -29,6 +30,7 @@
 #include "storm/api/storm.h"
 #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
+#include "storm/utility/NumberTraits.h"
 #include "storm/utility/Stopwatch.h"
 
 #include "storm/exceptions/UnexpectedException.h"
@@ -73,23 +75,6 @@ namespace storm {
                     formulaInfo.updateTargetStates(*pomdp, std::move(prob1States));
                     formulaInfo.updateSinkStates(*pomdp, std::move(prob0States));
                     preprocessingPerformed = true;
-                } else if (pomdpSettings.isGridApproximationSet()) {
-                    // We still might need to apply the KnownProbabilityTransformer, to ensure that the grid approximation works properly
-                    if (formulaInfo.isNonNestedReachabilityProbability()) {
-                        if (!formulaInfo.getTargetStates().observationClosed || !formulaInfo.getSinkStates().states.empty()) {
-                            // Make target states observation closed and/or sink states absorbing
-                            storm::pomdp::transformer::KnownProbabilityTransformer<ValueType> kpt = storm::pomdp::transformer::KnownProbabilityTransformer<ValueType>();
-                            auto prob0States = formulaInfo.getSinkStates().states;
-                            auto prob1States = formulaInfo.getTargetStates().states;
-                            pomdp = kpt.transform(*pomdp, prob0States, prob1States);
-                            // Update formulaInfo to changes from Preprocessing
-                            formulaInfo.updateTargetStates(*pomdp, std::move(prob1States));
-                            formulaInfo.updateSinkStates(*pomdp, std::move(prob0States));
-                            preprocessingPerformed = true;
-                        }
-                    } else if (formulaInfo.isNonNestedExpectedRewardFormula()) {
-                        STORM_LOG_THROW(formulaInfo.getTargetStates().observationClosed, storm::exceptions::NotSupportedException, "Target states of reward property are not observation closed. This case is not yet implemented.");
-                    }
                 }
                 return preprocessingPerformed;
             }
@@ -100,17 +85,23 @@ namespace storm {
                 bool analysisPerformed = false;
                 if (pomdpSettings.isGridApproximationSet()) {
                     STORM_PRINT_AND_LOG("Applying grid approximation... ");
-                    STORM_LOG_THROW(formulaInfo.isNonNestedReachabilityProbability() || formulaInfo.isNonNestedExpectedRewardFormula(), storm::exceptions::NotSupportedException, "Unsupported formula type for Grid approximation.");
-                    STORM_LOG_THROW(!formulaInfo.getTargetStates().empty(), storm::exceptions::UnexpectedException, "The set of target states is empty.");
-                    STORM_LOG_THROW(formulaInfo.getTargetStates().observationClosed, storm::exceptions::UnexpectedException, "Observations on target states also occur on non-target states. This is unexpected at this point.");
-                    storm::pomdp::modelchecker::ApproximatePOMDPModelchecker<ValueType> checker = storm::pomdp::modelchecker::ApproximatePOMDPModelchecker<ValueType>();
-                    std::unique_ptr<storm::pomdp::modelchecker::POMDPCheckResult<ValueType>> result;
-                    if (formulaInfo.isNonNestedReachabilityProbability()) {
-                        result = checker.refineReachabilityProbability(*pomdp, formulaInfo.getTargetStates().observations, formulaInfo.minimize(), pomdpSettings.getGridResolution(), pomdpSettings.getExplorationThreshold());
+                    auto const& gridSettings = storm::settings::getModule<storm::settings::modules::GridApproximationSettings>();
+                    typename storm::pomdp::modelchecker::ApproximatePOMDPModelchecker<ValueType>::Options options;
+                    options.initialGridResolution = gridSettings.getGridResolution();
+                    options.explorationThreshold = gridSettings.getExplorationThreshold();
+                    options.doRefinement = gridSettings.isRefineSet();
+                    options.refinementPrecision = gridSettings.getRefinementPrecision();
+                    options.numericPrecision = gridSettings.getNumericPrecision();
+                    if (storm::NumberTraits<ValueType>::IsExact) {
+                        if (gridSettings.isNumericPrecisionSetFromDefault()) {
+                            STORM_LOG_WARN_COND(storm::utility::isZero(options.numericPrecision), "Setting numeric precision to zero because exact arithmethic is used.");
+                            options.numericPrecision = storm::utility::zero<ValueType>();
                         } else {
-                        // TODO: no exploration threshold?
-                        result = checker.computeReachabilityReward(*pomdp, formulaInfo.getTargetStates().observations, formulaInfo.minimize(), pomdpSettings.getGridResolution());
+                            STORM_LOG_WARN_COND(storm::utility::isZero(options.numericPrecision), "A non-zero numeric precision was set although exact arithmethic is used. Results might be inexact.");
+                        }
                     }
+                    storm::pomdp::modelchecker::ApproximatePOMDPModelchecker<ValueType> checker = storm::pomdp::modelchecker::ApproximatePOMDPModelchecker<ValueType>(*pomdp, options);
+                    std::unique_ptr<storm::pomdp::modelchecker::POMDPCheckResult<ValueType>> result = checker.check(formula);
                     ValueType overRes = result->overApproxValue;
                     ValueType underRes = result->underApproxValue;
                     if (overRes != underRes) {