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