Storm 1.11.1.1
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, DiscountedFormulaTest) {
201 storm::parser::FormulaParser formulaParser;
202
203 std::string input = "Rmax=? [Cdiscount=0.9]";
204 std::shared_ptr<storm::logic::Formula const> formula(nullptr);
205
206 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
207
208 EXPECT_TRUE(formula->isRewardOperatorFormula());
209 ASSERT_TRUE(formula->asRewardOperatorFormula().getSubformula().isDiscountedTotalRewardFormula());
210 ASSERT_FALSE(formula->asRewardOperatorFormula().getSubformula().isTotalRewardFormula());
211 static const std::string discountFactorString1 = "9/10";
212 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(discountFactorString1),
213 formula->asRewardOperatorFormula().getSubformula().asDiscountedTotalRewardFormula().getDiscountFactor<storm::RationalNumber>());
214 EXPECT_FLOAT_EQ(0.9, formula->asRewardOperatorFormula().getSubformula().asDiscountedTotalRewardFormula().getDiscountFactor<double>());
215
216 input = "Rmin=? [C<=5discount=(0.95)]";
217
218 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
219
220 EXPECT_TRUE(formula->isRewardOperatorFormula());
221 ASSERT_TRUE(formula->asRewardOperatorFormula().getSubformula().isDiscountedCumulativeRewardFormula());
222 static const std::string discountFactorString2 = "19/20";
223 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(discountFactorString2),
224 formula->asRewardOperatorFormula().getSubformula().asDiscountedCumulativeRewardFormula().getDiscountFactor().evaluateAsRational());
225 EXPECT_FLOAT_EQ(0.95, formula->asRewardOperatorFormula().getSubformula().asDiscountedCumulativeRewardFormula().getDiscountFactor().evaluateAsDouble());
226 EXPECT_TRUE(formula->asRewardOperatorFormula().getSubformula().asDiscountedCumulativeRewardFormula().getTimeBoundReference().isTimeBound());
227 EXPECT_EQ(5, formula->asRewardOperatorFormula().getSubformula().asDiscountedCumulativeRewardFormula().getBound().evaluateAsInt());
228
229 input = "Rmax=? [Crew<8discount=(0.5)]";
230
231 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
232
233 EXPECT_TRUE(formula->isRewardOperatorFormula());
234 ASSERT_TRUE(formula->asRewardOperatorFormula().getSubformula().isDiscountedCumulativeRewardFormula());
235 static const std::string discountFactorString3 = "1/2";
236 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(discountFactorString3),
237 formula->asRewardOperatorFormula().getSubformula().asDiscountedCumulativeRewardFormula().getDiscountFactor().evaluateAsRational());
238 EXPECT_FLOAT_EQ(0.5, formula->asRewardOperatorFormula().getSubformula().asDiscountedCumulativeRewardFormula().getDiscountFactor().evaluateAsDouble());
239 EXPECT_FALSE(formula->asRewardOperatorFormula().getSubformula().asDiscountedCumulativeRewardFormula().getTimeBoundReference().isTimeBound());
240 EXPECT_TRUE(formula->asRewardOperatorFormula().getSubformula().asDiscountedCumulativeRewardFormula().getTimeBoundReference().isRewardBound());
241 EXPECT_EQ(8, formula->asRewardOperatorFormula().getSubformula().asDiscountedCumulativeRewardFormula().getBound().evaluateAsInt());
242}
243
244TEST(FormulaParserTest, CommentTest) {
245 storm::parser::FormulaParser formulaParser;
246
247 std::string input =
248 "// 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\" ] // "
249 "Another comment \n // And again: another comment.";
250 std::shared_ptr<storm::logic::Formula const> formula(nullptr);
251 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
252 EXPECT_TRUE(formula->isProbabilityOperatorFormula());
253 ASSERT_TRUE(formula->asProbabilityOperatorFormula().getSubformula().isNextFormula());
254 ASSERT_TRUE(formula->asProbabilityOperatorFormula().getSubformula().asNextFormula().getSubformula().isAtomicLabelFormula());
255}
256
257TEST(FormulaParserTest, WrongFormatTest) {
258 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
259 manager->declareBooleanVariable("x");
260 manager->declareIntegerVariable("y");
261
262 storm::parser::FormulaParser formulaParser(manager);
263 std::string input = "P>0.5 [ a ]";
264 std::shared_ptr<storm::logic::Formula const> formula(nullptr);
265 STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
266
267 input = "P=0.5 [F \"a\"]";
268 STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
269
270 input = "P>0.5 [F !(x = 0)]";
271 STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
272
273 input = "P>0.5 [F !y]";
274 STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
275
276 input = "P>0.5 [F y!=0)]";
277 STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
278
279 input = "P<0.9 [G F]";
280 STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
281
282 input = "P<0.9 [\"a\" U \"b\" U \"c\"]";
283 STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
284
285 input = "P<0.9 [X \"a\" U G \"b\" U X \"c\"]";
286 STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
287}
288
289TEST(FormulaParserTest, MultiObjectiveFormulaTest) {
290 storm::parser::FormulaParser formulaParser;
291
292 std::string input = "multi(P<0.9 [ F \"a\" ], R<42 [ F \"b\" ], Pmin=? [ F\"c\" ])";
293 std::shared_ptr<storm::logic::Formula const> formula;
294 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
295 ASSERT_TRUE(formula->isMultiObjectiveFormula());
296 storm::logic::MultiObjectiveFormula mof = formula->asMultiObjectiveFormula();
297 ASSERT_EQ(3ull, mof.getNumberOfSubformulas());
298
299 ASSERT_TRUE(mof.getSubformula(0).isProbabilityOperatorFormula());
300 ASSERT_TRUE(mof.getSubformula(0).asProbabilityOperatorFormula().getSubformula().isEventuallyFormula());
301 ASSERT_TRUE(mof.getSubformula(0).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isAtomicLabelFormula());
302 ASSERT_TRUE(mof.getSubformula(0).asProbabilityOperatorFormula().hasBound());
303
304 ASSERT_TRUE(mof.getSubformula(1).isRewardOperatorFormula());
305 ASSERT_TRUE(mof.getSubformula(1).asRewardOperatorFormula().getSubformula().isEventuallyFormula());
306 ASSERT_TRUE(mof.getSubformula(1).asRewardOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isAtomicLabelFormula());
307 ASSERT_TRUE(mof.getSubformula(1).asRewardOperatorFormula().hasBound());
308
309 ASSERT_TRUE(mof.getSubformula(2).isProbabilityOperatorFormula());
310 ASSERT_TRUE(mof.getSubformula(2).asProbabilityOperatorFormula().getSubformula().isEventuallyFormula());
311 ASSERT_TRUE(mof.getSubformula(2).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isAtomicLabelFormula());
312 ASSERT_TRUE(mof.getSubformula(2).asProbabilityOperatorFormula().hasOptimalityType());
313 ASSERT_TRUE(storm::solver::minimize(mof.getSubformula(2).asProbabilityOperatorFormula().getOptimalityType()));
314}
315
316TEST(FormulaParserTest, LogicalPrecedenceTest) {
317 // Test precedence of logical operators over temporal operators, etc.
318 storm::parser::FormulaParser formulaParser;
319 std::shared_ptr<storm::logic::Formula const> formula(nullptr);
320
321 std::string input = "P=? [ !\"a\" & \"b\" U ! \"c\" | \"b\" ]";
322 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
323 EXPECT_TRUE(formula->isProbabilityOperatorFormula());
324
325 auto const &nested1 = formula->asProbabilityOperatorFormula().getSubformula();
326 EXPECT_TRUE(nested1.isUntilFormula());
327 ASSERT_TRUE(nested1.asUntilFormula().getLeftSubformula().isBinaryBooleanStateFormula());
328 ASSERT_TRUE(nested1.asUntilFormula().getLeftSubformula().asBinaryBooleanStateFormula().getLeftSubformula().isUnaryBooleanStateFormula());
329 ASSERT_TRUE(nested1.asUntilFormula().getRightSubformula().isBinaryBooleanStateFormula());
330 ASSERT_TRUE(nested1.asUntilFormula().getRightSubformula().asBinaryBooleanStateFormula().getLeftSubformula().isUnaryBooleanStateFormula());
331
332 input = "P<0.9 [ F G !\"a\" | \"b\" ] ";
333 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
334 auto const &nested2 = formula->asProbabilityOperatorFormula().getSubformula();
335 EXPECT_TRUE(nested2.asEventuallyFormula().getSubformula().isGloballyFormula());
336 auto const &nested2Subformula = nested2.asEventuallyFormula().getSubformula().asGloballyFormula();
337 EXPECT_TRUE(nested2Subformula.getSubformula().isBinaryBooleanStateFormula());
338 ASSERT_TRUE(nested2Subformula.getSubformula().asBinaryBooleanStateFormula().getLeftSubformula().isUnaryBooleanStateFormula());
339
340 input = "P<0.9 [ X G \"a\" | !\"b\" | \"c\"] "; // from left to right
341 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
342 auto const &nested3 = formula->asProbabilityOperatorFormula().getSubformula();
343 EXPECT_TRUE(nested3.asNextFormula().getSubformula().isGloballyFormula());
344 EXPECT_TRUE(nested3.asNextFormula().getSubformula().asGloballyFormula().getSubformula().isBinaryBooleanStateFormula());
345 auto const &nested3Subformula = nested3.asNextFormula().getSubformula().asGloballyFormula().getSubformula().asBinaryBooleanStateFormula();
346 ASSERT_TRUE(nested3Subformula.getLeftSubformula().isBinaryBooleanStateFormula());
347 ASSERT_TRUE(nested3Subformula.asBinaryBooleanStateFormula().getRightSubformula().isAtomicLabelFormula());
348
349 input = "P<0.9 [ X F \"a\" | ! \"b\" & \"c\"] "; // & has precedence over | and ! over &
350 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
351 auto const &nested4 = formula->asProbabilityOperatorFormula().getSubformula();
352 EXPECT_TRUE(nested4.asNextFormula().getSubformula().isEventuallyFormula());
353 EXPECT_TRUE(nested4.asNextFormula().getSubformula().asEventuallyFormula().getSubformula().isBinaryBooleanStateFormula());
354 auto const &nested4Subformula = nested4.asNextFormula().getSubformula().asEventuallyFormula().getSubformula().asBinaryBooleanStateFormula();
355 ASSERT_TRUE(nested4Subformula.getLeftSubformula().isAtomicLabelFormula());
356 ASSERT_TRUE(nested4Subformula.getRightSubformula().isBinaryBooleanStateFormula());
357
358 input = "P<0.9 [X \"a\" | F \"b\"]"; // X (a | F b)
359 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
360 auto const &nested5 = formula->asProbabilityOperatorFormula().getSubformula();
361 EXPECT_TRUE(nested5.isNextFormula());
362 EXPECT_TRUE(nested5.asNextFormula().getSubformula().isBinaryBooleanPathFormula());
363 EXPECT_TRUE(nested5.asNextFormula().getSubformula().asBinaryPathFormula().getLeftSubformula().isAtomicLabelFormula());
364 EXPECT_TRUE(nested5.asNextFormula().getSubformula().asBinaryPathFormula().getRightSubformula().isEventuallyFormula());
365
366 input = "P<0.9 [F \"a\" | G \"b\" | X \"c\" ]"; // F (a | G (b | X c))
367 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
368 auto const &nested6 = formula->asProbabilityOperatorFormula().getSubformula();
369 EXPECT_TRUE(nested6.isEventuallyFormula());
370 EXPECT_TRUE(nested6.asEventuallyFormula().getSubformula().isBinaryBooleanPathFormula());
371 EXPECT_TRUE(nested6.asEventuallyFormula().getSubformula().asBinaryPathFormula().getLeftSubformula().isAtomicLabelFormula());
372 EXPECT_TRUE(nested6.asEventuallyFormula().getSubformula().asBinaryPathFormula().getRightSubformula().isGloballyFormula());
373 auto const &nested6Subformula = nested6.asEventuallyFormula().getSubformula().asBinaryPathFormula().getRightSubformula().asGloballyFormula();
374 EXPECT_TRUE(nested6Subformula.getSubformula().isBinaryBooleanPathFormula());
375 EXPECT_TRUE(nested6Subformula.getSubformula().asBinaryPathFormula().getLeftSubformula().isAtomicLabelFormula());
376 EXPECT_TRUE(nested6Subformula.getSubformula().asBinaryPathFormula().getRightSubformula().isNextFormula());
377 EXPECT_TRUE(nested6Subformula.getSubformula().asBinaryPathFormula().getRightSubformula().asNextFormula().getSubformula().isAtomicLabelFormula());
378}
379
380TEST(FormulaParserTest, TemporalPrecedenceTest) {
381 // Unary operators (F, G and X) have precedence over binary operators (U).
382 storm::parser::FormulaParser formulaParser;
383 std::shared_ptr<storm::logic::Formula const> formula(nullptr);
384
385 std::string input = "P=? [ F \"a\" U G \"b\" ]"; // (F a) U (G b)
386 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
387 auto const &nested1 = formula->asProbabilityOperatorFormula().getSubformula();
388 EXPECT_TRUE(nested1.isUntilFormula());
389 ASSERT_TRUE(nested1.asUntilFormula().getLeftSubformula().isEventuallyFormula());
390 ASSERT_TRUE(nested1.asUntilFormula().getRightSubformula().isGloballyFormula());
391
392 input = "P=? [ X ( F \"a\" U G \"b\") U G \"c\"]"; // X((F a) U (G b)) U (G c)
393 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
394 auto const &nested2 = formula->asProbabilityOperatorFormula().getSubformula();
395 EXPECT_TRUE(nested2.isUntilFormula());
396 EXPECT_TRUE(nested2.asUntilFormula().getLeftSubformula().isNextFormula());
397 EXPECT_TRUE(nested2.asUntilFormula().getLeftSubformula().asNextFormula().getSubformula().isUntilFormula());
398 EXPECT_TRUE(nested2.asUntilFormula().getRightSubformula().isGloballyFormula());
399
400 input = "P=? [ X F \"a\" U (G \"b\" U G \"c\")]"; // (XF a) U ((G b) U (G c))
401 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
402 auto const &nested3 = formula->asProbabilityOperatorFormula().getSubformula();
403 EXPECT_TRUE(nested3.isUntilFormula());
404 EXPECT_TRUE(nested3.asUntilFormula().getLeftSubformula().isNextFormula());
405 EXPECT_TRUE(nested3.asUntilFormula().getLeftSubformula().asNextFormula().getSubformula().isEventuallyFormula());
406 EXPECT_TRUE(nested3.asUntilFormula().getRightSubformula().isUntilFormula());
407 EXPECT_TRUE(nested3.asUntilFormula().getRightSubformula().asUntilFormula().getLeftSubformula().isGloballyFormula());
408 EXPECT_TRUE(nested3.asUntilFormula().getRightSubformula().asUntilFormula().getRightSubformula().isGloballyFormula());
409}
410
411TEST(FormulaParserTest, TemporalNegationTest) {
412 storm::parser::FormulaParser formulaParser;
413 std::shared_ptr<storm::logic::Formula const> formula(nullptr);
414
415 std::string input = "P<0.9 [ ! X \"a\" | \"b\"]";
416 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
417 auto const &nested1 = formula->asProbabilityOperatorFormula().getSubformula();
418 EXPECT_TRUE(nested1.isUnaryBooleanPathFormula());
419 EXPECT_TRUE(nested1.asUnaryPathFormula().getSubformula().isNextFormula());
420 EXPECT_TRUE(nested1.asUnaryPathFormula().getSubformula().asNextFormula().getSubformula().isBinaryBooleanStateFormula());
421
422 input = "P<0.9 [! F ! G \"b\"]";
423 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
424 auto const &nested2 = formula->asProbabilityOperatorFormula().getSubformula();
425 EXPECT_TRUE(nested2.isUnaryBooleanPathFormula());
426 EXPECT_TRUE(nested2.asUnaryPathFormula().getSubformula().isEventuallyFormula());
427 EXPECT_TRUE(nested2.asUnaryPathFormula().getSubformula().asEventuallyFormula().getSubformula().isUnaryBooleanPathFormula());
428 EXPECT_TRUE(nested2.asUnaryPathFormula().getSubformula().asEventuallyFormula().getSubformula().asUnaryPathFormula().getSubformula().isGloballyFormula());
429
430 input = "P<0.9 [! (\"a\" U \"b\")]";
431 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
432 auto const &nested3 = formula->asProbabilityOperatorFormula().getSubformula();
433 EXPECT_TRUE(nested3.isUnaryBooleanPathFormula());
434 EXPECT_TRUE(nested3.asUnaryPathFormula().getSubformula().isUntilFormula());
435}
436
437TEST(FormulaParserTest, ComplexPathFormulaTest) {
438 storm::parser::FormulaParser formulaParser;
439 std::shared_ptr<storm::logic::Formula const> formula(nullptr);
440
441 std::string input = "P<0.9 [(X !\"a\") & (F ( X \"b\" U G \"c\" & \"d\"))]"; // ((X ! a) & (F ( (X b) U (G (c & d)))))
442 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
443 auto const &nested1 = formula->asProbabilityOperatorFormula().getSubformula();
444 EXPECT_TRUE(nested1.asBinaryPathFormula().getRightSubformula().asEventuallyFormula().getSubformula().isUntilFormula());
445 auto const nested1Subformula = nested1.asBinaryPathFormula().getRightSubformula().asEventuallyFormula().getSubformula().asUntilFormula();
446 EXPECT_TRUE(nested1Subformula.getLeftSubformula().isNextFormula());
447 EXPECT_TRUE(nested1Subformula.getRightSubformula().asGloballyFormula().getSubformula().isBinaryBooleanStateFormula());
448
449 input = "P<0.9 [(F \"a\") & (G \"b\") | (! \"a\" U (F X ! \"b\"))]";
450 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
451 auto const &nested2 = formula->asProbabilityOperatorFormula().getSubformula();
452 ASSERT_TRUE(nested2.asBinaryPathFormula().getLeftSubformula().isBinaryPathFormula());
453 ASSERT_TRUE(nested2.asBinaryPathFormula().getRightSubformula().isUntilFormula());
454
455 input = "P=? [(X \"a\") U ( \"b\"& \"c\")]";
456 formula = formulaParser.parseSingleFormulaFromString(input);
457 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
458 auto const &nested3 = formula->asProbabilityOperatorFormula().getSubformula();
459 EXPECT_TRUE(nested3.asBinaryPathFormula().isUntilFormula());
460 EXPECT_TRUE(nested3.asBinaryPathFormula().getLeftSubformula().isNextFormula());
461}
462
463TEST(FormulaParserTest, HOAPathFormulaTest) {
464 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
465 manager->declareIntegerVariable("x");
466 manager->declareIntegerVariable("y");
467 storm::parser::FormulaParser formulaParser(manager);
468 std::shared_ptr<storm::logic::Formula const> formula(nullptr);
469
470 std::string input = "P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> !\"a\", \"p1\" -> \"b\" | \"c\" }]";
471 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
472 auto const &nested1 = formula->asProbabilityOperatorFormula().getSubformula();
473 EXPECT_TRUE(nested1.isHOAPathFormula());
474 EXPECT_TRUE(nested1.isPathFormula());
475
476 ASSERT_NO_THROW(std::string af = nested1.asHOAPathFormula().getAutomatonFile());
477 storm::automata::DeterministicAutomaton::ptr da1;
478 ASSERT_NO_THROW(da1 = nested1.asHOAPathFormula().readAutomaton());
479 EXPECT_EQ(3ul, da1->getNumberOfStates());
480 EXPECT_EQ(4ul, da1->getNumberOfEdgesPerState());
481
482 std::map<std::string, std::shared_ptr<storm::logic::Formula const>> apFormulaMap1 = nested1.asHOAPathFormula().getAPMapping();
483 EXPECT_TRUE(apFormulaMap1["p0"]->isUnaryBooleanStateFormula());
484 EXPECT_TRUE(apFormulaMap1["p1"]->isBinaryBooleanStateFormula());
485
486 input = "P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_UXp0p1.hoa\", \"p0\" -> (x < 7) & !(y = 2), \"p1\" -> (x > 0) }]";
487 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
488 auto const &nested2 = formula->asProbabilityOperatorFormula().getSubformula();
489 EXPECT_TRUE(nested2.isHOAPathFormula());
490 EXPECT_TRUE(nested2.isPathFormula());
491
492 ASSERT_NO_THROW(std::string af = nested2.asHOAPathFormula().getAutomatonFile());
493 storm::automata::DeterministicAutomaton::ptr da2;
494 ASSERT_NO_THROW(da2 = nested2.asHOAPathFormula().readAutomaton());
495 EXPECT_EQ(4ul, da2->getNumberOfStates());
496 EXPECT_EQ(4ul, da2->getNumberOfEdgesPerState());
497
498 std::map<std::string, std::shared_ptr<storm::logic::Formula const>> apFormulaMap2 = nested2.asHOAPathFormula().getAPMapping();
499 EXPECT_TRUE(apFormulaMap2["p0"]->isAtomicExpressionFormula());
500 EXPECT_TRUE(apFormulaMap2["p1"]->isAtomicExpressionFormula());
501
502 // Wrong format: p1 -> path formula
503 input = "P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_UXp0p1.hoa\", \"p0\" -> (x > 0), \"p1\" -> (x < 7) & (X y = 2) }]";
504 STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
505
506 // Exception: p1 not assigned
507 input = "P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_UXp0p1.hoa\", \"p0\" -> (x > 0)}]";
508 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
509 auto const &nested3 = formula->asProbabilityOperatorFormula().getSubformula();
510 storm::automata::DeterministicAutomaton::ptr da3;
511 STORM_SILENT_EXPECT_THROW(da3 = nested3.asHOAPathFormula().readAutomaton(), storm::exceptions::ExpressionEvaluationException);
512}
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:484
storm::logic::Formula::isProbabilityOperatorFormula
virtual bool isProbabilityOperatorFormula() const
Definition Formula.cpp:180
storm::logic::Formula::asProbabilityOperatorFormula
ProbabilityOperatorFormula & asProbabilityOperatorFormula()
Definition Formula.cpp:476
storm::logic::Formula::isRewardOperatorFormula
virtual bool isRewardOperatorFormula() const
Definition Formula.cpp:184
storm::logic::Formula::asEventuallyFormula
EventuallyFormula & asEventuallyFormula()
Definition Formula.cpp:341
storm::logic::Formula::isEventuallyFormula
virtual bool isEventuallyFormula() const
Definition Formula.cpp:88
storm::logic::Formula::asMultiObjectiveFormula
MultiObjectiveFormula & asMultiObjectiveFormula()
Definition Formula.cpp:237
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:86
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