test cases for iterative qualitative added

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

src/storm-pomdp/analysis/IterativePolicySearch.h

@@ -169,22 +169,14 @@ namespace pomdp {
                               std::shared_ptr<storm::utility::solver::SmtSolverFactory>& 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) {

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<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::MemlessSearchOptions options;
+    uint64_t lookahead = pomdp->getNumberOfStates();
+    storm::pomdp::IterativePolicySearch<double> 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\" ]");
@@ -76,3 +110,24 @@ TEST(QualitativeAnalysis, OneShots_Maze) {
     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);
+}