Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
JaniParserTest.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/exceptions/InvalidArgumentException.h"
7#include "storm/logic/Formulas.h"
8#include "storm/storage/jani/Model.h"
9#include "storm/storage/jani/ModelType.h"
10#include "storm/storage/jani/Property.h"
11
12TEST(JaniParser, DieExampleTest) {
13 std::string testInput = R"({
14 "jani-version": 1,
15 "name": "die.jani",
16 "type": "dtmc",
17 "features": [ "derived-operators" ],
18 "variables": [
19 {
20 "name": "s",
21 "type": {
22 "base": "int",
23 "kind": "bounded",
24 "lower-bound": 0,
25 "upper-bound": 7
26 },
27 "initial-value": 0
28 },
29 {
30 "name": "d",
31 "type": {
32 "base": "int",
33 "kind": "bounded",
34 "lower-bound": 0,
35 "upper-bound": 6
36 },
37 "initial-value": 0
38 }
39 ],
40 "properties": [
41 {
42 "name": "Probability to throw a six",
43 "expression": {
44 "op": "filter",
45 "fun": "max",
46 "states": { "op": "initial" },
47 "values": {
48 "op": "Pmin",
49 "exp": {
50 "op": "U",
51 "left": true,
52 "right": {
53 "op": "∧",
54 "left": {
55 "op": "=",
56 "left": "s",
57 "right": 7
58 },
59 "right": {
60 "op": "=",
61 "left": "d",
62 "right": 6
63 }
64 }
65 }
66 }
67 }
68 },
69 {
70 "name": "Expected number of coin flips",
71 "expression": {
72 "op": "filter",
73 "fun": "max",
74 "states": { "op": "initial" },
75 "values": {
76 "op": "Emin",
77 "accumulate": [ "steps" ],
78 "exp": 1,
79 "reach": {
80 "op": "=",
81 "left": "s",
82 "right": 7
83 }
84 }
85 }
86 },
87 {
88 "name": "Conjunction of path formulas",
89 "expression": {
90 "op": "filter",
91 "fun": "max",
92 "states": { "op": "initial" },
93 "values": {
94 "op": "Pmin",
95 "exp": {
96 "op": "∧",
97 "left": {
98 "op": "G",
99 "exp": {
100 "op": "≠",
101 "left": "d",
102 "right": 6
103 }
104 },
105 "right": {
106 "op": "F",
107 "exp": {
108 "op": "=",
109 "left": "s",
110 "right": 6
111 }
112 }
113 }
114 }
115 }
116 },
117 {
118 "name": "Disjunction of path formulas",
119 "expression": {
120 "op": "filter",
121 "fun": "max",
122 "states": { "op": "initial" },
123 "values": {
124 "op": "Pmin",
125 "exp": {
126 "op": "∨",
127 "left": {
128 "op": "G",
129 "exp": {
130 "op": "≠",
131 "left": "s",
132 "right": 3
133 }
134 },
135 "right": {
136 "op": "G",
137 "exp": {
138 "op": "≠",
139 "left": "s",
140 "right": 4
141 }
142 }
143 }
144 }
145 }
146 },
147 {
148 "name": "Negation of a path formula",
149 "expression": {
150 "op": "filter",
151 "fun": "max",
152 "states": { "op": "initial" },
153 "values": {
154 "op": "Pmin",
155 "exp": {
156 "op": "¬",
157 "exp": {
158 "op": "F",
159 "exp": {
160 "op": "=",
161 "left": "d",
162 "right": 1
163 }
164 }
165 }
166 }
167 }
168 },
169 {
170 "name": "Implication of path formulas",
171 "expression": {
172 "op": "filter",
173 "fun": "max",
174 "states": { "op": "initial" },
175 "values": {
176 "op": "Pmin",
177 "exp": {
178 "op": "⇒",
179 "left": {
180 "op": "F",
181 "exp": {
182 "op": "=",
183 "left": "s",
184 "right": 3
185 }
186 },
187 "right": {
188 "op": "F",
189 "exp": {
190 "op": "=",
191 "left": "d",
192 "right": 1
193 }
194 }
195 }
196 }
197 }
198 },
199 {
200 "name": "Conjunction of state formulas",
201 "expression": {
202 "op": "filter",
203 "fun": "count",
204 "states": true,
205 "values": {
206 "op": "∧",
207 "left": {
208 "op": "¬",
209 "exp": {
210 "op": "≥",
211 "left": {
212 "op": "Pmin",
213 "exp": {
214 "op": "F",
215 "exp": {
216 "op": "=",
217 "left": "d",
218 "right": 6
219 }
220 }
221 },
222 "right": 0.5
223 }
224 },
225 "right": {
226 "op": "≥",
227 "left": {
228 "op": "Pmin",
229 "exp": {
230 "op": "F",
231 "exp": {
232 "op": "≥",
233 "left": "d",
234 "right": 4
235 }
236 }
237 },
238 "right": 0.5
239 }
240 }
241 }
242 }
243 ],
244 "automata": [
245 {
246 "name": "die",
247 "locations": [{ "name": "l" }],
248 "initial-locations": ["l"],
249 "edges": [
250 {
251 "location": "l",
252 "guard": {
253 "exp": {
254 "op": "=",
255 "left": "s",
256 "right": 0
257 }
258 },
259 "destinations": [
260 {
261 "location": "l",
262 "probability": { "exp": 0.5 },
263 "assignments": [
264 {
265 "ref": "s",
266 "value": 1
267 }
268 ]
269 },
270 {
271 "location": "l",
272 "probability": { "exp": 0.5 },
273 "assignments": [
274 {
275 "ref": "s",
276 "value": 2
277 }
278 ]
279 }
280 ]
281 },
282 {
283 "location": "l",
284 "guard": {
285 "exp": {
286 "left": "s",
287 "op": "=",
288 "right": 1
289 }
290 },
291 "destinations": [
292 {
293 "location": "l",
294 "probability": { "exp": 0.5 },
295 "assignments": [
296 {
297 "ref": "s",
298 "value": 3
299 }
300 ]
301 },
302 {
303 "location": "l",
304 "probability": { "exp": 0.5 },
305 "assignments": [
306 {
307 "ref": "s",
308 "value": 4
309 }
310 ]
311 }
312 ]
313 },
314 {
315 "location": "l",
316 "guard": {
317 "exp": {
318 "left": "s",
319 "op": "=",
320 "right": 2
321 }
322 },
323 "destinations": [
324 {
325 "location": "l",
326 "probability": { "exp": 0.5 },
327 "assignments": [
328 {
329 "ref": "s",
330 "value": 5
331 }
332 ]
333 },
334 {
335 "location": "l",
336 "probability": { "exp": 0.5 },
337 "assignments": [
338 {
339 "ref": "s",
340 "value": 6
341 }
342 ]
343 }
344 ]
345 },
346 {
347 "location": "l",
348 "guard": {
349 "exp": {
350 "left": "s",
351 "op": "=",
352 "right": 3
353 }
354 },
355 "destinations": [
356 {
357 "location": "l",
358 "probability": { "exp": 0.5 },
359 "assignments": [
360 {
361 "ref": "s",
362 "value": 1
363 }
364 ]
365 },
366 {
367 "location": "l",
368 "probability": { "exp": 0.5 },
369 "assignments": [
370 {
371 "ref": "s",
372 "value": 7
373 },
374 {
375 "ref": "d",
376 "value": 1
377 }
378 ]
379 }
380 ]
381 },
382 {
383 "location": "l",
384 "guard": {
385 "exp": {
386 "left": "s",
387 "op": "=",
388 "right": 4
389 }
390 },
391 "destinations": [
392 {
393 "location": "l",
394 "probability": { "exp": 0.5 },
395 "assignments": [
396 {
397 "ref": "s",
398 "value": 7
399 },
400 {
401 "ref": "d",
402 "value": 2
403 }
404 ]
405 },
406 {
407 "location": "l",
408 "probability": { "exp": 0.5 },
409 "assignments": [
410 {
411 "ref": "s",
412 "value": 7
413 },
414 {
415 "ref": "d",
416 "value": 3
417 }
418 ]
419 }
420 ]
421 },
422 {
423 "location": "l",
424 "guard": {
425 "exp": {
426 "left": "s",
427 "op": "=",
428 "right": 5
429 }
430 },
431 "destinations": [
432 {
433 "location": "l",
434 "probability": { "exp": 0.5 },
435 "assignments": [
436 {
437 "ref": "s",
438 "value": 7
439 },
440 {
441 "ref": "d",
442 "value": 4
443 }
444 ]
445 },
446 {
447 "location": "l",
448 "probability": { "exp": 0.5 },
449 "assignments": [
450 {
451 "ref": "s",
452 "value": 7
453 },
454 {
455 "ref": "d",
456 "value": 5
457 }
458 ]
459 }
460 ]
461 },
462 {
463 "location": "l",
464 "guard": {
465 "exp": {
466 "left": "s",
467 "op": "=",
468 "right": 6
469 }
470 },
471 "destinations": [
472 {
473 "location": "l",
474 "probability": { "exp": 0.5 },
475 "assignments": [
476 {
477 "ref": "s",
478 "value": 2
479 }
480 ]
481 },
482 {
483 "location": "l",
484 "probability": { "exp": 0.5 },
485 "assignments": [
486 {
487 "ref": "s",
488 "value": 7
489 },
490 {
491 "ref": "d",
492 "value": 6
493 }
494 ]
495 }
496 ]
497 },
498 {
499 "location": "l",
500 "guard": {
501 "exp": {
502 "left": "s",
503 "op": "=",
504 "right": 7
505 }
506 },
507 "destinations": [
508 {
509 "location": "l",
510 "assignments": [
511 {
512 "ref": "s",
513 "value": 7
514 }
515 ]
516 }
517 ]
518 }
519 ]
520
521 }
522 ],
523 "system": {
524 "elements": [ { "automaton": "die" } ]
525 }
526 })";
527
528 std::pair<storm::jani::Model, std::vector<storm::jani::Property>> result;
529 EXPECT_NO_THROW(result = storm::api::parseJaniModelFromString(testInput));
530 EXPECT_EQ(storm::jani::ModelType::DTMC, result.first.getModelType());
531 EXPECT_TRUE(result.first.hasGlobalVariable("s"));
532 EXPECT_EQ(1ul, result.first.getNumberOfAutomata());
533
534 ASSERT_EQ(7ul, result.second.size());
535
536 auto const& conjunction = result.second[2].getRawFormula()->asProbabilityOperatorFormula().getSubformula();
537 ASSERT_TRUE(conjunction.isBinaryBooleanPathFormula());
538
539 auto const& disjunction = result.second[3].getRawFormula()->asProbabilityOperatorFormula().getSubformula();
540 ASSERT_TRUE(disjunction.isBinaryBooleanPathFormula());
541
542 auto const& negation = result.second[4].getRawFormula()->asProbabilityOperatorFormula().getSubformula();
543 ASSERT_TRUE(negation.isUnaryBooleanPathFormula());
544
545 auto const& implication = result.second[5].getRawFormula()->asProbabilityOperatorFormula().getSubformula();
546 ASSERT_TRUE(implication.isBinaryBooleanPathFormula());
547
548 auto const& stateConjunction = *result.second[6].getRawFormula();
549 ASSERT_TRUE(stateConjunction.isBinaryBooleanStateFormula());
550}
551
552TEST(JaniParser, DieArrayExampleTest) {
553 std::pair<storm::jani::Model, std::vector<storm::jani::Property>> result;
554 EXPECT_NO_THROW(result = storm::api::parseJaniModel(STORM_TEST_RESOURCES_DIR "/dtmc/die_array.jani"));
555 EXPECT_EQ(storm::jani::ModelType::DTMC, result.first.getModelType());
556 EXPECT_TRUE(result.first.containsArrayVariables());
557 EXPECT_TRUE(result.first.hasGlobalVariable("sd"));
558 EXPECT_EQ(1ul, result.first.getNumberOfAutomata());
559}
560
561TEST(JaniParser, FTWCTest) {
562 std::pair<storm::jani::Model, std::vector<storm::jani::Property>> result;
563 EXPECT_NO_THROW(result = storm::api::parseJaniModel(STORM_TEST_RESOURCES_DIR "/ma/ftwc.jani"));
564 EXPECT_EQ(storm::jani::ModelType::MA, result.first.getModelType());
565 EXPECT_TRUE(result.first.containsArrayVariables());
566 EXPECT_TRUE(result.first.hasGlobalVariable("workstations_up"));
567 EXPECT_TRUE(result.first.hasGlobalVariable("workstations_up"));
568 EXPECT_EQ(6ul, result.first.getNumberOfAutomata());
569 EXPECT_TRUE(result.first.getAutomaton("Switch").hasVariable("id"));
570 EXPECT_TRUE(result.first.getAutomaton("Switch_1").hasVariable("id"));
571 EXPECT_TRUE(result.first.getAutomaton("Workstation").hasVariable("id"));
572 EXPECT_TRUE(result.first.getAutomaton("Workstation_1").hasVariable("id"));
573 EXPECT_TRUE(result.first.getAutomaton(1).hasVariable("id"));
574}
575
576TEST(JaniParser, DieArrayNestedExampleTest) {
577 std::pair<storm::jani::Model, std::vector<storm::jani::Property>> result;
578 EXPECT_NO_THROW(result = storm::api::parseJaniModel(STORM_TEST_RESOURCES_DIR "/dtmc/die_array_nested.jani"));
579 EXPECT_EQ(storm::jani::ModelType::DTMC, result.first.getModelType());
580 EXPECT_TRUE(result.first.containsArrayVariables());
581 EXPECT_TRUE(result.first.hasGlobalVariable("sd"));
582 EXPECT_EQ(1ul, result.first.getNumberOfAutomata());
583}
584
585TEST(JaniParser, UnassignedVariablesTest) {
586 std::pair<storm::jani::Model, std::vector<storm::jani::Property>> result;
587 EXPECT_NO_THROW(result = storm::api::parseJaniModel(STORM_TEST_RESOURCES_DIR "/mdp/unassigned-variables.jani"));
588 EXPECT_EQ(storm::jani::ModelType::MDP, result.first.getModelType());
589 EXPECT_TRUE(result.first.hasConstant("c"));
590 EXPECT_EQ(2ul, result.first.getNumberOfAutomata());
591}
592
593TEST(JaniParser, TrigonometryAndTranscendentalNumbersTest) {
594 std::pair<storm::jani::Model, std::vector<storm::jani::Property>> result;
595 EXPECT_NO_THROW(result = storm::api::parseJaniModel(STORM_TEST_RESOURCES_DIR "/dtmc/test_trigonometry.jani"));
596 auto& model = result.first;
597 auto& properties = result.second;
598 EXPECT_EQ(storm::jani::ModelType::DTMC, model.getModelType());
599 EXPECT_EQ(model.getNumberOfAutomata(), 1U);
600 EXPECT_EQ(properties.size(), 2U);
601 EXPECT_NO_THROW(model.substitute({}, true));
602}
603
604TEST(JaniParser, MultiobjectiveTest) {
605 std::pair<storm::jani::Model, std::vector<storm::jani::Property>> result;
606 EXPECT_NO_THROW(result = storm::api::parseJaniModel(STORM_TEST_RESOURCES_DIR "/mdp/multiobj_consensus2_3_2.jani"));
607 auto& model = result.first;
608 EXPECT_EQ(storm::jani::ModelType::MDP, model.getModelType());
609 auto& properties = result.second;
610 ASSERT_EQ(properties.size(), 6U);
611 for (size_t i = 0; i < properties.size(); ++i) {
612 auto const& f = properties[i].getRawFormula();
613 ASSERT_TRUE(f->isMultiObjectiveFormula()) << "Property #" << i << ": " << *f;
614 // First three formulas are tradeoff, last three are lexicographic
615 EXPECT_EQ(i < 3, f->asMultiObjectiveFormula().isTradeoff()) << "Property #" << i << ": " << *f;
616 EXPECT_EQ(i >= 3, f->asMultiObjectiveFormula().isLexicographic()) << "Property #" << i << ": " << *f;
617 // Formulas #0 and #3 have Boolean results
618 EXPECT_EQ(i == 0 || i == 3, f->asMultiObjectiveFormula().hasQualitativeResult()) << "Property #" << i << ": " << *f;
619 // Formulas #2 and #5 have multi-dimensional results
620 EXPECT_EQ(i == 2 || i == 5, f->asMultiObjectiveFormula().hasMultiDimensionalResult()) << "Property #" << i << ": " << *f;
621 }
622}
TEST
TEST(JaniParser, DieExampleTest)
Definition JaniParserTest.cpp:12
model_descriptions.h
storm::api::parseJaniModel
std::pair< storm::jani::Model, std::vector< storm::jani::Property > > parseJaniModel(std::string const &filename, boost::optional< std::vector< std::string > > const &propertyFilter)
Definition model_descriptions.cpp:49
storm::api::parseJaniModelFromString
std::pair< storm::jani::Model, std::vector< storm::jani::Property > > parseJaniModelFromString(std::string const &jsonstring, boost::optional< std::vector< std::string > > const &propertyFilter)
Definition model_descriptions.cpp:58
storm_gtest.h