Storm 1.13.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 = storm::utility::prism::preprocess(program, 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 private:
77 storm::Environment _environment;
78};
79
80typedef ::testing::Types<DefaultDoubleVIEnvironment> TestingTypes;
81
82TYPED_TEST_SUITE(BeliefExplorationAPITest, TestingTypes, );
83
84TYPED_TEST(BeliefExplorationAPITest, simple_Pmax) {
85 typedef typename TestFixture::ValueType ValueType;
86
87 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmax=? [F \"goal\" ]", "slippery=0");
88 auto task = storm::api::createTask<ValueType>(data.formula, false);
89 auto result = storm::pomdp::api::underapproximateWithCutoffs<ValueType>(data.model, task, 100);
90
91 ValueType expected = this->parseNumber("7/10");
92 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
93
94 EXPECT_EQ(1ul, storm::pomdp::api::getNumberOfPreprocessingSchedulers<ValueType>(result));
95 EXPECT_NO_THROW(storm::pomdp::api::extractSchedulerAsMarkovChain<ValueType>(result));
96 EXPECT_NO_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 0));
97 EXPECT_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 1), std::out_of_range);
98}
99
100TYPED_TEST(BeliefExplorationAPITest, simple_Pmin) {
101 typedef typename TestFixture::ValueType ValueType;
102
103 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmin=? [F \"goal\" ]", "slippery=0");
104 auto task = storm::api::createTask<ValueType>(data.formula, false);
105 auto result = storm::pomdp::api::underapproximateWithCutoffs<ValueType>(data.model, task, 100);
106
107 ValueType expected = this->parseNumber("3/10");
108 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
109
110 EXPECT_EQ(1ul, storm::pomdp::api::getNumberOfPreprocessingSchedulers<ValueType>(result));
111 EXPECT_NO_THROW(storm::pomdp::api::extractSchedulerAsMarkovChain<ValueType>(result));
112 EXPECT_NO_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 0));
113 EXPECT_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 1), std::out_of_range);
114}
115
116TYPED_TEST(BeliefExplorationAPITest, simple_slippery_Pmax) {
117 typedef typename TestFixture::ValueType ValueType;
118
119 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmax=? [F \"goal\" ]", "slippery=0.4");
120 auto task = storm::api::createTask<ValueType>(data.formula, false);
121 auto result = storm::pomdp::api::underapproximateWithCutoffs<ValueType>(data.model, task, 100);
122
123 ValueType expected = this->parseNumber("7/10");
124 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
125
126 EXPECT_EQ(1ul, storm::pomdp::api::getNumberOfPreprocessingSchedulers<ValueType>(result));
127 EXPECT_NO_THROW(storm::pomdp::api::extractSchedulerAsMarkovChain<ValueType>(result));
128 EXPECT_NO_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 0));
129 EXPECT_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 1), std::out_of_range);
130}
131
132TYPED_TEST(BeliefExplorationAPITest, simple_slippery_Pmin) {
133 typedef typename TestFixture::ValueType ValueType;
134
135 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmin=? [F \"goal\" ]", "slippery=0.4");
136 auto task = storm::api::createTask<ValueType>(data.formula, false);
137 auto result = storm::pomdp::api::underapproximateWithCutoffs<ValueType>(data.model, task, 100);
138
139 ValueType expected = this->parseNumber("3/10");
140 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
141
142 EXPECT_EQ(1ul, storm::pomdp::api::getNumberOfPreprocessingSchedulers<ValueType>(result));
143
144 EXPECT_NO_THROW(storm::pomdp::api::extractSchedulerAsMarkovChain<ValueType>(result));
145 EXPECT_NO_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 0));
146 EXPECT_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 1), std::out_of_range);
147}
148
149TYPED_TEST(BeliefExplorationAPITest, simple_Rmax) {
150 typedef typename TestFixture::ValueType ValueType;
151
152 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmax=? [F s>4 ]", "slippery=0");
153 auto task = storm::api::createTask<ValueType>(data.formula, false);
154 auto result = storm::pomdp::api::underapproximateWithCutoffs<ValueType>(data.model, task, 100);
155
156 ValueType expected = this->parseNumber("29/50");
157 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
158
159 EXPECT_EQ(1ul, storm::pomdp::api::getNumberOfPreprocessingSchedulers<ValueType>(result));
160 EXPECT_NO_THROW(storm::pomdp::api::extractSchedulerAsMarkovChain<ValueType>(result));
161 EXPECT_NO_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 0));
162 EXPECT_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 1), std::out_of_range);
163}
164
165TYPED_TEST(BeliefExplorationAPITest, simple_Rmin) {
166 typedef typename TestFixture::ValueType ValueType;
167
168 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmin=? [F s>4 ]", "slippery=0");
169 auto task = storm::api::createTask<ValueType>(data.formula, false);
170 auto result = storm::pomdp::api::underapproximateWithCutoffs<ValueType>(data.model, task, 100);
171
172 ValueType expected = this->parseNumber("19/50");
173 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
174
175 EXPECT_EQ(1ul, storm::pomdp::api::getNumberOfPreprocessingSchedulers<ValueType>(result));
176 EXPECT_NO_THROW(storm::pomdp::api::extractSchedulerAsMarkovChain<ValueType>(result));
177 EXPECT_NO_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 0));
178 EXPECT_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 1), std::out_of_range);
179}
180
181TYPED_TEST(BeliefExplorationAPITest, simple_slippery_Rmax) {
182 typedef typename TestFixture::ValueType ValueType;
183
184 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmax=? [F s>4 ]", "slippery=0.4");
185 auto task = storm::api::createTask<ValueType>(data.formula, false);
186 auto result = storm::pomdp::api::underapproximateWithCutoffs<ValueType>(data.model, task, 100);
187
188 ValueType expected = this->parseNumber("29/30");
189 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
190
191 EXPECT_EQ(1ul, storm::pomdp::api::getNumberOfPreprocessingSchedulers<ValueType>(result));
192 EXPECT_NO_THROW(storm::pomdp::api::extractSchedulerAsMarkovChain<ValueType>(result));
193 EXPECT_NO_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 0));
194 EXPECT_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 5), std::out_of_range);
195}
196
197TYPED_TEST(BeliefExplorationAPITest, simple_slippery_Rmin) {
198 typedef typename TestFixture::ValueType ValueType;
199
200 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmin=? [F s>4 ]", "slippery=0.4");
201 auto task = storm::api::createTask<ValueType>(data.formula, false);
202 auto result = storm::pomdp::api::underapproximateWithCutoffs<ValueType>(data.model, task, 100);
203
204 ValueType expected = this->parseNumber("19/30");
205 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
206
207 EXPECT_EQ(1ul, storm::pomdp::api::getNumberOfPreprocessingSchedulers<ValueType>(result));
208 EXPECT_NO_THROW(storm::pomdp::api::extractSchedulerAsMarkovChain<ValueType>(result));
209 EXPECT_NO_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 0));
210 EXPECT_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 5), std::out_of_range);
211}
212
213TYPED_TEST(BeliefExplorationAPITest, maze2_Rmin) {
214 typedef typename TestFixture::ValueType ValueType;
215
216 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "Rmin=? [F \"goal\"]", "sl=0");
217 auto task = storm::api::createTask<ValueType>(data.formula, false);
218 auto result = storm::pomdp::api::underapproximateWithCutoffs<ValueType>(data.model, task, 100);
219
220 ValueType expected = this->parseNumber("74/91");
221 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
222
223 EXPECT_EQ(1ul, storm::pomdp::api::getNumberOfPreprocessingSchedulers<ValueType>(result));
224 EXPECT_NO_THROW(storm::pomdp::api::extractSchedulerAsMarkovChain<ValueType>(result));
225 EXPECT_NO_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 0));
226 EXPECT_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 1), std::out_of_range);
227}
228
229TYPED_TEST(BeliefExplorationAPITest, maze2_slippery_Rmin) {
230 typedef typename TestFixture::ValueType ValueType;
231
232 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "Rmin=? [F \"goal\"]", "sl=0.075");
233 auto task = storm::api::createTask<ValueType>(data.formula, false);
234 auto result = storm::pomdp::api::underapproximateWithCutoffs<ValueType>(data.model, task, 100);
235
236 ValueType expected = this->parseNumber("80/91");
237 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
238
239 EXPECT_EQ(1ul, storm::pomdp::api::getNumberOfPreprocessingSchedulers<ValueType>(result));
240 EXPECT_NO_THROW(storm::pomdp::api::extractSchedulerAsMarkovChain<ValueType>(result));
241 EXPECT_NO_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 0));
242 EXPECT_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 1), std::out_of_range);
243}
244
245TYPED_TEST(BeliefExplorationAPITest, refuel_Pmax) {
246 typedef typename TestFixture::ValueType ValueType;
247
248 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/refuel.prism", "Pmax=?[\"notbad\" U \"goal\"]", "N=4");
249 auto task = storm::api::createTask<ValueType>(data.formula, false);
250 auto result = storm::pomdp::api::underapproximateWithCutoffs<ValueType>(data.model, task, 100);
251
252 ValueType expected = this->parseNumber("38/155");
253 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
254
255 EXPECT_EQ(2ul, storm::pomdp::api::getNumberOfPreprocessingSchedulers<ValueType>(result));
256 EXPECT_NO_THROW(storm::pomdp::api::extractSchedulerAsMarkovChain<ValueType>(result));
257 EXPECT_NO_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 0));
258 EXPECT_NO_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 1));
259 EXPECT_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 2), std::out_of_range);
260}
261
262TYPED_TEST(BeliefExplorationAPITest, refuel_Pmin) {
263 typedef typename TestFixture::ValueType ValueType;
264
265 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/refuel.prism", "Pmin=?[\"notbad\" U \"goal\"]", "N=4");
266 auto task = storm::api::createTask<ValueType>(data.formula, false);
267 auto result = storm::pomdp::api::underapproximateWithCutoffs<ValueType>(data.model, task, 100);
268
269 ValueType expected = this->parseNumber("0");
270 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
271
272 EXPECT_EQ(1ul, storm::pomdp::api::getNumberOfPreprocessingSchedulers<ValueType>(result));
273 EXPECT_NO_THROW(storm::pomdp::api::extractSchedulerAsMarkovChain<ValueType>(result));
274 EXPECT_NO_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 0));
275 EXPECT_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 1), std::out_of_range);
276}
277
278TYPED_TEST(BeliefExplorationAPITest, simple2_Rmax) {
279 typedef typename TestFixture::ValueType ValueType;
280
281 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple2.prism", "Rmax=?[F \"goal\"]");
282 auto task = storm::api::createTask<ValueType>(data.formula, false);
283 auto result = storm::pomdp::api::underapproximateWithCutoffs<ValueType>(data.model, task, 10);
284
285 ValueType expected = this->parseNumber("59040588757/103747000000");
286 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
287
288 EXPECT_EQ(2ul, storm::pomdp::api::getNumberOfPreprocessingSchedulers<ValueType>(result));
289 EXPECT_NO_THROW(storm::pomdp::api::extractSchedulerAsMarkovChain<ValueType>(result));
290 EXPECT_NO_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 0));
291 EXPECT_NO_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 1));
292 EXPECT_THROW(storm::pomdp::api::getCutoffScheduler<ValueType>(result, 2), std::out_of_range);
293
294 std::vector<std::unordered_map<uint64_t, ValueType>> obs0vals{{{0, 0}, {1, 0}}, {{0, 0.7}}, {{0, 1}, {1, 1}}};
295 std::vector<std::unordered_map<uint64_t, ValueType>> obs1vals{{{2, 1}}, {{2, 1}}};
296 std::vector<std::vector<std::unordered_map<uint64_t, ValueType>>> additionalVals{obs0vals, obs1vals};
297
298 result = storm::pomdp::api::underapproximateWithCutoffs<ValueType>(data.model, task, 10, additionalVals);
299
300 EXPECT_LE(result.lowerBound, storm::utility::one<ValueType>() + this->modelcheckingPrecision());
301}
302
303TYPED_TEST(BeliefExplorationAPITest, noHeuristicValues) {
304 typedef typename TestFixture::ValueType ValueType;
305
306 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple2.prism", "Rmax=?[F \"goal\"]");
307 auto task = storm::api::createTask<ValueType>(data.formula, false);
308
309 std::vector<std::unordered_map<uint64_t, ValueType>> obs0vals{{{0, 0}, {1, 0}}, {{0, 0.7}}, {{0, 1}, {1, 1}}};
310 std::vector<std::unordered_map<uint64_t, ValueType>> obs1vals{{{2, 1}}, {{2, 1}}};
311 std::vector<std::vector<std::unordered_map<uint64_t, ValueType>>> additionalVals{obs0vals, obs1vals};
312
313 auto result = storm::pomdp::api::underapproximateWithoutHeuristicValues<ValueType>(data.model, task, 10, additionalVals);
314
315 EXPECT_LE(result.lowerBound, storm::utility::one<ValueType>() + this->modelcheckingPrecision());
316}
TYPED_TEST_SUITE
TYPED_TEST_SUITE(BeliefExplorationAPITest, TestingTypes,)
TYPED_TEST
TYPED_TEST(BeliefExplorationAPITest, simple_Pmax)
Definition BeliefExplorationAPITest.cpp:84
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:25
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:43
storm::models::sparse::Pomdp
This class represents a partially observable Markov decision process.
Definition Pomdp.h:13
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::buildSparseModel
std::shared_ptr< storm::models::sparse::Model< ValueType > > buildSparseModel(storm::storage::SymbolicModelDescription const &model, storm::builder::BuilderOptions const &options)
Definition builder.h:109
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:46
storm::api::parseProgram
storm::prism::Program parseProgram(std::string const &filename, bool prismCompatibility, bool simplify)
Definition model_descriptions.cpp:17
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:119
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:132
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:46
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:21
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:106
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:13
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:135
TestingTypes
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:59
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