From 6b5c7b26728aa60f8835f61eb902f40f76003cda Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@gmail.com>
Date: Sun, 23 May 2021 17:43:06 -0700
Subject: [PATCH] minimal test cases for qualitative analysis: graphs

---
 src/test/storm-pomdp/CMakeLists.txt           |  2 +-
 .../analysis/QualitativeAnalysisTest.cpp      | 39 +++++++++++++++++++
 2 files changed, 40 insertions(+), 1 deletion(-)
 create mode 100644 src/test/storm-pomdp/analysis/QualitativeAnalysisTest.cpp

diff --git a/src/test/storm-pomdp/CMakeLists.txt b/src/test/storm-pomdp/CMakeLists.txt
index 4b3f060d7..70ceeb3dd 100644
--- a/src/test/storm-pomdp/CMakeLists.txt
+++ b/src/test/storm-pomdp/CMakeLists.txt
@@ -9,7 +9,7 @@ register_source_groups_from_filestructure("${ALL_FILES}" test)
 # Note that the tests also need the source files, except for the main file
 include_directories(${GTEST_INCLUDE_DIR})
 
-foreach (testsuite transformation modelchecker)
+foreach (testsuite analysis transformation modelchecker)
 
 	  file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp)
       add_executable (test-pomdp-${testsuite} ${TEST_${testsuite}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp)
diff --git a/src/test/storm-pomdp/analysis/QualitativeAnalysisTest.cpp b/src/test/storm-pomdp/analysis/QualitativeAnalysisTest.cpp
new file mode 100644
index 000000000..a61ff0b80
--- /dev/null
+++ b/src/test/storm-pomdp/analysis/QualitativeAnalysisTest.cpp
@@ -0,0 +1,39 @@
+#include "test/storm_gtest.h"
+#include "storm-config.h"
+#include "storm/models/sparse/StandardRewardModel.h"
+#include "storm-parsers/parser/PrismParser.h"
+#include "storm/builder/ExplicitModelBuilder.h"
+#include "storm/api/storm.h"
+#include "storm-parsers/api/storm-parsers.h"
+#include "storm-pomdp/analysis/FormulaInformation.h"
+#include "storm-pomdp/analysis/QualitativeAnalysisOnGraphs.h"
+#include "storm-pomdp/transformer/MakePOMDPCanonic.h"
+
+void graphalgorithm_test(std::string const& path, std::string const& constants, std::string formulaString) {
+    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());
+}
+
+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\" ]");
+}
+
+TEST(QualitativeAnalysis, GraphAlgorithm_Maze) {
+    graphalgorithm_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [F \"goal\" ]");
+    graphalgorithm_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [F \"goal\" ]");
+    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\"]");
+}