Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SymbolicBisimulationDecompositionTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "storm/environment/Environment.h"
3#include "test/storm_gtest.h"
4
5#include "storm-parsers/parser/FormulaParser.h"
6#include "storm-parsers/parser/PrismParser.h"
7#include "storm/api/builder.h"
8#include "storm/builder/DdPrismModelBuilder.h"
9#include "storm/modelchecker/csl/HybridMarkovAutomatonCslModelChecker.h"
10#include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h"
11#include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h"
12#include "storm/modelchecker/results/CheckResult.h"
13#include "storm/modelchecker/results/QuantitativeCheckResult.h"
14#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
15#include "storm/models/sparse/Mdp.h"
16#include "storm/models/symbolic/Dtmc.h"
17#include "storm/models/symbolic/MarkovAutomaton.h"
18#include "storm/models/symbolic/Mdp.h"
19#include "storm/models/symbolic/StandardRewardModel.h"
20#include "storm/solver/SymbolicLinearEquationSolver.h"
21#include "storm/storage/SymbolicModelDescription.h"
22#include "storm/storage/dd/bisimulation/BisimulationDecomposition.h"
23#include "storm/storage/dd/bisimulation/BisimulationOptions.h"
24#include "storm/utility/constants.h"
25
26class Cudd {
27 public:
28 static void checkLibraryAvailable() {
29#ifndef STORM_HAVE_CUDD
30 GTEST_SKIP() << "Library CUDD not available.";
31#endif
32 }
33
34 static const storm::dd::DdType DdType = storm::dd::DdType::CUDD;
35};
36
37class Sylvan {
38 public:
39 static void checkLibraryAvailable() {
40#ifndef STORM_HAVE_SYLVAN
41 GTEST_SKIP() << "Library Sylvan not available.";
42#endif
43 }
44
45 static const storm::dd::DdType DdType = storm::dd::DdType::Sylvan;
46};
47
48template<typename TestType>
49class SymbolicModelBisimulationDecomposition : public ::testing::Test {
50 public:
51 void SetUp() override {
52 TestType::checkLibraryAvailable();
53 }
54
55 storm::Environment env;
56
57 static const storm::dd::DdType DdType = TestType::DdType;
58};
59
60typedef ::testing::Types<Cudd, Sylvan> TestingTypes;
61TYPED_TEST_SUITE(SymbolicModelBisimulationDecomposition, TestingTypes, );
62
63TYPED_TEST(SymbolicModelBisimulationDecomposition, Die) {
64 const storm::dd::DdType DdType = TestFixture::DdType;
65 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
66
67 std::shared_ptr<storm::models::symbolic::Model<DdType, double>> model = storm::builder::DdPrismModelBuilder<DdType, double>().build(this->env, program);
68 model->getManager().execute([&]() {
69 storm::dd::BisimulationDecomposition<DdType, double> decomposition(*model, storm::bisimulation::BisimulationType::Strong);
70 decomposition.compute();
71 std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
72
73 EXPECT_EQ(11ul, quotient->getNumberOfStates());
74 EXPECT_EQ(17ul, quotient->getNumberOfTransitions());
75 EXPECT_EQ(storm::models::ModelType::Dtmc, quotient->getType());
76 EXPECT_TRUE(quotient->isSymbolicModel());
77
78 storm::parser::FormulaParser formulaParser;
79 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
80
81 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
82 formulas.push_back(formula);
83
84 storm::dd::BisimulationDecomposition<DdType, double> decomposition2(*model, formulas, storm::bisimulation::BisimulationType::Strong);
85 decomposition2.compute();
86 quotient = decomposition2.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
87
88 EXPECT_EQ(5ul, quotient->getNumberOfStates());
89 EXPECT_EQ(8ul, quotient->getNumberOfTransitions());
90 EXPECT_EQ(storm::models::ModelType::Dtmc, quotient->getType());
91 EXPECT_TRUE(quotient->isSymbolicModel());
92 });
93}
94
95TYPED_TEST(SymbolicModelBisimulationDecomposition, DiePartialQuotient) {
96 const storm::dd::DdType DdType = TestFixture::DdType;
97 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
98
99 std::shared_ptr<storm::models::symbolic::Model<DdType, double>> model = storm::builder::DdPrismModelBuilder<DdType, double>().build(this->env, program);
100
101 model->getManager().execute([&]() {
102 storm::dd::BisimulationDecomposition<DdType, double> decomposition(*model, storm::bisimulation::BisimulationType::Strong);
103
104 std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
105 ASSERT_EQ(storm::models::ModelType::Mdp, quotient->getType());
106 ASSERT_TRUE(quotient->isSymbolicModel());
107
108 std::shared_ptr<storm::models::symbolic::Mdp<DdType, double>> quotientMdp = quotient->as<storm::models::symbolic::Mdp<DdType, double>>();
109
110 storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<DdType, double>> checker(*quotientMdp);
111
112 storm::parser::FormulaParser formulaParser;
113 std::shared_ptr<storm::logic::Formula const> minFormula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"one\"]");
114 std::shared_ptr<storm::logic::Formula const> maxFormula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"one\"]");
115
116 std::pair<double, double> resultBounds;
117
118 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*minFormula);
119 result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotientMdp->getReachableStates(), quotientMdp->getInitialStates()));
120 resultBounds.first = result->asQuantitativeCheckResult<double>().sum();
121 result = checker.check(*maxFormula);
122 result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotientMdp->getReachableStates(), quotientMdp->getInitialStates()));
123 resultBounds.second = result->asQuantitativeCheckResult<double>().sum();
124
125 EXPECT_EQ(resultBounds.first, storm::utility::zero<double>());
126 EXPECT_EQ(resultBounds.second, storm::utility::one<double>());
127
128 // Perform only one step.
129 decomposition.compute(1);
130
131 quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
132 ASSERT_EQ(storm::models::ModelType::Mdp, quotient->getType());
133 ASSERT_TRUE(quotient->isSymbolicModel());
134 quotientMdp = quotient->as<storm::models::symbolic::Mdp<DdType, double>>();
135
136 storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<DdType, double>> checker2(*quotientMdp);
137
138 result = checker2.check(*minFormula);
139 result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotientMdp->getReachableStates(), quotientMdp->getInitialStates()));
140 resultBounds.first = result->asQuantitativeCheckResult<double>().sum();
141 result = checker2.check(*maxFormula);
142 result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotientMdp->getReachableStates(), quotientMdp->getInitialStates()));
143 resultBounds.second = result->asQuantitativeCheckResult<double>().sum();
144
145 EXPECT_EQ(resultBounds.first, storm::utility::zero<double>());
146 EXPECT_NEAR(resultBounds.second, static_cast<double>(1) / 3, 1e-6);
147
148 // Perform only one step.
149 decomposition.compute(1);
150
151 quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
152 ASSERT_EQ(storm::models::ModelType::Mdp, quotient->getType());
153 ASSERT_TRUE(quotient->isSymbolicModel());
154 quotientMdp = quotient->as<storm::models::symbolic::Mdp<DdType, double>>();
155
156 storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<DdType, double>> checker3(*quotientMdp);
157
158 result = checker3.check(*minFormula);
159 result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotientMdp->getReachableStates(), quotientMdp->getInitialStates()));
160 resultBounds.first = result->asQuantitativeCheckResult<double>().sum();
161 result = checker3.check(*maxFormula);
162 result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotientMdp->getReachableStates(), quotientMdp->getInitialStates()));
163 resultBounds.second = result->asQuantitativeCheckResult<double>().sum();
164
165 EXPECT_NEAR(resultBounds.first, static_cast<double>(1) / 6, 1e-6);
166 EXPECT_NEAR(resultBounds.second, static_cast<double>(1) / 6, 1e-6);
167 EXPECT_NEAR(resultBounds.first, resultBounds.second, 1e-6);
168
169 decomposition.compute(1);
170
171 quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
172 ASSERT_EQ(storm::models::ModelType::Dtmc, quotient->getType());
173 ASSERT_TRUE(quotient->isSymbolicModel());
174 std::shared_ptr<storm::models::symbolic::Dtmc<DdType, double>> quotientDtmc = quotient->as<storm::models::symbolic::Dtmc<DdType, double>>();
175
176 storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<DdType, double>> checker4(*quotientDtmc);
177
178 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
179
180 result = checker4.check(*formula);
181 result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotientDtmc->getReachableStates(), quotientDtmc->getInitialStates()));
182 resultBounds.first = resultBounds.second = result->asQuantitativeCheckResult<double>().sum();
183
184 EXPECT_NEAR(resultBounds.first, static_cast<double>(1) / 6, 1e-6);
185 });
186}
187
188TYPED_TEST(SymbolicModelBisimulationDecomposition, Crowds) {
189 const storm::dd::DdType DdType = TestFixture::DdType;
190 storm::storage::SymbolicModelDescription smd = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds5_5.pm");
191
192 // Preprocess model to substitute all constants.
193 smd = smd.preprocess();
194
195 std::shared_ptr<storm::models::symbolic::Model<DdType, double>> model =
196 storm::builder::DdPrismModelBuilder<DdType, double>().build(this->env, smd.asPrismProgram());
197
198 model->getManager().execute([&]() {
199 storm::dd::BisimulationDecomposition<DdType, double> decomposition(*model, storm::bisimulation::BisimulationType::Strong);
200 decomposition.compute();
201 std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
202
203 EXPECT_EQ(2007ul, quotient->getNumberOfStates());
204 EXPECT_EQ(3738ul, quotient->getNumberOfTransitions());
205 EXPECT_EQ(storm::models::ModelType::Dtmc, quotient->getType());
206 EXPECT_TRUE(quotient->isSymbolicModel());
207
208 storm::parser::FormulaParser formulaParser;
209 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
210
211 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
212 formulas.push_back(formula);
213
214 storm::dd::BisimulationDecomposition<DdType, double> decomposition2(*model, formulas, storm::bisimulation::BisimulationType::Strong);
215 decomposition2.compute();
216 quotient = decomposition2.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
217
218 EXPECT_EQ(65ul, quotient->getNumberOfStates());
219 EXPECT_EQ(105ul, quotient->getNumberOfTransitions());
220 EXPECT_EQ(storm::models::ModelType::Dtmc, quotient->getType());
221 EXPECT_TRUE(quotient->isSymbolicModel());
222 });
223}
224
225TYPED_TEST(SymbolicModelBisimulationDecomposition, TwoDice) {
226 const storm::dd::DdType DdType = TestFixture::DdType;
227 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
228
229 std::shared_ptr<storm::models::symbolic::Model<DdType, double>> model = storm::builder::DdPrismModelBuilder<DdType, double>().build(this->env, program);
230
231 model->getManager().execute([&]() {
232 storm::dd::BisimulationDecomposition<DdType, double> decomposition(*model, storm::bisimulation::BisimulationType::Strong);
233 decomposition.compute();
234 std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
235
236 EXPECT_EQ(77ul, quotient->getNumberOfStates());
237 EXPECT_EQ(210ul, quotient->getNumberOfTransitions());
238 EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType());
239 EXPECT_TRUE(quotient->isSymbolicModel());
240 EXPECT_EQ(116ul, (quotient->as<storm::models::symbolic::Mdp<DdType, double>>()->getNumberOfChoices()));
241
242 storm::parser::FormulaParser formulaParser;
243 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
244
245 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
246 formulas.push_back(formula);
247
248 storm::dd::BisimulationDecomposition<DdType, double> decomposition2(*model, formulas, storm::bisimulation::BisimulationType::Strong);
249 decomposition2.compute();
250 quotient = decomposition2.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
251
252 EXPECT_EQ(11ul, quotient->getNumberOfStates());
253 EXPECT_EQ(34ul, quotient->getNumberOfTransitions());
254 EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType());
255 EXPECT_TRUE(quotient->isSymbolicModel());
256 EXPECT_EQ(19ul, (quotient->as<storm::models::symbolic::Mdp<DdType, double>>()->getNumberOfChoices()));
257 });
258}
259
260TYPED_TEST(SymbolicModelBisimulationDecomposition, AsynchronousLeader) {
261 const storm::dd::DdType DdType = TestFixture::DdType;
262 storm::storage::SymbolicModelDescription smd = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader4.nm");
263
264 // Preprocess model to substitute all constants.
265 smd = smd.preprocess();
266
267 storm::parser::FormulaParser formulaParser;
268 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
269
270 std::shared_ptr<storm::models::symbolic::Model<DdType, double>> model = storm::builder::DdPrismModelBuilder<DdType, double>().build(
271 this->env, smd.asPrismProgram(), typename storm::builder::DdPrismModelBuilder<DdType, double>::Options(*formula));
272
273 model->getManager().execute([&]() {
274 storm::dd::BisimulationDecomposition<DdType, double> decomposition(*model, storm::bisimulation::BisimulationType::Strong);
275 decomposition.compute();
276 std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
277
278 EXPECT_EQ(252ul, quotient->getNumberOfStates());
279 EXPECT_EQ(624ul, quotient->getNumberOfTransitions());
280 EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType());
281 EXPECT_TRUE(quotient->isSymbolicModel());
282 EXPECT_EQ(500ul, (quotient->as<storm::models::symbolic::Mdp<DdType, double>>()->getNumberOfChoices()));
283
284 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
285 formulas.push_back(formula);
286
287 storm::dd::BisimulationDecomposition<DdType, double> decomposition2(*model, formulas, storm::bisimulation::BisimulationType::Strong);
288 decomposition2.compute();
289 quotient = decomposition2.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
290
291 EXPECT_EQ(1107ul, quotient->getNumberOfStates());
292 EXPECT_EQ(2684ul, quotient->getNumberOfTransitions());
293 EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType());
294 EXPECT_TRUE(quotient->isSymbolicModel());
295 EXPECT_EQ(2152ul, (quotient->as<storm::models::symbolic::Mdp<DdType, double>>()->getNumberOfChoices()));
296 });
297}
298
299namespace {
300
301// The exit rate of the initial state is lambda + lambda = 4, so the expected time to reach "done" is 1/4. Before
302// the fix, a quotient's/converted model's exit rate incorrectly collapsed to 1, yielding 1 instead of 0.25.
303template<storm::dd::DdType DdType, typename ValueType>
304void checkMarkovAutomatonExitRatePreserved(storm::Environment const& env, storm::models::symbolic::MarkovAutomaton<DdType, ValueType> const& ma) {
305 storm::modelchecker::HybridMarkovAutomatonCslModelChecker<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>> checker(ma);
306 storm::parser::FormulaParser formulaParser;
307 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Tmin=? [F \"done\"]");
308 storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> task(*formula);
309
310 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(env, task);
311 result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(ma.getReachableStates(), ma.getInitialStates()));
312 EXPECT_NEAR(0.25, storm::utility::convertNumber<double>(result->asQuantitativeCheckResult<ValueType>().sum()), 1e-6);
313}
314
315// Bisimulation minimization must preserve the exit rates of Markovian states, for any ValueType.
316template<storm::dd::DdType DdType, typename ValueType>
317void checkMarkovAutomatonExitRatesPreservedUnderBisimulation(storm::Environment const& env, storm::storage::SymbolicModelDescription const& modelDescription) {
318 std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> model = storm::api::buildSymbolicModel<DdType, ValueType>(
319 env, modelDescription, std::vector<std::shared_ptr<storm::logic::Formula const>>(), /*buildFullModel=*/true);
320
321 model->getManager().execute([&]() {
322 ASSERT_EQ(storm::models::ModelType::MarkovAutomaton, model->getType());
323 EXPECT_EQ(3ul, model->getNumberOfStates());
324
325 // Exercise both Dd-quotient extraction paths: the default one operating on new block variables (as used,
326 // e.g., by the hybrid engine) and the one reusing the original row/column variables (--bisimulation:origvars).
327 for (bool useOriginalVariables : {false, true}) {
328 storm::dd::bisimulation::BisimulationOptions options;
329 options.useOriginalVariables = useOriginalVariables;
330 storm::dd::BisimulationDecomposition<DdType, ValueType> decomposition(*model, storm::bisimulation::BisimulationType::Strong, options);
331 decomposition.compute();
332 std::shared_ptr<storm::models::Model<ValueType>> quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
333
334 ASSERT_EQ(storm::models::ModelType::MarkovAutomaton, quotient->getType());
335 ASSERT_TRUE(quotient->isSymbolicModel());
336 // The bisimilar states 1 and 2 should have been merged into a single block.
337 EXPECT_EQ(2ul, quotient->getNumberOfStates());
338
339 checkMarkovAutomatonExitRatePreserved(env, *quotient->template as<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>());
340 }
341 });
342}
343
344} // namespace
345
346TYPED_TEST(SymbolicModelBisimulationDecomposition, MarkovAutomatonExitRates) {
347 const storm::dd::DdType DdType = TestFixture::DdType;
348 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/bisimulation_exit_rates.ma").preprocess();
349
350 // The Dd-based Prism model builder does not support Markov automata directly, so we go via Jani.
351 storm::storage::SymbolicModelDescription modelDescription(program.toJani());
352
353 checkMarkovAutomatonExitRatesPreservedUnderBisimulation<DdType, double>(this->env, modelDescription);
354
355 // RationalNumber models are only supported by Sylvan, not CUDD.
356 if constexpr (TestFixture::DdType == storm::dd::DdType::Sylvan) {
357 checkMarkovAutomatonExitRatesPreservedUnderBisimulation<DdType, storm::RationalNumber>(this->env, modelDescription);
358
359 // Also test exact building with conversion to double.
360 std::shared_ptr<storm::models::symbolic::Model<DdType, storm::RationalNumber>> exactModel =
361 storm::api::buildSymbolicModel<DdType, storm::RationalNumber>(this->env, modelDescription,
362 std::vector<std::shared_ptr<storm::logic::Formula const>>(), /*buildFullModel=*/true);
363
364 exactModel->getManager().execute([&]() {
365 auto exactMa = exactModel->template as<storm::models::symbolic::MarkovAutomaton<DdType, storm::RationalNumber>>();
366 ASSERT_TRUE(exactMa->hasLabel("done"));
367 auto doubleMa = exactMa->template toValueType<double>();
368 ASSERT_TRUE(doubleMa->hasLabel("done"));
369
370 checkMarkovAutomatonExitRatePreserved(this->env, *doubleMa);
371 });
372 }
373}
TYPED_TEST_SUITE
TYPED_TEST_SUITE(SymbolicModelBisimulationDecomposition, TestingTypes,)
TYPED_TEST
TYPED_TEST(SymbolicModelBisimulationDecomposition, Die)
Definition SymbolicBisimulationDecompositionTest.cpp:63
Cudd::DdType
static const storm::dd::DdType DdType
Definition GraphTest.cpp:33
Sylvan::DdType
static const storm::dd::DdType DdType
Definition GraphTest.cpp:44
storm::builder::DdPrismModelBuilder::build
std::shared_ptr< storm::models::symbolic::Model< Type, ValueType > > build(storm::Environment const &env, storm::prism::Program const &program, Options const &options=Options())
Translates the given program into a symbolic model (i.e.
Definition DdPrismModelBuilder.cpp:1565
storm::dd::BisimulationDecomposition::compute
void compute(bisimulation::SignatureMode const &mode=bisimulation::SignatureMode::Eager)
Performs partition refinement until a fixpoint has been reached.
Definition BisimulationDecomposition.cpp:94
storm::dd::BisimulationDecomposition::getQuotient
std::shared_ptr< storm::models::Model< ExportValueType > > getQuotient(storm::dd::bisimulation::QuotientFormat const &quotientFormat) const
Retrieves the quotient model after the bisimulation decomposition was computed.
Definition BisimulationDecomposition.cpp:158
storm::models::symbolic::Dtmc
This class represents a discrete-time Markov chain.
Definition Dtmc.h:13
storm::models::symbolic::MarkovAutomaton
This class represents a discrete-time Markov decision process.
Definition MarkovAutomaton.h:15
storm::models::symbolic::Mdp
This class represents a discrete-time Markov decision process.
Definition Mdp.h:13
storm::models::symbolic::Model::getInitialStates
storm::dd::Bdd< Type > const & getInitialStates() const
Retrieves the initial states of the model.
Definition Model.cpp:104
storm::models::symbolic::Model::getReachableStates
storm::dd::Bdd< Type > const & getReachableStates() const
Retrieves the reachable states of the model.
Definition Model.cpp:99
storm::models::symbolic::NondeterministicModel::getNumberOfChoices
virtual uint_fast64_t getNumberOfChoices() const override
Retrieves the number of nondeterministic choices in the model.
Definition NondeterministicModel.cpp:43
storm::parser::FormulaParser::parseSingleFormulaFromString
std::shared_ptr< storm::logic::Formula const > parseSingleFormulaFromString(std::string const &formulaString) const
Parses the formula given by the provided string.
Definition FormulaParser.cpp:55
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::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::prism::Program::toJani
storm::jani::Model toJani(bool allVariablesGlobal=true, std::string suffix="") const
Converts the PRISM model into an equivalent JANI model.
Definition Program.cpp:2350
storm::storage::SymbolicModelDescription::asPrismProgram
storm::prism::Program const & asPrismProgram() const
Definition SymbolicModelDescription.cpp:112
storm::storage::SymbolicModelDescription::preprocess
SymbolicModelDescription preprocess(std::string const &constantDefinitionString="") const
Definition SymbolicModelDescription.cpp:162
storm::api::buildSymbolicModel
std::shared_ptr< storm::models::symbolic::Model< LibraryType, ValueType > > buildSymbolicModel(storm::Environment const &env, storm::storage::SymbolicModelDescription const &model, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas, bool buildFullModel=false, bool applyMaximumProgress=true, bool fixDeadlocks=true)
Definition builder.h:37
storm::utility::zero
ValueType zero()
Definition constants.cpp:26
storm::utility::one
ValueType one()
Definition constants.cpp:21
storm::utility::convertNumber
TargetType convertNumber(SourceType const &number)
Definition constants.cpp:145
TestingTypes
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:61
storm_gtest.h