Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
FormulaParserTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "storm-parsers/parser/FormulaParser.h"
3#include "storm/automata/DeterministicAutomaton.h"
4#include "storm/exceptions/ExpressionEvaluationException.h"
5#include "storm/exceptions/WrongFormatException.h"
6#include "storm/logic/FragmentSpecification.h"
7#include "storm/storage/expressions/ExpressionManager.h"
8#include "test/storm_gtest.h"
9
10TEST(FormulaParserTest, LabelTest) {
11 storm::parser::FormulaParser formulaParser;
12
13 std::string input = "\"label\"";
14 std::shared_ptr<storm::logic::Formula const> formula(nullptr);
15 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
16
17 EXPECT_TRUE(formula->isAtomicLabelFormula());
18}
19
20TEST(FormulaParserTest, ComplexLabelTest) {
21 storm::parser::FormulaParser formulaParser;
22
23 std::string input = "!(\"a\" & \"b\") | \"a\" & !\"c\"";
24 std::shared_ptr<storm::logic::Formula const> formula(nullptr);
25 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
26
27 EXPECT_TRUE(formula->isInFragment(storm::logic::propositional()));
28 EXPECT_TRUE(formula->isBinaryBooleanStateFormula());
29}
30
31TEST(FormulaParserTest, ExpressionTest) {
32 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
33 manager->declareBooleanVariable("x");
34 manager->declareIntegerVariable("y");
35
36 storm::parser::FormulaParser formulaParser(manager);
37
38 std::string input = "!(x | y > 3)";
39 std::shared_ptr<storm::logic::Formula const> formula(nullptr);
40 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
41
42 EXPECT_TRUE(formula->isInFragment(storm::logic::propositional()));
43 EXPECT_TRUE(formula->isAtomicExpressionFormula());
44}
45
46TEST(FormulaParserTest, ExpressionTest2) {
47 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
48
49 storm::parser::FormulaParser formulaParser(manager);
50
51 std::string input = "(false)=false";
52 std::shared_ptr<storm::logic::Formula const> formula(nullptr);
53 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
54
55 EXPECT_TRUE(formula->isInFragment(storm::logic::propositional()));
56 EXPECT_TRUE(formula->isAtomicExpressionFormula());
57}
58
59TEST(FormulaParserTest, ExpressionTest3) {
60 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
61
62 storm::parser::FormulaParser formulaParser(manager);
63
64 std::string input = "1 & false";
65 STORM_SILENT_ASSERT_THROW(formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
66}
67
68TEST(FormulaParserTest, LabelAndExpressionTest) {
69 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
70 manager->declareBooleanVariable("x");
71 manager->declareIntegerVariable("y");
72
73 storm::parser::FormulaParser formulaParser(manager);
74
75 std::string input = "!\"a\" | x | y > 3";
76 std::shared_ptr<storm::logic::Formula const> formula(nullptr);
77 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
78
79 EXPECT_TRUE(formula->isInFragment(storm::logic::propositional()));
80
81 input = "x | y > 3 | !\"a\"";
82 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
83 EXPECT_TRUE(formula->isInFragment(storm::logic::propositional()));
84}
85
86TEST(FormulaParserTest, ProbabilityOperatorTest) {
87 storm::parser::FormulaParser formulaParser;
88
89 std::string input = "P<0.9 [\"a\" U \"b\"]";
90 std::shared_ptr<storm::logic::Formula const> formula(nullptr);
91 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
92
93 EXPECT_TRUE(formula->isProbabilityOperatorFormula());
94 EXPECT_TRUE(formula->asProbabilityOperatorFormula().hasBound());
95 EXPECT_FALSE(formula->asProbabilityOperatorFormula().hasOptimalityType());
96}
97
98TEST(FormulaParserTest, ProbabilityOperatorTest2) {
99 storm::parser::FormulaParser formulaParser;
100
101 std::string input = "1 = 1 & 2 = 2 & true & P<0.9 [\"a\" U \"b\"]";
102 std::shared_ptr<storm::logic::Formula const> formula(nullptr);
103 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
104
105 ASSERT_TRUE(formula->isBinaryBooleanStateFormula());
106 EXPECT_TRUE(formula->asBinaryBooleanStateFormula().isAnd());
107 EXPECT_TRUE(formula->asBinaryBooleanStateFormula().getLeftSubformula().isAtomicExpressionFormula());
108 EXPECT_TRUE(formula->asBinaryBooleanStateFormula().getRightSubformula().isProbabilityOperatorFormula());
109}
110
111TEST(FormulaParserTest, UntilOperatorTest) {
112 // API does not allow direct test of until, so we have to pack it in a probability operator.
113 storm::parser::FormulaParser formulaParser;
114
115 std::string input = "P<0.9 [\"a\" U \"b\"]";
116 std::shared_ptr<storm::logic::Formula const> formula(nullptr);
117 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
118 auto const &nested1 = formula->asProbabilityOperatorFormula().getSubformula();
119 EXPECT_TRUE(nested1.isUntilFormula());
120 EXPECT_FALSE(nested1.isBoundedUntilFormula());
121
122 input = "P<0.9 [\"a\" U<=3 \"b\"]";
123 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
124 auto const &nested2 = formula->asProbabilityOperatorFormula().getSubformula();
125 EXPECT_TRUE(nested2.isBoundedUntilFormula());
126 EXPECT_TRUE(nested2.asBoundedUntilFormula().getTimeBoundReference().isTimeBound());
127 EXPECT_EQ(3, nested2.asBoundedUntilFormula().getUpperBound().evaluateAsInt());
128
129 input = "P<0.9 [\"a\" U{\"rewardname\"}<=3 \"b\"]";
130 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
131 auto const &nested3 = formula->asProbabilityOperatorFormula().getSubformula();
132 EXPECT_TRUE(nested3.isBoundedUntilFormula());
133 EXPECT_TRUE(nested3.asBoundedUntilFormula().getTimeBoundReference().isRewardBound());
134 EXPECT_TRUE(nested3.asBoundedUntilFormula().getTimeBoundReference().hasRewardModelName());
135 EXPECT_EQ("rewardname", nested3.asBoundedUntilFormula().getTimeBoundReference().getRewardName());
136 EXPECT_EQ(3, nested3.asBoundedUntilFormula().getUpperBound().evaluateAsInt());
137
138 input = "P<0.9 [\"a\" Urew{\"rewardname\"}<=3 \"b\"]";
139 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
140 auto const &nested4 = formula->asProbabilityOperatorFormula().getSubformula();
141 EXPECT_TRUE(nested4.isBoundedUntilFormula());
142 EXPECT_TRUE(nested4.asBoundedUntilFormula().getTimeBoundReference().isRewardBound());
143 EXPECT_TRUE(nested4.asBoundedUntilFormula().getTimeBoundReference().hasRewardModelName());
144 EXPECT_EQ("rewardname", nested4.asBoundedUntilFormula().getTimeBoundReference().getRewardName());
145 EXPECT_EQ(3, nested4.asBoundedUntilFormula().getUpperBound().evaluateAsInt());
146
147 input = "P<0.9 [\"a\" Urew<=3 \"b\"]";
148 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
149 auto const &nested5 = formula->asProbabilityOperatorFormula().getSubformula();
150 EXPECT_TRUE(nested5.isBoundedUntilFormula());
151 EXPECT_TRUE(nested5.asBoundedUntilFormula().getTimeBoundReference().isRewardBound());
152 EXPECT_FALSE(nested5.asBoundedUntilFormula().getTimeBoundReference().hasRewardModelName());
153 EXPECT_EQ(3, nested5.asBoundedUntilFormula().getUpperBound().evaluateAsInt());
154}
155
156TEST(FormulaParserTest, RewardOperatorTest) {
157 storm::parser::FormulaParser formulaParser;
158
159 std::string input = "Rmin<0.9 [F \"a\"]";
160 std::shared_ptr<storm::logic::Formula const> formula(nullptr);
161 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
162
163 EXPECT_TRUE(formula->isRewardOperatorFormula());
164 EXPECT_TRUE(formula->asRewardOperatorFormula().hasBound());
165 EXPECT_TRUE(formula->asRewardOperatorFormula().hasOptimalityType());
166
167 input = "R=? [I=10]";
168 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
169
170 EXPECT_TRUE(formula->isRewardOperatorFormula());
171 EXPECT_FALSE(formula->asRewardOperatorFormula().hasBound());
172 EXPECT_FALSE(formula->asRewardOperatorFormula().hasOptimalityType());
173 EXPECT_TRUE(formula->asRewardOperatorFormula().getSubformula().isInstantaneousRewardFormula());
174}
175
176TEST(FormulaParserTest, ConditionalProbabilityTest) {
177 storm::parser::FormulaParser formulaParser;
178
179 std::string input = "P<0.9 [F \"a\" || F \"b\"]";
180 std::shared_ptr<storm::logic::Formula const> formula(nullptr);
181 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
182
183 EXPECT_TRUE(formula->isProbabilityOperatorFormula());
184 storm::logic::ProbabilityOperatorFormula const &probFormula = formula->asProbabilityOperatorFormula();
185 EXPECT_TRUE(probFormula.getSubformula().isConditionalProbabilityFormula());
186}
187
188TEST(FormulaParserTest, NestedPathFormulaTest) {
189 storm::parser::FormulaParser formulaParser;
190
191 std::string input = "P<0.9 [F X \"a\"]";
192 std::shared_ptr<storm::logic::Formula const> formula(nullptr);
193 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
194
195 EXPECT_TRUE(formula->isProbabilityOperatorFormula());
196 ASSERT_TRUE(formula->asProbabilityOperatorFormula().getSubformula().isEventuallyFormula());
197 ASSERT_TRUE(formula->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isNextFormula());
198}
199
200TEST(FormulaParserTest, CommentTest) {
201 storm::parser::FormulaParser formulaParser;
202
203 std::string input =
204 "// This is a comment. And this is a commented out formula: P<=0.5 [ F \"a\" ] The next line contains the actual formula. \n P<=0.5 [ X \"b\" ] // "
205 "Another comment \n // And again: another comment.";
206 std::shared_ptr<storm::logic::Formula const> formula(nullptr);
207 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
208 EXPECT_TRUE(formula->isProbabilityOperatorFormula());
209 ASSERT_TRUE(formula->asProbabilityOperatorFormula().getSubformula().isNextFormula());
210 ASSERT_TRUE(formula->asProbabilityOperatorFormula().getSubformula().asNextFormula().getSubformula().isAtomicLabelFormula());
211}
212
213TEST(FormulaParserTest, WrongFormatTest) {
214 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
215 manager->declareBooleanVariable("x");
216 manager->declareIntegerVariable("y");
217
218 storm::parser::FormulaParser formulaParser(manager);
219 std::string input = "P>0.5 [ a ]";
220 std::shared_ptr<storm::logic::Formula const> formula(nullptr);
221 STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
222
223 input = "P=0.5 [F \"a\"]";
224 STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
225
226 input = "P>0.5 [F !(x = 0)]";
227 STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
228
229 input = "P>0.5 [F !y]";
230 STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
231
232 input = "P>0.5 [F y!=0)]";
233 STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
234
235 input = "P<0.9 [G F]";
236 STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
237
238 input = "P<0.9 [\"a\" U \"b\" U \"c\"]";
239 STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
240
241 input = "P<0.9 [X \"a\" U G \"b\" U X \"c\"]";
242 STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
243}
244
245TEST(FormulaParserTest, MultiObjectiveFormulaTest) {
246 storm::parser::FormulaParser formulaParser;
247
248 std::string input = "multi(P<0.9 [ F \"a\" ], R<42 [ F \"b\" ], Pmin=? [ F\"c\" ])";
249 std::shared_ptr<storm::logic::Formula const> formula;
250 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
251 ASSERT_TRUE(formula->isMultiObjectiveFormula());
252 storm::logic::MultiObjectiveFormula mof = formula->asMultiObjectiveFormula();
253 ASSERT_EQ(3ull, mof.getNumberOfSubformulas());
254
255 ASSERT_TRUE(mof.getSubformula(0).isProbabilityOperatorFormula());
256 ASSERT_TRUE(mof.getSubformula(0).asProbabilityOperatorFormula().getSubformula().isEventuallyFormula());
257 ASSERT_TRUE(mof.getSubformula(0).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isAtomicLabelFormula());
258 ASSERT_TRUE(mof.getSubformula(0).asProbabilityOperatorFormula().hasBound());
259
260 ASSERT_TRUE(mof.getSubformula(1).isRewardOperatorFormula());
261 ASSERT_TRUE(mof.getSubformula(1).asRewardOperatorFormula().getSubformula().isEventuallyFormula());
262 ASSERT_TRUE(mof.getSubformula(1).asRewardOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isAtomicLabelFormula());
263 ASSERT_TRUE(mof.getSubformula(1).asRewardOperatorFormula().hasBound());
264
265 ASSERT_TRUE(mof.getSubformula(2).isProbabilityOperatorFormula());
266 ASSERT_TRUE(mof.getSubformula(2).asProbabilityOperatorFormula().getSubformula().isEventuallyFormula());
267 ASSERT_TRUE(mof.getSubformula(2).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isAtomicLabelFormula());
268 ASSERT_TRUE(mof.getSubformula(2).asProbabilityOperatorFormula().hasOptimalityType());
269 ASSERT_TRUE(storm::solver::minimize(mof.getSubformula(2).asProbabilityOperatorFormula().getOptimalityType()));
270}
271
272TEST(FormulaParserTest, LogicalPrecedenceTest) {
273 // Test precedence of logical operators over temporal operators, etc.
274 storm::parser::FormulaParser formulaParser;
275 std::shared_ptr<storm::logic::Formula const> formula(nullptr);
276
277 std::string input = "P=? [ !\"a\" & \"b\" U ! \"c\" | \"b\" ]";
278 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
279 EXPECT_TRUE(formula->isProbabilityOperatorFormula());
280
281 auto const &nested1 = formula->asProbabilityOperatorFormula().getSubformula();
282 EXPECT_TRUE(nested1.isUntilFormula());
283 ASSERT_TRUE(nested1.asUntilFormula().getLeftSubformula().isBinaryBooleanStateFormula());
284 ASSERT_TRUE(nested1.asUntilFormula().getLeftSubformula().asBinaryBooleanStateFormula().getLeftSubformula().isUnaryBooleanStateFormula());
285 ASSERT_TRUE(nested1.asUntilFormula().getRightSubformula().isBinaryBooleanStateFormula());
286 ASSERT_TRUE(nested1.asUntilFormula().getRightSubformula().asBinaryBooleanStateFormula().getLeftSubformula().isUnaryBooleanStateFormula());
287
288 input = "P<0.9 [ F G !\"a\" | \"b\" ] ";
289 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
290 auto const &nested2 = formula->asProbabilityOperatorFormula().getSubformula();
291 EXPECT_TRUE(nested2.asEventuallyFormula().getSubformula().isGloballyFormula());
292 auto const &nested2Subformula = nested2.asEventuallyFormula().getSubformula().asGloballyFormula();
293 EXPECT_TRUE(nested2Subformula.getSubformula().isBinaryBooleanStateFormula());
294 ASSERT_TRUE(nested2Subformula.getSubformula().asBinaryBooleanStateFormula().getLeftSubformula().isUnaryBooleanStateFormula());
295
296 input = "P<0.9 [ X G \"a\" | !\"b\" | \"c\"] "; // from left to right
297 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
298 auto const &nested3 = formula->asProbabilityOperatorFormula().getSubformula();
299 EXPECT_TRUE(nested3.asNextFormula().getSubformula().isGloballyFormula());
300 EXPECT_TRUE(nested3.asNextFormula().getSubformula().asGloballyFormula().getSubformula().isBinaryBooleanStateFormula());
301 auto const &nested3Subformula = nested3.asNextFormula().getSubformula().asGloballyFormula().getSubformula().asBinaryBooleanStateFormula();
302 ASSERT_TRUE(nested3Subformula.getLeftSubformula().isBinaryBooleanStateFormula());
303 ASSERT_TRUE(nested3Subformula.asBinaryBooleanStateFormula().getRightSubformula().isAtomicLabelFormula());
304
305 input = "P<0.9 [ X F \"a\" | ! \"b\" & \"c\"] "; // & has precedence over | and ! over &
306 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
307 auto const &nested4 = formula->asProbabilityOperatorFormula().getSubformula();
308 EXPECT_TRUE(nested4.asNextFormula().getSubformula().isEventuallyFormula());
309 EXPECT_TRUE(nested4.asNextFormula().getSubformula().asEventuallyFormula().getSubformula().isBinaryBooleanStateFormula());
310 auto const &nested4Subformula = nested4.asNextFormula().getSubformula().asEventuallyFormula().getSubformula().asBinaryBooleanStateFormula();
311 ASSERT_TRUE(nested4Subformula.getLeftSubformula().isAtomicLabelFormula());
312 ASSERT_TRUE(nested4Subformula.getRightSubformula().isBinaryBooleanStateFormula());
313
314 input = "P<0.9 [X \"a\" | F \"b\"]"; // X (a | F b)
315 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
316 auto const &nested5 = formula->asProbabilityOperatorFormula().getSubformula();
317 EXPECT_TRUE(nested5.isNextFormula());
318 EXPECT_TRUE(nested5.asNextFormula().getSubformula().isBinaryBooleanPathFormula());
319 EXPECT_TRUE(nested5.asNextFormula().getSubformula().asBinaryPathFormula().getLeftSubformula().isAtomicLabelFormula());
320 EXPECT_TRUE(nested5.asNextFormula().getSubformula().asBinaryPathFormula().getRightSubformula().isEventuallyFormula());
321
322 input = "P<0.9 [F \"a\" | G \"b\" | X \"c\" ]"; // F (a | G (b | X c))
323 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
324 auto const &nested6 = formula->asProbabilityOperatorFormula().getSubformula();
325 EXPECT_TRUE(nested6.isEventuallyFormula());
326 EXPECT_TRUE(nested6.asEventuallyFormula().getSubformula().isBinaryBooleanPathFormula());
327 EXPECT_TRUE(nested6.asEventuallyFormula().getSubformula().asBinaryPathFormula().getLeftSubformula().isAtomicLabelFormula());
328 EXPECT_TRUE(nested6.asEventuallyFormula().getSubformula().asBinaryPathFormula().getRightSubformula().isGloballyFormula());
329 auto const &nested6Subformula = nested6.asEventuallyFormula().getSubformula().asBinaryPathFormula().getRightSubformula().asGloballyFormula();
330 EXPECT_TRUE(nested6Subformula.getSubformula().isBinaryBooleanPathFormula());
331 EXPECT_TRUE(nested6Subformula.getSubformula().asBinaryPathFormula().getLeftSubformula().isAtomicLabelFormula());
332 EXPECT_TRUE(nested6Subformula.getSubformula().asBinaryPathFormula().getRightSubformula().isNextFormula());
333 EXPECT_TRUE(nested6Subformula.getSubformula().asBinaryPathFormula().getRightSubformula().asNextFormula().getSubformula().isAtomicLabelFormula());
334}
335
336TEST(FormulaParserTest, TemporalPrecedenceTest) {
337 // Unary operators (F, G and X) have precedence over binary operators (U).
338 storm::parser::FormulaParser formulaParser;
339 std::shared_ptr<storm::logic::Formula const> formula(nullptr);
340
341 std::string input = "P=? [ F \"a\" U G \"b\" ]"; // (F a) U (G b)
342 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
343 auto const &nested1 = formula->asProbabilityOperatorFormula().getSubformula();
344 EXPECT_TRUE(nested1.isUntilFormula());
345 ASSERT_TRUE(nested1.asUntilFormula().getLeftSubformula().isEventuallyFormula());
346 ASSERT_TRUE(nested1.asUntilFormula().getRightSubformula().isGloballyFormula());
347
348 input = "P=? [ X ( F \"a\" U G \"b\") U G \"c\"]"; // X((F a) U (G b)) U (G c)
349 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
350 auto const &nested2 = formula->asProbabilityOperatorFormula().getSubformula();
351 EXPECT_TRUE(nested2.isUntilFormula());
352 EXPECT_TRUE(nested2.asUntilFormula().getLeftSubformula().isNextFormula());
353 EXPECT_TRUE(nested2.asUntilFormula().getLeftSubformula().asNextFormula().getSubformula().isUntilFormula());
354 EXPECT_TRUE(nested2.asUntilFormula().getRightSubformula().isGloballyFormula());
355
356 input = "P=? [ X F \"a\" U (G \"b\" U G \"c\")]"; // (XF a) U ((G b) U (G c))
357 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
358 auto const &nested3 = formula->asProbabilityOperatorFormula().getSubformula();
359 EXPECT_TRUE(nested3.isUntilFormula());
360 EXPECT_TRUE(nested3.asUntilFormula().getLeftSubformula().isNextFormula());
361 EXPECT_TRUE(nested3.asUntilFormula().getLeftSubformula().asNextFormula().getSubformula().isEventuallyFormula());
362 EXPECT_TRUE(nested3.asUntilFormula().getRightSubformula().isUntilFormula());
363 EXPECT_TRUE(nested3.asUntilFormula().getRightSubformula().asUntilFormula().getLeftSubformula().isGloballyFormula());
364 EXPECT_TRUE(nested3.asUntilFormula().getRightSubformula().asUntilFormula().getRightSubformula().isGloballyFormula());
365}
366
367TEST(FormulaParserTest, TemporalNegationTest) {
368 storm::parser::FormulaParser formulaParser;
369 std::shared_ptr<storm::logic::Formula const> formula(nullptr);
370
371 std::string input = "P<0.9 [ ! X \"a\" | \"b\"]";
372 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
373 auto const &nested1 = formula->asProbabilityOperatorFormula().getSubformula();
374 EXPECT_TRUE(nested1.isUnaryBooleanPathFormula());
375 EXPECT_TRUE(nested1.asUnaryPathFormula().getSubformula().isNextFormula());
376 EXPECT_TRUE(nested1.asUnaryPathFormula().getSubformula().asNextFormula().getSubformula().isBinaryBooleanStateFormula());
377
378 input = "P<0.9 [! F ! G \"b\"]";
379 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
380 auto const &nested2 = formula->asProbabilityOperatorFormula().getSubformula();
381 EXPECT_TRUE(nested2.isUnaryBooleanPathFormula());
382 EXPECT_TRUE(nested2.asUnaryPathFormula().getSubformula().isEventuallyFormula());
383 EXPECT_TRUE(nested2.asUnaryPathFormula().getSubformula().asEventuallyFormula().getSubformula().isUnaryBooleanPathFormula());
384 EXPECT_TRUE(nested2.asUnaryPathFormula().getSubformula().asEventuallyFormula().getSubformula().asUnaryPathFormula().getSubformula().isGloballyFormula());
385
386 input = "P<0.9 [! (\"a\" U \"b\")]";
387 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
388 auto const &nested3 = formula->asProbabilityOperatorFormula().getSubformula();
389 EXPECT_TRUE(nested3.isUnaryBooleanPathFormula());
390 EXPECT_TRUE(nested3.asUnaryPathFormula().getSubformula().isUntilFormula());
391}
392
393TEST(FormulaParserTest, ComplexPathFormulaTest) {
394 storm::parser::FormulaParser formulaParser;
395 std::shared_ptr<storm::logic::Formula const> formula(nullptr);
396
397 std::string input = "P<0.9 [(X !\"a\") & (F ( X \"b\" U G \"c\" & \"d\"))]"; // ((X ! a) & (F ( (X b) U (G (c & d)))))
398 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
399 auto const &nested1 = formula->asProbabilityOperatorFormula().getSubformula();
400 EXPECT_TRUE(nested1.asBinaryPathFormula().getRightSubformula().asEventuallyFormula().getSubformula().isUntilFormula());
401 auto const nested1Subformula = nested1.asBinaryPathFormula().getRightSubformula().asEventuallyFormula().getSubformula().asUntilFormula();
402 EXPECT_TRUE(nested1Subformula.getLeftSubformula().isNextFormula());
403 EXPECT_TRUE(nested1Subformula.getRightSubformula().asGloballyFormula().getSubformula().isBinaryBooleanStateFormula());
404
405 input = "P<0.9 [(F \"a\") & (G \"b\") | (! \"a\" U (F X ! \"b\"))]";
406 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
407 auto const &nested2 = formula->asProbabilityOperatorFormula().getSubformula();
408 ASSERT_TRUE(nested2.asBinaryPathFormula().getLeftSubformula().isBinaryPathFormula());
409 ASSERT_TRUE(nested2.asBinaryPathFormula().getRightSubformula().isUntilFormula());
410
411 input = "P=? [(X \"a\") U ( \"b\"& \"c\")]";
412 formula = formulaParser.parseSingleFormulaFromString(input);
413 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
414 auto const &nested3 = formula->asProbabilityOperatorFormula().getSubformula();
415 EXPECT_TRUE(nested3.asBinaryPathFormula().isUntilFormula());
416 EXPECT_TRUE(nested3.asBinaryPathFormula().getLeftSubformula().isNextFormula());
417}
418
419TEST(FormulaParserTest, HOAPathFormulaTest) {
420 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
421 manager->declareIntegerVariable("x");
422 manager->declareIntegerVariable("y");
423 storm::parser::FormulaParser formulaParser(manager);
424 std::shared_ptr<storm::logic::Formula const> formula(nullptr);
425
426 std::string input = "P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> !\"a\", \"p1\" -> \"b\" | \"c\" }]";
427 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
428 auto const &nested1 = formula->asProbabilityOperatorFormula().getSubformula();
429 EXPECT_TRUE(nested1.isHOAPathFormula());
430 EXPECT_TRUE(nested1.isPathFormula());
431
432 ASSERT_NO_THROW(std::string af = nested1.asHOAPathFormula().getAutomatonFile());
433 storm::automata::DeterministicAutomaton::ptr da1;
434 ASSERT_NO_THROW(da1 = nested1.asHOAPathFormula().readAutomaton());
435 EXPECT_EQ(3ul, da1->getNumberOfStates());
436 EXPECT_EQ(4ul, da1->getNumberOfEdgesPerState());
437
438 std::map<std::string, std::shared_ptr<storm::logic::Formula const>> apFormulaMap1 = nested1.asHOAPathFormula().getAPMapping();
439 EXPECT_TRUE(apFormulaMap1["p0"]->isUnaryBooleanStateFormula());
440 EXPECT_TRUE(apFormulaMap1["p1"]->isBinaryBooleanStateFormula());
441
442 input = "P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_UXp0p1.hoa\", \"p0\" -> (x < 7) & !(y = 2), \"p1\" -> (x > 0) }]";
443 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
444 auto const &nested2 = formula->asProbabilityOperatorFormula().getSubformula();
445 EXPECT_TRUE(nested2.isHOAPathFormula());
446 EXPECT_TRUE(nested2.isPathFormula());
447
448 ASSERT_NO_THROW(std::string af = nested2.asHOAPathFormula().getAutomatonFile());
449 storm::automata::DeterministicAutomaton::ptr da2;
450 ASSERT_NO_THROW(da2 = nested2.asHOAPathFormula().readAutomaton());
451 EXPECT_EQ(4ul, da2->getNumberOfStates());
452 EXPECT_EQ(4ul, da2->getNumberOfEdgesPerState());
453
454 std::map<std::string, std::shared_ptr<storm::logic::Formula const>> apFormulaMap2 = nested2.asHOAPathFormula().getAPMapping();
455 EXPECT_TRUE(apFormulaMap2["p0"]->isAtomicExpressionFormula());
456 EXPECT_TRUE(apFormulaMap2["p1"]->isAtomicExpressionFormula());
457
458 // Wrong format: p1 -> path formula
459 input = "P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_UXp0p1.hoa\", \"p0\" -> (x > 0), \"p1\" -> (x < 7) & (X y = 2) }]";
460 STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
461
462 // Exception: p1 not assigned
463 input = "P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_UXp0p1.hoa\", \"p0\" -> (x > 0)}]";
464 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
465 auto const &nested3 = formula->asProbabilityOperatorFormula().getSubformula();
466 storm::automata::DeterministicAutomaton::ptr da3;
467 STORM_SILENT_EXPECT_THROW(da3 = nested3.asHOAPathFormula().readAutomaton(), storm::exceptions::ExpressionEvaluationException);
468}
TEST
TEST(FormulaParserTest, LabelTest)
Definition FormulaParserTest.cpp:10
storm::automata::DeterministicAutomaton::ptr
std::shared_ptr< DeterministicAutomaton > ptr
Definition DeterministicAutomaton.h:14
storm::expressions::ExpressionManager
This class is responsible for managing a set of typed variables and all expressions using these varia...
Definition ExpressionManager.h:72
storm::logic::Formula::asRewardOperatorFormula
RewardOperatorFormula & asRewardOperatorFormula()
Definition Formula.cpp:461
storm::logic::Formula::isProbabilityOperatorFormula
virtual bool isProbabilityOperatorFormula() const
Definition Formula.cpp:172
storm::logic::Formula::asProbabilityOperatorFormula
ProbabilityOperatorFormula & asProbabilityOperatorFormula()
Definition Formula.cpp:453
storm::logic::Formula::isRewardOperatorFormula
virtual bool isRewardOperatorFormula() const
Definition Formula.cpp:176
storm::logic::Formula::asEventuallyFormula
EventuallyFormula & asEventuallyFormula()
Definition Formula.cpp:333
storm::logic::Formula::isEventuallyFormula
virtual bool isEventuallyFormula() const
Definition Formula.cpp:88
storm::logic::Formula::asMultiObjectiveFormula
MultiObjectiveFormula & asMultiObjectiveFormula()
Definition Formula.cpp:229
storm::logic::Formula::isConditionalProbabilityFormula
virtual bool isConditionalProbabilityFormula() const
Definition Formula.cpp:112
storm::logic::Formula::isAtomicLabelFormula
virtual bool isAtomicLabelFormula() const
Definition Formula.cpp:76
storm::logic::MultiObjectiveFormula::getSubformula
Formula const & getSubformula(uint_fast64_t index) const
Definition MultiObjectiveFormula.cpp:54
storm::logic::OperatorFormula::getOptimalityType
storm::solver::OptimizationDirection const & getOptimalityType() const
Definition OperatorFormula.cpp:79
storm::logic::UnaryPathFormula::getSubformula
Formula const & getSubformula() const
Definition UnaryPathFormula.cpp:13
storm::logic::UnaryStateFormula::getSubformula
Formula const & getSubformula() const
Definition UnaryStateFormula.cpp:15
storm::parser::FormulaParser::parseSingleFormulaFromString
std::shared_ptr< storm::logic::Formula const > parseSingleFormulaFromString(std::string const &formulaString) const
Parses the formula given by the provided string.
Definition FormulaParser.cpp:55
storm::logic::propositional
FragmentSpecification propositional()
Definition FragmentSpecification.cpp:9
storm::solver::minimize
bool constexpr minimize(OptimizationDirection d)
Definition OptimizationDirection.h:10
storm_gtest.h
STORM_SILENT_EXPECT_THROW
#define STORM_SILENT_EXPECT_THROW(statement, expected_exception)
Definition storm_gtest.h:104
STORM_SILENT_ASSERT_THROW
#define STORM_SILENT_ASSERT_THROW(statement, expected_exception)
Definition storm_gtest.h:99