Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
DdJaniModelBuilderTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include "storm-parsers/api/model_descriptions.h"
5#include "storm-parsers/parser/JaniParser.h"
6#include "storm-parsers/parser/PrismParser.h"
7#include "storm/builder/DdJaniModelBuilder.h"
8#include "storm/exceptions/WrongFormatException.h"
9#include "storm/models/symbolic/Ctmc.h"
10#include "storm/models/symbolic/Dtmc.h"
11#include "storm/models/symbolic/Mdp.h"
12#include "storm/models/symbolic/StandardRewardModel.h"
13#include "storm/storage/SymbolicModelDescription.h"
14#include "storm/storage/dd/Add.h"
15#include "storm/storage/dd/Bdd.h"
16#include "storm/storage/jani/Compositions.h"
17
18namespace {
19
20class Cudd {
21 public:
22 static const storm::dd::DdType DdType = storm::dd::DdType::CUDD;
23};
24
25class Sylvan {
26 public:
27 static const storm::dd::DdType DdType = storm::dd::DdType::Sylvan;
28};
29
30template<typename TestType>
31class DdJaniModelBuilderTest : public ::testing::Test {
32 public:
33 static const storm::dd::DdType DdType = TestType::DdType;
34
35 storm::jani::Model getJaniModelFromPrism(std::string const& pathInTestResourcesDir, bool prismCompatability = false) {
36 storm::storage::SymbolicModelDescription modelDescription =
37 storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/" + pathInTestResourcesDir, prismCompatability);
38 auto m = modelDescription.toJani(true).preprocess().asJaniModel();
39 auto unsupportedFeatures = m.restrictToFeatures(storm::builder::DdJaniModelBuilder<DdType, double>::getSupportedJaniFeatures());
40 EXPECT_TRUE(unsupportedFeatures.empty()) << "Model '" << pathInTestResourcesDir << "' uses unsupported feature(s) " << unsupportedFeatures.toString();
41 return m;
42 }
43};
44
45typedef ::testing::Types<Cudd, Sylvan> TestingTypes;
46TYPED_TEST_SUITE(DdJaniModelBuilderTest, TestingTypes, );
47
48TYPED_TEST(DdJaniModelBuilderTest, Dtmc) {
49 const storm::dd::DdType DdType = TestFixture::DdType;
50 auto janiModel = this->getJaniModelFromPrism("/dtmc/die.pm");
51
52 storm::builder::DdJaniModelBuilder<DdType, double> builder;
53 std::shared_ptr<storm::models::symbolic::Model<DdType>> model = builder.build(janiModel);
54 EXPECT_EQ(13ul, model->getNumberOfStates());
55 EXPECT_EQ(20ul, model->getNumberOfTransitions());
56
57 janiModel = this->getJaniModelFromPrism("/dtmc/brp-16-2.pm");
58 model = builder.build(janiModel);
59 EXPECT_EQ(677ul, model->getNumberOfStates());
60 EXPECT_EQ(867ul, model->getNumberOfTransitions());
61
62 janiModel = this->getJaniModelFromPrism("/dtmc/crowds-5-5.pm");
63 model = builder.build(janiModel);
64 EXPECT_EQ(8607ul, model->getNumberOfStates());
65 EXPECT_EQ(15113ul, model->getNumberOfTransitions());
66
67 janiModel = this->getJaniModelFromPrism("/dtmc/leader-3-5.pm");
68 model = builder.build(janiModel);
69 EXPECT_EQ(273ul, model->getNumberOfStates());
70 EXPECT_EQ(397ul, model->getNumberOfTransitions());
71
72 janiModel = this->getJaniModelFromPrism("/dtmc/nand-5-2.pm");
73 model = builder.build(janiModel);
74 EXPECT_EQ(1728ul, model->getNumberOfStates());
75 EXPECT_EQ(2505ul, model->getNumberOfTransitions());
76}
77
78TYPED_TEST(DdJaniModelBuilderTest, Ctmc) {
79 const storm::dd::DdType DdType = TestFixture::DdType;
80 auto janiModel = this->getJaniModelFromPrism("/ctmc/cluster2.sm", true);
81 storm::builder::DdJaniModelBuilder<DdType, double> builder;
82 std::shared_ptr<storm::models::symbolic::Model<DdType>> model = builder.build(janiModel);
83 EXPECT_EQ(276ul, model->getNumberOfStates());
84 EXPECT_EQ(1120ul, model->getNumberOfTransitions());
85
86 janiModel = this->getJaniModelFromPrism("/ctmc/embedded2.sm", true);
87 model = builder.build(janiModel);
88 EXPECT_EQ(3478ul, model->getNumberOfStates());
89 EXPECT_EQ(14639ul, model->getNumberOfTransitions());
90
91 janiModel = this->getJaniModelFromPrism("/ctmc/polling2.sm", true);
92 model = builder.build(janiModel);
93 EXPECT_EQ(12ul, model->getNumberOfStates());
94 EXPECT_EQ(22ul, model->getNumberOfTransitions());
95
96 janiModel = this->getJaniModelFromPrism("/ctmc/fms2.sm", true);
97 model = builder.build(janiModel);
98 EXPECT_EQ(810ul, model->getNumberOfStates());
99 EXPECT_EQ(3699ul, model->getNumberOfTransitions());
100
101 janiModel = this->getJaniModelFromPrism("/ctmc/tandem5.sm", true);
102 model = builder.build(janiModel);
103 EXPECT_EQ(66ul, model->getNumberOfStates());
104 EXPECT_EQ(189ul, model->getNumberOfTransitions());
105}
106
107TYPED_TEST(DdJaniModelBuilderTest, Mdp) {
108 const storm::dd::DdType DdType = TestFixture::DdType;
109 auto janiModel = this->getJaniModelFromPrism("/mdp/two_dice.nm");
110 storm::builder::DdJaniModelBuilder<DdType, double> builder;
111 std::shared_ptr<storm::models::symbolic::Model<DdType>> model = builder.build(janiModel);
112
113 EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
114 std::shared_ptr<storm::models::symbolic::Mdp<DdType>> mdp = model->template as<storm::models::symbolic::Mdp<DdType>>();
115
116 EXPECT_EQ(169ul, mdp->getNumberOfStates());
117 EXPECT_EQ(436ul, mdp->getNumberOfTransitions());
118 EXPECT_EQ(254ul, mdp->getNumberOfChoices());
119
120 janiModel = this->getJaniModelFromPrism("/mdp/leader3.nm");
121 model = builder.build(janiModel);
122
123 EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
124 mdp = model->template as<storm::models::symbolic::Mdp<DdType>>();
125
126 EXPECT_EQ(364ul, mdp->getNumberOfStates());
127 EXPECT_EQ(654ul, mdp->getNumberOfTransitions());
128 EXPECT_EQ(573ul, mdp->getNumberOfChoices());
129
130 janiModel = this->getJaniModelFromPrism("/mdp/coin2-2.nm");
131 model = builder.build(janiModel);
132
133 EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
134 mdp = model->template as<storm::models::symbolic::Mdp<DdType>>();
135
136 EXPECT_EQ(272ul, mdp->getNumberOfStates());
137 EXPECT_EQ(492ul, mdp->getNumberOfTransitions());
138 EXPECT_EQ(400ul, mdp->getNumberOfChoices());
139
140 janiModel = this->getJaniModelFromPrism("/mdp/csma2-2.nm");
141 model = builder.build(janiModel);
142
143 EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
144 mdp = model->template as<storm::models::symbolic::Mdp<DdType>>();
145
146 EXPECT_EQ(1038ul, mdp->getNumberOfStates());
147 EXPECT_EQ(1282ul, mdp->getNumberOfTransitions());
148 EXPECT_EQ(1054ul, mdp->getNumberOfChoices());
149
150 janiModel = this->getJaniModelFromPrism("/mdp/firewire3-0.5.nm");
151 model = builder.build(janiModel);
152
153 EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
154 mdp = model->template as<storm::models::symbolic::Mdp<DdType>>();
155
156 EXPECT_EQ(4093ul, mdp->getNumberOfStates());
157 EXPECT_EQ(5585ul, mdp->getNumberOfTransitions());
158 EXPECT_EQ(5519ul, mdp->getNumberOfChoices());
159
160 janiModel = this->getJaniModelFromPrism("/mdp/wlan0-2-2.nm");
161 model = builder.build(janiModel);
162
163 EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
164 mdp = model->template as<storm::models::symbolic::Mdp<DdType>>();
165
166 EXPECT_EQ(37ul, mdp->getNumberOfStates());
167 EXPECT_EQ(59ul, mdp->getNumberOfTransitions());
168 EXPECT_EQ(59ul, mdp->getNumberOfChoices());
169
170 janiModel = this->getJaniModelFromPrism("/mdp/sync.nm");
171 model = builder.build(janiModel);
172
173 EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
174 mdp = model->template as<storm::models::symbolic::Mdp<DdType>>();
175
176 EXPECT_EQ(5ul, mdp->getNumberOfStates());
177 EXPECT_EQ(24ul, mdp->getNumberOfTransitions());
178 EXPECT_EQ(12ul, mdp->getNumberOfChoices());
179}
180
181TYPED_TEST(DdJaniModelBuilderTest, SynchronizationVectors) {
182 const storm::dd::DdType DdType = TestFixture::DdType;
183 auto janiModel = this->getJaniModelFromPrism("/mdp/SmallPrismTest.nm");
184
185 storm::builder::DdJaniModelBuilder<DdType, double> builder;
186
187 // Start by checking the original composition.
188 std::shared_ptr<storm::models::symbolic::Model<DdType>> model = builder.build(janiModel);
189 EXPECT_EQ(7ul, model->getNumberOfStates());
190 EXPECT_EQ(10ul, model->getNumberOfTransitions());
191
192 // Now we tweak it's system composition to check whether synchronization vectors work.
193 std::vector<std::shared_ptr<storm::jani::Composition>> automataCompositions;
194 automataCompositions.push_back(std::make_shared<storm::jani::AutomatonComposition>("one"));
195 automataCompositions.push_back(std::make_shared<storm::jani::AutomatonComposition>("two"));
196 automataCompositions.push_back(std::make_shared<storm::jani::AutomatonComposition>("three"));
197
198 // First, make all actions non-synchronizing.
199 std::vector<storm::jani::SynchronizationVector> synchronizationVectors;
200
201 std::vector<std::string> inputVector;
202 inputVector.push_back("a");
203 inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
204 inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
205 synchronizationVectors.emplace_back(inputVector);
206 inputVector.clear();
207 inputVector.push_back("c");
208 inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
209 inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
210 synchronizationVectors.emplace_back(inputVector);
211 inputVector.clear();
212 inputVector.push_back("d");
213 inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
214 inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
215 synchronizationVectors.emplace_back(inputVector);
216 inputVector.clear();
217 inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
218 inputVector.push_back("b");
219 inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
220 synchronizationVectors.emplace_back(inputVector);
221 inputVector.clear();
222 inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
223 inputVector.push_back("c");
224 inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
225 synchronizationVectors.emplace_back(inputVector);
226 inputVector.clear();
227 inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
228 inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
229 inputVector.push_back("c");
230 synchronizationVectors.emplace_back(inputVector);
231 inputVector.clear();
232
233 std::shared_ptr<storm::jani::Composition> newComposition = std::make_shared<storm::jani::ParallelComposition>(automataCompositions, synchronizationVectors);
234 janiModel.setSystemComposition(newComposition);
235 model = builder.build(janiModel);
236 EXPECT_EQ(24ul, model->getNumberOfStates());
237 EXPECT_EQ(48ul, model->getNumberOfTransitions());
238
239 // Then, make only a, b and c synchronize.
240 synchronizationVectors.clear();
241 inputVector.clear();
242 inputVector.push_back("a");
243 inputVector.push_back("b");
244 inputVector.push_back("c");
245 synchronizationVectors.emplace_back(inputVector, "d");
246 inputVector.clear();
247 inputVector.push_back("c");
248 inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
249 inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
250 synchronizationVectors.emplace_back(inputVector);
251 inputVector.clear();
252 inputVector.push_back("d");
253 inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
254 inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
255 synchronizationVectors.emplace_back(inputVector);
256 inputVector.clear();
257 inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
258 inputVector.push_back("c");
259 inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
260 synchronizationVectors.emplace_back(inputVector);
261
262 newComposition = std::make_shared<storm::jani::ParallelComposition>(automataCompositions, synchronizationVectors);
263 janiModel.setSystemComposition(newComposition);
264 model = builder.build(janiModel);
265 EXPECT_EQ(7ul, model->getNumberOfStates());
266 EXPECT_EQ(10ul, model->getNumberOfTransitions());
267
268 synchronizationVectors.clear();
269 inputVector.clear();
270 inputVector.push_back("a");
271 inputVector.push_back("b");
272 inputVector.push_back("c");
273 synchronizationVectors.emplace_back(inputVector, "d");
274 inputVector.clear();
275 inputVector.push_back("c");
276 inputVector.push_back("c");
277 inputVector.push_back("a");
278 synchronizationVectors.emplace_back(inputVector, "d");
279 inputVector.clear();
280 inputVector.push_back("d");
281 inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
282 inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
283 synchronizationVectors.emplace_back(inputVector);
284 newComposition = std::make_shared<storm::jani::ParallelComposition>(automataCompositions, synchronizationVectors);
285 janiModel.setSystemComposition(newComposition);
286 model = builder.build(janiModel);
287 EXPECT_EQ(3ul, model->getNumberOfStates());
288 EXPECT_EQ(3ul, model->getNumberOfTransitions());
289
290 synchronizationVectors.clear();
291 inputVector.clear();
292 inputVector.push_back("a");
293 inputVector.push_back("b");
294 inputVector.push_back("c");
295 synchronizationVectors.emplace_back(inputVector, "d");
296 inputVector.clear();
297 inputVector.push_back("c");
298 inputVector.push_back("c");
299 inputVector.push_back("a");
300 synchronizationVectors.emplace_back(inputVector, "d");
301 inputVector.clear();
302 inputVector.push_back("d");
303 inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
304 inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
305 synchronizationVectors.emplace_back(inputVector);
306 inputVector.clear();
307 inputVector.push_back("d");
308 inputVector.push_back("c");
309 inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
310 synchronizationVectors.emplace_back(inputVector, "b");
311 newComposition = std::make_shared<storm::jani::ParallelComposition>(automataCompositions, synchronizationVectors);
312 janiModel.setSystemComposition(newComposition);
313 model = builder.build(janiModel);
314 EXPECT_EQ(4ul, model->getNumberOfStates());
315 EXPECT_EQ(5ul, model->getNumberOfTransitions());
316}
317
318TYPED_TEST(DdJaniModelBuilderTest, Composition) {
319 const storm::dd::DdType DdType = TestFixture::DdType;
320 auto janiModel = this->getJaniModelFromPrism("/mdp/system_composition.nm");
321
322 storm::builder::DdJaniModelBuilder<DdType, double> builder;
323 STORM_SILENT_EXPECT_THROW(std::shared_ptr<storm::models::symbolic::Model<DdType>> model = builder.build(janiModel),
324 storm::exceptions::WrongFormatException);
325
326 janiModel = this->getJaniModelFromPrism("/mdp/system_composition2.nm");
327 STORM_SILENT_EXPECT_THROW(std::shared_ptr<storm::models::symbolic::Model<DdType>> model = builder.build(janiModel),
328 storm::exceptions::WrongFormatException);
329}
330
331TYPED_TEST(DdJaniModelBuilderTest, InputEnabling) {
332 const storm::dd::DdType DdType = TestFixture::DdType;
333 auto janiModel = this->getJaniModelFromPrism("/mdp/SmallPrismTest2.nm");
334
335 storm::builder::DdJaniModelBuilder<DdType, double> builder;
336
337 // Make some automaton compositions input-enabled.
338 std::vector<std::shared_ptr<storm::jani::Composition>> automataCompositions;
339 automataCompositions.push_back(std::make_shared<storm::jani::AutomatonComposition>("one"));
340 automataCompositions.push_back(std::make_shared<storm::jani::AutomatonComposition>("two"));
341 automataCompositions.push_back(std::make_shared<storm::jani::AutomatonComposition>("three", std::set<std::string>{"a"}));
342
343 // Create the synchronization vectors.
344 std::vector<storm::jani::SynchronizationVector> synchronizationVectors;
345 std::vector<std::string> inputVector;
346 inputVector.push_back("a");
347 inputVector.push_back("b");
348 inputVector.push_back("c");
349 synchronizationVectors.emplace_back(inputVector, "d");
350 inputVector.clear();
351 inputVector.push_back("c");
352 inputVector.push_back("c");
353 inputVector.push_back("a");
354 synchronizationVectors.emplace_back(inputVector, "d");
355 inputVector.clear();
356 inputVector.push_back("d");
357 inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
358 inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
359 synchronizationVectors.emplace_back(inputVector);
360
361 std::shared_ptr<storm::jani::Composition> newComposition = std::make_shared<storm::jani::ParallelComposition>(automataCompositions, synchronizationVectors);
362 janiModel.setSystemComposition(newComposition);
363 std::shared_ptr<storm::models::symbolic::Model<DdType>> model = builder.build(janiModel);
364 EXPECT_EQ(4ul, model->getNumberOfStates());
365 EXPECT_EQ(5ul, model->getNumberOfTransitions());
366}
367
368} // namespace
Cudd::DdType
static const storm::dd::DdType DdType
Definition GraphTest.cpp:25
Sylvan::DdType
static const storm::dd::DdType DdType
Definition GraphTest.cpp:30
storm::builder::DdJaniModelBuilder::build
std::shared_ptr< storm::models::symbolic::Model< Type, ValueType > > build(storm::jani::Model const &model, Options const &options=Options())
Translates the given program into a symbolic model (i.e.
Definition DdJaniModelBuilder.cpp:2411
storm::jani::ModelFeatures::toString
std::string toString() const
Definition ModelFeatures.cpp:25
storm::jani::Model::restrictToFeatures
ModelFeatures restrictToFeatures(ModelFeatures const &modelFeatures)
Attempts to eliminate all features of this model that are not in the given set of features.
Definition Model.cpp:1243
storm::jani::SynchronizationVector::NO_ACTION_INPUT
static const std::string NO_ACTION_INPUT
Definition ParallelComposition.h:51
storm::models::sparse::Dtmc
This class represents a discrete-time Markov chain.
Definition Dtmc.h:14
storm::models::sparse::Mdp
This class represents a (discrete-time) Markov decision process.
Definition Mdp.h:14
storm::models::symbolic::Model
Base class for all symbolic models.
Definition Model.h:46
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::toJani
SymbolicModelDescription toJani(bool makeVariablesGlobal=true) const
Definition SymbolicModelDescription.cpp:138
storm::storage::SymbolicModelDescription::asJaniModel
storm::jani::Model const & asJaniModel() const
Definition SymbolicModelDescription.cpp:100
storm::storage::SymbolicModelDescription::preprocess
SymbolicModelDescription preprocess(std::string const &constantDefinitionString="") const
Definition SymbolicModelDescription.cpp:162
model_descriptions.h
TYPED_TEST
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
Definition GraphTest.cpp:49
TYPED_TEST_SUITE
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
TestingTypes
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:46
storm_gtest.h
STORM_SILENT_EXPECT_THROW
#define STORM_SILENT_EXPECT_THROW(statement, expected_exception)
Definition storm_gtest.h:104