Storm 1.14.0.1
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 "test/storm_gtest.h"
3
4#include "storm-parsers/api/storm-parsers.h"
5#include "storm-parsers/parser/PrismParser.h"
6#include "storm-pomdp/analysis/FormulaInformation.h"
7#include "storm-pomdp/analysis/IterativePolicySearch.h"
8#include "storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.h"
9#include "storm-pomdp/analysis/OneShotPolicySearch.h"
10#include "storm-pomdp/analysis/QualitativeAnalysisOnGraphs.h"
11#include "storm/api/storm.h"
12#include "storm/builder/ExplicitModelBuilder.h"
13#include "storm/environment/Environment.h"
14#include "storm/environment/solver/SolverEnvironment.h"
15#include "storm/models/sparse/StandardRewardModel.h"
16#include "storm/transformer/MakePOMDPCanonic.h"
17
18void graphalgorithm_test(std::string const& path, std::string const& constants, std::string formulaString) {
19 storm::prism::Program program = storm::parser::PrismParser::parse(path);
20 program = program.preprocess(constants);
21 std::shared_ptr<storm::logic::Formula const> formula = storm::api::parsePropertiesForPrismProgram(formulaString, program).front().getRawFormula();
22 std::shared_ptr<storm::models::sparse::Pomdp<double>> pomdp =
23 storm::api::buildSparseModel<double>(program, {formula})->as<storm::models::sparse::Pomdp<double>>();
24 storm::transformer::MakePOMDPCanonic<double> makeCanonic(*pomdp);
25 pomdp = makeCanonic.transform();
26
27 // Run graph algorithm
28 auto formulaInfo = storm::pomdp::analysis::getFormulaInformation(*pomdp, *formula);
29 storm::analysis::QualitativeAnalysisOnGraphs<double> qualitativeAnalysis(*pomdp);
30 storm::storage::BitVector surelyNotAlmostSurelyReachTarget = qualitativeAnalysis.analyseProbSmaller1(formula->asProbabilityOperatorFormula());
31 pomdp->getTransitionMatrix().makeRowGroupsAbsorbing(surelyNotAlmostSurelyReachTarget);
32 storm::storage::BitVector targetStates = qualitativeAnalysis.analyseProb1(formula->asProbabilityOperatorFormula());
33}
34
35void oneshot_test(std::string const& path, std::string const& constants, std::string formulaString, uint64_t lookahead) {
36 storm::prism::Program program = storm::parser::PrismParser::parse(path);
37 program = program.preprocess(constants);
38 std::shared_ptr<storm::logic::Formula const> formula = storm::api::parsePropertiesForPrismProgram(formulaString, program).front().getRawFormula();
39 std::shared_ptr<storm::models::sparse::Pomdp<double>> pomdp =
40 storm::api::buildSparseModel<double>(program, {formula})->as<storm::models::sparse::Pomdp<double>>();
41 storm::transformer::MakePOMDPCanonic<double> makeCanonic(*pomdp);
42 pomdp = makeCanonic.transform();
43
44 // Run graph algorithm
45 auto formulaInfo = storm::pomdp::analysis::getFormulaInformation(*pomdp, *formula);
46 storm::analysis::QualitativeAnalysisOnGraphs<double> qualitativeAnalysis(*pomdp);
47 storm::storage::BitVector surelyNotAlmostSurelyReachTarget = qualitativeAnalysis.analyseProbSmaller1(formula->asProbabilityOperatorFormula());
48 pomdp->getTransitionMatrix().makeRowGroupsAbsorbing(surelyNotAlmostSurelyReachTarget);
49 storm::storage::BitVector targetStates = qualitativeAnalysis.analyseProb1(formula->asProbabilityOperatorFormula());
50 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
51 storm::pomdp::OneShotPolicySearch<double> memlessSearch(storm::Environment(), *pomdp, targetStates, surelyNotAlmostSurelyReachTarget, smtSolverFactory);
52 memlessSearch.analyzeForInitialStates(lookahead);
53}
54
55void iterativesearch_test(std::string const& path, std::string const& constants, std::string formulaString, bool wr) {
56 storm::prism::Program program = storm::parser::PrismParser::parse(path);
57 program = program.preprocess(constants);
58 std::shared_ptr<storm::logic::Formula const> formula = storm::api::parsePropertiesForPrismProgram(formulaString, program).front().getRawFormula();
59 std::shared_ptr<storm::models::sparse::Pomdp<double>> pomdp =
60 storm::api::buildSparseModel<double>(program, {formula})->as<storm::models::sparse::Pomdp<double>>();
61 storm::transformer::MakePOMDPCanonic<double> makeCanonic(*pomdp);
62 pomdp = makeCanonic.transform();
63
64 // Run graph algorithm
65 auto formulaInfo = storm::pomdp::analysis::getFormulaInformation(*pomdp, *formula);
66 storm::analysis::QualitativeAnalysisOnGraphs<double> qualitativeAnalysis(*pomdp);
67 storm::storage::BitVector surelyNotAlmostSurelyReachTarget = qualitativeAnalysis.analyseProbSmaller1(formula->asProbabilityOperatorFormula());
68 pomdp->getTransitionMatrix().makeRowGroupsAbsorbing(surelyNotAlmostSurelyReachTarget);
69 storm::storage::BitVector targetStates = qualitativeAnalysis.analyseProb1(formula->asProbabilityOperatorFormula());
70
71 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
72 storm::pomdp::MemlessSearchOptions options;
73 uint64_t lookahead = pomdp->getNumberOfStates();
74 storm::pomdp::IterativePolicySearch<double> search(storm::Environment(), *pomdp, targetStates, surelyNotAlmostSurelyReachTarget, smtSolverFactory, options);
75 if (wr) {
76 search.computeWinningRegion(lookahead);
77 } else {
78 search.analyzeForInitialStates(lookahead);
79 }
80}
81
82void symbolicbelsup_test(std::string const& path, std::string const& constants, std::string formulaString, bool wr) {
83 storm::prism::Program program = storm::parser::PrismParser::parse(path);
84 program = program.preprocess(constants);
85 std::shared_ptr<storm::logic::Formula const> formula = storm::api::parsePropertiesForPrismProgram(formulaString, program).front().getRawFormula();
86 std::shared_ptr<storm::models::sparse::Pomdp<double>> pomdp =
87 storm::api::buildSparseModel<double>(program, {formula})->as<storm::models::sparse::Pomdp<double>>();
88 storm::transformer::MakePOMDPCanonic<double> makeCanonic(*pomdp);
89 pomdp = makeCanonic.transform();
90
91 // Run graph algorithm
92 auto formulaInfo = storm::pomdp::analysis::getFormulaInformation(*pomdp, *formula);
93 storm::analysis::QualitativeAnalysisOnGraphs<double> qualitativeAnalysis(*pomdp);
94 storm::storage::BitVector surelyNotAlmostSurelyReachTarget = qualitativeAnalysis.analyseProbSmaller1(formula->asProbabilityOperatorFormula());
95 pomdp->getTransitionMatrix().makeRowGroupsAbsorbing(surelyNotAlmostSurelyReachTarget);
96 storm::storage::BitVector targetStates = qualitativeAnalysis.analyseProb1(formula->asProbabilityOperatorFormula());
97
98 storm::pomdp::qualitative::JaniBeliefSupportMdpGenerator<double> janicreator(*pomdp);
99 janicreator.generate(targetStates, surelyNotAlmostSurelyReachTarget);
100 bool initialOnly = !wr;
101 janicreator.verifySymbolic(storm::Environment(), initialOnly);
102}
103
104class QualitativeAnalysis : public ::testing::Test {
105 protected:
106 void SetUp() override {
107#ifndef STORM_HAVE_Z3
108 GTEST_SKIP() << "Z3 not available.";
109#endif
110 }
111};
112
113namespace {
114
115class RecordingSmtSolverFactory : public storm::utility::solver::Z3SmtSolverFactory {
116 public:
117 std::unique_ptr<storm::solver::SmtSolver> create(storm::expressions::ExpressionManager& manager) const override {
118 ADD_FAILURE() << "Policy search must pass its environment to the SMT factory.";
119 return Z3SmtSolverFactory::create(manager);
120 }
121
122 std::unique_ptr<storm::solver::SmtSolver> create(storm::Environment const& env, storm::expressions::ExpressionManager& manager) const override {
123 environment = &env;
124 return Z3SmtSolverFactory::create(env, manager);
125 }
126
127 mutable storm::Environment const* environment = nullptr;
128};
129
130} // namespace
131
132TEST_F(QualitativeAnalysis, PolicySearchUsesEnvironment) {
133 auto program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/pomdp/simple_unit_rewards.prism").preprocess("slippery=0");
134 auto formula = storm::api::parsePropertiesForPrismProgram("Pmax=? [F \"goal\"]", program).front().getRawFormula();
135 auto pomdp = storm::api::buildSparseModel<double>(program, {formula})->as<storm::models::sparse::Pomdp<double>>();
136 pomdp = storm::transformer::MakePOMDPCanonic<double>(*pomdp).transform();
137 storm::analysis::QualitativeAnalysisOnGraphs<double> qualitativeAnalysis(*pomdp);
138 auto sinkStates = qualitativeAnalysis.analyseProbSmaller1(formula->asProbabilityOperatorFormula());
139 pomdp->getTransitionMatrix().makeRowGroupsAbsorbing(sinkStates);
140 auto targetStates = qualitativeAnalysis.analyseProb1(formula->asProbabilityOperatorFormula());
141
142 storm::Environment env;
143 env.solver().setSmtSolverType(storm::solver::SmtSolverType::Mathsat);
144 // An explicit factory can still choose Z3, even when the supplied environment selects another backend.
145 for (bool iterative : {false, true}) {
146 SCOPED_TRACE(iterative ? "iterative" : "one-shot");
147 auto recordingFactory = std::make_shared<RecordingSmtSolverFactory>();
148 std::shared_ptr<storm::utility::solver::SmtSolverFactory> factory = recordingFactory;
149 if (iterative) {
150 storm::pomdp::IterativePolicySearch<double> search(env, *pomdp, targetStates, sinkStates, factory, storm::pomdp::MemlessSearchOptions());
151 EXPECT_FALSE(search.analyzeForInitialStates(pomdp->getNumberOfStates()));
152 } else {
153 storm::pomdp::OneShotPolicySearch<double> search(env, *pomdp, targetStates, sinkStates, factory);
154 EXPECT_FALSE(search.analyzeForInitialStates(pomdp->getNumberOfStates()));
155 }
156 EXPECT_EQ(recordingFactory->environment, &env);
157 }
158}
159
160TEST_F(QualitativeAnalysis, GraphAlgorithm_Simple) {
161 graphalgorithm_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.4", "Pmax=? [F \"goal\" ]");
162 graphalgorithm_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.0", "Pmax=? [F \"goal\" ]");
163}
164
165TEST_F(QualitativeAnalysis, GraphAlgorithm_Maze) {
166 graphalgorithm_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [F \"goal\" ]");
167 graphalgorithm_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [F \"goal\" ]");
168 graphalgorithm_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [!\"bad\" U \"goal\" ]");
169 graphalgorithm_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [!\"bad\" U \"goal\"]");
170}
171
172TEST_F(QualitativeAnalysis, OneShot_Simple) {
173 oneshot_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.4", "Pmax=? [F \"goal\" ]", 5);
174 oneshot_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.0", "Pmax=? [F \"goal\" ]", 5);
175}
176
177TEST_F(QualitativeAnalysis, OneShots_Maze) {
178 oneshot_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [F \"goal\" ]", 5);
179 oneshot_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [F \"goal\" ]", 5);
180 oneshot_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [F \"goal\" ]", 30);
181 oneshot_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [F \"goal\" ]", 30);
182 oneshot_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [!\"bad\" U \"goal\" ]", 5);
183 oneshot_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [!\"bad\" U \"goal\"]", 5);
184}
185
186TEST_F(QualitativeAnalysis, Iterative_Simple) {
187 iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.4", "Pmax=? [F \"goal\" ]", false);
188 iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.0", "Pmax=? [F \"goal\" ]", false);
189
190 iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.4", "Pmax=? [F \"goal\" ]", true);
191 iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.0", "Pmax=? [F \"goal\" ]", true);
192}
193
194TEST_F(QualitativeAnalysis, Iterative_Maze) {
195 iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [F \"goal\" ]", false);
196 iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [F \"goal\" ]", false);
197 iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [!\"bad\" U \"goal\" ]", false);
198 iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [!\"bad\" U \"goal\"]", false);
199
200 iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [F \"goal\" ]", true);
201 iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [F \"goal\" ]", true);
202 iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [!\"bad\" U \"goal\" ]", true);
203 iterativesearch_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [!\"bad\" U \"goal\"]", true);
204}
205
206TEST_F(QualitativeAnalysis, SymbolicBelSup_Simple) {
207#ifdef STORM_HAVE_SYLVAN
208 symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.4", "Pmax=? [F \"goal\" ]", false);
209 symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.0", "Pmax=? [F \"goal\" ]", false);
210
211 symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.4", "Pmax=? [F \"goal\" ]", true);
212 symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.0", "Pmax=? [F \"goal\" ]", true);
213#else
214 GTEST_SKIP() << "Library Sylvan not available.";
215#endif
216}
217
218TEST_F(QualitativeAnalysis, SymbolicBelSup_Maze) {
219#ifdef STORM_HAVE_SYLVAN
220 symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [F \"goal\" ]", false);
221 symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [F \"goal\" ]", false);
222 symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [!\"bad\" U \"goal\" ]", false);
223 symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [!\"bad\" U \"goal\"]", false);
224
225 symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [F \"goal\" ]", true);
226 symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [F \"goal\" ]", true);
227 symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [!\"bad\" U \"goal\" ]", true);
228 symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [!\"bad\" U \"goal\"]", true);
229#else
230 GTEST_SKIP() << "Library Sylvan not available.";
231#endif
232}
oneshot_test
void oneshot_test(std::string const &path, std::string const &constants, std::string formulaString, uint64_t lookahead)
Definition QualitativeAnalysisTest.cpp:35
symbolicbelsup_test
void symbolicbelsup_test(std::string const &path, std::string const &constants, std::string formulaString, bool wr)
Definition QualitativeAnalysisTest.cpp:82
TEST_F
TEST_F(QualitativeAnalysis, PolicySearchUsesEnvironment)
Definition QualitativeAnalysisTest.cpp:132
graphalgorithm_test
void graphalgorithm_test(std::string const &path, std::string const &constants, std::string formulaString)
Definition QualitativeAnalysisTest.cpp:18
iterativesearch_test
void iterativesearch_test(std::string const &path, std::string const &constants, std::string formulaString, bool wr)
Definition QualitativeAnalysisTest.cpp:55
storm::Environment::solver
SolverEnvironment & solver()
Definition Environment.cpp:52
storm::SolverEnvironment::setSmtSolverType
void setSmtSolverType(storm::solver::SmtSolverType const &value, bool isSetFromDefault=false)
Definition SolverEnvironment.cpp:194
storm::analysis::QualitativeAnalysisOnGraphs::analyseProbSmaller1
storm::storage::BitVector analyseProbSmaller1(storm::logic::ProbabilityOperatorFormula const &formula) const
Definition QualitativeAnalysisOnGraphs.cpp:32
storm::analysis::QualitativeAnalysisOnGraphs::analyseProb1
storm::storage::BitVector analyseProb1(storm::logic::ProbabilityOperatorFormula const &formula) const
Definition QualitativeAnalysisOnGraphs.cpp:27
storm::models::sparse::Pomdp
This class represents a partially observable Markov decision process.
Definition Pomdp.h:13
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:56
storm::pomdp::qualitative::JaniBeliefSupportMdpGenerator::generate
void generate(storm::storage::BitVector const &targetStates, storm::storage::BitVector const &badStates)
Definition JaniBeliefSupportMdpGenerator.cpp:39
storm::pomdp::qualitative::JaniBeliefSupportMdpGenerator::verifySymbolic
void verifySymbolic(storm::Environment const &env, bool onlyInitial=true)
Definition JaniBeliefSupportMdpGenerator.cpp:189
storm::prism::Program::preprocess
Program preprocess(std::map< storm::expressions::Variable, storm::expressions::Expression > const &constantDefinitions) const
Preprocesses the program by defining the given constant definitions, substituting constants and formu...
Definition Program.cpp:1170
storm::storage::BitVector
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:16
storm::transformer::MakePOMDPCanonic::transform
std::shared_ptr< storm::models::sparse::Pomdp< ValueType > > transform() const
Definition MakePOMDPCanonic.cpp:127
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:70
storm::api::buildSparseModel
std::shared_ptr< storm::models::sparse::Model< ValueType > > buildSparseModel(storm::storage::SymbolicModelDescription const &model, storm::builder::BuilderOptions const &options, typename storm::builder::ExplicitModelBuilder< ValueType >::Options const &explorationOptions=typename storm::builder::ExplicitModelBuilder< ValueType >::Options())
Definition builder.h:117
storm::pomdp::analysis::getFormulaInformation
FormulaInformation getFormulaInformation(PomdpType const &pomdp, storm::logic::ProbabilityOperatorFormula const &formula)
Definition FormulaInformation.cpp:140
storm_gtest.h