From 37fa53c4d827ff78b27cc49b5d712e02361961e0 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 1 Apr 2020 12:39:02 +0200 Subject: [PATCH] Added a command-line-switch to disable making a pomdp canonic (for prism compatibility) --- .../settings/modules/POMDPSettings.cpp | 6 +++++ .../settings/modules/POMDPSettings.h | 1 + src/storm-pomdp-cli/storm-pomdp.cpp | 26 +++++++++---------- 3 files changed, 19 insertions(+), 14 deletions(-) diff --git a/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp b/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp index 4ba3f8148..57c065f7a 100644 --- a/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp +++ b/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp @@ -13,6 +13,7 @@ namespace storm { namespace modules { const std::string POMDPSettings::moduleName = "pomdp"; + const std::string noCanonicOption = "nocanonic"; const std::string exportAsParametricModelOption = "parametric-drn"; const std::string gridApproximationOption = "gridapproximation"; const std::string qualitativeReductionOption = "qualitativereduction"; @@ -31,6 +32,7 @@ namespace storm { const std::string checkFullyObservableOption = "check-fully-observable"; POMDPSettings::POMDPSettings() : ModuleSettings(moduleName) { + this->addOption(storm::settings::OptionBuilder(moduleName, noCanonicOption, false, "If this is set, actions will not be ordered canonically. Could yield incorrect results.").build()); 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()); this->addOption(storm::settings::OptionBuilder(moduleName, qualitativeReductionOption, false, "Reduces the model size by performing qualitative analysis (E.g. merge states with prob. 1.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, analyzeUniqueObservationsOption, false, "Computes the states with a unique observation").build()); @@ -47,6 +49,10 @@ namespace storm { } + bool POMDPSettings::isNoCanonicSet() const { + return this->getOption(noCanonicOption).getHasOptionBeenSet(); + } + bool POMDPSettings::isExportToParametricSet() const { return this->getOption(exportAsParametricModelOption).getHasOptionBeenSet(); } diff --git a/src/storm-pomdp-cli/settings/modules/POMDPSettings.h b/src/storm-pomdp-cli/settings/modules/POMDPSettings.h index 768766536..6754ac55c 100644 --- a/src/storm-pomdp-cli/settings/modules/POMDPSettings.h +++ b/src/storm-pomdp-cli/settings/modules/POMDPSettings.h @@ -26,6 +26,7 @@ namespace storm { bool isQualitativeReductionSet() const; + bool isNoCanonicSet() const; bool isGridApproximationSet() const; bool isAnalyzeUniqueObservationsSet() const; bool isMecReductionSet() const; diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index 58637c6e7..9b3026832 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/src/storm-pomdp-cli/storm-pomdp.cpp @@ -102,7 +102,7 @@ namespace storm { if (pomdpSettings.isGridApproximationSet()) { STORM_PRINT_AND_LOG("Applying grid approximation... "); auto const& gridSettings = storm::settings::getModule(); - typename storm::pomdp::modelchecker::ApproximatePOMDPModelchecker::Options options; + typename storm::pomdp::modelchecker::ApproximatePOMDPModelchecker>::Options options; options.initialGridResolution = gridSettings.getGridResolution(); options.explorationThreshold = storm::utility::convertNumber(gridSettings.getExplorationThreshold()); options.doRefinement = gridSettings.isRefineSet(); @@ -117,20 +117,16 @@ namespace storm { 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); + storm::pomdp::modelchecker::ApproximatePOMDPModelchecker> checker(*pomdp, options); + auto result = checker.check(formula); checker.printStatisticsToStream(std::cout); - if (result) { - if (storm::utility::resources::isTerminate()) { - STORM_PRINT_AND_LOG("\nResult till abort: ") - } else { - STORM_PRINT_AND_LOG("\nResult: ") - } - printResult(result->underApproxValue, result->overApproxValue); - STORM_PRINT_AND_LOG(std::endl); + if (storm::utility::resources::isTerminate()) { + STORM_PRINT_AND_LOG("\nResult till abort: ") } else { - STORM_PRINT_AND_LOG("\nResult: Not available." << std::endl); + STORM_PRINT_AND_LOG("\nResult: ") } + printResult(result.lowerBound, result.upperBound); + STORM_PRINT_AND_LOG(std::endl); analysisPerformed = true; } if (pomdpSettings.isMemlessSearchSet()) { @@ -263,8 +259,10 @@ namespace storm { STORM_LOG_THROW(model->getType() == storm::models::ModelType::Pomdp && model->isSparseModel(), storm::exceptions::WrongFormatException, "Expected a POMDP in sparse representation."); std::shared_ptr> pomdp = model->template as>(); - storm::transformer::MakePOMDPCanonic makeCanonic(*pomdp); - pomdp = makeCanonic.transform(); + if (!pomdpSettings.isNoCanonicSet()) { + storm::transformer::MakePOMDPCanonic makeCanonic(*pomdp); + pomdp = makeCanonic.transform(); + } std::shared_ptr formula; if (!symbolicInput.properties.empty()) {