From bf7f84f796d48a2886e50665bf638e0021c3b1a1 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 18 Mar 2020 09:53:48 +0100 Subject: [PATCH] Added --check-fully-observable option to easily check the underlying MDP --- .../settings/modules/POMDPSettings.cpp | 9 ++++++++- .../settings/modules/POMDPSettings.h | 1 + src/storm-pomdp-cli/storm-pomdp.cpp | 18 ++++++++++++++---- 3 files changed, 23 insertions(+), 5 deletions(-) diff --git a/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp b/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp index 37addcbab..dc5539b43 100644 --- a/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp +++ b/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp @@ -29,6 +29,7 @@ namespace storm { const std::string transformSimpleOption = "transformsimple"; const std::string memlessSearchOption = "memlesssearch"; std::vector memlessSearchMethods = {"none", "ccdmemless", "ccdmemory", "iterative"}; + const std::string checkFullyObservableOption = "check-fully-observable"; POMDPSettings::POMDPSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, exportAsParametricModelOption, false, "Export the parametric file.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which to write the model.").build()).build()); @@ -41,10 +42,12 @@ 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).addValidatorUnsignedInteger(storm::settings::ArgumentValidatorFactory::createUnsignedGreaterValidator(0)).build()).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, 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()); + } bool POMDPSettings::isExportToParametricSet() const { @@ -83,6 +86,10 @@ namespace storm { return this->getOption(memlessSearchOption).getHasOptionBeenSet(); } + bool POMDPSettings::isCheckFullyObservableSet() const { + return this->getOption(checkFullyObservableOption).getHasOptionBeenSet(); + } + std::string POMDPSettings::getMemlessSearchMethod() const { return this->getOption(memlessSearchOption).getArgumentByName("method").getValueAsString(); } diff --git a/src/storm-pomdp-cli/settings/modules/POMDPSettings.h b/src/storm-pomdp-cli/settings/modules/POMDPSettings.h index 5af7ea589..891cca9e0 100644 --- a/src/storm-pomdp-cli/settings/modules/POMDPSettings.h +++ b/src/storm-pomdp-cli/settings/modules/POMDPSettings.h @@ -34,6 +34,7 @@ namespace storm { bool isTransformSimpleSet() const; bool isTransformBinarySet() const; bool isMemlessSearchSet() const; + bool isCheckFullyObservableSet() const; std::string getMemlessSearchMethod() const; std::string getFscApplicationTypeString() const; uint64_t getMemoryBound() const; diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index 634316e33..ee1877531 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/src/storm-pomdp-cli/storm-pomdp.cpp @@ -27,6 +27,8 @@ #include "storm-pomdp/analysis/QualitativeStrategySearchNaive.h" #include "storm/api/storm.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/utility/Stopwatch.h" #include "storm/exceptions/UnexpectedException.h" @@ -93,10 +95,11 @@ namespace storm { } template - bool performAnalysis(std::shared_ptr> const& pomdp, storm::pomdp::analysis::FormulaInformation const& formulaInfo) { + bool performAnalysis(std::shared_ptr> const& pomdp, storm::pomdp::analysis::FormulaInformation const& formulaInfo, storm::logic::Formula const& formula) { auto const& pomdpSettings = storm::settings::getModule(); 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."); @@ -111,8 +114,8 @@ namespace storm { ValueType overRes = result->overApproxValue; ValueType underRes = result->underApproxValue; if (overRes != underRes) { - STORM_PRINT("Overapproximation Result: " << overRes << std::endl) - STORM_PRINT("Underapproximation Result: " << underRes << std::endl) + STORM_PRINT("Overapproximation Result: " << overRes << std::endl); + STORM_PRINT("Underapproximation Result: " << underRes << std::endl); } else { STORM_PRINT("Result: " << overRes << std::endl) } @@ -138,6 +141,13 @@ namespace storm { } analysisPerformed = true; } + if (pomdpSettings.isCheckFullyObservableSet()) { + STORM_PRINT_AND_LOG("Analyzing the formula on the fully observable MDP ... "); + auto result = storm::api::verifyWithSparseEngine(pomdp->template as>(), storm::api::createTask(formula.asSharedPointer(), true))->template asExplicitQuantitativeCheckResult(); + result.filter(storm::modelchecker::ExplicitQualitativeCheckResult(pomdp->getInitialStates())); + STORM_PRINT_AND_LOG("Result: " << result.getMax() << std::endl); + analysisPerformed = true; + } return analysisPerformed; } @@ -259,7 +269,7 @@ namespace storm { } sw.restart(); - if (performAnalysis(pomdp, formulaInfo)) { + if (performAnalysis(pomdp, formulaInfo, *formula)) { sw.stop(); STORM_PRINT_AND_LOG("Time for POMDP analysis: " << sw << "s." << std::endl); }