From 3aaea1eb0a3d3a846d050eb6df56155eaf7ef6ce Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 18 Mar 2020 13:45:32 +0100 Subject: [PATCH] Added new CLI settings for GridApproximation --- .../settings/PomdpSettings.cpp | 2 + .../modules/GridApproximationSettings.cpp | 63 +++++++++++++++++++ .../modules/GridApproximationSettings.h | 40 ++++++++++++ .../settings/modules/POMDPSettings.cpp | 17 +---- .../settings/modules/POMDPSettings.h | 3 - src/storm-pomdp-cli/storm-pomdp.cpp | 45 ++++++------- 6 files changed, 124 insertions(+), 46 deletions(-) create mode 100644 src/storm-pomdp-cli/settings/modules/GridApproximationSettings.cpp create mode 100644 src/storm-pomdp-cli/settings/modules/GridApproximationSettings.h diff --git a/src/storm-pomdp-cli/settings/PomdpSettings.cpp b/src/storm-pomdp-cli/settings/PomdpSettings.cpp index f08dbe932..1181bb2ff 100644 --- a/src/storm-pomdp-cli/settings/PomdpSettings.cpp +++ b/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::addModule(); + storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); diff --git a/src/storm-pomdp-cli/settings/modules/GridApproximationSettings.cpp b/src/storm-pomdp-cli/settings/modules/GridApproximationSettings.cpp new file mode 100644 index 000000000..2aaf3239c --- /dev/null +++ b/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 diff --git a/src/storm-pomdp-cli/settings/modules/GridApproximationSettings.h b/src/storm-pomdp-cli/settings/modules/GridApproximationSettings.h new file mode 100644 index 000000000..5c1e281d4 --- /dev/null +++ b/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 diff --git a/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp b/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp index dc5539b43..4ba3f8148 100644 --- a/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp +++ b/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(); } diff --git a/src/storm-pomdp-cli/settings/modules/POMDPSettings.h b/src/storm-pomdp-cli/settings/modules/POMDPSettings.h index 891cca9e0..768766536 100644 --- a/src/storm-pomdp-cli/settings/modules/POMDPSettings.h +++ b/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; diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index ee1877531..e62b93f4b 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/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 kpt = storm::pomdp::transformer::KnownProbabilityTransformer(); - 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 checker = storm::pomdp::modelchecker::ApproximatePOMDPModelchecker(); - std::unique_ptr> result; - if (formulaInfo.isNonNestedReachabilityProbability()) { - result = checker.refineReachabilityProbability(*pomdp, formulaInfo.getTargetStates().observations, formulaInfo.minimize(), pomdpSettings.getGridResolution(), pomdpSettings.getExplorationThreshold()); - } else { - // TODO: no exploration threshold? - result = checker.computeReachabilityReward(*pomdp, formulaInfo.getTargetStates().observations, formulaInfo.minimize(), pomdpSettings.getGridResolution()); + auto const& gridSettings = storm::settings::getModule(); + typename storm::pomdp::modelchecker::ApproximatePOMDPModelchecker::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::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(); + } else { + 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 checker = storm::pomdp::modelchecker::ApproximatePOMDPModelchecker(*pomdp, options); + std::unique_ptr> result = checker.check(formula); ValueType overRes = result->overApproxValue; ValueType underRes = result->underApproxValue; if (overRes != underRes) {