diff --git a/src/storm-pomdp-cli/settings/PomdpSettings.cpp b/src/storm-pomdp-cli/settings/PomdpSettings.cpp index 1181bb2ff..257a62e08 100644 --- a/src/storm-pomdp-cli/settings/PomdpSettings.cpp +++ b/src/storm-pomdp-cli/settings/PomdpSettings.cpp @@ -32,6 +32,7 @@ #include "storm-pomdp-cli/settings/modules/POMDPSettings.h" #include "storm-pomdp-cli/settings/modules/GridApproximationSettings.h" +#include "storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h" namespace storm { namespace settings { @@ -46,7 +47,9 @@ namespace storm { storm::settings::addModule(); storm::settings::addModule(); - + storm::settings::addModule(); + + storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); diff --git a/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp b/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp index 4ba3f8148..16b516b5b 100644 --- a/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp +++ b/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp @@ -27,7 +27,7 @@ namespace storm { const std::string transformBinaryOption = "transformbinary"; const std::string transformSimpleOption = "transformsimple"; const std::string memlessSearchOption = "memlesssearch"; - std::vector memlessSearchMethods = {"none", "ccdmemless", "ccdmemory", "iterative"}; + std::vector memlessSearchMethods = {"none", "ccd-memless", "ccd-memory", "iterative"}; const std::string checkFullyObservableOption = "check-fully-observable"; POMDPSettings::POMDPSettings() : ModuleSettings(moduleName) { diff --git a/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.cpp b/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.cpp index 6c9a62d18..85bfd78dc 100644 --- a/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.cpp +++ b/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.cpp @@ -13,15 +13,17 @@ namespace storm { namespace modules { const std::string QualitativePOMDPAnalysisSettings::moduleName = "pomdpQualitative"; - const std::string exportSATCallsOption = "exportSATCallsPath"; - const std::string lookaheadHorizonOption = "lookaheadHorizon"; - const std::string onlyDeterministicOption = "onlyDeterministic"; + const std::string exportSATCallsOption = "exportSATcallspath"; + const std::string lookaheadHorizonOption = "lookaheadhorizon"; + const std::string onlyDeterministicOption = "onlydeterministic"; + const std::string winningRegionOption = "winningregion"; 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, 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, winningRegionOption, false, "Search for the winning region").build()); } uint64_t QualitativePOMDPAnalysisSettings::getLookahead() const { @@ -39,6 +41,9 @@ namespace storm { return this->getOption(onlyDeterministicOption).getHasOptionBeenSet(); } + bool QualitativePOMDPAnalysisSettings::isWinningRegionSet() const { + return this->getOption(winningRegionOption).getHasOptionBeenSet(); + } void QualitativePOMDPAnalysisSettings::finalize() { } diff --git a/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h b/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h index 30682e625..62ab3357e 100644 --- a/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h +++ b/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h @@ -24,6 +24,7 @@ namespace storm { bool isExportSATCallsSet() const; std::string getExportSATCallsPath() const; bool isOnlyDeterministicSet() const; + bool isWinningRegionSet() const; virtual ~QualitativePOMDPAnalysisSettings() = default; diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index c339e40c8..a62191829 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/src/storm-pomdp-cli/storm-pomdp.cpp @@ -4,6 +4,7 @@ #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/modules/QualitativePOMDPAnalysisSettings.h" #include "storm-pomdp-cli/settings/PomdpSettings.h" #include "storm/analysis/GraphConditions.h" @@ -115,14 +116,15 @@ // return validFormula; //} // -//template -//std::set extractObservations(storm::models::sparse::Pomdp const& pomdp, storm::storage::BitVector const& states) { -// std::set observations; -// for(auto state : states) { -// observations.insert(pomdp.getObservation(state)); -// } -// return observations; -//} +template +std::set extractObservations(storm::models::sparse::Pomdp const& pomdp, storm::storage::BitVector const& states) { + // TODO move. + std::set observations; + for(auto state : states) { + observations.insert(pomdp.getObservation(state)); + } + return observations; +} // ///*! // * Entry point for the pomdp backend. @@ -236,7 +238,6 @@ namespace storm { STORM_PRINT_AND_LOG(oldChoiceCount - pomdp->getNumberOfChoices() << " choices eliminated through self-loop elimination." << std::endl); preprocessingPerformed = true; } ->>>>>>> prism-pomdp } if (pomdpSettings.isQualitativeReductionSet() && formulaInfo.isNonNestedReachabilityProbability()) { storm::analysis::QualitativeAnalysis qualitativeAnalysis(*pomdp); @@ -271,6 +272,78 @@ namespace storm { STORM_PRINT_AND_LOG(")"); } } + + 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(); + auto const& qualSettings = 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::QualitativeAnalysis qualitativeAnalysis(*pomdp); + // After preprocessing, this might be done cheaper. + storm::storage::BitVector targetStates = qualitativeAnalysis.analyseProb1(formula.asProbabilityOperatorFormula()); + STORM_LOG_TRACE("target states: " << targetStates); + storm::storage::BitVector surelyNotAlmostSurelyReachTarget = qualitativeAnalysis.analyseProbSmaller1(formula.asProbabilityOperatorFormula()); + std::set targetObservationSet = extractObservations(*pomdp, targetStates); + + storm::expressions::ExpressionManager expressionManager; + std::shared_ptr smtSolverFactory = std::make_shared(); + + uint64_t lookahead = qualSettings.getLookahead(); + if (lookahead == 0) { + lookahead = pomdp->getNumberOfStates(); + } + storm::pomdp::MemlessSearchOptions options; + + options.onlyDeterministicStrategies = qualSettings.isOnlyDeterministicSet(); + uint64_t loglevel = 0; + // TODO a big ugly, but we have our own loglevels. + if(storm::utility::getLogLevel() == l3pp::LogLevel::INFO) { + loglevel = 1; + } + else if(storm::utility::getLogLevel() == l3pp::LogLevel::DEBUG) { + loglevel = 2; + } + else if(storm::utility::getLogLevel() == l3pp::LogLevel::TRACE) { + loglevel = 3; + } + options.setDebugLevel(loglevel); + + if (qualSettings.isExportSATCallsSet()) { + options.setExportSATCalls(qualSettings.getExportSATCallsPath()); + } + + if (storm::utility::graph::checkIfECWithChoiceExists(pomdp->getTransitionMatrix(), pomdp->getBackwardTransitions(), ~targetStates & ~surelyNotAlmostSurelyReachTarget, storm::storage::BitVector(pomdp->getNumberOfChoices(), true))) { + options.lookaheadRequired = true; + STORM_LOG_DEBUG("Lookahead required."); + } else { + options.lookaheadRequired = false; + STORM_LOG_DEBUG("No lookahead required."); + } + + STORM_LOG_TRACE("target states: " << targetStates); + if (pomdpSettings.getMemlessSearchMethod() == "ccd-memless") { + storm::pomdp::QualitativeStrategySearchNaive memlessSearch(*pomdp, targetObservationSet, 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, targetObservationSet, targetStates, surelyNotAlmostSurelyReachTarget, smtSolverFactory, options); + if (qualSettings.isWinningRegionSet()) { + search.findNewStrategyForSomeState(lookahead); + } else { + search.analyzeForInitialStates(lookahead); + } + search.finalizeStatistics(); + search.getStatistics().print(); + } else { + STORM_LOG_ERROR("This method is not implemented."); + } + } template bool performAnalysis(std::shared_ptr> const& pomdp, storm::pomdp::analysis::FormulaInformation const& formulaInfo, storm::logic::Formula const& formula) { @@ -311,69 +384,9 @@ namespace storm { analysisPerformed = true; } if (pomdpSettings.isMemlessSearchSet()) { - STORM_LOG_THROW(formulaInfo.isNonNestedReachabilityProbability(), storm::exceptions::NotSupportedException, "Qualitative memoryless scheduler search is not implemented for this property type."); - - storm::analysis::QualitativeAnalysis qualitativeAnalysis(*pomdp); - // After preprocessing, this might be done cheaper. - storm::storage::BitVector targetStates = qualitativeAnalysis.analyseProb1(formula->asProbabilityOperatorFormula()); - storm::storage::BitVector surelyNotAlmostSurelyReachTarget = qualitativeAnalysis.analyseProbSmaller1(formula->asProbabilityOperatorFormula()); - std::set targetObservationSet = extractObservations(*pomdp, targetStates); - - - - // std::cout << std::endl; - // pomdp->writeDotToStream(std::cout); - // std::cout << std::endl; - // std::cout << std::endl; - - storm::expressions::ExpressionManager expressionManager; - std::shared_ptr smtSolverFactory = std::make_shared(); - - uint64_t lookahead = pomdpQualSettings.getLookahead(); - if (lookahead == 0) { - lookahead = pomdp->getNumberOfStates(); - } - storm::pomdp::MemlessSearchOptions options; - - options.onlyDeterministicStrategies = pomdpQualSettings.isOnlyDeterministicSet(); - uint64_t loglevel = 0; - // TODO a big ugly, but we have our own loglevels. - if(storm::utility::getLogLevel() == l3pp::LogLevel::INFO) { - loglevel = 1; - } - else if(storm::utility::getLogLevel() == l3pp::LogLevel::DEBUG) { - loglevel = 2; - } - else if(storm::utility::getLogLevel() == l3pp::LogLevel::TRACE) { - loglevel = 3; - } - options.setDebugLevel(loglevel); - - if (pomdpQualSettings.isExportSATCallsSet()) { - options.setExportSATCalls(pomdpQualSettings.getExportSATCallsPath()); - } - - if (storm::utility::graph::checkIfECWithChoiceExists(pomdp->getTransitionMatrix(), pomdp->getBackwardTransitions(), ~targetStates & ~surelyNotAlmostSurelyReachTarget, storm::storage::BitVector(pomdp->getNumberOfChoices(), true))) { - options.lookaheadRequired = true; - STORM_LOG_DEBUG("Lookahead required."); - } else { - options.lookaheadRequired = false; - STORM_LOG_DEBUG("No lookahead required."); - } - - - if (pomdpSettings.getMemlessSearchMethod() == "ccd16memless") { - storm::pomdp::QualitativeStrategySearchNaive memlessSearch(*pomdp, targetObservationSet, targetStates, surelyNotAlmostSurelyReachTarget, smtSolverFactory); - memlessSearch.findNewStrategyForSomeState(lookahead); - } else if (pomdpSettings.getMemlessSearchMethod() == "iterative") { - storm::pomdp::MemlessStrategySearchQualitative memlessSearch(*pomdp, targetObservationSet, targetStates, surelyNotAlmostSurelyReachTarget, smtSolverFactory, options); - memlessSearch.findNewStrategyForSomeState(lookahead); - memlessSearch.finalizeStatistics(); - memlessSearch.getStatistics().print(); - } else { - STORM_LOG_ERROR("This method is not implemented."); - } + performQualitativeAnalysis(pomdp, formulaInfo, formula); analysisPerformed = true; + } if (pomdpSettings.isCheckFullyObservableSet()) { STORM_PRINT_AND_LOG("Analyzing the formula on the fully observable MDP ... "); @@ -488,15 +501,6 @@ namespace storm { storm::transformer::MakePOMDPCanonic makeCanonic(*pomdp); pomdp = makeCanonic.transform(); -// if (ioSettings.isExportDotSet()) { -// std::shared_ptr> sparseModel = pomdp; -// storm::api::exportSparseModelAsDot(sparseModel, ioSettings.getExportDotFilename(), ioSettings.getExportDotMaxWidth()); -// } -// if (ioSettings.isExportExplicitSet()) { -// std::shared_ptr> sparseModel = pomdp; -// storm::api::exportSparseModelAsDrn(sparseModel, ioSettings.getExportExplicitFilename()); -// } - std::shared_ptr formula; if (!symbolicInput.properties.empty()) { formula = symbolicInput.properties.front().getRawFormula(); @@ -521,18 +525,20 @@ namespace storm { STORM_PRINT_AND_LOG("Time for graph-based POMDP (pre-)processing: " << sw << "s." << std::endl); pomdp->printModelInformationToStream(std::cout); } - + sw.restart(); - if (performAnalysis(pomdp, formulaInfo, *formula)) { + if (performTransformation(pomdp, *formula)) { sw.stop(); - STORM_PRINT_AND_LOG("Time for POMDP analysis: " << sw << "s." << std::endl); + STORM_PRINT_AND_LOG("Time for POMDP transformation(s): " << sw << "s." << std::endl); } sw.restart(); - if (performTransformation(pomdp, *formula)) { + if (performAnalysis(pomdp, formulaInfo, *formula)) { sw.stop(); - STORM_PRINT_AND_LOG("Time for POMDP transformation(s): " << sw << "s." << std::endl); + STORM_PRINT_AND_LOG("Time for POMDP analysis: " << sw << "s." << std::endl); } + + } else { STORM_LOG_WARN("Nothing to be done. Did you forget to specify a formula?"); }