diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index 19c04dc6a..61a8f6194 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/src/storm-pomdp-cli/storm-pomdp.cpp @@ -185,7 +185,16 @@ namespace storm { if (qualSettings.isWinningRegionSet()) { search.computeWinningRegion(lookahead); } else { - search.analyzeForInitialStates(lookahead); + bool result = search.analyzeForInitialStates(lookahead); + if (result) { + STORM_PRINT_AND_LOG("From initial state, one can almost-surely reach the target."); + } else { + if (k == pomdp.getNumberOfStates()) { + STORM_PRINT_AND_LOG("From initial state, one cannot almost-surely reach the target."); + } else { + STORM_PRINT_AND_LOG("From initial state, one may not almost-surely reach the target."); + } + } } if (qualSettings.isPrintWinningRegionSet()) { diff --git a/src/storm-pomdp/analysis/IterativePolicySearch.h b/src/storm-pomdp/analysis/IterativePolicySearch.h index b0c172659..1e03bc2ff 100644 --- a/src/storm-pomdp/analysis/IterativePolicySearch.h +++ b/src/storm-pomdp/analysis/IterativePolicySearch.h @@ -169,22 +169,14 @@ namespace pomdp { std::shared_ptr& smtSolverFactory, MemlessSearchOptions const& options); - void analyzeForInitialStates(uint64_t k) { + bool analyzeForInitialStates(uint64_t k) { stats.totalTimer.start(); 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()); stats.totalTimer.stop(); - if (result) { - STORM_PRINT_AND_LOG("From initial state, one can almost-surely reach the target."); - } else { - if (k == pomdp.getNumberOfStates()) { - STORM_PRINT_AND_LOG("From initial state, one cannot almost-surely reach the target."); - } else { - STORM_PRINT_AND_LOG("From initial state, one may not almost-surely reach the target."); - } - } + return result; } void computeWinningRegion(uint64_t k) { diff --git a/src/test/storm-pomdp/analysis/QualitativeAnalysisTest.cpp b/src/test/storm-pomdp/analysis/QualitativeAnalysisTest.cpp index c2e802510..d4d46ce54 100644 --- a/src/test/storm-pomdp/analysis/QualitativeAnalysisTest.cpp +++ b/src/test/storm-pomdp/analysis/QualitativeAnalysisTest.cpp @@ -8,6 +8,8 @@ #include "storm-pomdp/analysis/FormulaInformation.h" #include "storm-pomdp/analysis/QualitativeAnalysisOnGraphs.h" #include "storm-pomdp/analysis/OneShotPolicySearch.h" +#include "storm-pomdp/analysis/IterativePolicySearch.h" + #include "storm-pomdp/transformer/MakePOMDPCanonic.h" void graphalgorithm_test(std::string const& path, std::string const& constants, std::string formulaString) { @@ -50,6 +52,38 @@ void oneshot_test(std::string const& path, std::string const& constants, std::st } +void iterativesearch_test(std::string const& path, std::string const& constants, std::string formulaString, bool wr) { + 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::MemlessSearchOptions options; + uint64_t lookahead = pomdp->getNumberOfStates(); + storm::pomdp::IterativePolicySearch search(*pomdp, targetStates, + surelyNotAlmostSurelyReachTarget, + smtSolverFactory, options); + if (wr) { + search.computeWinningRegion(lookahead); + } else { + search.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\" ]"); @@ -75,4 +109,25 @@ TEST(QualitativeAnalysis, OneShots_Maze) { 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); +} + + +TEST(QualitativeAnalysis, Iterative_Simple) { + iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.4", "Pmax=? [F \"goal\" ]", false); + iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.0", "Pmax=? [F \"goal\" ]", false); + + iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.4", "Pmax=? [F \"goal\" ]", true); + iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.0", "Pmax=? [F \"goal\" ]", true); +} + +TEST(QualitativeAnalysis, Iterative_Maze) { + iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [F \"goal\" ]", false); + iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [F \"goal\" ]", false); + iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [!\"bad\" U \"goal\" ]", false); + iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [!\"bad\" U \"goal\"]", false); + + iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [F \"goal\" ]", true); + iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [F \"goal\" ]", true); + iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [!\"bad\" U \"goal\" ]", true); + iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [!\"bad\" U \"goal\"]", true); } \ No newline at end of file