Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
BeliefExplorationAPITest.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-pomdp/analysis/QualitativeAnalysisOnGraphs.h"
6#include "storm-pomdp/api/verification.h"
7#include "storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.h"
8#include "storm-pomdp/transformer/KnownProbabilityTransformer.h"
9#include "storm/api/storm.h"
10#include "storm/environment/solver/MinMaxSolverEnvironment.h"
11#include "storm/transformer/MakePOMDPCanonic.h"
12
13class DefaultDoubleVIEnvironment {
14 public:
15 typedef double ValueType;
16 static storm::Environment createEnvironment() {
17 storm::Environment env;
18 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
19 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
20 return env;
21 }
22 static bool const isExactModelChecking = false;
23 static ValueType precision() {
24 return storm::utility::convertNumber<ValueType>(0.12);
25 } // there actually aren't any precision guarantees, but we still want to detect if results are weird.
26 static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>&) { /* intentionally left empty */ }
27};
28
29template<typename TestType>
30class BeliefExplorationAPITest : public ::testing::Test {
31 public:
32 typedef typename TestType::ValueType ValueType;
33 BeliefExplorationAPITest() : _environment(TestType::createEnvironment()) {}
34
35 void SetUp() override {
36#ifndef STORM_HAVE_Z3
37 GTEST_SKIP() << "Z3 not available.";
38#endif
39 }
40
41 storm::Environment const& env() const {
42 return _environment;
43 }
44
45 ValueType parseNumber(std::string const& str) {
46 return storm::utility::convertNumber<ValueType>(str);
47 }
48 struct Input {
49 std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> model;
50 std::shared_ptr<storm::logic::Formula const> formula;
51 };
52 Input buildPrism(std::string const& programFile, std::string const& formulaAsString, std::string const& constantsAsString = "") const {
53 // Parse and build input
54 storm::prism::Program program = storm::api::parseProgram(programFile);
55 program = program.preprocess(constantsAsString);
56 Input input;
57 input.formula = storm::api::parsePropertiesForPrismProgram(formulaAsString, program).front().getRawFormula();
58 input.model = storm::api::buildSparseModel<ValueType>(program, {input.formula})->template as<storm::models::sparse::Pomdp<ValueType>>();
59
60 // Preprocess
61 storm::transformer::MakePOMDPCanonic<ValueType> makeCanonic(*input.model);
62 input.model = makeCanonic.transform();
63 EXPECT_TRUE(input.model->isCanonic());
64 return input;
65 }
66 ValueType precision() const {
67 return TestType::precision();
68 }
69 ValueType modelcheckingPrecision() const {
70 if (TestType::isExactModelChecking) {
71 return storm::utility::zero<ValueType>();
72 } else {
73 return storm::utility::convertNumber<ValueType>(1e-6);
74 }
75 }
76
77 private:
78 storm::Environment _environment;
79};
80
81typedef ::testing::Types<DefaultDoubleVIEnvironment> TestingTypes;
82
83TYPED_TEST_SUITE(BeliefExplorationAPITest, TestingTypes, );
84
85TYPED_TEST(BeliefExplorationAPITest, simple_Pmax) {
86 typedef typename TestFixture::ValueType ValueType;
87
88 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmax=? [F \"goal\" ]", "slippery=0");
89 auto task = storm::api::createTask<ValueType>(data.formula, false);
90 auto result = storm::pomdp::api::underapproximateWithCutoffs<ValueType>(data.model, task, 100);
91
92 ValueType expected = this->parseNumber("7/10");
93 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
94
95 EXPECT_EQ(1ul, storm::pomdp::api::getNumberOfPreprocessingSchedulers<ValueType>(result));
96 EXPECT_NO_THROW(storm::pomdp::api::extractSchedulerAsMarkovChain<ValueType>(result));
97 EXPECT_NO_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 0));
98 EXPECT_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 1), std::out_of_range);
99}
100
101TYPED_TEST(BeliefExplorationAPITest, simple_Pmin) {
102 typedef typename TestFixture::ValueType ValueType;
103
104 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmin=? [F \"goal\" ]", "slippery=0");
105 auto task = storm::api::createTask<ValueType>(data.formula, false);
106 auto result = storm::pomdp::api::underapproximateWithCutoffs<ValueType>(data.model, task, 100);
107
108 ValueType expected = this->parseNumber("3/10");
109 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
110
111 EXPECT_EQ(1ul, storm::pomdp::api::getNumberOfPreprocessingSchedulers<ValueType>(result));
112 EXPECT_NO_THROW(storm::pomdp::api::extractSchedulerAsMarkovChain<ValueType>(result));
113 EXPECT_NO_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 0));
114 EXPECT_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 1), std::out_of_range);
115}
116
117TYPED_TEST(BeliefExplorationAPITest, simple_slippery_Pmax) {
118 typedef typename TestFixture::ValueType ValueType;
119
120 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmax=? [F \"goal\" ]", "slippery=0.4");
121 auto task = storm::api::createTask<ValueType>(data.formula, false);
122 auto result = storm::pomdp::api::underapproximateWithCutoffs<ValueType>(data.model, task, 100);
123
124 ValueType expected = this->parseNumber("7/10");
125 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
126
127 EXPECT_EQ(1ul, storm::pomdp::api::getNumberOfPreprocessingSchedulers<ValueType>(result));
128 EXPECT_NO_THROW(storm::pomdp::api::extractSchedulerAsMarkovChain<ValueType>(result));
129 EXPECT_NO_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 0));
130 EXPECT_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 1), std::out_of_range);
131}
132
133TYPED_TEST(BeliefExplorationAPITest, simple_slippery_Pmin) {
134 typedef typename TestFixture::ValueType ValueType;
135
136 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmin=? [F \"goal\" ]", "slippery=0.4");
137 auto task = storm::api::createTask<ValueType>(data.formula, false);
138 auto result = storm::pomdp::api::underapproximateWithCutoffs<ValueType>(data.model, task, 100);
139
140 ValueType expected = this->parseNumber("3/10");
141 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
142
143 EXPECT_EQ(1ul, storm::pomdp::api::getNumberOfPreprocessingSchedulers<ValueType>(result));
144
145 EXPECT_NO_THROW(storm::pomdp::api::extractSchedulerAsMarkovChain<ValueType>(result));
146 EXPECT_NO_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 0));
147 EXPECT_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 1), std::out_of_range);
148}
149
150TYPED_TEST(BeliefExplorationAPITest, simple_Rmax) {
151 typedef typename TestFixture::ValueType ValueType;
152
153 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmax=? [F s>4 ]", "slippery=0");
154 auto task = storm::api::createTask<ValueType>(data.formula, false);
155 auto result = storm::pomdp::api::underapproximateWithCutoffs<ValueType>(data.model, task, 100);
156
157 ValueType expected = this->parseNumber("29/50");
158 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
159
160 EXPECT_EQ(1ul, storm::pomdp::api::getNumberOfPreprocessingSchedulers<ValueType>(result));
161 EXPECT_NO_THROW(storm::pomdp::api::extractSchedulerAsMarkovChain<ValueType>(result));
162 EXPECT_NO_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 0));
163 EXPECT_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 1), std::out_of_range);
164}
165
166TYPED_TEST(BeliefExplorationAPITest, simple_Rmin) {
167 typedef typename TestFixture::ValueType ValueType;
168
169 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmin=? [F s>4 ]", "slippery=0");
170 auto task = storm::api::createTask<ValueType>(data.formula, false);
171 auto result = storm::pomdp::api::underapproximateWithCutoffs<ValueType>(data.model, task, 100);
172
173 ValueType expected = this->parseNumber("19/50");
174 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
175
176 EXPECT_EQ(1ul, storm::pomdp::api::getNumberOfPreprocessingSchedulers<ValueType>(result));
177 EXPECT_NO_THROW(storm::pomdp::api::extractSchedulerAsMarkovChain<ValueType>(result));
178 EXPECT_NO_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 0));
179 EXPECT_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 1), std::out_of_range);
180}
181
182TYPED_TEST(BeliefExplorationAPITest, simple_slippery_Rmax) {
183 typedef typename TestFixture::ValueType ValueType;
184
185 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmax=? [F s>4 ]", "slippery=0.4");
186 auto task = storm::api::createTask<ValueType>(data.formula, false);
187 auto result = storm::pomdp::api::underapproximateWithCutoffs<ValueType>(data.model, task, 100);
188
189 ValueType expected = this->parseNumber("29/30");
190 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
191
192 EXPECT_EQ(1ul, storm::pomdp::api::getNumberOfPreprocessingSchedulers<ValueType>(result));
193 EXPECT_NO_THROW(storm::pomdp::api::extractSchedulerAsMarkovChain<ValueType>(result));
194 EXPECT_NO_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 0));
195 EXPECT_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 5), std::out_of_range);
196}
197
198TYPED_TEST(BeliefExplorationAPITest, simple_slippery_Rmin) {
199 typedef typename TestFixture::ValueType ValueType;
200
201 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmin=? [F s>4 ]", "slippery=0.4");
202 auto task = storm::api::createTask<ValueType>(data.formula, false);
203 auto result = storm::pomdp::api::underapproximateWithCutoffs<ValueType>(data.model, task, 100);
204
205 ValueType expected = this->parseNumber("19/30");
206 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
207
208 EXPECT_EQ(1ul, storm::pomdp::api::getNumberOfPreprocessingSchedulers<ValueType>(result));
209 EXPECT_NO_THROW(storm::pomdp::api::extractSchedulerAsMarkovChain<ValueType>(result));
210 EXPECT_NO_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 0));
211 EXPECT_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 5), std::out_of_range);
212}
213
214TYPED_TEST(BeliefExplorationAPITest, maze2_Rmin) {
215 typedef typename TestFixture::ValueType ValueType;
216
217 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "Rmin=? [F \"goal\"]", "sl=0");
218 auto task = storm::api::createTask<ValueType>(data.formula, false);
219 auto result = storm::pomdp::api::underapproximateWithCutoffs<ValueType>(data.model, task, 100);
220
221 ValueType expected = this->parseNumber("74/91");
222 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
223
224 EXPECT_EQ(1ul, storm::pomdp::api::getNumberOfPreprocessingSchedulers<ValueType>(result));
225 EXPECT_NO_THROW(storm::pomdp::api::extractSchedulerAsMarkovChain<ValueType>(result));
226 EXPECT_NO_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 0));
227 EXPECT_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 1), std::out_of_range);
228}
229
230TYPED_TEST(BeliefExplorationAPITest, maze2_slippery_Rmin) {
231 typedef typename TestFixture::ValueType ValueType;
232
233 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "Rmin=? [F \"goal\"]", "sl=0.075");
234 auto task = storm::api::createTask<ValueType>(data.formula, false);
235 auto result = storm::pomdp::api::underapproximateWithCutoffs<ValueType>(data.model, task, 100);
236
237 ValueType expected = this->parseNumber("80/91");
238 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
239
240 EXPECT_EQ(1ul, storm::pomdp::api::getNumberOfPreprocessingSchedulers<ValueType>(result));
241 EXPECT_NO_THROW(storm::pomdp::api::extractSchedulerAsMarkovChain<ValueType>(result));
242 EXPECT_NO_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 0));
243 EXPECT_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 1), std::out_of_range);
244}
245
246TYPED_TEST(BeliefExplorationAPITest, refuel_Pmax) {
247 typedef typename TestFixture::ValueType ValueType;
248
249 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/refuel.prism", "Pmax=?[\"notbad\" U \"goal\"]", "N=4");
250 auto task = storm::api::createTask<ValueType>(data.formula, false);
251 auto result = storm::pomdp::api::underapproximateWithCutoffs<ValueType>(data.model, task, 100);
252
253 ValueType expected = this->parseNumber("38/155");
254 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
255
256 EXPECT_EQ(2ul, storm::pomdp::api::getNumberOfPreprocessingSchedulers<ValueType>(result));
257 EXPECT_NO_THROW(storm::pomdp::api::extractSchedulerAsMarkovChain<ValueType>(result));
258 EXPECT_NO_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 0));
259 EXPECT_NO_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 1));
260 EXPECT_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 2), std::out_of_range);
261}
262
263TYPED_TEST(BeliefExplorationAPITest, refuel_Pmin) {
264 typedef typename TestFixture::ValueType ValueType;
265
266 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/refuel.prism", "Pmin=?[\"notbad\" U \"goal\"]", "N=4");
267 auto task = storm::api::createTask<ValueType>(data.formula, false);
268 auto result = storm::pomdp::api::underapproximateWithCutoffs<ValueType>(data.model, task, 100);
269
270 ValueType expected = this->parseNumber("0");
271 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
272
273 EXPECT_EQ(1ul, storm::pomdp::api::getNumberOfPreprocessingSchedulers<ValueType>(result));
274 EXPECT_NO_THROW(storm::pomdp::api::extractSchedulerAsMarkovChain<ValueType>(result));
275 EXPECT_NO_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 0));
276 EXPECT_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 1), std::out_of_range);
277}
278
279TYPED_TEST(BeliefExplorationAPITest, simple2_Rmax) {
280 typedef typename TestFixture::ValueType ValueType;
281
282 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple2.prism", "Rmax=?[F \"goal\"]");
283 auto task = storm::api::createTask<ValueType>(data.formula, false);
284 auto result = storm::pomdp::api::underapproximateWithCutoffs<ValueType>(data.model, task, 10);
285
286 ValueType expected = this->parseNumber("59040588757/103747000000");
287 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
288
289 EXPECT_EQ(2ul, storm::pomdp::api::getNumberOfPreprocessingSchedulers<ValueType>(result));
290 EXPECT_NO_THROW(storm::pomdp::api::extractSchedulerAsMarkovChain<ValueType>(result));
291 EXPECT_NO_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 0));
292 EXPECT_NO_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 1));
293 EXPECT_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 2), std::out_of_range);
294
295 std::vector<std::unordered_map<uint64_t, ValueType>> obs0vals{{{0, 0}, {1, 0}}, {{0, 0.7}}, {{0, 1}, {1, 1}}};
296 std::vector<std::unordered_map<uint64_t, ValueType>> obs1vals{{{2, 1}}, {{2, 1}}};
297 std::vector<std::vector<std::unordered_map<uint64_t, ValueType>>> additionalVals{obs0vals, obs1vals};
298
299 result = storm::pomdp::api::underapproximateWithCutoffs<ValueType>(data.model, task, 10, additionalVals);
300
301 EXPECT_LE(result.lowerBound, storm::utility::one<ValueType>() + this->modelcheckingPrecision());
302}
303
304TYPED_TEST(BeliefExplorationAPITest, noHeuristicValues) {
305 typedef typename TestFixture::ValueType ValueType;
306
307 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple2.prism", "Rmax=?[F \"goal\"]");
308 auto task = storm::api::createTask<ValueType>(data.formula, false);
309
310 std::vector<std::unordered_map<uint64_t, ValueType>> obs0vals{{{0, 0}, {1, 0}}, {{0, 0.7}}, {{0, 1}, {1, 1}}};
311 std::vector<std::unordered_map<uint64_t, ValueType>> obs1vals{{{2, 1}}, {{2, 1}}};
312 std::vector<std::vector<std::unordered_map<uint64_t, ValueType>>> additionalVals{obs0vals, obs1vals};
313
314 auto result = storm::pomdp::api::underapproximateWithoutHeuristicValues<ValueType>(data.model, task, 10, additionalVals);
315
316 EXPECT_LE(result.lowerBound, storm::utility::one<ValueType>() + this->modelcheckingPrecision());
317}
TYPED_TEST_SUITE
TYPED_TEST_SUITE(BeliefExplorationAPITest, TestingTypes,)
TYPED_TEST
TYPED_TEST(BeliefExplorationAPITest, simple_Pmax)
Definition BeliefExplorationAPITest.cpp:85
BeliefExplorationAPITest::env
storm::Environment const & env() const
Definition BeliefExplorationAPITest.cpp:41
BeliefExplorationAPITest::buildPrism
Input buildPrism(std::string const &programFile, std::string const &formulaAsString, std::string const &constantsAsString="") const
Definition BeliefExplorationAPITest.cpp:52
BeliefExplorationAPITest::parseNumber
ValueType parseNumber(std::string const &str)
Definition BeliefExplorationAPITest.cpp:45
DefaultDoubleVIEnvironment::adaptOptions
static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions< ValueType > &)
Definition BeliefExplorationAPITest.cpp:26
DefaultDoubleVIEnvironment::createEnvironment
static storm::Environment createEnvironment()
Definition BeliefExplorationAPITest.cpp:16
storm::Environment::solver
SolverEnvironment & solver()
Definition Environment.cpp:26
storm::MinMaxSolverEnvironment::setPrecision
void setPrecision(storm::RationalNumber value)
Definition MinMaxSolverEnvironment.cpp:60
storm::MinMaxSolverEnvironment::setMethod
void setMethod(storm::solver::MinMaxMethod value, bool isSetFromDefault=false)
Definition MinMaxSolverEnvironment.cpp:43
storm::SolverEnvironment::minMax
MinMaxSolverEnvironment & minMax()
Definition SolverEnvironment.cpp:48
storm::models::sparse::Pomdp
This class represents a partially observable Markov decision process.
Definition Pomdp.h:13
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::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:69
storm::api::createTask
storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > createTask(std::shared_ptr< const storm::logic::Formula > const &formula, bool onlyInitialStatesRelevant=false)
Definition verification.h:44
storm::api::parseProgram
storm::prism::Program parseProgram(std::string const &filename, bool prismCompatibility, bool simplify)
Definition model_descriptions.cpp:17
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::api::getCutoffScheduler
storm::storage::Scheduler< ValueType > getCutoffScheduler(typename storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker< storm::models::sparse::Pomdp< ValueType > >::Result modelcheckingResult, uint64_t schedId)
Get a specific scheduler used to generate cut-off values from the result struct.
Definition verification.h:129
storm::pomdp::api::getNumberOfPreprocessingSchedulers
uint64_t getNumberOfPreprocessingSchedulers(typename storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker< storm::models::sparse::Pomdp< ValueType > >::Result modelcheckingResult)
Get the overall number of schedulers generated by the pre-processing for the under-approximation from...
Definition verification.h:142
storm::pomdp::api::underapproximateWithoutHeuristicValues
storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker< storm::models::sparse::Pomdp< ValueType > >::Result underapproximateWithoutHeuristicValues(std::shared_ptr< storm::models::sparse::Pomdp< ValueType > > pomdp, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task, uint64_t sizeThreshold, std::vector< std::vector< std::unordered_map< uint64_t, ValueType > > > pomdpStateValues)
Uses the belief exploration with cut-offs without the pre-processing to generate cut-off values to un...
Definition verification.h:56
storm::pomdp::api::underapproximateWithCutoffs
storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker< storm::models::sparse::Pomdp< ValueType > >::Result underapproximateWithCutoffs(std::shared_ptr< storm::models::sparse::Pomdp< ValueType > > pomdp, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task, uint64_t sizeThreshold, std::vector< std::vector< std::unordered_map< uint64_t, ValueType > > > additionalPomdpStateValues=std::vector< std::vector< std::unordered_map< uint64_t, ValueType > > >())
Uses the belief exploration with cut-offs to under-approximate the given objective on a POMDP.
Definition verification.h:31
storm::pomdp::api::extractSchedulerAsMarkovChain
std::shared_ptr< storm::models::sparse::Model< ValueType > > extractSchedulerAsMarkovChain(typename storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker< storm::models::sparse::Pomdp< ValueType > >::Result modelcheckingResult)
Extract the scheduler generated by an under-approximation from the given result struct.
Definition verification.h:116
storm::utility::zero
ValueType zero()
Definition constants.cpp:24
storm::utility::one
ValueType one()
Definition constants.cpp:19
storm::utility::convertNumber
TargetType convertNumber(SourceType const &number)
Definition constants.cpp:143
TestingTypes
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:61
storm_gtest.h
BeliefExplorationAPITest::Input::formula
std::shared_ptr< storm::logic::Formula const > formula
Definition BeliefExplorationAPITest.cpp:50
BeliefExplorationAPITest::Input::model
std::shared_ptr< storm::models::sparse::Pomdp< ValueType > > model
Definition BeliefExplorationAPITest.cpp:49