Added a switch to control the size of the under-approximation via command line.

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

@@ -19,6 +19,7 @@ namespace storm {
             const std::string limitBeliefExplorationOption = "limit-exploration";
             const std::string numericPrecisionOption = "numeric-precision";
             const std::string cacheSimplicesOption = "cache-simplices";
+            const std::string unfoldBeliefMdpOption = "unfold-belief-mdp";
 
             GridApproximationSettings::GridApproximationSettings() : ModuleSettings(moduleName) {
                 
@@ -35,6 +36,7 @@ namespace storm {
                 
                 this->addOption(storm::settings::OptionBuilder(moduleName, cacheSimplicesOption, false,"Enables caching of simplices which requires more memory but can be faster.").build());
                 
+                this->addOption(storm::settings::OptionBuilder(moduleName, unfoldBeliefMdpOption, false,"Sets the (initial-) size threshold of the unfolded belief MDP (higher means more precise results, 0 means automatic choice)").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value","the maximal number of states").setDefaultValueUnsignedInteger(0).build()).build());
             }
 
             bool GridApproximationSettings::isRefineSet() const {
@@ -65,6 +67,14 @@ namespace storm {
                 return this->getOption(cacheSimplicesOption).getHasOptionBeenSet();
             }
             
+            bool GridApproximationSettings::isUnfoldBeliefMdpSizeThresholdSet() const {
+                return this->getOption(unfoldBeliefMdpOption).getHasOptionBeenSet();
+            }
+            
+            uint64_t GridApproximationSettings::getUnfoldBeliefMdpSizeThreshold() const {
+                return this->getOption(unfoldBeliefMdpOption).getArgumentByName("value").getValueAsUnsignedInteger();
+            }
+            
         } // namespace modules
     } // namespace settings
 } // namespace storm

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

@@ -27,7 +27,8 @@ namespace storm {
                 bool isNumericPrecisionSetFromDefault() const;
                 double getNumericPrecision() const;
                 bool isCacheSimplicesSet() const;
-                
+                bool isUnfoldBeliefMdpSizeThresholdSet() const;
+                uint64_t getUnfoldBeliefMdpSizeThreshold() const;
                 // The name of the module.
                 static const std::string moduleName;
 

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

@@ -109,6 +109,7 @@ namespace storm {
                     options.refinementPrecision = storm::utility::convertNumber<ValueType>(gridSettings.getRefinementPrecision());
                     options.numericPrecision = storm::utility::convertNumber<ValueType>(gridSettings.getNumericPrecision());
                     options.cacheSubsimplices = gridSettings.isCacheSimplicesSet();
+                    options.beliefMdpSizeThreshold = gridSettings.getUnfoldBeliefMdpSizeThreshold();
                     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.");

src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp

@@ -35,6 +35,7 @@ namespace storm {
                 refinementPrecision = storm::utility::convertNumber<ValueType>(1e-4);
                 numericPrecision = storm::NumberTraits<ValueType>::IsExact ? storm::utility::zero<ValueType>() : storm::utility::convertNumber<ValueType>(1e-9);
                 cacheSubsimplices = false;
+                beliefMdpSizeThreshold = 0ull;
             }
             
             template<typename PomdpModelType, typename BeliefValueType>
@@ -180,7 +181,7 @@ namespace storm {
                         approx->getExploredMdp()->printModelInformationToStream(std::cout);
                         ValueType& resultValue = min ? result.lowerBound : result.upperBound;
                         resultValue = approx->getComputedValueAtInitialState();
-                        underApproxSizeThreshold = approx->getExploredMdp()->getNumberOfStates();
+                        underApproxSizeThreshold = std::max(approx->getExploredMdp()->getNumberOfStates(), underApproxSizeThreshold);
                     }
                 }
                 { // Underapproximation (Uses a fresh Belief manager)
@@ -189,6 +190,12 @@ namespace storm {
                         manager->setRewardModel(rewardModelName);
                     }
                     auto approx = std::make_shared<ExplorerType>(manager, lowerPomdpValueBounds, upperPomdpValueBounds);
+                    if (options.beliefMdpSizeThreshold) {
+                        underApproxSizeThreshold = options.beliefMdpSizeThreshold.get();
+                    }
+                    if (underApproxSizeThreshold == 0) {
+                        underApproxSizeThreshold = pomdp.getNumberOfStates() * pomdp.getMaxNrStatesWithSameObservation(); // Heuristically select this (only relevant if the over-approx could not be build)
+                    }
                     buildUnderApproximation(targetObservations, min, rewardModelName.is_initialized(), underApproxSizeThreshold, manager, approx);
                     if (approx->hasComputedValues()) {
                         STORM_PRINT_AND_LOG("Explored and checked Under-Approximation MDP:\n");
@@ -221,7 +228,12 @@ namespace storm {
                 overApproxValue = overApproximation->getComputedValueAtInitialState();
                 
                 // UnderApproximation
-                uint64_t underApproxSizeThreshold = std::max<uint64_t>(overApproximation->getExploredMdp()->getNumberOfStates(), 10);
+                uint64_t underApproxSizeThreshold;
+                if (options.beliefMdpSizeThreshold && options.beliefMdpSizeThreshold.get() > 0ull) {
+                    underApproxSizeThreshold = options.beliefMdpSizeThreshold.get();
+                } else {
+                    underApproxSizeThreshold = overApproximation->getExploredMdp()->getNumberOfStates();
+                }
                 auto underApproximation = std::make_shared<ExplorerType>(underApproxBeliefManager, lowerPomdpValueBounds, upperPomdpValueBounds);
                 buildUnderApproximation(targetObservations, min, rewardModelName.is_initialized(), underApproxSizeThreshold, underApproxBeliefManager, underApproximation);
                 if (!underApproximation->hasComputedValues()) {

src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h

@@ -34,6 +34,7 @@ namespace storm {
                     ValueType refinementPrecision; /// Used to decide when the refinement should terminate
                     ValueType numericPrecision; /// Used to decide whether two values are equal
                     bool cacheSubsimplices; /// Enables caching of subsimplices
+                    boost::optional<uint64_t> beliefMdpSizeThreshold; /// Sets the (initial) size of the unfolded belief MDP. 0 means auto selection.
                 };
                 
                 struct Result {