sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Added --check-fully-observable option to easily check the underlying MDP

tempestpy_adaptions
Tim Quatmann 5 years ago
parent
5bdcb66fcb
commit
bf7f84f796
3 changed files with 23 additions and 5 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 9
      src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp
  2. 1
      src/storm-pomdp-cli/settings/modules/POMDPSettings.h
  3. 18
      src/storm-pomdp-cli/storm-pomdp.cpp

9
src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp
View File

@ -29,6 +29,7 @@ namespace storm {
const std::string transformSimpleOption = "transformsimple";
const std::string memlessSearchOption = "memlesssearch";
std::vector<std::string> 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();
}

1
src/storm-pomdp-cli/settings/modules/POMDPSettings.h
View File

@ -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;

18
src/storm-pomdp-cli/storm-pomdp.cpp
View File

@ -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<typename ValueType, storm::dd::DdType DdType>
bool performAnalysis(std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> const& pomdp, storm::pomdp::analysis::FormulaInformation const& formulaInfo) {
bool performAnalysis(std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> const& pomdp, storm::pomdp::analysis::FormulaInformation const& formulaInfo, storm::logic::Formula const& formula) {
auto const& pomdpSettings = storm::settings::getModule<storm::settings::modules::POMDPSettings>();
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<ValueType>(pomdp->template as<storm::models::sparse::Mdp<ValueType>>(), storm::api::createTask<ValueType>(formula.asSharedPointer(), true))->template asExplicitQuantitativeCheckResult<ValueType>();
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<ValueType, DdType>(pomdp, formulaInfo)) {
if (performAnalysis<ValueType, DdType>(pomdp, formulaInfo, *formula)) {
sw.stop();
STORM_PRINT_AND_LOG("Time for POMDP analysis: " << sw << "s." << std::endl);
}

Write Preview
Loading…
Cancel
Save