Storm
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 "test/storm_gtest.h"
3
22
23class Cudd {
24 public:
26};
27
28class Sylvan {
29 public:
31};
32
33template<typename TestType>
34class SymbolicModelBisimulationDecomposition : public ::testing::Test {
35 public:
36 static const storm::dd::DdType DdType = TestType::DdType;
37};
38
39typedef ::testing::Types<Cudd, Sylvan> TestingTypes;
41
43 const storm::dd::DdType DdType = TestFixture::DdType;
44 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
45
46 std::shared_ptr<storm::models::symbolic::Model<DdType, double>> model = storm::builder::DdPrismModelBuilder<DdType, double>().build(program);
47 model->getManager().execute([&]() {
49 decomposition.compute();
50 std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
51
52 EXPECT_EQ(11ul, quotient->getNumberOfStates());
53 EXPECT_EQ(17ul, quotient->getNumberOfTransitions());
54 EXPECT_EQ(storm::models::ModelType::Dtmc, quotient->getType());
55 EXPECT_TRUE(quotient->isSymbolicModel());
56
57 storm::parser::FormulaParser formulaParser;
58 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
59
60 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
61 formulas.push_back(formula);
62
64 decomposition2.compute();
66
67 EXPECT_EQ(5ul, quotient->getNumberOfStates());
68 EXPECT_EQ(8ul, quotient->getNumberOfTransitions());
69 EXPECT_EQ(storm::models::ModelType::Dtmc, quotient->getType());
70 EXPECT_TRUE(quotient->isSymbolicModel());
71 });
72}
73
75 const storm::dd::DdType DdType = TestFixture::DdType;
76 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
77
78 std::shared_ptr<storm::models::symbolic::Model<DdType, double>> model = storm::builder::DdPrismModelBuilder<DdType, double>().build(program);
79
80 model->getManager().execute([&]() {
82
83 std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
84 ASSERT_EQ(storm::models::ModelType::Mdp, quotient->getType());
85 ASSERT_TRUE(quotient->isSymbolicModel());
86
87 std::shared_ptr<storm::models::symbolic::Mdp<DdType, double>> quotientMdp = quotient->as<storm::models::symbolic::Mdp<DdType, double>>();
88
90
91 storm::parser::FormulaParser formulaParser;
92 std::shared_ptr<storm::logic::Formula const> minFormula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"one\"]");
93 std::shared_ptr<storm::logic::Formula const> maxFormula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"one\"]");
94
95 std::pair<double, double> resultBounds;
96
97 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*minFormula);
98 result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotientMdp->getReachableStates(), quotientMdp->getInitialStates()));
99 resultBounds.first = result->asQuantitativeCheckResult<double>().sum();
100 result = checker.check(*maxFormula);
101 result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotientMdp->getReachableStates(), quotientMdp->getInitialStates()));
102 resultBounds.second = result->asQuantitativeCheckResult<double>().sum();
103
104 EXPECT_EQ(resultBounds.first, storm::utility::zero<double>());
105 EXPECT_EQ(resultBounds.second, storm::utility::one<double>());
106
107 // Perform only one step.
108 decomposition.compute(1);
109
111 ASSERT_EQ(storm::models::ModelType::Mdp, quotient->getType());
112 ASSERT_TRUE(quotient->isSymbolicModel());
113 quotientMdp = quotient->as<storm::models::symbolic::Mdp<DdType, double>>();
114
116
117 result = checker2.check(*minFormula);
118 result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotientMdp->getReachableStates(), quotientMdp->getInitialStates()));
119 resultBounds.first = result->asQuantitativeCheckResult<double>().sum();
120 result = checker2.check(*maxFormula);
121 result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotientMdp->getReachableStates(), quotientMdp->getInitialStates()));
122 resultBounds.second = result->asQuantitativeCheckResult<double>().sum();
123
124 EXPECT_EQ(resultBounds.first, storm::utility::zero<double>());
125 EXPECT_NEAR(resultBounds.second, static_cast<double>(1) / 3, 1e-6);
126
127 // Perform only one step.
128 decomposition.compute(1);
129
131 ASSERT_EQ(storm::models::ModelType::Mdp, quotient->getType());
132 ASSERT_TRUE(quotient->isSymbolicModel());
133 quotientMdp = quotient->as<storm::models::symbolic::Mdp<DdType, double>>();
134
136
137 result = checker3.check(*minFormula);
138 result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotientMdp->getReachableStates(), quotientMdp->getInitialStates()));
139 resultBounds.first = result->asQuantitativeCheckResult<double>().sum();
140 result = checker3.check(*maxFormula);
141 result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotientMdp->getReachableStates(), quotientMdp->getInitialStates()));
142 resultBounds.second = result->asQuantitativeCheckResult<double>().sum();
143
144 EXPECT_NEAR(resultBounds.first, static_cast<double>(1) / 6, 1e-6);
145 EXPECT_NEAR(resultBounds.second, static_cast<double>(1) / 6, 1e-6);
146 EXPECT_NEAR(resultBounds.first, resultBounds.second, 1e-6);
147
148 decomposition.compute(1);
149
151 ASSERT_EQ(storm::models::ModelType::Dtmc, quotient->getType());
152 ASSERT_TRUE(quotient->isSymbolicModel());
153 std::shared_ptr<storm::models::symbolic::Dtmc<DdType, double>> quotientDtmc = quotient->as<storm::models::symbolic::Dtmc<DdType, double>>();
154
156
157 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
158
159 result = checker4.check(*formula);
160 result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotientDtmc->getReachableStates(), quotientDtmc->getInitialStates()));
161 resultBounds.first = resultBounds.second = result->asQuantitativeCheckResult<double>().sum();
162
163 EXPECT_NEAR(resultBounds.first, static_cast<double>(1) / 6, 1e-6);
164 });
165}
166
168 const storm::dd::DdType DdType = TestFixture::DdType;
169 storm::storage::SymbolicModelDescription smd = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds5_5.pm");
170
171 // Preprocess model to substitute all constants.
172 smd = smd.preprocess();
173
174 std::shared_ptr<storm::models::symbolic::Model<DdType, double>> model = storm::builder::DdPrismModelBuilder<DdType, double>().build(smd.asPrismProgram());
175
176 model->getManager().execute([&]() {
178 decomposition.compute();
179 std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
180
181 EXPECT_EQ(2007ul, quotient->getNumberOfStates());
182 EXPECT_EQ(3738ul, quotient->getNumberOfTransitions());
183 EXPECT_EQ(storm::models::ModelType::Dtmc, quotient->getType());
184 EXPECT_TRUE(quotient->isSymbolicModel());
185
186 storm::parser::FormulaParser formulaParser;
187 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
188
189 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
190 formulas.push_back(formula);
191
193 decomposition2.compute();
195
196 EXPECT_EQ(65ul, quotient->getNumberOfStates());
197 EXPECT_EQ(105ul, quotient->getNumberOfTransitions());
198 EXPECT_EQ(storm::models::ModelType::Dtmc, quotient->getType());
199 EXPECT_TRUE(quotient->isSymbolicModel());
200 });
201}
202
204 const storm::dd::DdType DdType = TestFixture::DdType;
205 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
206
207 std::shared_ptr<storm::models::symbolic::Model<DdType, double>> model = storm::builder::DdPrismModelBuilder<DdType, double>().build(program);
208
209 model->getManager().execute([&]() {
211 decomposition.compute();
212 std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
213
214 EXPECT_EQ(77ul, quotient->getNumberOfStates());
215 EXPECT_EQ(210ul, quotient->getNumberOfTransitions());
216 EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType());
217 EXPECT_TRUE(quotient->isSymbolicModel());
218 EXPECT_EQ(116ul, (quotient->as<storm::models::symbolic::Mdp<DdType, double>>()->getNumberOfChoices()));
219
220 storm::parser::FormulaParser formulaParser;
221 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
222
223 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
224 formulas.push_back(formula);
225
227 decomposition2.compute();
229
230 EXPECT_EQ(11ul, quotient->getNumberOfStates());
231 EXPECT_EQ(34ul, quotient->getNumberOfTransitions());
232 EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType());
233 EXPECT_TRUE(quotient->isSymbolicModel());
234 EXPECT_EQ(19ul, (quotient->as<storm::models::symbolic::Mdp<DdType, double>>()->getNumberOfChoices()));
235 });
236}
237
239 const storm::dd::DdType DdType = TestFixture::DdType;
240 storm::storage::SymbolicModelDescription smd = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader4.nm");
241
242 // Preprocess model to substitute all constants.
243 smd = smd.preprocess();
244
245 storm::parser::FormulaParser formulaParser;
246 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
247
248 std::shared_ptr<storm::models::symbolic::Model<DdType, double>> model =
250
251 model->getManager().execute([&]() {
253 decomposition.compute();
254 std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
255
256 EXPECT_EQ(252ul, quotient->getNumberOfStates());
257 EXPECT_EQ(624ul, quotient->getNumberOfTransitions());
258 EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType());
259 EXPECT_TRUE(quotient->isSymbolicModel());
260 EXPECT_EQ(500ul, (quotient->as<storm::models::symbolic::Mdp<DdType, double>>()->getNumberOfChoices()));
261
262 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
263 formulas.push_back(formula);
264
266 decomposition2.compute();
268
269 EXPECT_EQ(1107ul, quotient->getNumberOfStates());
270 EXPECT_EQ(2684ul, quotient->getNumberOfTransitions());
271 EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType());
272 EXPECT_TRUE(quotient->isSymbolicModel());
273 EXPECT_EQ(2152ul, (quotient->as<storm::models::symbolic::Mdp<DdType, double>>()->getNumberOfChoices()));
274 });
275}
TYPED_TEST_SUITE(SymbolicModelBisimulationDecomposition, TestingTypes,)
TYPED_TEST(SymbolicModelBisimulationDecomposition, Die)
::testing::Types< Cudd, Sylvan > TestingTypes
static const storm::dd::DdType DdType
Definition GraphTest.cpp:25
static const storm::dd::DdType DdType
Definition GraphTest.cpp:30
std::shared_ptr< storm::models::symbolic::Model< Type, ValueType > > build(storm::prism::Program const &program, Options const &options=Options())
Translates the given program into a symbolic model (i.e.
void compute(bisimulation::SignatureMode const &mode=bisimulation::SignatureMode::Eager)
Performs partition refinement until a fixpoint has been reached.
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.
This class represents a discrete-time Markov chain.
Definition Dtmc.h:15
This class represents a discrete-time Markov decision process.
Definition Mdp.h:15
virtual uint_fast64_t getNumberOfChoices() const override
Retrieves the number of nondeterministic choices in the model.
std::shared_ptr< storm::logic::Formula const > parseSingleFormulaFromString(std::string const &formulaString) const
Parses the formula given by the provided string.
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.
storm::prism::Program const & asPrismProgram() const
SymbolicModelDescription preprocess(std::string const &constantDefinitionString="") const
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:46