diff --git a/CHANGELOG.md b/CHANGELOG.md index 8a20071d4..40ee6caa3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -16,6 +16,7 @@ Version 1.5.x - `storm-counterexamples`: fix when computing multiple counterexamples in debug mode - `storm-dft`: Renamed setting `--show-dft-stats` to `dft-statistics` and added approximation information to statistics. - `storm-pomdp`: Implemented approximation algorithms that explore (a discritization of) the belief MDP, allowing to compute safe lower- and upper bounds for a given property. +- `storm-pomdp`: Implemented almost-sure reachability computations: graph-based, one-shot SAT-based, and iterative SAT-based ## Version 1.5.1 (2020/03) - Jani models are now parsed using exact arithmetic. diff --git a/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp b/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp index 6fb690c24..c009ba36d 100644 --- a/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp +++ b/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp @@ -28,9 +28,8 @@ namespace storm { std::vector fscModes = {"standard", "simple-linear", "simple-linear-inverse"}; const std::string transformBinaryOption = "transformbinary"; const std::string transformSimpleOption = "transformsimple"; - const std::string memlessSearchOption = "memlesssearch"; - std::vector memlessSearchMethods = {"none", "ccd-memless", "ccd-memory", "iterative"}; const std::string checkFullyObservableOption = "check-fully-observable"; + const std::string isQualitativeOption = "qualitative-analysis"; 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()); @@ -45,9 +44,8 @@ namespace storm { 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, beliefExplorationOption, false,"Analyze the POMDP by exploring the belief state-space.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "Sets whether lower, upper, or interval result bounds are computed.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(beliefExplorationModes)).setDefaultValueString("both").makeOptional().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()); - + this->addOption(storm::settings::OptionBuilder(moduleName, isQualitativeOption, false, "Sets the option qualitative analysis").build()); } bool POMDPSettings::isNoCanonicSet() const { @@ -92,18 +90,15 @@ namespace storm { return isBeliefExplorationSet() && (arg == "unfold" || arg == "both"); } - bool POMDPSettings::isMemlessSearchSet() const { - 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(); + bool POMDPSettings::isQualitativeAnalysisSet() const { + return this->getOption(isQualitativeOption).getHasOptionBeenSet(); } + 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 d1a9e6b82..30b0adc53 100644 --- a/src/storm-pomdp-cli/settings/modules/POMDPSettings.h +++ b/src/storm-pomdp-cli/settings/modules/POMDPSettings.h @@ -35,9 +35,8 @@ namespace storm { bool isSelfloopReductionSet() const; bool isTransformSimpleSet() const; bool isTransformBinarySet() const; - bool isMemlessSearchSet() const; bool isCheckFullyObservableSet() const; - std::string getMemlessSearchMethod() const; + bool isQualitativeAnalysisSet() const; std::string getFscApplicationTypeString() const; uint64_t getMemoryBound() const; diff --git a/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.cpp b/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.cpp index 86a5e5ee8..1d6ff6d49 100644 --- a/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.cpp +++ b/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.cpp @@ -18,19 +18,38 @@ namespace storm { const std::string onlyDeterministicOption = "onlydeterministic"; const std::string winningRegionOption = "winningregion"; const std::string validationLevel = "validate"; + const std::string lookaheadTypeOption = "lookaheadtype"; + const std::string expensiveStatsOption = "allstats"; + const std::string printWinningRegionOption = "printwinningregion"; + const std::string exportWinningRegionOption = "exportwinningregion"; + const std::string preventGraphPreprocessing = "nographprocessing"; + const std::string memlessSearchOption = "memlesssearch"; + std::vector memlessSearchMethods = {"one-shot", "iterative"}; + QualitativePOMDPAnalysisSettings::QualitativePOMDPAnalysisSettings() : ModuleSettings(moduleName) { - this->addOption(storm::settings::OptionBuilder(moduleName, exportSATCallsOption, false, "Export the SAT calls?.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "The name of the file to which to write the model.").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, memlessSearchOption, false, "Search for a qualitative memoryless scheduler").addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "method name").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(memlessSearchMethods)).setDefaultValueString("iterative").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, exportSATCallsOption, false, "Export the SAT calls?.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "The name of the path to which to write the models.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, lookaheadHorizonOption, false, "In reachability in combination with a discrete ranking function, a lookahead is necessary.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("bound", "The lookahead. Use 0 for the number of states.").setDefaultValueUnsignedInteger(0).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, onlyDeterministicOption, false, "Search only for deterministic schedulers").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, onlyDeterministicOption, false, "Search only for deterministic schedulers").setIsAdvanced().build()); this->addOption(storm::settings::OptionBuilder(moduleName, winningRegionOption, false, "Search for the winning region").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, validationLevel, false, "Validate algorithm during runtime (for debugging)").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("level", "how regular to apply this validation. Use 0 for never, 1 for the end, and >=2 within computation steps.").setDefaultValueUnsignedInteger(0).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, lookaheadTypeOption, false, "What type to use for the ranking function").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("type", "The type.").setDefaultValueString("real").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator({"bool", "int", "real"})).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, validationLevel, true, "Validate algorithm during runtime (for debugging)").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("level", "how regular to apply this validation. Use 0 for never, 1 for the end, and >=2 within computation steps.").setDefaultValueUnsignedInteger(0).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, expensiveStatsOption, true, "Compute all stats, even if this is expensive.").setIsAdvanced().build()); + this->addOption(storm::settings::OptionBuilder(moduleName, printWinningRegionOption, false, "Print Winning Region").setIsAdvanced().build()); + this->addOption(storm::settings::OptionBuilder(moduleName, exportWinningRegionOption, false, "Export the winning region.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "The name of the file to which to write the winning region.").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, preventGraphPreprocessing, true, "Prevent graph preprocessing (for debugging)").setIsAdvanced().build()); } uint64_t QualitativePOMDPAnalysisSettings::getLookahead() const { return this->getOption(lookaheadHorizonOption).getArgumentByName("bound").getValueAsUnsignedInteger(); } + + std::string QualitativePOMDPAnalysisSettings::getLookaheadType() const { + return this->getOption(lookaheadTypeOption).getArgumentByName("type").getValueAsString(); + } + bool QualitativePOMDPAnalysisSettings::isExportSATCallsSet() const { return this->getOption(exportSATCallsOption).getHasOptionBeenSet(); } @@ -54,6 +73,30 @@ namespace storm { return this->getOption(validationLevel).getArgumentByName("level").getValueAsUnsignedInteger() >= 1; } + bool QualitativePOMDPAnalysisSettings::computeExpensiveStats() const { + return this->getOption(expensiveStatsOption).getHasOptionBeenSet(); + } + + std::string QualitativePOMDPAnalysisSettings::exportWinningRegionPath() const { + return this->getOption(exportWinningRegionOption).getArgumentByName("path").getValueAsString(); + } + + bool QualitativePOMDPAnalysisSettings::isExportWinningRegionSet() const { + return this->getOption(exportWinningRegionOption).getHasOptionBeenSet(); + } + + bool QualitativePOMDPAnalysisSettings::isPrintWinningRegionSet() const { + return this->getOption(printWinningRegionOption).getHasOptionBeenSet(); + } + + bool QualitativePOMDPAnalysisSettings::isMemlessSearchSet() const { + return this->getOption(memlessSearchOption).getHasOptionBeenSet(); + } + + std::string QualitativePOMDPAnalysisSettings::getMemlessSearchMethod() const { + return this->getOption(memlessSearchOption).getArgumentByName("method").getValueAsString(); + } + void QualitativePOMDPAnalysisSettings::finalize() { } diff --git a/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h b/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h index 6f0fb3ebc..cebb356e3 100644 --- a/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h +++ b/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h @@ -21,12 +21,21 @@ namespace storm { QualitativePOMDPAnalysisSettings(); uint64_t getLookahead() const; + std::string getLookaheadType() const; bool isExportSATCallsSet() const; std::string getExportSATCallsPath() const; bool isOnlyDeterministicSet() const; bool isWinningRegionSet() const; bool validateIntermediateSteps() const; bool validateFinalResult() const; + bool computeExpensiveStats() const; + bool isPrintWinningRegionSet() const; + bool isExportWinningRegionSet() const; + std::string exportWinningRegionPath() const; + bool isGraphPreprocessingAllowed() const; + bool isMemlessSearchSet() const; + std::string getMemlessSearchMethod() const; + virtual ~QualitativePOMDPAnalysisSettings() = default; diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index 6cdcfd95e..d42ac48e6 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/src/storm-pomdp-cli/storm-pomdp.cpp @@ -129,6 +129,8 @@ namespace storm { options.validateEveryStep = qualSettings.validateIntermediateSteps(); options.validateResult = qualSettings.validateFinalResult(); + options.pathVariableType = storm::pomdp::pathVariableTypeFromString(qualSettings.getLookaheadType()); + if (qualSettings.isExportSATCallsSet()) { options.setExportSATCalls(qualSettings.getExportSATCallsPath()); } @@ -137,42 +139,79 @@ namespace storm { } template - void performQualitativeAnalysis(std::shared_ptr> const& pomdp, storm::pomdp::analysis::FormulaInformation const& formulaInfo, storm::logic::Formula const& formula) { - auto const& pomdpSettings = storm::settings::getModule(); + void performQualitativeAnalysis(std::shared_ptr> const& origpomdp, storm::pomdp::analysis::FormulaInformation const& formulaInfo, storm::logic::Formula const& formula) { auto const& qualSettings = storm::settings::getModule(); + auto const& coreSettings = storm::settings::getModule(); STORM_LOG_THROW(formulaInfo.isNonNestedReachabilityProbability(), storm::exceptions::NotSupportedException, "Qualitative memoryless scheduler search is not implemented for this property type."); STORM_LOG_TRACE("Run qualitative preprocessing..."); - storm::analysis::QualitativeAnalysisOnGraphs qualitativeAnalysis(*pomdp); + storm::models::sparse::Pomdp pomdp(*origpomdp); + storm::analysis::QualitativeAnalysisOnGraphs qualitativeAnalysis(pomdp); // After preprocessing, this might be done cheaper. + storm::storage::BitVector surelyNotAlmostSurelyReachTarget = qualitativeAnalysis.analyseProbSmaller1( + formula.asProbabilityOperatorFormula()); + pomdp.getTransitionMatrix().makeRowGroupsAbsorbing(surelyNotAlmostSurelyReachTarget); storm::storage::BitVector targetStates = qualitativeAnalysis.analyseProb1(formula.asProbabilityOperatorFormula()); - storm::storage::BitVector surelyNotAlmostSurelyReachTarget = qualitativeAnalysis.analyseProbSmaller1(formula.asProbabilityOperatorFormula()); storm::expressions::ExpressionManager expressionManager; std::shared_ptr smtSolverFactory = std::make_shared(); - storm::pomdp::MemlessSearchOptions options = fillMemlessSearchOptionsFromSettings(); uint64_t lookahead = qualSettings.getLookahead(); if (lookahead == 0) { - lookahead = pomdp->getNumberOfStates(); + lookahead = pomdp.getNumberOfStates(); } STORM_LOG_TRACE("target states: " << targetStates); - if (pomdpSettings.getMemlessSearchMethod() == "ccd-memless") { - storm::pomdp::QualitativeStrategySearchNaive memlessSearch(*pomdp, targetStates, surelyNotAlmostSurelyReachTarget, smtSolverFactory); + if (qualSettings.getMemlessSearchMethod() == "one-shot") { + storm::pomdp::QualitativeStrategySearchNaive memlessSearch(pomdp, targetStates, surelyNotAlmostSurelyReachTarget, smtSolverFactory); if (qualSettings.isWinningRegionSet()) { STORM_LOG_ERROR("Computing winning regions is not supported by ccd-memless."); } else { memlessSearch.analyzeForInitialStates(lookahead); } - } else if (pomdpSettings.getMemlessSearchMethod() == "iterative") { - storm::pomdp::MemlessStrategySearchQualitative search(*pomdp, targetStates, surelyNotAlmostSurelyReachTarget, smtSolverFactory, options); + } else if (qualSettings.getMemlessSearchMethod() == "iterative") { + storm::pomdp::MemlessStrategySearchQualitative search(pomdp, targetStates, surelyNotAlmostSurelyReachTarget, smtSolverFactory, options); if (qualSettings.isWinningRegionSet()) { search.computeWinningRegion(lookahead); } else { search.analyzeForInitialStates(lookahead); } + + if (qualSettings.isPrintWinningRegionSet()) { + search.getLastWinningRegion().print(); + std::cout << std::endl; + } + if (qualSettings.isExportWinningRegionSet()) { + search.getLastWinningRegion().storeToFile(qualSettings.exportWinningRegionPath()); + } + search.finalizeStatistics(); - search.getStatistics().print(); + if(pomdp.getInitialStates().getNumberOfSetBits() == 1) { + uint64_t initialState = pomdp.getInitialStates().getNextSetIndex(0); + uint64_t initialObservation = pomdp.getObservation(initialState); + // TODO this is inefficient. + uint64_t offset = 0; + for (uint64_t state = 0; state < pomdp.getNumberOfStates(); ++state) { + if (state == initialState) { + break; + } + if (pomdp.getObservation(state) == initialObservation) { + ++offset; + } + } + STORM_PRINT_AND_LOG("Initial state is safe: " << search.getLastWinningRegion().isWinning(initialObservation, offset)); + } else { + STORM_LOG_WARN("Output for multiple initial states is incomplete"); + } + std::cout << "Number of belief support states: " << search.getLastWinningRegion().beliefSupportStates() << std::endl; + if (coreSettings.isShowStatisticsSet() && qualSettings.computeExpensiveStats()) { + auto wbss = search.getLastWinningRegion().computeNrWinningBeliefs(); + STORM_PRINT_AND_LOG( "Number of winning belief support states: [" << wbss.first << "," << wbss.second + << "]"); + } + if (coreSettings.isShowStatisticsSet()) { + search.getStatistics().print(); + } + } else { STORM_LOG_ERROR("This method is not implemented."); } @@ -199,7 +238,7 @@ namespace storm { STORM_PRINT_AND_LOG(std::endl); analysisPerformed = true; } - if (pomdpSettings.isMemlessSearchSet()) { + if (pomdpSettings.isQualitativeAnalysisSet()) { performQualitativeAnalysis(pomdp, formulaInfo, formula); analysisPerformed = true;