Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
PrismParserTest.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/PrismParser.h"
5#include "storm/exceptions/InvalidArgumentException.h"
6#include "storm/exceptions/WrongFormatException.h"
7
8TEST(PrismParser, StandardModelTest) {
9 storm::prism::Program result;
10 EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2.nm"));
11 EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds5_5.pm"));
12 EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2_2.nm"));
13 EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"));
14 EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/firewire.nm"));
15 EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm"));
16 EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader3_5.pm"));
17 EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"));
18 EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0_collide.nm"));
19}
20
21TEST(PrismParser, SimpleTest) {
22 std::string testInput =
23 R"(dtmc
24 module mod1
25 b : bool;
26 [a] true -> 1: (b'=true != false = b => false);
27 endmodule)";
28
29 storm::prism::Program result;
30 EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"));
31 EXPECT_EQ(1ul, result.getNumberOfModules());
32 EXPECT_EQ(storm::prism::Program::ModelType::DTMC, result.getModelType());
33 EXPECT_FALSE(result.hasUnboundedVariables());
34
35 testInput =
36 R"(mdp
37
38 module main
39 x : [1..5] init 1;
40 [] x=1 -> 1:(x'=2);
41 [] x=2 -> 1:(x'=3);
42 [] x=3 -> 1:(x'=1);
43 [] x=3 -> 1:(x'=4);
44 [] x=4 -> 1:(x'=5);
45 [] x=5 -> 1: true;
46 endmodule)";
47 EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"));
48 EXPECT_EQ(1ul, result.getNumberOfModules());
49 EXPECT_EQ(storm::prism::Program::ModelType::MDP, result.getModelType());
50 EXPECT_FALSE(result.hasUnboundedVariables());
51}
52
53TEST(PrismParser, expressionTest) {
54 std::string testInput = R"(dtmc
55
56 module test
57 c : [0..1] init 0;
58 [] c = ceil(log(1,2)) -> (c'=1);
59 endmodule)";
60
61 storm::prism::Program result;
62 EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"));
63 EXPECT_EQ(storm::prism::Program::ModelType::DTMC, result.getModelType());
64 EXPECT_FALSE(result.hasUnboundedVariables());
65 EXPECT_EQ(1ul, result.getNumberOfModules());
66 ASSERT_TRUE(result.hasModule("test"));
67 EXPECT_EQ(1ul, result.getModule("test").getNumberOfCommands());
68 auto const& guard = result.getModule("test").getCommands().front().getGuardExpression().getBaseExpression();
69 ASSERT_TRUE(guard.isBinaryRelationExpression());
70 EXPECT_EQ(0ll, guard.asBinaryRelationExpression().getSecondOperand()->evaluateAsInt());
71}
72
73TEST(PrismParser, FormulaOrderTest) {
74 // Regression test for #313: a boolean formula referencing an int-typed formula declared afterwards
75 // must not raise a spurious type error while resolving the formula dependency order.
76 std::string testInput =
77 R"(mdp
78
79 formula leader_set = ((A_mark & A_leader = current_min_leader_calc | A_mark = false)?true:false) & ((B_mark & B_leader = current_min_leader_calc | B_mark = false)?true:false);
80
81 formula current_min_leader_calc = min((A_mark?A_leader:8), (B_mark?B_leader:8));
82
83 module whatever
84 A_mark : bool init true;
85 B_mark : bool init true;
86
87 test1 : bool init false;
88
89 A_leader : [0..10] init 1;
90 B_leader : [0..10] init 1;
91
92 [] A_mark = true & leader_set & test1 = false -> (test1'=true);
93 endmodule)";
94
95 storm::prism::Program result;
96 EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"));
97 ASSERT_TRUE(result.hasModule("whatever"));
98 EXPECT_EQ(1ul, result.getModule("whatever").getNumberOfCommands());
99}
100
101TEST(PrismParser, NonReservedPlayerKeywordTest) {
102 // Regression test for #335: "player"/"endplayer" are only reserved for SMGs.
103 std::string testInput =
104 R"(mdp
105
106 module test
107 player : [0..5] init 0;
108 [] player < 5 -> (player'=player+1);
109 endmodule)";
110
111 storm::prism::Program result;
112 EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"));
113 ASSERT_TRUE(result.hasModule("test"));
114 ASSERT_EQ(1ul, result.getModule("test").getNumberOfIntegerVariables());
115 EXPECT_EQ("player", result.getModule("test").getIntegerVariables().front().getName());
116}
117
118TEST(PrismParser, NonReservedInvariantKeywordTest) {
119 // Regression test for #955 review feedback: "invariant"/"endinvariant" are only reserved for PTAs.
120 std::string testInput =
121 R"(mdp
122
123 module test
124 invariant : [0..5] init 0;
125 [] invariant < 5 -> (invariant'=invariant+1);
126 endmodule)";
127
128 storm::prism::Program result;
129 EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"));
130 ASSERT_TRUE(result.hasModule("test"));
131 ASSERT_EQ(1ul, result.getModule("test").getNumberOfIntegerVariables());
132 EXPECT_EQ("invariant", result.getModule("test").getIntegerVariables().front().getName());
133}
134
135TEST(PrismParser, ComplexTest) {
136 std::string testInput =
137 R"(ma
138
139 const int a;
140 const int b = 10;
141 const bool c;
142 const bool d = true | false;
143 const double e;
144 const double f = 9;
145
146 formula test = a >= 10 & (max(a,b) > floor(e));
147 formula test2 = a+b;
148 formula test3 = (a + b > 10 ? floor(e) : h) + a;
149
150 global g : bool init false;
151 global h : [0 .. b];
152
153 module mod1
154 i : bool;
155 j : bool init c;
156 k : [125..a] init a;
157
158 [a] test&false -> (i'=true)&(k'=1+1) + 1 : (k'=floor(e) + max(k, b) - 1 + k);
159 [b] true -> (i'=i);
160 endmodule
161
162 module mod2
163 [] (k > 3) & false & (min(a, 0) < max(h, k)) -> 1-e: (g'=(1-a) * 2 + floor(f) > 2);
164 endmodule
165
166 module mod3 = mod1 [ i = i1, j = j1, k = k1 ] endmodule
167
168 label "mal" = max(a, 10) > 0;
169
170 rewards "testrewards"
171 [a] true : a + 7;
172 max(f, a) <= 8 : 2*b;
173 endrewards
174
175 rewards "testrewards2"
176 [b] true : a + 7;
177 max(f, a) <= 8 : 2*b;
178 endrewards)";
179
180 storm::prism::Program result;
181 EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"));
182 EXPECT_EQ(storm::prism::Program::ModelType::MA, result.getModelType());
183 EXPECT_EQ(3ul, result.getNumberOfModules());
184 EXPECT_EQ(2ul, result.getNumberOfRewardModels());
185 EXPECT_EQ(1ul, result.getNumberOfLabels());
186 EXPECT_FALSE(result.hasUnboundedVariables());
187}
188
189TEST(PrismParser, UnboundedTest) {
190 std::string testInput =
191 R"(mdp
192 module main
193 b : int;
194 [a] true -> 1: (b'=b+1);
195 endmodule)";
196
197 storm::prism::Program result;
198 EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"));
199 EXPECT_EQ(1ul, result.getNumberOfModules());
200 EXPECT_EQ(storm::prism::Program::ModelType::MDP, result.getModelType());
201 EXPECT_TRUE(result.hasUnboundedVariables());
202}
203
204TEST(PrismParser, POMDPInputTest) {
205 std::string testInput =
206 R"(pomdp
207
208 observables
209 i
210 endobservables
211
212 module example
213 s : [0..4] init 0;
214 i : bool init true;
215 [] s=0 -> 0.5: (s'=1) & (i'=false) + 0.5: (s'=2) & (i'=false);
216 [] s=1 | s=2 -> 1: (s'=3) & (i'=true);
217 [r] s=1 -> 1: (s'=4) & (i'=true);
218 [r] s=2 -> 1: (s'=3) & (i'=true);
219 endmodule
220
221 )";
222
223 storm::prism::Program result;
224 EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"));
225
226 std::string testInput2 =
227 R"(pomdp
228
229 observable intermediate = s=1 | s=2;
230
231 module example
232 s : [0..4] init 0;
233 [] s=0 -> 0.5: (s'=1) + 0.5: (s'=2);
234 [l] s=1 -> 1: (s'=3);
235 [l] s=2 -> 1: (s'=4);
236 [r] s=1 -> 1: (s'=4);
237 [r] s=2 -> 1: (s'=3);
238 endmodule
239
240 )";
241
242 EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput2, "testfile"));
243
244 std::string testInput3 =
245 R"(pomdp
246
247 formula f = 1;
248
249 observables
250 i
251 endobservables
252
253 module example
254 s : [0..4] init 0;
255 i : bool init true;
256 [] s=0 -> 0.5: (s'=1) & (i'=false) + 0.5: (s'=2) & (i'=false);
257 [] s=1 | s=2 -> 1: (s'=3) & (i'=true);
258 [r] s=1 -> 1: (s'=4) & (i'=true);
259 [r] s=2 -> 1: (s'=3) & (i'=true);
260 endmodule
261
262 )";
263
264 EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput3, "testfile"));
265 ASSERT_TRUE(result.getModule(0).getBooleanVariables().size() == 1);
266 EXPECT_TRUE(result.getModule(0).getBooleanVariables().front().isObservable());
267
268 std::string testInput4 =
269 R"(pomdp
270
271 observables
272 i
273 endobservables
274
275 formula f = 1;
276
277 observables
278 s
279 endobservables
280
281 module example
282 s : [0..4] init 0;
283 i : bool init true;
284 [] s=0 -> 0.5: (s'=1) & (i'=false) + 0.5: (s'=2) & (i'=false);
285 [] s=1 | s=2 -> 1: (s'=3) & (i'=true);
286 [r] s=1 -> 1: (s'=4) & (i'=true);
287 [r] s=2 -> 1: (s'=3) & (i'=true);
288 endmodule
289
290 )";
291
292 EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput4, "testfile"), storm::exceptions::WrongFormatException);
293}
294
295TEST(PrismParser, NAryPredicates) {
296 std::string testInput =
297 R"(dtmc
298
299 module example
300 s : [0..4] init 0;
301 i : bool init true;
302 [] s=0 -> 0.5: (s'=1) & (i'=false) + 0.5: (s'=2) & (i'=false);
303 [] s=1 | s=2 -> 1: (s'=3) & (i'=true);
304 [r] s=1 -> 1: (s'=4) & (i'=true);
305 [r] s=2 -> 1: (s'=3) & (i'=true);
306 endmodule
307
308 label "test" = atMostOneOf(s=0, s=3, s=4);
309 label "test2" = exactlyOneOf(s=0, i, !i & s=3);
310 )";
311 storm::prism::Program result;
312
313 EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"));
314}
315
316TEST(PrismParser, Intervals) {
317 std::string testInput =
318 R"(dtmc
319
320 module example
321 s : [0..4] init 0;
322 i : bool init true;
323 [] s=0 -> [0.5,0.9]: (s'=1) & (i'=false) + [0.4,0.6] : (s'=2) & (i'=false);
324 [] s=1 -> 1: (s'=3) & (i'=true);
325 [] s>0 -> [i?0.3:1/s,1]: (s'=4) & (i'=true) + 0.5 : (s'=3);
326 [r] s=2 -> 1: (s'=3) & (i'=true);
327 endmodule
328 module example2 = example [ s = t, i = j ] endmodule
329
330 )";
331 storm::prism::Program result;
332
333 EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"));
334}
335
336TEST(PrismParser, IllegalInputTest) {
337 std::string testInput =
338 R"(ctmc
339
340 const int a;
341 const bool a = true;
342
343 module mod1
344 c : [0 .. 8] init 1;
345 [] c < 3 -> 2: (c' = c+1);
346 endmodule
347 )";
348
349 storm::prism::Program result;
350 STORM_SILENT_EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException);
351
352 testInput =
353 R"(dtmc
354
355 const int a;
356
357 module mod1
358 a : [0 .. 8] init 1;
359 [] a < 3 -> 1: (a' = a+1);
360 endmodule)";
361
362 STORM_SILENT_EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException);
363
364 testInput =
365 R"(dtmc
366
367 const int a = 2;
368 formula a = 41;
369
370 module mod1
371 c : [0 .. 8] init 1;
372 [] c < 3 -> 1: (c' = c+1);
373 endmodule)";
374
375 STORM_SILENT_EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException);
376
377 testInput =
378 R"(dtmc
379
380 const int a = 2;
381
382 init
383 c > 3
384 endinit
385
386 module mod1
387 c : [0 .. 8] init 1;
388 [] c < 3 -> 1: (c' = c+1);
389 endmodule
390
391 init
392 c > 3
393 endinit
394
395 )";
396
397 STORM_SILENT_EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException);
398
399 testInput =
400 R"(dtmc
401
402 module mod1
403 c : [0 .. 8] init 1;
404 [] c < 3 -> 1: (c' = c+1);
405 endmodule
406
407 module mod2
408 [] c < 3 -> 1: (c' = c+1);
409 endmodule)";
410
411 STORM_SILENT_EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException);
412
413 testInput =
414 R"(dtmc
415
416 module mod1
417 c : [0 .. 8] init 1;
418 [] c < 3 -> 1: (c' = c+1)&(c'=c-1);
419 endmodule)";
420
421 STORM_SILENT_EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException);
422
423 testInput =
424 R"(dtmc
425
426 module mod1
427 c : [0 .. 8] init 1;
428 [] c < 3 -> 1: (c' = true || false);
429 endmodule)";
430
431 STORM_SILENT_EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException);
432
433 testInput =
434 R"(dtmc
435
436 module mod1
437 c : [0 .. 8] init 1;
438 [] c + 3 -> 1: (c' = 1);
439 endmodule)";
440
441 STORM_SILENT_EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException);
442
443 testInput =
444 R"(dtmc
445
446 module mod1
447 c : [0 .. 8] init 1;
448 [] c + 3 -> 1: (c' = 1);
449 endmodule
450
451 label "test" = c + 1;
452
453 )";
454
455 STORM_SILENT_EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException);
456
457 // Regression test for #319: reserved keyword used as a variable name.
458 testInput =
459 R"(mdp
460
461 module test
462 ma : [0..5] init 0;
463 [] ma < 5 -> (ma'=ma+1);
464 endmodule)";
465
466 STORM_SILENT_EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException);
467
468 // Regression test for #335: "player" remains reserved for SMGs.
469 testInput =
470 R"(smg
471
472 module test
473 player : [0..5] init 0;
474 [] player < 5 -> (player'=player+1);
475 endmodule)";
476
477 STORM_SILENT_EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException);
478
479 // Regression test for #955 review feedback: "invariant" remains reserved for PTAs.
480 testInput =
481 R"(pta
482
483 module test
484 invariant : [0..5] init 0;
485 endmodule)";
486
487 STORM_SILENT_EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException);
488}
489
490TEST(PrismParser, IllegalSynchronizedWriteTest) {
491 STORM_SILENT_EXPECT_THROW(storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2-illegalSynchronizingWrite.nm"),
492 storm::exceptions::WrongFormatException);
493}
TEST
TEST(PrismParser, StandardModelTest)
Definition PrismParserTest.cpp:8
storm::parser::PrismParser::parseFromString
static storm::prism::Program parseFromString(std::string const &input, std::string const &filename, bool prismCompatability=false)
Parses the given input stream into the PRISM storage classes assuming it complies with the PRISM synt...
Definition PrismParser.cpp:9
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::prism::Module::getCommands
std::vector< storm::prism::Command > const & getCommands() const
Retrieves the commands of the module.
Definition Module.cpp:133
storm::prism::Module::getIntegerVariables
std::vector< storm::prism::IntegerVariable > const & getIntegerVariables() const
Retrieves the integer variables of the module.
Definition Module.cpp:74
storm::prism::Module::getBooleanVariables
std::vector< storm::prism::BooleanVariable > const & getBooleanVariables() const
Retrieves the boolean variables of the module.
Definition Module.cpp:63
storm::prism::Module::getNumberOfIntegerVariables
std::size_t getNumberOfIntegerVariables() const
Retrieves the number of integer variables in the module.
Definition Module.cpp:52
storm::prism::Module::getNumberOfCommands
std::size_t getNumberOfCommands() const
Retrieves the number of commands of this module.
Definition Module.cpp:117
storm::prism::Program::getModelType
ModelType getModelType() const
Retrieves the model type of the model.
Definition Program.cpp:243
storm::prism::Program::getNumberOfLabels
std::size_t getNumberOfLabels() const
Retrieves the number of labels in the program.
Definition Program.cpp:880
storm::prism::Program::getModule
Module const & getModule(uint_fast64_t index) const
Retrieves the module with the given index.
Definition Program.cpp:611
storm::prism::Program::getNumberOfRewardModels
std::size_t getNumberOfRewardModels() const
Retrieves the number of reward models in the program.
Definition Program.cpp:821
storm::prism::Program::hasModule
bool hasModule(std::string const &moduleName) const
Retrieves whether the program has a module with the given name.
Definition Program.cpp:615
storm::prism::Program::hasUnboundedVariables
bool hasUnboundedVariables() const
Definition Program.cpp:267
storm::prism::Program::getNumberOfModules
std::size_t getNumberOfModules() const
Retrieves the number of modules in the program.
Definition Program.cpp:607
storm_gtest.h
STORM_SILENT_EXPECT_THROW
#define STORM_SILENT_EXPECT_THROW(statement, expected_exception)
Definition storm_gtest.h:19