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