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