qualitative search: oneshot cleaning and tests

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<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
-                    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<ValueType> search(pomdp, targetStates,
                                                                               surelyNotAlmostSurelyReachTarget,
                                                                               smtSolverFactory, options);

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());

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<storm::logic::Formula const> formula = storm::api::parsePropertiesForPrismProgram(formulaString, program).front().getRawFormula();
+    std::shared_ptr<storm::models::sparse::Pomdp<double>> pomdp = storm::api::buildSparseModel<double>(program, {formula})->as<storm::models::sparse::Pomdp<double>>();
+    storm::transformer::MakePOMDPCanonic<double> makeCanonic(*pomdp);
+    pomdp = makeCanonic.transform();
+
+    // Run graph algorithm
+    auto formulaInfo = storm::pomdp::analysis::getFormulaInformation(*pomdp, *formula);
+    storm::analysis::QualitativeAnalysisOnGraphs<double> 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<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
+    storm::pomdp::OneShotPolicySearch<double> 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);
+}