Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
QualitativeAnalysisTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "storm-parsers/api/storm-parsers.h"
3#include "storm-parsers/parser/PrismParser.h"
4#include "storm-pomdp/analysis/FormulaInformation.h"
5#include "storm-pomdp/analysis/IterativePolicySearch.h"
6#include "storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.h"
7#include "storm-pomdp/analysis/OneShotPolicySearch.h"
8#include "storm-pomdp/analysis/QualitativeAnalysisOnGraphs.h"
9#include "storm/api/storm.h"
10#include "storm/builder/ExplicitModelBuilder.h"
11#include "storm/models/sparse/StandardRewardModel.h"
12#include "test/storm_gtest.h"
13
14#include "storm-pomdp/transformer/MakePOMDPCanonic.h"
15
16void graphalgorithm_test(std::string const& path, std::string const& constants, std::string formulaString) {
17 storm::prism::Program program = storm::parser::PrismParser::parse(path);
18 program = storm::utility::prism::preprocess(program, constants);
19 std::shared_ptr<storm::logic::Formula const> formula = storm::api::parsePropertiesForPrismProgram(formulaString, program).front().getRawFormula();
20 std::shared_ptr<storm::models::sparse::Pomdp<double>> pomdp =
21 storm::api::buildSparseModel<double>(program, {formula})->as<storm::models::sparse::Pomdp<double>>();
22 storm::transformer::MakePOMDPCanonic<double> makeCanonic(*pomdp);
23 pomdp = makeCanonic.transform();
24
25 // Run graph algorithm
26 auto formulaInfo = storm::pomdp::analysis::getFormulaInformation(*pomdp, *formula);
27 storm::analysis::QualitativeAnalysisOnGraphs<double> qualitativeAnalysis(*pomdp);
28 storm::storage::BitVector surelyNotAlmostSurelyReachTarget = qualitativeAnalysis.analyseProbSmaller1(formula->asProbabilityOperatorFormula());
29 pomdp->getTransitionMatrix().makeRowGroupsAbsorbing(surelyNotAlmostSurelyReachTarget);
30 storm::storage::BitVector targetStates = qualitativeAnalysis.analyseProb1(formula->asProbabilityOperatorFormula());
31}
32
33void oneshot_test(std::string const& path, std::string const& constants, std::string formulaString, uint64_t lookahead) {
34 storm::prism::Program program = storm::parser::PrismParser::parse(path);
35 program = storm::utility::prism::preprocess(program, constants);
36 std::shared_ptr<storm::logic::Formula const> formula = storm::api::parsePropertiesForPrismProgram(formulaString, program).front().getRawFormula();
37 std::shared_ptr<storm::models::sparse::Pomdp<double>> pomdp =
38 storm::api::buildSparseModel<double>(program, {formula})->as<storm::models::sparse::Pomdp<double>>();
39 storm::transformer::MakePOMDPCanonic<double> makeCanonic(*pomdp);
40 pomdp = makeCanonic.transform();
41
42 // Run graph algorithm
43 auto formulaInfo = storm::pomdp::analysis::getFormulaInformation(*pomdp, *formula);
44 storm::analysis::QualitativeAnalysisOnGraphs<double> qualitativeAnalysis(*pomdp);
45 storm::storage::BitVector surelyNotAlmostSurelyReachTarget = qualitativeAnalysis.analyseProbSmaller1(formula->asProbabilityOperatorFormula());
46 pomdp->getTransitionMatrix().makeRowGroupsAbsorbing(surelyNotAlmostSurelyReachTarget);
47 storm::storage::BitVector targetStates = qualitativeAnalysis.analyseProb1(formula->asProbabilityOperatorFormula());
48 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
49 storm::pomdp::OneShotPolicySearch<double> memlessSearch(*pomdp, targetStates, surelyNotAlmostSurelyReachTarget, smtSolverFactory);
50 memlessSearch.analyzeForInitialStates(lookahead);
51}
52
53void iterativesearch_test(std::string const& path, std::string const& constants, std::string formulaString, bool wr) {
54 storm::prism::Program program = storm::parser::PrismParser::parse(path);
55 program = storm::utility::prism::preprocess(program, constants);
56 std::shared_ptr<storm::logic::Formula const> formula = storm::api::parsePropertiesForPrismProgram(formulaString, program).front().getRawFormula();
57 std::shared_ptr<storm::models::sparse::Pomdp<double>> pomdp =
58 storm::api::buildSparseModel<double>(program, {formula})->as<storm::models::sparse::Pomdp<double>>();
59 storm::transformer::MakePOMDPCanonic<double> makeCanonic(*pomdp);
60 pomdp = makeCanonic.transform();
61
62 // Run graph algorithm
63 auto formulaInfo = storm::pomdp::analysis::getFormulaInformation(*pomdp, *formula);
64 storm::analysis::QualitativeAnalysisOnGraphs<double> qualitativeAnalysis(*pomdp);
65 storm::storage::BitVector surelyNotAlmostSurelyReachTarget = qualitativeAnalysis.analyseProbSmaller1(formula->asProbabilityOperatorFormula());
66 pomdp->getTransitionMatrix().makeRowGroupsAbsorbing(surelyNotAlmostSurelyReachTarget);
67 storm::storage::BitVector targetStates = qualitativeAnalysis.analyseProb1(formula->asProbabilityOperatorFormula());
68
69 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
70 storm::pomdp::MemlessSearchOptions options;
71 uint64_t lookahead = pomdp->getNumberOfStates();
72 storm::pomdp::IterativePolicySearch<double> search(*pomdp, targetStates, surelyNotAlmostSurelyReachTarget, smtSolverFactory, options);
73 if (wr) {
74 search.computeWinningRegion(lookahead);
75 } else {
76 search.analyzeForInitialStates(lookahead);
77 }
78}
79
80void symbolicbelsup_test(std::string const& path, std::string const& constants, std::string formulaString, bool wr) {
81 storm::prism::Program program = storm::parser::PrismParser::parse(path);
82 program = storm::utility::prism::preprocess(program, constants);
83 std::shared_ptr<storm::logic::Formula const> formula = storm::api::parsePropertiesForPrismProgram(formulaString, program).front().getRawFormula();
84 std::shared_ptr<storm::models::sparse::Pomdp<double>> pomdp =
85 storm::api::buildSparseModel<double>(program, {formula})->as<storm::models::sparse::Pomdp<double>>();
86 storm::transformer::MakePOMDPCanonic<double> makeCanonic(*pomdp);
87 pomdp = makeCanonic.transform();
88
89 // Run graph algorithm
90 auto formulaInfo = storm::pomdp::analysis::getFormulaInformation(*pomdp, *formula);
91 storm::analysis::QualitativeAnalysisOnGraphs<double> qualitativeAnalysis(*pomdp);
92 storm::storage::BitVector surelyNotAlmostSurelyReachTarget = qualitativeAnalysis.analyseProbSmaller1(formula->asProbabilityOperatorFormula());
93 pomdp->getTransitionMatrix().makeRowGroupsAbsorbing(surelyNotAlmostSurelyReachTarget);
94 storm::storage::BitVector targetStates = qualitativeAnalysis.analyseProb1(formula->asProbabilityOperatorFormula());
95
96 storm::pomdp::qualitative::JaniBeliefSupportMdpGenerator<double> janicreator(*pomdp);
97 janicreator.generate(targetStates, surelyNotAlmostSurelyReachTarget);
98 bool initialOnly = !wr;
99 janicreator.verifySymbolic(initialOnly);
100}
101
102class QualitativeAnalysis : public ::testing::Test {
103 protected:
104 void SetUp() override {
105#ifndef STORM_HAVE_Z3
106 GTEST_SKIP() << "Z3 not available.";
107#endif
108 }
109};
110
111TEST_F(QualitativeAnalysis, GraphAlgorithm_Simple) {
112 graphalgorithm_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.4", "Pmax=? [F \"goal\" ]");
113 graphalgorithm_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.0", "Pmax=? [F \"goal\" ]");
114}
115
116TEST_F(QualitativeAnalysis, GraphAlgorithm_Maze) {
117 graphalgorithm_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [F \"goal\" ]");
118 graphalgorithm_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [F \"goal\" ]");
119 graphalgorithm_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [!\"bad\" U \"goal\" ]");
120 graphalgorithm_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [!\"bad\" U \"goal\"]");
121}
122
123TEST_F(QualitativeAnalysis, OneShot_Simple) {
124 oneshot_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.4", "Pmax=? [F \"goal\" ]", 5);
125 oneshot_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.0", "Pmax=? [F \"goal\" ]", 5);
126}
127
128TEST_F(QualitativeAnalysis, OneShots_Maze) {
129 oneshot_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [F \"goal\" ]", 5);
130 oneshot_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [F \"goal\" ]", 5);
131 oneshot_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [F \"goal\" ]", 30);
132 oneshot_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [F \"goal\" ]", 30);
133 oneshot_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [!\"bad\" U \"goal\" ]", 5);
134 oneshot_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [!\"bad\" U \"goal\"]", 5);
135}
136
137TEST_F(QualitativeAnalysis, Iterative_Simple) {
138 iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.4", "Pmax=? [F \"goal\" ]", false);
139 iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.0", "Pmax=? [F \"goal\" ]", false);
140
141 iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.4", "Pmax=? [F \"goal\" ]", true);
142 iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.0", "Pmax=? [F \"goal\" ]", true);
143}
144
145TEST_F(QualitativeAnalysis, Iterative_Maze) {
146 iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [F \"goal\" ]", false);
147 iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [F \"goal\" ]", false);
148 iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [!\"bad\" U \"goal\" ]", false);
149 iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [!\"bad\" U \"goal\"]", false);
150
151 iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [F \"goal\" ]", true);
152 iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [F \"goal\" ]", true);
153 iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [!\"bad\" U \"goal\" ]", true);
154 iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [!\"bad\" U \"goal\"]", true);
155}
156
157TEST_F(QualitativeAnalysis, SymbolicBelSup_Simple) {
158 symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.4", "Pmax=? [F \"goal\" ]", false);
159 symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.0", "Pmax=? [F \"goal\" ]", false);
160
161 symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.4", "Pmax=? [F \"goal\" ]", true);
162 symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.0", "Pmax=? [F \"goal\" ]", true);
163}
164
165TEST_F(QualitativeAnalysis, SymbolicBelSup_Maze) {
166 symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [F \"goal\" ]", false);
167 symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [F \"goal\" ]", false);
168 symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [!\"bad\" U \"goal\" ]", false);
169 symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [!\"bad\" U \"goal\"]", false);
170
171 symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [F \"goal\" ]", true);
172 symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [F \"goal\" ]", true);
173 symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [!\"bad\" U \"goal\" ]", true);
174 symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [!\"bad\" U \"goal\"]", true);
175}
oneshot_test
void oneshot_test(std::string const &path, std::string const &constants, std::string formulaString, uint64_t lookahead)
Definition QualitativeAnalysisTest.cpp:33
symbolicbelsup_test
void symbolicbelsup_test(std::string const &path, std::string const &constants, std::string formulaString, bool wr)
Definition QualitativeAnalysisTest.cpp:80
TEST_F
TEST_F(QualitativeAnalysis, GraphAlgorithm_Simple)
Definition QualitativeAnalysisTest.cpp:111
graphalgorithm_test
void graphalgorithm_test(std::string const &path, std::string const &constants, std::string formulaString)
Definition QualitativeAnalysisTest.cpp:16
iterativesearch_test
void iterativesearch_test(std::string const &path, std::string const &constants, std::string formulaString, bool wr)
Definition QualitativeAnalysisTest.cpp:53
storm::analysis::QualitativeAnalysisOnGraphs::analyseProbSmaller1
storm::storage::BitVector analyseProbSmaller1(storm::logic::ProbabilityOperatorFormula const &formula) const
Definition QualitativeAnalysisOnGraphs.cpp:33
storm::analysis::QualitativeAnalysisOnGraphs::analyseProb1
storm::storage::BitVector analyseProb1(storm::logic::ProbabilityOperatorFormula const &formula) const
Definition QualitativeAnalysisOnGraphs.cpp:28
storm::models::sparse::Pomdp
This class represents a partially observable Markov decision process.
Definition Pomdp.h:15
storm::parser::PrismParser::parse
static storm::prism::Program parse(std::string const &filename, bool prismCompatability=false)
Parses the given file into the PRISM storage classes assuming it complies with the PRISM syntax.
Definition PrismParser.cpp:5
storm::pomdp::OneShotPolicySearch::analyzeForInitialStates
bool analyzeForInitialStates(uint64_t k)
Check if you can find a memoryless policy from the initial states.
Definition OneShotPolicySearch.h:54
storm::pomdp::qualitative::JaniBeliefSupportMdpGenerator::generate
void generate(storm::storage::BitVector const &targetStates, storm::storage::BitVector const &badStates)
Definition JaniBeliefSupportMdpGenerator.cpp:39
storm::storage::BitVector
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:18
storm::transformer::MakePOMDPCanonic::transform
std::shared_ptr< storm::models::sparse::Pomdp< ValueType > > transform() const
Definition MakePOMDPCanonic.cpp:126
storm::api::parsePropertiesForPrismProgram
std::vector< storm::jani::Property > parsePropertiesForPrismProgram(std::string const &inputString, storm::prism::Program const &program, boost::optional< std::set< std::string > > const &propertyFilter)
Definition properties.cpp:69
storm::pomdp::analysis::getFormulaInformation
FormulaInformation getFormulaInformation(PomdpType const &pomdp, storm::logic::ProbabilityOperatorFormula const &formula)
Definition FormulaInformation.cpp:119
storm::utility::prism::preprocess
storm::prism::Program preprocess(storm::prism::Program const &program, std::map< storm::expressions::Variable, storm::expressions::Expression > const &constantDefinitions)
Definition prism.cpp:19
storm_gtest.h