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