Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
WeakBisimulationTest.cpp
Go to the documentation of this file.
1#include "BisimulationTestHelper.h"
2
3#include <cstdint>
4#include <map>
5#include <memory>
6#include <random>
7#include <string>
8#include <vector>
9
10namespace {
11
12using storm::test::bisimulation::buildFromPrism;
13using storm::test::bisimulation::buildModel;
14using storm::test::bisimulation::BuildOptions;
15using storm::test::bisimulation::checkFormula;
16using storm::test::bisimulation::Options;
17using storm::test::bisimulation::StateLabelPreservation;
18using storm::test::bisimulation::strongOptions;
19using storm::test::bisimulation::weakOptions;
20
21using ValueType = double;
22
23// ------------------------------------------------------------
24// Silent states and divergence
25// ------------------------------------------------------------
26
31TEST(WeakBisimulationTest, SilentChain) {
32 storm::storage::SparseMatrixBuilder<ValueType> builder(5, 5);
33 builder.addNextValue(0, 1, 1.0);
34 builder.addNextValue(1, 2, 1.0);
35 builder.addNextValue(2, 3, 0.5);
36 builder.addNextValue(2, 4, 0.5);
37 builder.addNextValue(3, 3, 1.0);
38 builder.addNextValue(4, 4, 1.0);
39 auto const model = buildModel<storm::models::sparse::Dtmc<ValueType>>(builder.build(), {{"goal", {3}}});
40
41 auto const strongQuotient = storm::bisimulation::performBisimulationMinimization<ValueType>(*model, {}, strongOptions()).quotient;
42 EXPECT_EQ(5ull, strongQuotient->getNumberOfStates());
43
44 auto const quotient = storm::bisimulation::performBisimulationMinimization<ValueType>(*model, {}, weakOptions()).quotient;
45 // {0,1,2}, {3} and {4}. The two absorbing blocks are divergent, so they keep their self-loop; the chain moves on with probability 1/2 each.
46 EXPECT_EQ(3ull, quotient->getNumberOfStates());
47 EXPECT_EQ(4ull, quotient->getNumberOfTransitions());
48 EXPECT_NEAR(checkFormula<ValueType>(model, "P=? [F \"goal\"]"), 0.5, 1e-12);
49 EXPECT_NEAR(checkFormula<ValueType>(quotient, "P=? [F \"goal\"]"), 0.5, 1e-12);
50}
51
56TEST(WeakBisimulationTest, SilentStatesReachingDifferentClasses) {
57 // 0 -> {2, 3}, 1 -> 2, 2 -> {4, 5}, 3 -> 5, and 4, 5 are absorbing and labeled.
58 storm::storage::SparseMatrixBuilder<ValueType> builder(6, 6);
59 builder.addNextValue(0, 2, 0.5);
60 builder.addNextValue(0, 3, 0.5);
61 builder.addNextValue(1, 2, 1.0);
62 builder.addNextValue(2, 4, 0.5);
63 builder.addNextValue(2, 5, 0.5);
64 builder.addNextValue(3, 5, 1.0);
65 builder.addNextValue(4, 4, 1.0);
66 builder.addNextValue(5, 5, 1.0);
67 auto const model = buildModel<storm::models::sparse::Dtmc<ValueType>>(builder.build(), {{"c", {4}}, {"d", {5}}});
68
69 auto const quotient = storm::bisimulation::performBisimulationMinimization<ValueType>(*model, {}, weakOptions()).quotient;
70 // States 1 and 2 both reach "c" with probability 1/2, state 0 with probability 1/4 and state 3 with probability 0.
71 EXPECT_EQ(5ull, quotient->getNumberOfStates());
72 EXPECT_NEAR(checkFormula<ValueType>(model, "P=? [F \"c\"]"), 0.25, 1e-12);
73 EXPECT_NEAR(checkFormula<ValueType>(quotient, "P=? [F \"c\"]"), 0.25, 1e-12);
74}
75
81TEST(WeakBisimulationTest, ClassSilentOnlyWithinBlock) {
82 storm::storage::SparseMatrixBuilder<ValueType> builder(6, 6);
83 builder.addNextValue(0, 2, 0.5);
84 builder.addNextValue(0, 3, 0.5);
85 builder.addNextValue(1, 0, 1.0);
86 builder.addNextValue(2, 4, 1.0);
87 builder.addNextValue(3, 5, 1.0);
88 builder.addNextValue(4, 4, 1.0);
89 builder.addNextValue(5, 5, 1.0);
90 auto const model = buildModel<storm::models::sparse::Dtmc<ValueType>>(builder.build(), {{"g", {4}}, {"h", {5}}});
91
92 auto const quotient = storm::bisimulation::performBisimulationMinimization<ValueType>(*model, {}, weakOptions()).quotient;
93 EXPECT_EQ(5ull, quotient->getNumberOfStates()); // {0,1}, {2}, {3}, {4}, {5}
94 EXPECT_NEAR(checkFormula<ValueType>(model, "P=? [F \"g\"]"), 0.5, 1e-12);
95 EXPECT_NEAR(checkFormula<ValueType>(quotient, "P=? [F \"g\"]"), 0.5, 1e-12);
96}
97
101TEST(WeakBisimulationTest, DivergentStates) {
102 // 0 -> {1, 3}; 1 <-> 2 forever; 3 absorbing and labeled "goal".
103 storm::storage::SparseMatrixBuilder<ValueType> builder(4, 4);
104 builder.addNextValue(0, 1, 0.5);
105 builder.addNextValue(0, 3, 0.5);
106 builder.addNextValue(1, 2, 1.0);
107 builder.addNextValue(2, 1, 1.0);
108 builder.addNextValue(3, 3, 1.0);
109 auto const model = buildModel<storm::models::sparse::Dtmc<ValueType>>(builder.build(), {{"goal", {3}}});
110
111 auto const quotient = storm::bisimulation::performBisimulationMinimization<ValueType>(*model, {}, weakOptions()).quotient;
112 // {0}, {1,2} and {3}: states 1 and 2 are divergent, state 0 is not (it can leave the block).
113 EXPECT_EQ(3ull, quotient->getNumberOfStates());
114 EXPECT_NEAR(checkFormula<ValueType>(model, "P=? [F \"goal\"]"), 0.5, 1e-12);
115 EXPECT_NEAR(checkFormula<ValueType>(quotient, "P=? [F \"goal\"]"), 0.5, 1e-12);
116}
117
121TEST(WeakBisimulationTest, ZeroProbabilityIsNeverGroupedWithNonZeroProbability) {
122 // 0 moves to 1 and 2; 1 reaches "goal" (3) with a tiny probability and "sink" (4) otherwise; 2 only moves to "sink".
123 storm::storage::SparseMatrixBuilder<ValueType> builder(5, 5);
124 builder.addNextValue(0, 1, 0.5);
125 builder.addNextValue(0, 2, 0.5);
126 builder.addNextValue(1, 3, 1e-10);
127 builder.addNextValue(1, 4, 1.0 - 1e-10);
128 builder.addNextValue(2, 4, 1.0);
129 builder.addNextValue(3, 3, 1.0);
130 builder.addNextValue(4, 4, 1.0);
131 auto const model = buildModel<storm::models::sparse::Dtmc<ValueType>>(builder.build(), {{"goal", {3}}, {"sink", {4}}});
132
133 Options options = weakOptions();
134 options.tolerance = storm::utility::convertNumber<storm::RationalNumber>(1e-9);
135 auto const quotient = storm::bisimulation::performBisimulationMinimization<ValueType>(*model, {}, options).quotient;
136 EXPECT_EQ(5ull, quotient->getNumberOfStates());
137 EXPECT_NEAR(checkFormula<ValueType>(quotient, "P=? [F \"goal\"]") / 5e-11, 1.0, 1e-6);
138}
139
140// ------------------------------------------------------------
141// Continuous-time models
142// ------------------------------------------------------------
143
147TEST(WeakBisimulationTest, CtmcInternalRate) {
148 // 0 -> 1 with rate 100 and 0 -> 2 with rate 1; 1 -> 2 with rate 1; 2 absorbing (self-loop) and labeled "goal".
149 storm::storage::SparseMatrixBuilder<ValueType> builder(3, 3);
150 builder.addNextValue(0, 1, 100.0);
151 builder.addNextValue(0, 2, 1.0);
152 builder.addNextValue(1, 2, 1.0);
153 builder.addNextValue(2, 2, 1.0);
154 auto const model = buildModel<storm::models::sparse::Ctmc<ValueType>>(builder.build(), {{"goal", {2}}});
155
156 auto const strongQuotient = storm::bisimulation::performBisimulationMinimization<ValueType>(*model, {}, strongOptions()).quotient;
157 EXPECT_EQ(3ull, strongQuotient->getNumberOfStates());
158
159 auto const quotient = storm::bisimulation::performBisimulationMinimization<ValueType>(*model, {}, weakOptions()).quotient;
160 EXPECT_EQ(2ull, quotient->getNumberOfStates());
161 // Both states of the merged block reach "goal" after an Exp(1)-distributed amount of time.
162 ValueType const expected = 1.0 - std::exp(-1.0);
163 EXPECT_NEAR(checkFormula<ValueType>(model, "P=? [F<=1 \"goal\"]"), expected, 1e-6);
164 EXPECT_NEAR(checkFormula<ValueType>(quotient, "P=? [F<=1 \"goal\"]"), expected, 1e-6);
165}
166
171TEST(WeakBisimulationTest, CtmcSplitChangesSilence) {
172 // 0 -> 1 (silent, not a predecessor of the goal); 1 -> 2 (non-silent predecessor); 2 is the absorbing goal.
173 storm::storage::SparseMatrixBuilder<ValueType> builder(3, 3);
174 builder.addNextValue(0, 1, 1.0);
175 builder.addNextValue(1, 2, 1.0);
176 builder.addNextValue(2, 2, 1.0);
177 auto const model = buildModel<storm::models::sparse::Ctmc<ValueType>>(builder.build(), {{"goal", {2}}});
178
179 auto const quotient = storm::bisimulation::performBisimulationMinimization<ValueType>(*model, {}, weakOptions()).quotient;
180 EXPECT_EQ(3ull, quotient->getNumberOfStates());
181 ValueType const expected = checkFormula<ValueType>(model, "P=? [F<=1 \"goal\"]");
182 EXPECT_NEAR(checkFormula<ValueType>(quotient, "P=? [F<=1 \"goal\"]"), expected, 1e-9);
183}
184
189TEST(WeakBisimulationTest, CtmcRateRewards) {
190 // Same model as CtmcInternalRate, but states 0 and 1 earn reward at rate one until "goal" is reached.
191 storm::storage::SparseMatrixBuilder<ValueType> builder(3, 3);
192 builder.addNextValue(0, 1, 100.0);
193 builder.addNextValue(0, 2, 1.0);
194 builder.addNextValue(1, 2, 1.0);
195 builder.addNextValue(2, 2, 1.0);
196 auto const model = buildModel<storm::models::sparse::Ctmc<ValueType>>(builder.build(), {{"goal", {2}}}, {1.0, 1.0, 0.0});
197
198 auto const quotient = storm::bisimulation::performBisimulationMinimization<ValueType>(*model, {}, weakOptions()).quotient;
199 // The two states are merged despite their different internal rates, and the reward does not prevent that.
200 EXPECT_EQ(2ull, quotient->getNumberOfStates());
201 // "goal" is reached after an Exp(1)-distributed amount of time, during which reward accumulates at rate one.
202 EXPECT_NEAR(checkFormula<ValueType>(model, "R{\"rew\"}=? [F \"goal\"]"), 1.0, 1e-9);
203 EXPECT_NEAR(checkFormula<ValueType>(quotient, "R{\"rew\"}=? [F \"goal\"]"), 1.0, 1e-9);
204}
205
209TEST(WeakBisimulationTest, CtmcExpectedTime) {
210 // 0 -> 1 with rate 100 and 0 -> 2 with rate 1; 1 -> 2 with rate 1; 2 absorbing and labeled "goal". Both 0 and 1 leave {0, 1} with rate 1.
211 storm::storage::SparseMatrixBuilder<ValueType> builder(3, 3);
212 builder.addNextValue(0, 1, 100.0);
213 builder.addNextValue(0, 2, 1.0);
214 builder.addNextValue(1, 2, 1.0);
215 builder.addNextValue(2, 2, 1.0);
216 auto const model = buildModel<storm::models::sparse::Ctmc<ValueType>>(builder.build(), {{"goal", {2}}});
217
218 storm::parser::FormulaParser formulaParser;
219 std::vector<std::shared_ptr<storm::logic::Formula const>> const formulas{formulaParser.parseSingleFormulaFromString("T=? [F \"goal\"]")};
220 auto const quotient = storm::bisimulation::performBisimulationMinimization<ValueType>(*model, formulas, weakOptions()).quotient;
221 EXPECT_EQ(2ull, quotient->getNumberOfStates());
222 EXPECT_NEAR(checkFormula<ValueType>(model, "T=? [F \"goal\"]"), 1.0, 1e-9);
223 EXPECT_NEAR(checkFormula<ValueType>(quotient, "T=? [F \"goal\"]"), 1.0, 1e-9);
224}
225
226// ------------------------------------------------------------
227// Rewards and step sensitive states
228// ------------------------------------------------------------
229
234TEST(WeakBisimulationTest, Rewards) {
235 // 0 -> {0, 2}, 1 -> 2, 2 absorbing and labeled "goal". States 0 and 1 have reward 1.
236 storm::storage::SparseMatrixBuilder<ValueType> builder(3, 3);
237 builder.addNextValue(0, 0, 0.5);
238 builder.addNextValue(0, 2, 0.5);
239 builder.addNextValue(1, 2, 1.0);
240 builder.addNextValue(2, 2, 1.0);
241 auto const model = buildModel<storm::models::sparse::Dtmc<ValueType>>(builder.build(), {{"goal", {2}}}, {1.0, 1.0, 0.0});
242
243 Options optionsWithoutRewards = weakOptions();
244 optionsWithoutRewards.preserveAllRewards = false;
245 auto const quotient = storm::bisimulation::performBisimulationMinimization<ValueType>(*model, {}, optionsWithoutRewards).quotient;
246 EXPECT_EQ(2ull, quotient->getNumberOfStates());
247 EXPECT_NEAR(checkFormula<ValueType>(quotient, "P=? [F \"goal\"]"), 1.0, 1e-12);
248
249 auto const rewardQuotient = storm::bisimulation::performBisimulationMinimization<ValueType>(*model, {}, weakOptions()).quotient;
250 EXPECT_EQ(3ull, rewardQuotient->getNumberOfStates());
251 // From state 0 we expect two steps (each earning reward 1) until "goal" is reached.
252 EXPECT_NEAR(checkFormula<ValueType>(model, "R{\"rew\"}=? [F \"goal\"]"), 2.0, 1e-12);
253 EXPECT_NEAR(checkFormula<ValueType>(rewardQuotient, "R{\"rew\"}=? [F \"goal\"]"), 2.0, 1e-12);
254}
255
259TEST(WeakBisimulationTest, StateActionRewards) {
260 // 0 -> {0, 2}, 1 -> 2, 2 absorbing and labeled "goal". Taking a transition out of 0 or 1 earns a reward of one.
261 storm::storage::SparseMatrixBuilder<ValueType> builder(3, 3);
262 builder.addNextValue(0, 0, 0.5);
263 builder.addNextValue(0, 2, 0.5);
264 builder.addNextValue(1, 2, 1.0);
265 builder.addNextValue(2, 2, 1.0);
266 auto const model = buildModel<storm::models::sparse::Dtmc<ValueType>>(builder.build(), {{"goal", {2}}}, {}, {1.0, 1.0, 0.0});
267
268 auto const quotient = storm::bisimulation::performBisimulationMinimization<ValueType>(*model, {}, weakOptions()).quotient;
269 EXPECT_EQ(3ull, quotient->getNumberOfStates());
270 // From state 0 we expect two transitions (each earning reward one) until "goal" is reached.
271 EXPECT_NEAR(checkFormula<ValueType>(model, "R{\"rew\"}=? [F \"goal\"]"), 2.0, 1e-12);
272 EXPECT_NEAR(checkFormula<ValueType>(quotient, "R{\"rew\"}=? [F \"goal\"]"), 2.0, 1e-12);
273}
274
279TEST(WeakBisimulationTest, ZeroRewardIsNeverGroupedWithNonZeroReward) {
280 // States 0 and 1 behave identically and differ only in their reward, which is zero for 0 and tiny but non-zero for 1.
281 storm::storage::SparseMatrixBuilder<ValueType> builder(3, 3);
282 builder.addNextValue(0, 2, 1.0);
283 builder.addNextValue(1, 2, 1.0);
284 builder.addNextValue(2, 2, 1.0);
285 auto const model = buildModel<storm::models::sparse::Dtmc<ValueType>>(builder.build(), {{"goal", {2}}}, {0.0, 1e-9, 0.0});
286
287 Options options = weakOptions();
288 options.tolerance = storm::utility::convertNumber<storm::RationalNumber>(1e-6);
289 auto const quotient = storm::bisimulation::performBisimulationMinimization<ValueType>(*model, {}, options).quotient;
290 EXPECT_EQ(3ull, quotient->getNumberOfStates());
291
292 // Without any reward to preserve, the tolerance does merge the two states.
293 options.preserveAllRewards = false;
294 auto const rewardlessQuotient = storm::bisimulation::performBisimulationMinimization<ValueType>(*model, {}, options).quotient;
295 EXPECT_EQ(2ull, rewardlessQuotient->getNumberOfStates());
296}
297
302TEST(WeakBisimulationTest, DivergentStepSensitiveBlock) {
303 // 0 -> {1, 3}; 1 and 2 carry a reward and can only ever reach each other; 3 is the absorbing goal.
304 storm::storage::SparseMatrixBuilder<ValueType> builder(4, 4);
305 builder.addNextValue(0, 1, 0.5);
306 builder.addNextValue(0, 3, 0.5);
307 builder.addNextValue(1, 1, 0.5);
308 builder.addNextValue(1, 2, 0.5);
309 builder.addNextValue(2, 2, 1.0);
310 builder.addNextValue(3, 3, 1.0);
311 auto const model = buildModel<storm::models::sparse::Dtmc<ValueType>>(builder.build(), {{"d", {1, 2}}, {"goal", {3}}}, {0.0, 1.0, 1.0, 0.0});
312
313 auto const quotient = storm::bisimulation::performBisimulationMinimization<ValueType>(*model, {}, weakOptions()).quotient;
314 EXPECT_EQ(3ull, quotient->getNumberOfStates()); // {0}, {1,2} and {3}
315 EXPECT_NEAR(checkFormula<ValueType>(model, "P=? [F \"goal\"]"), 0.5, 1e-12);
316 EXPECT_NEAR(checkFormula<ValueType>(quotient, "P=? [F \"goal\"]"), 0.5, 1e-12);
317 // "goal" is not reached almost surely, so the expected reward is infinite either way.
318 EXPECT_TRUE(std::isinf(checkFormula<ValueType>(model, "R{\"rew\"}=? [F \"goal\"]")));
319 EXPECT_TRUE(std::isinf(checkFormula<ValueType>(quotient, "R{\"rew\"}=? [F \"goal\"]")));
320}
321
326TEST(WeakBisimulationTest, StepSensitiveSplitChangesSilence) {
327 // 0 -> 1 (silent, not a predecessor of the goal); 1 -> {1, 2} (non-silent predecessor). Both carry a reward, so they are refined strongly.
328 storm::storage::SparseMatrixBuilder<ValueType> builder(3, 3);
329 builder.addNextValue(0, 1, 1.0);
330 builder.addNextValue(1, 1, 0.5);
331 builder.addNextValue(1, 2, 0.5);
332 builder.addNextValue(2, 2, 1.0);
333 auto const model = buildModel<storm::models::sparse::Dtmc<ValueType>>(builder.build(), {{"goal", {2}}}, {1.0, 1.0, 0.0});
334
335 auto const quotient = storm::bisimulation::performBisimulationMinimization<ValueType>(*model, {}, weakOptions()).quotient;
336 EXPECT_EQ(3ull, quotient->getNumberOfStates());
337 EXPECT_NEAR(checkFormula<ValueType>(model, "R{\"rew\"}=? [F \"goal\"]"), 3.0, 1e-9);
338 EXPECT_NEAR(checkFormula<ValueType>(quotient, "R{\"rew\"}=? [F \"goal\"]"), 3.0, 1e-9);
339}
340
346TEST(WeakBisimulationTest, SplitterSplitDuringItsOwnRound) {
347 storm::storage::SparseMatrixBuilder<ValueType> builder(9, 9);
348 for (uint64_t b = 0; b < 3; ++b) {
349 builder.addNextValue(b, 4, 0.5);
350 builder.addNextValue(b, 8, 0.5);
351 }
352 builder.addNextValue(3, 3, 0.5);
353 builder.addNextValue(3, 5, 0.5);
354 builder.addNextValue(4, 4, 0.25);
355 builder.addNextValue(4, 5, 0.75);
356 for (uint64_t e = 5; e < 8; ++e) {
357 builder.addNextValue(e, 8, 1.0);
358 }
359 builder.addNextValue(8, 8, 1.0);
360 auto const model = buildModel<storm::models::sparse::Dtmc<ValueType>>(builder.build(), {{"b", {0, 1, 2}}, {"c", {3, 4}}, {"e", {5, 6, 7}}, {"t", {8}}},
361 {0.0, 0.0, 0.0, 1.0, 1.0, 0.0, 0.0, 0.0, 0.0});
362
363 auto const quotient = storm::bisimulation::performBisimulationMinimization<ValueType>(*model, {}, weakOptions()).quotient;
364 auto const requotient = storm::bisimulation::performBisimulationMinimization<ValueType>(*quotient, {}, weakOptions()).quotient;
365 EXPECT_EQ(quotient->getNumberOfStates(), requotient->getNumberOfStates());
366 EXPECT_NEAR(checkFormula<ValueType>(quotient, "P=? [F \"t\"]"), checkFormula<ValueType>(model, "P=? [F \"t\"]"), 1e-9);
367}
368
369// ------------------------------------------------------------
370// Preserved formulas
371// ------------------------------------------------------------
372
376TEST(WeakBisimulationTest, PropositionalSubformulas) {
377 // A silent chain 0 -> 1 -> 2 branches into the absorbing states 3, 4 and 5. 3 is labeled with "a" and "b", 4 is unlabeled and 5 is labeled with "a".
378 storm::storage::SparseMatrixBuilder<ValueType> builder(6, 6);
379 builder.addNextValue(0, 1, 1.0);
380 builder.addNextValue(1, 2, 1.0);
381 builder.addNextValue(2, 3, 0.25);
382 builder.addNextValue(2, 4, 0.25);
383 builder.addNextValue(2, 5, 0.5);
384 builder.addNextValue(3, 3, 1.0);
385 builder.addNextValue(4, 4, 1.0);
386 builder.addNextValue(5, 5, 1.0);
387 auto const model = buildModel<storm::models::sparse::Dtmc<ValueType>>(builder.build(), {{"a", {3, 5}}, {"b", {3}}});
388 std::string const formulaString = "P=? [F \"a\" & !\"b\"]";
389 storm::parser::FormulaParser formulaParser;
390 std::vector<std::shared_ptr<storm::logic::Formula const>> const formulas{formulaParser.parseSingleFormulaFromString(formulaString)};
391
392 auto const quotient = storm::bisimulation::performBisimulationMinimization<ValueType>(*model, formulas, weakOptions()).quotient;
393 EXPECT_EQ(3ull, quotient->getNumberOfStates()); // {0, 1, 2}, {3, 4} and {5}
394 EXPECT_NEAR(checkFormula<ValueType>(quotient, formulaString), 0.5, 1e-12);
395
396 Options options = weakOptions();
397 options.stateLabelPreservation = StateLabelPreservation::FormulaIndividual;
398 auto const individualQuotient = storm::bisimulation::performBisimulationMinimization<ValueType>(*model, formulas, options).quotient;
399 EXPECT_EQ(4ull, individualQuotient->getNumberOfStates()); // {0, 1, 2}, {3}, {4} and {5}
400 EXPECT_NEAR(checkFormula<ValueType>(individualQuotient, formulaString), 0.5, 1e-12);
401}
402
403// ------------------------------------------------------------
404// Randomized self-checks
405// ------------------------------------------------------------
406
411template<typename ModelType>
412std::shared_ptr<ModelType> buildRandomModel(uint64_t const numStates, uint64_t const seed) {
413 std::mt19937_64 rng(seed);
414 storm::storage::SparseMatrixBuilder<ValueType> builder(numStates, numStates);
415 for (uint64_t state = 0; state < numStates; ++state) {
416 uint64_t const numSuccessors = 1 + rng() % 3;
417 std::map<uint64_t, ValueType> row;
418 for (uint64_t i = 0; i < numSuccessors; ++i) {
419 // Small values keep the rows short and make coinciding distributions (and thus actual merges) reasonably likely.
420 row[rng() % numStates] += static_cast<ValueType>(1 + rng() % 4);
421 }
422 if constexpr (std::is_same_v<ModelType, storm::models::sparse::Dtmc<ValueType>>) {
423 ValueType sum = storm::utility::zero<ValueType>();
424 for (auto const& [_, value] : row) {
425 sum += value;
426 }
427 for (auto& [_, value] : row) {
428 value /= sum;
429 }
430 }
431 for (auto const& [column, value] : row) {
432 builder.addNextValue(state, column, value);
433 }
434 }
435 std::map<std::string, std::vector<uint64_t>> labels{{"a", {}}, {"b", {}}};
436 for (uint64_t state = 0; state < numStates; ++state) {
437 if (rng() % 3 == 0) {
438 labels["a"].push_back(state);
439 }
440 if (rng() % 4 == 0) {
441 labels["b"].push_back(state);
442 }
443 }
444 return buildModel<ModelType>(builder.build(), labels);
445}
446
455template<typename ModelType>
456void testIdempotence(uint64_t const numStates, uint64_t const numSeeds, std::string const& formulaString) {
457 for (uint64_t seed = 0; seed < numSeeds; ++seed) {
458 auto const model = buildRandomModel<ModelType>(numStates, seed);
459 Options options = weakOptions();
460 options.tolerance = storm::utility::convertNumber<storm::RationalNumber>(1e-6);
461 auto const quotient = storm::bisimulation::performBisimulationMinimization<ValueType>(*model, {}, options).quotient;
462 ASSERT_LE(quotient->getNumberOfStates(), model->getNumberOfStates()) << "Seed " << seed << ".";
463 auto const quotientOfQuotient = storm::bisimulation::performBisimulationMinimization<ValueType>(*quotient, {}, options).quotient;
464 EXPECT_EQ(quotient->getNumberOfStates(), quotientOfQuotient->getNumberOfStates()) << "Weak bisimulation is not idempotent for seed " << seed << ".";
465 EXPECT_EQ(quotient->getNumberOfTransitions(), quotientOfQuotient->getNumberOfTransitions())
466 << "Weak bisimulation is not idempotent for seed " << seed << ".";
467 // The comparison is against the default precision of the underlying equation solver, not against the exactness of the quotient.
468 EXPECT_NEAR(checkFormula<ValueType>(quotient, formulaString), checkFormula<ValueType>(model, formulaString), 1e-6) << "Seed " << seed << ".";
469 }
470}
471
472TEST(WeakBisimulationTest, RandomDtmcs) {
473 testIdempotence<storm::models::sparse::Dtmc<ValueType>>(12, 500, "P=? [F \"a\"]");
474 testIdempotence<storm::models::sparse::Dtmc<ValueType>>(60, 200, "P=? [(!\"b\") U \"a\"]");
475}
476
477TEST(WeakBisimulationTest, RandomCtmcs) {
478 testIdempotence<storm::models::sparse::Ctmc<ValueType>>(12, 500, "P=? [F \"a\"]");
479 testIdempotence<storm::models::sparse::Ctmc<ValueType>>(60, 200, "P=? [(!\"b\") U \"a\"]");
480}
481
482// ------------------------------------------------------------
483// Benchmark models
484// ------------------------------------------------------------
485
493void testAgainstOriginal(std::string const& prismFile, std::string const& formulaString, uint64_t expectedModelStates, uint64_t expectedStrongStates,
494 uint64_t expectedWeakStates, uint64_t expectedWeakTransitions, BuildOptions const& buildOptions = {}, double const tolerance = 0.0) {
495#ifndef STORM_HAVE_Z3
496 GTEST_SKIP() << "Z3 not available.";
497#endif
498 auto const [model, formulas] = buildFromPrism<ValueType>(prismFile, formulaString, buildOptions);
499 ASSERT_EQ(expectedModelStates, model->getNumberOfStates());
500
501 auto strong = strongOptions();
502 auto weak = weakOptions();
503 strong.tolerance = storm::utility::convertNumber<storm::RationalNumber>(tolerance);
504 weak.tolerance = strong.tolerance;
505 if (buildOptions.allLabels) {
506 strong.stateLabelPreservation = StateLabelPreservation::All;
507 weak.stateLabelPreservation = StateLabelPreservation::All;
508 }
509
510 auto const strongQuotient = storm::bisimulation::performBisimulationMinimization<ValueType>(*model, formulas, strong).quotient;
511 EXPECT_EQ(model->getType(), strongQuotient->getType());
512 EXPECT_EQ(expectedStrongStates, strongQuotient->getNumberOfStates());
513 auto const weakQuotient = storm::bisimulation::performBisimulationMinimization<ValueType>(*model, formulas, weak).quotient;
514 EXPECT_EQ(model->getType(), weakQuotient->getType());
515 EXPECT_EQ(expectedWeakStates, weakQuotient->getNumberOfStates());
516 EXPECT_EQ(expectedWeakTransitions, weakQuotient->getNumberOfTransitions());
517
518 ValueType const expected = checkFormula<ValueType>(model, formulaString);
519 EXPECT_NEAR(checkFormula<ValueType>(strongQuotient, formulaString), expected, 1e-9);
520 EXPECT_NEAR(checkFormula<ValueType>(weakQuotient, formulaString), expected, 1e-9);
521}
522
523TEST(WeakBisimulationTest, Die) {
524 testAgainstOriginal(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm", "P=? [F \"one\"]", 13ull, 5ull, 5ull, 8ull);
525}
526
527TEST(WeakBisimulationTest, DieAllLabels) {
528 testAgainstOriginal(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm", "P=? [F \"one\"]", 13ull, 11ull, 9ull, 13ull, {.allLabels = true});
529}
530
531TEST(WeakBisimulationTest, Crowds) {
532 testAgainstOriginal(STORM_TEST_RESOURCES_DIR "/dtmc/crowds5_5.pm", "P=? [F \"observe0Greater1\"]", 7403ull, 65ull, 43ull, 83ull);
533}
534
535TEST(WeakBisimulationTest, CrowdsAllLabels) {
536 // The model is larger than above because the target states of the formula are no longer made absorbing.
537 testAgainstOriginal(STORM_TEST_RESOURCES_DIR "/dtmc/crowds5_5.pm", "P=? [F \"observe0Greater1\"]", 8607ull, 2149ull, 1556ull, 3287ull, {.allLabels = true});
538}
539
545TEST(WeakBisimulationTest, CtmcEmbedded) {
546 testAgainstOriginal(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", "P=? [F<=10000 \"down\"]", 2076ull, 310ull, 158ull, 898ull, {}, 1e-9);
547}
548
549TEST(WeakBisimulationTest, CtmcEmbeddedAllLabels) {
550 testAgainstOriginal(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", "P=? [F<=10000 \"down\"]", 3478ull, 1127ull, 659ull, 3392ull, {.allLabels = true}, 1e-9);
551}
552
557TEST(WeakBisimulationTest, CtmcClusterChoiceLabelsAndOrigins) {
558 testAgainstOriginal(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", "P=? [F<=100 !\"minimum\"]", 276ull, 276ull, 276ull, 1120ull,
559 {.choiceLabels = true, .choiceOrigins = true});
560}
561
562TEST(WeakBisimulationTest, DtmcBrpChoiceLabelsAndOrigins) {
563 testAgainstOriginal(STORM_TEST_RESOURCES_DIR "/dtmc/brp-16-2.pm", "P=? [F \"target\"]", 613ull, 412ull, 412ull, 572ull,
564 {.choiceLabels = true, .choiceOrigins = true});
565}
566} // namespace
TEST
TEST(RegionConstraintCheckerTest, AffineConstraintHoldsThroughout)
Definition RegionConstraintCheckerTest.cpp:75
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::storage::SparseMatrixBuilder
A class that can be used to build a sparse matrix by adding value by value.
Definition SparseMatrix.h:134
storm::bisimulation::performBisimulationMinimization
ReturnType< ValueType > performBisimulationMinimization(storm::models::sparse::Model< ValueType > const &model, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas, Options options)
Computes the bisimulation quotient of the given model.
Definition Bisimulation.cpp:25
storm::dft::modelchecker::ValueType
SFTBDDChecker::ValueType ValueType
Definition SFTBDDChecker.cpp:12
storm::expressions::sum
Expression sum(std::vector< storm::expressions::Expression > const &expressions)
Definition Expression.cpp:536
storm::test::bisimulation::StateLabelPreservation
storm::bisimulation::StateLabelPreservation StateLabelPreservation
Definition BisimulationTestHelper.h:38
storm::test::bisimulation::checkFormula
ValueType checkFormula(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, std::shared_ptr< storm::logic::Formula const > const &formula)
Definition BisimulationTestHelper.h:112
storm::test::bisimulation::Options
storm::bisimulation::Options Options
Definition BisimulationTestHelper.h:37
storm::test::bisimulation::buildModel
std::shared_ptr< ModelType > buildModel(storm::storage::SparseMatrix< ValueType > matrix, std::map< std::string, std::vector< uint64_t > > const &labels, std::vector< ValueType > const &stateRewards={}, std::vector< ValueType > const &stateActionRewards={})
Builds a deterministic model with the given (probability or rate) matrix.
Definition BisimulationTestHelper.h:60
storm::test::bisimulation::buildFromPrism
PrismInput< ValueType > buildFromPrism(std::string const &prismFile, std::string const &formulaString, BuildOptions const &buildOptions={})
Definition BisimulationTestHelper.h:148
storm::utility::zero
ValueType zero()
Definition constants.cpp:26
storm::utility::convertNumber
TargetType convertNumber(SourceType const &number)
Definition constants.cpp:145
storm::test::bisimulation::BuildOptions
What to build from a PRISM program in addition to what the formulas require.
Definition BisimulationTestHelper.h:139