Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
DeterministicModelBisimulationDecompositionTest.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/AutoParser.h"
5#include "storm-parsers/parser/FormulaParser.h"
6#include "storm-parsers/parser/PrismParser.h"
7#include "storm/builder/ExplicitModelBuilder.h"
8#include "storm/models/sparse/Ctmc.h"
9#include "storm/models/sparse/Dtmc.h"
10#include "storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.h"
11
12namespace {
13static constexpr double DefaultTestTolerance = 1e-6;
14}
15
16TEST(DeterministicModelBisimulationDecomposition, Die) {
17 std::shared_ptr<storm::models::sparse::Model<double>> abstractModel =
18 storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/die.tra", STORM_TEST_RESOURCES_DIR "/lab/die.lab", "", "");
19
20 ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
21 std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
22
23 using OptionsType = typename storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>::Options;
24
25 storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> bisim(
26 *dtmc, OptionsType::preservingAllLabels(DefaultTestTolerance));
27 ASSERT_NO_THROW(bisim.computeBisimulationDecomposition());
28 std::shared_ptr<storm::models::sparse::Model<double>> result;
29 ASSERT_NO_THROW(result = bisim.getQuotient());
30
31 EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType());
32 EXPECT_EQ(13ul, result->getNumberOfStates());
33 EXPECT_EQ(20ul, result->getNumberOfTransitions());
34
35 OptionsType options = OptionsType::preservingAllLabels(DefaultTestTolerance);
36 options.respectedAtomicPropositions = std::set<std::string>({"one"});
37
38 storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> bisim2(*dtmc, options);
39 ASSERT_NO_THROW(bisim2.computeBisimulationDecomposition());
40 ASSERT_NO_THROW(result = bisim2.getQuotient());
41
42 EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType());
43 EXPECT_EQ(5ul, result->getNumberOfStates());
44 EXPECT_EQ(8ul, result->getNumberOfTransitions());
45
46 options.setType(storm::storage::BisimulationType::Weak);
47
48 storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> bisim3(*dtmc, options);
49 ASSERT_NO_THROW(bisim3.computeBisimulationDecomposition());
50 ASSERT_NO_THROW(result = bisim3.getQuotient());
51
52 EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType());
53 EXPECT_EQ(5ul, result->getNumberOfStates());
54 EXPECT_EQ(8ul, result->getNumberOfTransitions());
55
56 storm::parser::FormulaParser formulaParser;
57 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
58
59 OptionsType options2(*dtmc, *formula, DefaultTestTolerance);
60
61 storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> bisim4(*dtmc, options2);
62 ASSERT_NO_THROW(bisim4.computeBisimulationDecomposition());
63 ASSERT_NO_THROW(result = bisim4.getQuotient());
64 EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType());
65 EXPECT_EQ(5ul, result->getNumberOfStates());
66 EXPECT_EQ(8ul, result->getNumberOfTransitions());
67}
68
69TEST(DeterministicModelBisimulationDecomposition, Crowds) {
70 std::shared_ptr<storm::models::sparse::Model<double>> abstractModel =
71 storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/crowds5_5.tra", STORM_TEST_RESOURCES_DIR "/lab/crowds5_5.lab", "", "");
72
73 ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
74 std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
75
76 using OptionsType = typename storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>::Options;
77
78 storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> bisim(
79 *dtmc, OptionsType::preservingAllLabels(DefaultTestTolerance));
80 std::shared_ptr<storm::models::sparse::Model<double>> result;
81 ASSERT_NO_THROW(bisim.computeBisimulationDecomposition());
82 ASSERT_NO_THROW(result = bisim.getQuotient());
83
84 EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType());
85 EXPECT_EQ(334ul, result->getNumberOfStates());
86 EXPECT_EQ(546ul, result->getNumberOfTransitions());
87
88 OptionsType options = OptionsType::preservingAllLabels(DefaultTestTolerance);
89 options.respectedAtomicPropositions = std::set<std::string>({"observe0Greater1"});
90
91 storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> bisim2(*dtmc, options);
92 ASSERT_NO_THROW(bisim2.computeBisimulationDecomposition());
93 ASSERT_NO_THROW(result = bisim2.getQuotient());
94
95 EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType());
96 EXPECT_EQ(65ul, result->getNumberOfStates());
97 EXPECT_EQ(105ul, result->getNumberOfTransitions());
98
99 options.setType(storm::storage::BisimulationType::Weak);
100
101 storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> bisim3(*dtmc, options);
102 ASSERT_NO_THROW(bisim3.computeBisimulationDecomposition());
103 ASSERT_NO_THROW(result = bisim3.getQuotient());
104
105 EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType());
106 EXPECT_EQ(43ul, result->getNumberOfStates());
107 EXPECT_EQ(83ul, result->getNumberOfTransitions());
108
109 storm::parser::FormulaParser formulaParser;
110 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
111
112 OptionsType options3(*dtmc, *formula, DefaultTestTolerance);
113
114 storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> bisim5(*dtmc, options3);
115 ASSERT_NO_THROW(bisim5.computeBisimulationDecomposition());
116 ASSERT_NO_THROW(result = bisim5.getQuotient());
117
118 EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType());
119 EXPECT_EQ(64ul, result->getNumberOfStates());
120 EXPECT_EQ(104ul, result->getNumberOfTransitions());
121
122 formula = formulaParser.parseSingleFormulaFromString("P=? [true U<=50 \"observe0Greater1\"] ");
123
124 OptionsType options4(*dtmc, *formula, DefaultTestTolerance);
125
126 storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> bisim6(*dtmc, options4);
127 ASSERT_NO_THROW(bisim6.computeBisimulationDecomposition());
128 ASSERT_NO_THROW(result = bisim6.getQuotient());
129
130 EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType());
131 EXPECT_EQ(65ul, result->getNumberOfStates());
132 EXPECT_EQ(105ul, result->getNumberOfTransitions());
133}
134
135// Suppress compiler warning on unreachable code due to skipped test
136#pragma clang diagnostic push
137#pragma clang diagnostic ignored "-Wunreachable-code"
138TEST(DeterministicModelBisimulationDecomposition, Cluster) {
139 // TODO FIXME
140 GTEST_SKIP() << "CTMC bisimulation currently yields unstable results.";
141#ifndef STORM_HAVE_Z3
142 GTEST_SKIP() << "Z3 not available.";
143#endif
144 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true);
145 std::shared_ptr<storm::models::sparse::Model<double>> model =
146 storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
147
148 ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc);
149 std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
150 ASSERT_EQ(3478ul, ctmc->getNumberOfStates());
151 ASSERT_EQ(14639ul, ctmc->getNumberOfTransitions());
152
153 using OptionsType = typename storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Ctmc<double>>::Options;
154
155 storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Ctmc<double>> bisim(
156 *ctmc, OptionsType::preservingAllLabels(DefaultTestTolerance));
157 std::shared_ptr<storm::models::sparse::Model<double>> result;
158 ASSERT_NO_THROW(bisim.computeBisimulationDecomposition());
159 ASSERT_NO_THROW(result = bisim.getQuotient());
160
161 EXPECT_EQ(storm::models::ModelType::Ctmc, result->getType());
162 EXPECT_EQ(1731ul, result->getNumberOfStates());
163 EXPECT_EQ(8619ul, result->getNumberOfTransitions());
164
165 OptionsType options = OptionsType::preservingAllLabels(DefaultTestTolerance);
166 options.respectedAtomicPropositions = std::set<std::string>({"down"});
167 storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Ctmc<double>> bisim2(*ctmc, options);
168 ASSERT_NO_THROW(bisim2.computeBisimulationDecomposition());
169 ASSERT_NO_THROW(result = bisim2.getQuotient());
170
171 EXPECT_EQ(storm::models::ModelType::Ctmc, result->getType());
172 EXPECT_EQ(1618ul, result->getNumberOfStates());
173 EXPECT_EQ(8816ul, result->getNumberOfTransitions());
174
175 options.setType(storm::storage::BisimulationType::Weak);
176 storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Ctmc<double>> bisim3(*ctmc, options);
177 ASSERT_NO_THROW(bisim3.computeBisimulationDecomposition());
178 ASSERT_NO_THROW(result = bisim3.getQuotient());
179
180 EXPECT_EQ(storm::models::ModelType::Ctmc, result->getType());
181 EXPECT_EQ(41ul, result->getNumberOfStates());
182 EXPECT_EQ(159ul, result->getNumberOfTransitions());
183
184 storm::parser::FormulaParser formulaParser;
185 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10000 \"down\"]");
186 OptionsType options3(*ctmc, *formula, DefaultTestTolerance);
187 storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Ctmc<double>> bisim5(*ctmc, options3);
188 ASSERT_NO_THROW(bisim5.computeBisimulationDecomposition());
189 ASSERT_NO_THROW(result = bisim5.getQuotient());
190
191 EXPECT_EQ(storm::models::ModelType::Ctmc, result->getType());
192 EXPECT_EQ(1618ul, result->getNumberOfStates());
193 EXPECT_EQ(8816ul, result->getNumberOfTransitions());
194}
195#pragma clang diagnostic pop
TEST
TEST(DeterministicModelBisimulationDecomposition, Die)
Definition DeterministicModelBisimulationDecompositionTest.cpp:16
storm::builder::ExplicitModelBuilder::build
std::shared_ptr< storm::models::sparse::Model< ValueType, RewardModelType > > build()
Convert the program given at construction time to an abstract model.
Definition ExplicitModelBuilder.cpp:71
storm::models::sparse::Ctmc
This class represents a continuous-time Markov chain.
Definition Ctmc.h:13
storm::models::sparse::Dtmc
This class represents a discrete-time Markov chain.
Definition Dtmc.h:13
storm::parser::AutoParser::parseModel
static std::shared_ptr< storm::models::sparse::Model< ValueType, storm::models::sparse::StandardRewardModel< RewardValueType > > > parseModel(std::string const &transitionsFilename, std::string const &labelingFilename, std::string const &stateRewardFilename="", std::string const &transitionRewardFilename="", std::string const &choiceLabelingFilename="", ExplicitModelParserOptions const &options=ExplicitModelParserOptions())
Checks the given files and parses the model within these files.
Definition AutoParser.cpp:20
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::BisimulationDecomposition::getQuotient
std::shared_ptr< ModelType > getQuotient() const
Retrieves the quotient of the model under the computed bisimulation.
Definition BisimulationDecomposition.cpp:293
storm::storage::BisimulationDecomposition::computeBisimulationDecomposition
void computeBisimulationDecomposition()
Computes the decomposition of the model into bisimulation equivalence classes.
Definition BisimulationDecomposition.cpp:209
storm::storage::DeterministicModelBisimulationDecomposition
This class represents the decomposition of a deterministic model into its bisimulation quotient.
Definition DeterministicModelBisimulationDecomposition.h:13
storm::generator::NextStateGeneratorOptions
storm::builder::BuilderOptions NextStateGeneratorOptions
Definition NextStateGenerator.h:25
storm_gtest.h