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/builder/DdPrismModelBuilder.h"
8#include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h"
9#include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h"
10#include "storm/modelchecker/results/CheckResult.h"
11#include "storm/modelchecker/results/QuantitativeCheckResult.h"
12#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
13#include "storm/models/sparse/Mdp.h"
14#include "storm/models/symbolic/Dtmc.h"
15#include "storm/models/symbolic/Mdp.h"
16#include "storm/models/symbolic/StandardRewardModel.h"
17#include "storm/solver/SymbolicLinearEquationSolver.h"
18#include "storm/storage/SymbolicModelDescription.h"
19#include "storm/storage/dd/bisimulation/BisimulationDecomposition.h"
20
21class Cudd {
22 public:
23 static void checkLibraryAvailable() {
24#ifndef STORM_HAVE_CUDD
25 GTEST_SKIP() << "Library CUDD not available.";
26#endif
27 }
28
29 static const storm::dd::DdType DdType = storm::dd::DdType::CUDD;
30};
31
32class Sylvan {
33 public:
34 static void checkLibraryAvailable() {
35#ifndef STORM_HAVE_SYLVAN
36 GTEST_SKIP() << "Library Sylvan not available.";
37#endif
38 }
39
40 static const storm::dd::DdType DdType = storm::dd::DdType::Sylvan;
41};
42
43template<typename TestType>
44class SymbolicModelBisimulationDecomposition : public ::testing::Test {
45 public:
46 void SetUp() override {
47 TestType::checkLibraryAvailable();
48 }
49
50 storm::Environment env;
51
52 static const storm::dd::DdType DdType = TestType::DdType;
53};
54
55typedef ::testing::Types<Cudd, Sylvan> TestingTypes;
56TYPED_TEST_SUITE(SymbolicModelBisimulationDecomposition, TestingTypes, );
57
58TYPED_TEST(SymbolicModelBisimulationDecomposition, Die) {
59 const storm::dd::DdType DdType = TestFixture::DdType;
60 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
61
62 std::shared_ptr<storm::models::symbolic::Model<DdType, double>> model = storm::builder::DdPrismModelBuilder<DdType, double>().build(this->env, program);
63 model->getManager().execute([&]() {
64 storm::dd::BisimulationDecomposition<DdType, double> decomposition(*model, storm::storage::BisimulationType::Strong);
65 decomposition.compute();
66 std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
67
68 EXPECT_EQ(11ul, quotient->getNumberOfStates());
69 EXPECT_EQ(17ul, quotient->getNumberOfTransitions());
70 EXPECT_EQ(storm::models::ModelType::Dtmc, quotient->getType());
71 EXPECT_TRUE(quotient->isSymbolicModel());
72
73 storm::parser::FormulaParser formulaParser;
74 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
75
76 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
77 formulas.push_back(formula);
78
79 storm::dd::BisimulationDecomposition<DdType, double> decomposition2(*model, formulas, storm::storage::BisimulationType::Strong);
80 decomposition2.compute();
81 quotient = decomposition2.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
82
83 EXPECT_EQ(5ul, quotient->getNumberOfStates());
84 EXPECT_EQ(8ul, quotient->getNumberOfTransitions());
85 EXPECT_EQ(storm::models::ModelType::Dtmc, quotient->getType());
86 EXPECT_TRUE(quotient->isSymbolicModel());
87 });
88}
89
90TYPED_TEST(SymbolicModelBisimulationDecomposition, DiePartialQuotient) {
91 const storm::dd::DdType DdType = TestFixture::DdType;
92 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
93
94 std::shared_ptr<storm::models::symbolic::Model<DdType, double>> model = storm::builder::DdPrismModelBuilder<DdType, double>().build(this->env, program);
95
96 model->getManager().execute([&]() {
97 storm::dd::BisimulationDecomposition<DdType, double> decomposition(*model, storm::storage::BisimulationType::Strong);
98
99 std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
100 ASSERT_EQ(storm::models::ModelType::Mdp, quotient->getType());
101 ASSERT_TRUE(quotient->isSymbolicModel());
102
103 std::shared_ptr<storm::models::symbolic::Mdp<DdType, double>> quotientMdp = quotient->as<storm::models::symbolic::Mdp<DdType, double>>();
104
105 storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<DdType, double>> checker(*quotientMdp);
106
107 storm::parser::FormulaParser formulaParser;
108 std::shared_ptr<storm::logic::Formula const> minFormula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"one\"]");
109 std::shared_ptr<storm::logic::Formula const> maxFormula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"one\"]");
110
111 std::pair<double, double> resultBounds;
112
113 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*minFormula);
114 result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotientMdp->getReachableStates(), quotientMdp->getInitialStates()));
115 resultBounds.first = result->asQuantitativeCheckResult<double>().sum();
116 result = checker.check(*maxFormula);
117 result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotientMdp->getReachableStates(), quotientMdp->getInitialStates()));
118 resultBounds.second = result->asQuantitativeCheckResult<double>().sum();
119
120 EXPECT_EQ(resultBounds.first, storm::utility::zero<double>());
121 EXPECT_EQ(resultBounds.second, storm::utility::one<double>());
122
123 // Perform only one step.
124 decomposition.compute(1);
125
126 quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
127 ASSERT_EQ(storm::models::ModelType::Mdp, quotient->getType());
128 ASSERT_TRUE(quotient->isSymbolicModel());
129 quotientMdp = quotient->as<storm::models::symbolic::Mdp<DdType, double>>();
130
131 storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<DdType, double>> checker2(*quotientMdp);
132
133 result = checker2.check(*minFormula);
134 result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotientMdp->getReachableStates(), quotientMdp->getInitialStates()));
135 resultBounds.first = result->asQuantitativeCheckResult<double>().sum();
136 result = checker2.check(*maxFormula);
137 result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotientMdp->getReachableStates(), quotientMdp->getInitialStates()));
138 resultBounds.second = result->asQuantitativeCheckResult<double>().sum();
139
140 EXPECT_EQ(resultBounds.first, storm::utility::zero<double>());
141 EXPECT_NEAR(resultBounds.second, static_cast<double>(1) / 3, 1e-6);
142
143 // Perform only one step.
144 decomposition.compute(1);
145
146 quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
147 ASSERT_EQ(storm::models::ModelType::Mdp, quotient->getType());
148 ASSERT_TRUE(quotient->isSymbolicModel());
149 quotientMdp = quotient->as<storm::models::symbolic::Mdp<DdType, double>>();
150
151 storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<DdType, double>> checker3(*quotientMdp);
152
153 result = checker3.check(*minFormula);
154 result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotientMdp->getReachableStates(), quotientMdp->getInitialStates()));
155 resultBounds.first = result->asQuantitativeCheckResult<double>().sum();
156 result = checker3.check(*maxFormula);
157 result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotientMdp->getReachableStates(), quotientMdp->getInitialStates()));
158 resultBounds.second = result->asQuantitativeCheckResult<double>().sum();
159
160 EXPECT_NEAR(resultBounds.first, static_cast<double>(1) / 6, 1e-6);
161 EXPECT_NEAR(resultBounds.second, static_cast<double>(1) / 6, 1e-6);
162 EXPECT_NEAR(resultBounds.first, resultBounds.second, 1e-6);
163
164 decomposition.compute(1);
165
166 quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
167 ASSERT_EQ(storm::models::ModelType::Dtmc, quotient->getType());
168 ASSERT_TRUE(quotient->isSymbolicModel());
169 std::shared_ptr<storm::models::symbolic::Dtmc<DdType, double>> quotientDtmc = quotient->as<storm::models::symbolic::Dtmc<DdType, double>>();
170
171 storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<DdType, double>> checker4(*quotientDtmc);
172
173 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
174
175 result = checker4.check(*formula);
176 result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotientDtmc->getReachableStates(), quotientDtmc->getInitialStates()));
177 resultBounds.first = resultBounds.second = result->asQuantitativeCheckResult<double>().sum();
178
179 EXPECT_NEAR(resultBounds.first, static_cast<double>(1) / 6, 1e-6);
180 });
181}
182
183TYPED_TEST(SymbolicModelBisimulationDecomposition, Crowds) {
184 const storm::dd::DdType DdType = TestFixture::DdType;
185 storm::storage::SymbolicModelDescription smd = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds5_5.pm");
186
187 // Preprocess model to substitute all constants.
188 smd = smd.preprocess();
189
190 std::shared_ptr<storm::models::symbolic::Model<DdType, double>> model =
191 storm::builder::DdPrismModelBuilder<DdType, double>().build(this->env, smd.asPrismProgram());
192
193 model->getManager().execute([&]() {
194 storm::dd::BisimulationDecomposition<DdType, double> decomposition(*model, storm::storage::BisimulationType::Strong);
195 decomposition.compute();
196 std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
197
198 EXPECT_EQ(2007ul, quotient->getNumberOfStates());
199 EXPECT_EQ(3738ul, quotient->getNumberOfTransitions());
200 EXPECT_EQ(storm::models::ModelType::Dtmc, quotient->getType());
201 EXPECT_TRUE(quotient->isSymbolicModel());
202
203 storm::parser::FormulaParser formulaParser;
204 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
205
206 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
207 formulas.push_back(formula);
208
209 storm::dd::BisimulationDecomposition<DdType, double> decomposition2(*model, formulas, storm::storage::BisimulationType::Strong);
210 decomposition2.compute();
211 quotient = decomposition2.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
212
213 EXPECT_EQ(65ul, quotient->getNumberOfStates());
214 EXPECT_EQ(105ul, quotient->getNumberOfTransitions());
215 EXPECT_EQ(storm::models::ModelType::Dtmc, quotient->getType());
216 EXPECT_TRUE(quotient->isSymbolicModel());
217 });
218}
219
220TYPED_TEST(SymbolicModelBisimulationDecomposition, TwoDice) {
221 const storm::dd::DdType DdType = TestFixture::DdType;
222 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
223
224 std::shared_ptr<storm::models::symbolic::Model<DdType, double>> model = storm::builder::DdPrismModelBuilder<DdType, double>().build(this->env, program);
225
226 model->getManager().execute([&]() {
227 storm::dd::BisimulationDecomposition<DdType, double> decomposition(*model, storm::storage::BisimulationType::Strong);
228 decomposition.compute();
229 std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
230
231 EXPECT_EQ(77ul, quotient->getNumberOfStates());
232 EXPECT_EQ(210ul, quotient->getNumberOfTransitions());
233 EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType());
234 EXPECT_TRUE(quotient->isSymbolicModel());
235 EXPECT_EQ(116ul, (quotient->as<storm::models::symbolic::Mdp<DdType, double>>()->getNumberOfChoices()));
236
237 storm::parser::FormulaParser formulaParser;
238 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
239
240 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
241 formulas.push_back(formula);
242
243 storm::dd::BisimulationDecomposition<DdType, double> decomposition2(*model, formulas, storm::storage::BisimulationType::Strong);
244 decomposition2.compute();
245 quotient = decomposition2.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
246
247 EXPECT_EQ(11ul, quotient->getNumberOfStates());
248 EXPECT_EQ(34ul, quotient->getNumberOfTransitions());
249 EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType());
250 EXPECT_TRUE(quotient->isSymbolicModel());
251 EXPECT_EQ(19ul, (quotient->as<storm::models::symbolic::Mdp<DdType, double>>()->getNumberOfChoices()));
252 });
253}
254
255TYPED_TEST(SymbolicModelBisimulationDecomposition, AsynchronousLeader) {
256 const storm::dd::DdType DdType = TestFixture::DdType;
257 storm::storage::SymbolicModelDescription smd = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader4.nm");
258
259 // Preprocess model to substitute all constants.
260 smd = smd.preprocess();
261
262 storm::parser::FormulaParser formulaParser;
263 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
264
265 std::shared_ptr<storm::models::symbolic::Model<DdType, double>> model = storm::builder::DdPrismModelBuilder<DdType, double>().build(
266 this->env, smd.asPrismProgram(), typename storm::builder::DdPrismModelBuilder<DdType, double>::Options(*formula));
267
268 model->getManager().execute([&]() {
269 storm::dd::BisimulationDecomposition<DdType, double> decomposition(*model, storm::storage::BisimulationType::Strong);
270 decomposition.compute();
271 std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
272
273 EXPECT_EQ(252ul, quotient->getNumberOfStates());
274 EXPECT_EQ(624ul, quotient->getNumberOfTransitions());
275 EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType());
276 EXPECT_TRUE(quotient->isSymbolicModel());
277 EXPECT_EQ(500ul, (quotient->as<storm::models::symbolic::Mdp<DdType, double>>()->getNumberOfChoices()));
278
279 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
280 formulas.push_back(formula);
281
282 storm::dd::BisimulationDecomposition<DdType, double> decomposition2(*model, formulas, storm::storage::BisimulationType::Strong);
283 decomposition2.compute();
284 quotient = decomposition2.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);
285
286 EXPECT_EQ(1107ul, quotient->getNumberOfStates());
287 EXPECT_EQ(2684ul, quotient->getNumberOfTransitions());
288 EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType());
289 EXPECT_TRUE(quotient->isSymbolicModel());
290 EXPECT_EQ(2152ul, (quotient->as<storm::models::symbolic::Mdp<DdType, double>>()->getNumberOfChoices()));
291 });
292}
TYPED_TEST_SUITE
TYPED_TEST_SUITE(SymbolicModelBisimulationDecomposition, TestingTypes,)
TYPED_TEST
TYPED_TEST(SymbolicModelBisimulationDecomposition, Die)
Definition SymbolicBisimulationDecompositionTest.cpp:58
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:97
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:161
storm::models::symbolic::Dtmc
This class represents a discrete-time Markov chain.
Definition Dtmc.h:13
storm::models::symbolic::Mdp
This class represents a discrete-time Markov decision process.
Definition Mdp.h:13
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::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::utility::zero
ValueType zero()
Definition constants.cpp:24
storm::utility::one
ValueType one()
Definition constants.cpp:19
TestingTypes
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:61
storm_gtest.h