From 4844573b6323b05c758c6d52d89f1621a8e835fe Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sun, 23 May 2021 17:56:29 -0700 Subject: [PATCH] qualitative search: oneshot cleaning and tests --- src/storm-pomdp-cli/storm-pomdp.cpp | 10 +++-- .../analysis/OneShotPolicySearch.h | 9 +---- .../analysis/QualitativeAnalysisTest.cpp | 39 +++++++++++++++++++ 3 files changed, 48 insertions(+), 10 deletions(-) diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index 08b64a406..19c04dc6a 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/src/storm-pomdp-cli/storm-pomdp.cpp @@ -158,9 +158,7 @@ namespace storm { bool computedSomething = false; if (qualSettings.isMemlessSearchSet()) { computedSomething = true; - 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(); @@ -172,9 +170,15 @@ namespace storm { if (qualSettings.isWinningRegionSet()) { STORM_LOG_ERROR("Computing winning regions is not supported by the one-shot method."); } else { - memlessSearch.analyzeForInitialStates(lookahead); + bool result = memlessSearch.analyzeForInitialStates(lookahead); + if (result) { + STORM_PRINT_AND_LOG("From initial state, one can almost-surely reach the target." << std::endl); + } else { + STORM_PRINT_AND_LOG("From initial state, one may not almost-surely reach the target ." << std::endl); + } } } else if (qualSettings.getMemlessSearchMethod() == "iterative") { + storm::pomdp::MemlessSearchOptions options = fillMemlessSearchOptionsFromSettings(); storm::pomdp::IterativePolicySearch search(pomdp, targetStates, surelyNotAlmostSurelyReachTarget, smtSolverFactory, options); diff --git a/src/storm-pomdp/analysis/OneShotPolicySearch.h b/src/storm-pomdp/analysis/OneShotPolicySearch.h index af7203cea..46d566d16 100644 --- a/src/storm-pomdp/analysis/OneShotPolicySearch.h +++ b/src/storm-pomdp/analysis/OneShotPolicySearch.h @@ -49,16 +49,11 @@ namespace storm { surelyReachSinkStates = surelyReachSink; } - void analyzeForInitialStates(uint64_t k) { + bool analyzeForInitialStates(uint64_t k) { STORM_LOG_TRACE("Bad states: " << surelyReachSinkStates); STORM_LOG_TRACE("Target states: " << targetStates); STORM_LOG_TRACE("Questionmark states: " << (~surelyReachSinkStates & ~targetStates)); - bool result = analyze(k, ~surelyReachSinkStates & ~targetStates, pomdp.getInitialStates()); - if (result) { - STORM_PRINT_AND_LOG("From initial state, one can almost-surely reach the target." << std::endl); - } else { - STORM_PRINT_AND_LOG("From initial state, one may not almost-surely reach the target ." << std::endl); - } + return analyze(k, ~surelyReachSinkStates & ~targetStates, pomdp.getInitialStates()); } bool analyze(uint64_t k, storm::storage::BitVector const& oneOfTheseStates, storm::storage::BitVector const& allOfTheseStates = storm::storage::BitVector()); diff --git a/src/test/storm-pomdp/analysis/QualitativeAnalysisTest.cpp b/src/test/storm-pomdp/analysis/QualitativeAnalysisTest.cpp index a61ff0b80..c2e802510 100644 --- a/src/test/storm-pomdp/analysis/QualitativeAnalysisTest.cpp +++ b/src/test/storm-pomdp/analysis/QualitativeAnalysisTest.cpp @@ -7,6 +7,7 @@ #include "storm-parsers/api/storm-parsers.h" #include "storm-pomdp/analysis/FormulaInformation.h" #include "storm-pomdp/analysis/QualitativeAnalysisOnGraphs.h" +#include "storm-pomdp/analysis/OneShotPolicySearch.h" #include "storm-pomdp/transformer/MakePOMDPCanonic.h" void graphalgorithm_test(std::string const& path, std::string const& constants, std::string formulaString) { @@ -26,6 +27,29 @@ void graphalgorithm_test(std::string const& path, std::string const& constants, storm::storage::BitVector targetStates = qualitativeAnalysis.analyseProb1(formula->asProbabilityOperatorFormula()); } +void oneshot_test(std::string const& path, std::string const& constants, std::string formulaString, uint64_t lookahead) { + storm::prism::Program program = storm::parser::PrismParser::parse(path); + program = storm::utility::prism::preprocess(program, constants); + std::shared_ptr formula = storm::api::parsePropertiesForPrismProgram(formulaString, program).front().getRawFormula(); + std::shared_ptr> pomdp = storm::api::buildSparseModel(program, {formula})->as>(); + storm::transformer::MakePOMDPCanonic makeCanonic(*pomdp); + pomdp = makeCanonic.transform(); + + // Run graph algorithm + auto formulaInfo = storm::pomdp::analysis::getFormulaInformation(*pomdp, *formula); + storm::analysis::QualitativeAnalysisOnGraphs qualitativeAnalysis(*pomdp); + storm::storage::BitVector surelyNotAlmostSurelyReachTarget = qualitativeAnalysis.analyseProbSmaller1( + formula->asProbabilityOperatorFormula()); + pomdp->getTransitionMatrix().makeRowGroupsAbsorbing(surelyNotAlmostSurelyReachTarget); + storm::storage::BitVector targetStates = qualitativeAnalysis.analyseProb1(formula->asProbabilityOperatorFormula()); + std::shared_ptr smtSolverFactory = std::make_shared(); + storm::pomdp::OneShotPolicySearch memlessSearch(*pomdp, targetStates, + surelyNotAlmostSurelyReachTarget, + smtSolverFactory); + memlessSearch.analyzeForInitialStates(lookahead); +} + + TEST(QualitativeAnalysis, GraphAlgorithm_Simple) { graphalgorithm_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.4", "Pmax=? [F \"goal\" ]"); graphalgorithm_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.0", "Pmax=? [F \"goal\" ]"); @@ -37,3 +61,18 @@ TEST(QualitativeAnalysis, GraphAlgorithm_Maze) { graphalgorithm_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [!\"bad\" U \"goal\" ]"); graphalgorithm_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [!\"bad\" U \"goal\"]"); } + + +TEST(QualitativeAnalysis, OneShot_Simple) { + oneshot_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.4", "Pmax=? [F \"goal\" ]", 5); + oneshot_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.0", "Pmax=? [F \"goal\" ]", 5); +} + +TEST(QualitativeAnalysis, OneShots_Maze) { + oneshot_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [F \"goal\" ]", 5); + oneshot_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [F \"goal\" ]", 5); + oneshot_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [F \"goal\" ]", 30); + oneshot_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [F \"goal\" ]", 30); + oneshot_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [!\"bad\" U \"goal\" ]", 5); + oneshot_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [!\"bad\" U \"goal\"]", 5); +} \ No newline at end of file