From 03889958dab727f7a50f0f2f703a6a0c4fb055ec Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 8 Apr 2020 11:29:37 +0200 Subject: [PATCH] Added a switch to control the size of the under-approximation via command line. --- .../modules/GridApproximationSettings.cpp | 10 ++++++++++ .../settings/modules/GridApproximationSettings.h | 3 ++- src/storm-pomdp-cli/storm-pomdp.cpp | 1 + .../ApproximatePOMDPModelchecker.cpp | 16 ++++++++++++++-- .../modelchecker/ApproximatePOMDPModelchecker.h | 1 + 5 files changed, 28 insertions(+), 3 deletions(-) diff --git a/src/storm-pomdp-cli/settings/modules/GridApproximationSettings.cpp b/src/storm-pomdp-cli/settings/modules/GridApproximationSettings.cpp index 8006b3851..6b5b17677 100644 --- a/src/storm-pomdp-cli/settings/modules/GridApproximationSettings.cpp +++ b/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 diff --git a/src/storm-pomdp-cli/settings/modules/GridApproximationSettings.h b/src/storm-pomdp-cli/settings/modules/GridApproximationSettings.h index a01fdbd77..88e484128 100644 --- a/src/storm-pomdp-cli/settings/modules/GridApproximationSettings.h +++ b/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; diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index 9b3026832..181c5c31f 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/src/storm-pomdp-cli/storm-pomdp.cpp @@ -109,6 +109,7 @@ namespace storm { options.refinementPrecision = storm::utility::convertNumber(gridSettings.getRefinementPrecision()); options.numericPrecision = storm::utility::convertNumber(gridSettings.getNumericPrecision()); options.cacheSubsimplices = gridSettings.isCacheSimplicesSet(); + options.beliefMdpSizeThreshold = gridSettings.getUnfoldBeliefMdpSizeThreshold(); if (storm::NumberTraits::IsExact) { if (gridSettings.isNumericPrecisionSetFromDefault()) { STORM_LOG_WARN_COND(storm::utility::isZero(options.numericPrecision), "Setting numeric precision to zero because exact arithmethic is used."); diff --git a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp index eb116fc7b..070279ac4 100644 --- a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp +++ b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp @@ -35,6 +35,7 @@ namespace storm { refinementPrecision = storm::utility::convertNumber(1e-4); numericPrecision = storm::NumberTraits::IsExact ? storm::utility::zero() : storm::utility::convertNumber(1e-9); cacheSubsimplices = false; + beliefMdpSizeThreshold = 0ull; } template @@ -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(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(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(underApproxBeliefManager, lowerPomdpValueBounds, upperPomdpValueBounds); buildUnderApproximation(targetObservations, min, rewardModelName.is_initialized(), underApproxSizeThreshold, underApproxBeliefManager, underApproximation); if (!underApproximation->hasComputedValues()) { diff --git a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h index 1d5521b6a..823eebf60 100644 --- a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h +++ b/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 beliefMdpSizeThreshold; /// Sets the (initial) size of the unfolded belief MDP. 0 means auto selection. }; struct Result {