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 std::shared_ptr<storm::logic::Formula const> formula;
294
295 auto checkSubformulas = [](storm::logic::MultiObjectiveFormula const &mof) {
296 ASSERT_EQ(3ull, mof.getNumberOfSubformulas());
297
298 ASSERT_TRUE(mof.getSubformula(0).isProbabilityOperatorFormula());
299 ASSERT_TRUE(mof.getSubformula(0).asProbabilityOperatorFormula().getSubformula().isEventuallyFormula());
300 ASSERT_TRUE(mof.getSubformula(0).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isAtomicLabelFormula());
301 ASSERT_TRUE(mof.getSubformula(0).asProbabilityOperatorFormula().hasBound());
302
303 ASSERT_TRUE(mof.getSubformula(1).isRewardOperatorFormula());
304 ASSERT_TRUE(mof.getSubformula(1).asRewardOperatorFormula().getSubformula().isEventuallyFormula());
305 ASSERT_TRUE(mof.getSubformula(1).asRewardOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isAtomicLabelFormula());
306 ASSERT_TRUE(mof.getSubformula(1).asRewardOperatorFormula().hasBound());
307
308 ASSERT_TRUE(mof.getSubformula(2).isProbabilityOperatorFormula());
309 ASSERT_TRUE(mof.getSubformula(2).asProbabilityOperatorFormula().getSubformula().isEventuallyFormula());
310 ASSERT_TRUE(mof.getSubformula(2).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isAtomicLabelFormula());
311 ASSERT_TRUE(mof.getSubformula(2).asProbabilityOperatorFormula().hasOptimalityType());
312 ASSERT_TRUE(storm::solver::minimize(mof.getSubformula(2).asProbabilityOperatorFormula().getOptimalityType()));
313 };
314
315 std::string input = "multi(P<0.9 [ F \"a\" ], R<42 [ F \"b\" ], Pmin=? [ F\"c\" ])";
316 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
317 ASSERT_TRUE(formula->isMultiObjectiveFormula());
318 storm::logic::MultiObjectiveFormula const &mof = formula->asMultiObjectiveFormula();
319 ASSERT_TRUE(mof.isTradeoff());
320 checkSubformulas(mof);
321
322 input = "multilex(P<0.9 [ F \"a\" ], R<42 [ F \"b\" ], Pmin=? [ F\"c\" ])";
323 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
324 ASSERT_TRUE(formula->isMultiObjectiveFormula());
325 storm::logic::MultiObjectiveFormula const &mlof = formula->asMultiObjectiveFormula();
326 ASSERT_TRUE(mlof.isLexicographic());
327 checkSubformulas(mlof);
328}
329
330TEST(FormulaParserTest, LogicalPrecedenceTest) {
331 // Test precedence of logical operators over temporal operators, etc.
332 storm::parser::FormulaParser formulaParser;
333 std::shared_ptr<storm::logic::Formula const> formula(nullptr);
334
335 std::string input = "P=? [ !\"a\" & \"b\" U ! \"c\" | \"b\" ]";
336 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
337 EXPECT_TRUE(formula->isProbabilityOperatorFormula());
338
339 auto const &nested1 = formula->asProbabilityOperatorFormula().getSubformula();
340 EXPECT_TRUE(nested1.isUntilFormula());
341 ASSERT_TRUE(nested1.asUntilFormula().getLeftSubformula().isBinaryBooleanStateFormula());
342 ASSERT_TRUE(nested1.asUntilFormula().getLeftSubformula().asBinaryBooleanStateFormula().getLeftSubformula().isUnaryBooleanStateFormula());
343 ASSERT_TRUE(nested1.asUntilFormula().getRightSubformula().isBinaryBooleanStateFormula());
344 ASSERT_TRUE(nested1.asUntilFormula().getRightSubformula().asBinaryBooleanStateFormula().getLeftSubformula().isUnaryBooleanStateFormula());
345
346 input = "P<0.9 [ F G !\"a\" | \"b\" ] ";
347 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
348 auto const &nested2 = formula->asProbabilityOperatorFormula().getSubformula();
349 EXPECT_TRUE(nested2.asEventuallyFormula().getSubformula().isGloballyFormula());
350 auto const &nested2Subformula = nested2.asEventuallyFormula().getSubformula().asGloballyFormula();
351 EXPECT_TRUE(nested2Subformula.getSubformula().isBinaryBooleanStateFormula());
352 ASSERT_TRUE(nested2Subformula.getSubformula().asBinaryBooleanStateFormula().getLeftSubformula().isUnaryBooleanStateFormula());
353
354 input = "P<0.9 [ X G \"a\" | !\"b\" | \"c\"] "; // from left to right
355 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
356 auto const &nested3 = formula->asProbabilityOperatorFormula().getSubformula();
357 EXPECT_TRUE(nested3.asNextFormula().getSubformula().isGloballyFormula());
358 EXPECT_TRUE(nested3.asNextFormula().getSubformula().asGloballyFormula().getSubformula().isBinaryBooleanStateFormula());
359 auto const &nested3Subformula = nested3.asNextFormula().getSubformula().asGloballyFormula().getSubformula().asBinaryBooleanStateFormula();
360 ASSERT_TRUE(nested3Subformula.getLeftSubformula().isBinaryBooleanStateFormula());
361 ASSERT_TRUE(nested3Subformula.asBinaryBooleanStateFormula().getRightSubformula().isAtomicLabelFormula());
362
363 input = "P<0.9 [ X F \"a\" | ! \"b\" & \"c\"] "; // & has precedence over | and ! over &
364 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
365 auto const &nested4 = formula->asProbabilityOperatorFormula().getSubformula();
366 EXPECT_TRUE(nested4.asNextFormula().getSubformula().isEventuallyFormula());
367 EXPECT_TRUE(nested4.asNextFormula().getSubformula().asEventuallyFormula().getSubformula().isBinaryBooleanStateFormula());
368 auto const &nested4Subformula = nested4.asNextFormula().getSubformula().asEventuallyFormula().getSubformula().asBinaryBooleanStateFormula();
369 ASSERT_TRUE(nested4Subformula.getLeftSubformula().isAtomicLabelFormula());
370 ASSERT_TRUE(nested4Subformula.getRightSubformula().isBinaryBooleanStateFormula());
371
372 input = "P<0.9 [X \"a\" | F \"b\"]"; // X (a | F b)
373 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
374 auto const &nested5 = formula->asProbabilityOperatorFormula().getSubformula();
375 EXPECT_TRUE(nested5.isNextFormula());
376 EXPECT_TRUE(nested5.asNextFormula().getSubformula().isBinaryBooleanPathFormula());
377 EXPECT_TRUE(nested5.asNextFormula().getSubformula().asBinaryPathFormula().getLeftSubformula().isAtomicLabelFormula());
378 EXPECT_TRUE(nested5.asNextFormula().getSubformula().asBinaryPathFormula().getRightSubformula().isEventuallyFormula());
379
380 input = "P<0.9 [F \"a\" | G \"b\" | X \"c\" ]"; // F (a | G (b | X c))
381 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
382 auto const &nested6 = formula->asProbabilityOperatorFormula().getSubformula();
383 EXPECT_TRUE(nested6.isEventuallyFormula());
384 EXPECT_TRUE(nested6.asEventuallyFormula().getSubformula().isBinaryBooleanPathFormula());
385 EXPECT_TRUE(nested6.asEventuallyFormula().getSubformula().asBinaryPathFormula().getLeftSubformula().isAtomicLabelFormula());
386 EXPECT_TRUE(nested6.asEventuallyFormula().getSubformula().asBinaryPathFormula().getRightSubformula().isGloballyFormula());
387 auto const &nested6Subformula = nested6.asEventuallyFormula().getSubformula().asBinaryPathFormula().getRightSubformula().asGloballyFormula();
388 EXPECT_TRUE(nested6Subformula.getSubformula().isBinaryBooleanPathFormula());
389 EXPECT_TRUE(nested6Subformula.getSubformula().asBinaryPathFormula().getLeftSubformula().isAtomicLabelFormula());
390 EXPECT_TRUE(nested6Subformula.getSubformula().asBinaryPathFormula().getRightSubformula().isNextFormula());
391 EXPECT_TRUE(nested6Subformula.getSubformula().asBinaryPathFormula().getRightSubformula().asNextFormula().getSubformula().isAtomicLabelFormula());
392}
393
394TEST(FormulaParserTest, TemporalPrecedenceTest) {
395 // Unary operators (F, G and X) have precedence over binary operators (U).
396 storm::parser::FormulaParser formulaParser;
397 std::shared_ptr<storm::logic::Formula const> formula(nullptr);
398
399 std::string input = "P=? [ F \"a\" U G \"b\" ]"; // (F a) U (G b)
400 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
401 auto const &nested1 = formula->asProbabilityOperatorFormula().getSubformula();
402 EXPECT_TRUE(nested1.isUntilFormula());
403 ASSERT_TRUE(nested1.asUntilFormula().getLeftSubformula().isEventuallyFormula());
404 ASSERT_TRUE(nested1.asUntilFormula().getRightSubformula().isGloballyFormula());
405
406 input = "P=? [ X ( F \"a\" U G \"b\") U G \"c\"]"; // X((F a) U (G b)) U (G c)
407 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
408 auto const &nested2 = formula->asProbabilityOperatorFormula().getSubformula();
409 EXPECT_TRUE(nested2.isUntilFormula());
410 EXPECT_TRUE(nested2.asUntilFormula().getLeftSubformula().isNextFormula());
411 EXPECT_TRUE(nested2.asUntilFormula().getLeftSubformula().asNextFormula().getSubformula().isUntilFormula());
412 EXPECT_TRUE(nested2.asUntilFormula().getRightSubformula().isGloballyFormula());
413
414 input = "P=? [ X F \"a\" U (G \"b\" U G \"c\")]"; // (XF a) U ((G b) U (G c))
415 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
416 auto const &nested3 = formula->asProbabilityOperatorFormula().getSubformula();
417 EXPECT_TRUE(nested3.isUntilFormula());
418 EXPECT_TRUE(nested3.asUntilFormula().getLeftSubformula().isNextFormula());
419 EXPECT_TRUE(nested3.asUntilFormula().getLeftSubformula().asNextFormula().getSubformula().isEventuallyFormula());
420 EXPECT_TRUE(nested3.asUntilFormula().getRightSubformula().isUntilFormula());
421 EXPECT_TRUE(nested3.asUntilFormula().getRightSubformula().asUntilFormula().getLeftSubformula().isGloballyFormula());
422 EXPECT_TRUE(nested3.asUntilFormula().getRightSubformula().asUntilFormula().getRightSubformula().isGloballyFormula());
423}
424
425TEST(FormulaParserTest, TemporalNegationTest) {
426 storm::parser::FormulaParser formulaParser;
427 std::shared_ptr<storm::logic::Formula const> formula(nullptr);
428
429 std::string input = "P<0.9 [ ! X \"a\" | \"b\"]";
430 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
431 auto const &nested1 = formula->asProbabilityOperatorFormula().getSubformula();
432 EXPECT_TRUE(nested1.isUnaryBooleanPathFormula());
433 EXPECT_TRUE(nested1.asUnaryPathFormula().getSubformula().isNextFormula());
434 EXPECT_TRUE(nested1.asUnaryPathFormula().getSubformula().asNextFormula().getSubformula().isBinaryBooleanStateFormula());
435
436 input = "P<0.9 [! F ! G \"b\"]";
437 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
438 auto const &nested2 = formula->asProbabilityOperatorFormula().getSubformula();
439 EXPECT_TRUE(nested2.isUnaryBooleanPathFormula());
440 EXPECT_TRUE(nested2.asUnaryPathFormula().getSubformula().isEventuallyFormula());
441 EXPECT_TRUE(nested2.asUnaryPathFormula().getSubformula().asEventuallyFormula().getSubformula().isUnaryBooleanPathFormula());
442 EXPECT_TRUE(nested2.asUnaryPathFormula().getSubformula().asEventuallyFormula().getSubformula().asUnaryPathFormula().getSubformula().isGloballyFormula());
443
444 input = "P<0.9 [! (\"a\" U \"b\")]";
445 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
446 auto const &nested3 = formula->asProbabilityOperatorFormula().getSubformula();
447 EXPECT_TRUE(nested3.isUnaryBooleanPathFormula());
448 EXPECT_TRUE(nested3.asUnaryPathFormula().getSubformula().isUntilFormula());
449}
450
451TEST(FormulaParserTest, ComplexPathFormulaTest) {
452 storm::parser::FormulaParser formulaParser;
453 std::shared_ptr<storm::logic::Formula const> formula(nullptr);
454
455 std::string input = "P<0.9 [(X !\"a\") & (F ( X \"b\" U G \"c\" & \"d\"))]"; // ((X ! a) & (F ( (X b) U (G (c & d)))))
456 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
457 auto const &nested1 = formula->asProbabilityOperatorFormula().getSubformula();
458 EXPECT_TRUE(nested1.asBinaryPathFormula().getRightSubformula().asEventuallyFormula().getSubformula().isUntilFormula());
459 auto const nested1Subformula = nested1.asBinaryPathFormula().getRightSubformula().asEventuallyFormula().getSubformula().asUntilFormula();
460 EXPECT_TRUE(nested1Subformula.getLeftSubformula().isNextFormula());
461 EXPECT_TRUE(nested1Subformula.getRightSubformula().asGloballyFormula().getSubformula().isBinaryBooleanStateFormula());
462
463 input = "P<0.9 [(F \"a\") & (G \"b\") | (! \"a\" U (F X ! \"b\"))]";
464 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
465 auto const &nested2 = formula->asProbabilityOperatorFormula().getSubformula();
466 ASSERT_TRUE(nested2.asBinaryPathFormula().getLeftSubformula().isBinaryPathFormula());
467 ASSERT_TRUE(nested2.asBinaryPathFormula().getRightSubformula().isUntilFormula());
468
469 input = "P=? [(X \"a\") U ( \"b\"& \"c\")]";
470 formula = formulaParser.parseSingleFormulaFromString(input);
471 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
472 auto const &nested3 = formula->asProbabilityOperatorFormula().getSubformula();
473 EXPECT_TRUE(nested3.asBinaryPathFormula().isUntilFormula());
474 EXPECT_TRUE(nested3.asBinaryPathFormula().getLeftSubformula().isNextFormula());
475}
476
477TEST(FormulaParserTest, HOAPathFormulaTest) {
478 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
479 manager->declareIntegerVariable("x");
480 manager->declareIntegerVariable("y");
481 storm::parser::FormulaParser formulaParser(manager);
482 std::shared_ptr<storm::logic::Formula const> formula(nullptr);
483
484 std::string input = "P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> !\"a\", \"p1\" -> \"b\" | \"c\" }]";
485 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
486 auto const &nested1 = formula->asProbabilityOperatorFormula().getSubformula();
487 EXPECT_TRUE(nested1.isHOAPathFormula());
488 EXPECT_TRUE(nested1.isPathFormula());
489
490 ASSERT_NO_THROW(std::string af = nested1.asHOAPathFormula().getAutomatonFile());
491 storm::automata::DeterministicAutomaton::ptr da1;
492 ASSERT_NO_THROW(da1 = nested1.asHOAPathFormula().readAutomaton());
493 EXPECT_EQ(3ul, da1->getNumberOfStates());
494 EXPECT_EQ(4ul, da1->getNumberOfEdgesPerState());
495
496 std::map<std::string, std::shared_ptr<storm::logic::Formula const>> apFormulaMap1 = nested1.asHOAPathFormula().getAPMapping();
497 EXPECT_TRUE(apFormulaMap1["p0"]->isUnaryBooleanStateFormula());
498 EXPECT_TRUE(apFormulaMap1["p1"]->isBinaryBooleanStateFormula());
499
500 input = "P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_UXp0p1.hoa\", \"p0\" -> (x < 7) & !(y = 2), \"p1\" -> (x > 0) }]";
501 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
502 auto const &nested2 = formula->asProbabilityOperatorFormula().getSubformula();
503 EXPECT_TRUE(nested2.isHOAPathFormula());
504 EXPECT_TRUE(nested2.isPathFormula());
505
506 ASSERT_NO_THROW(std::string af = nested2.asHOAPathFormula().getAutomatonFile());
507 storm::automata::DeterministicAutomaton::ptr da2;
508 ASSERT_NO_THROW(da2 = nested2.asHOAPathFormula().readAutomaton());
509 EXPECT_EQ(4ul, da2->getNumberOfStates());
510 EXPECT_EQ(4ul, da2->getNumberOfEdgesPerState());
511
512 std::map<std::string, std::shared_ptr<storm::logic::Formula const>> apFormulaMap2 = nested2.asHOAPathFormula().getAPMapping();
513 EXPECT_TRUE(apFormulaMap2["p0"]->isAtomicExpressionFormula());
514 EXPECT_TRUE(apFormulaMap2["p1"]->isAtomicExpressionFormula());
515
516 // Wrong format: p1 -> path formula
517 input = "P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_UXp0p1.hoa\", \"p0\" -> (x > 0), \"p1\" -> (x < 7) & (X y = 2) }]";
518 STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
519
520 // Exception: p1 not assigned
521 input = "P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_UXp0p1.hoa\", \"p0\" -> (x > 0)}]";
522 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
523 auto const &nested3 = formula->asProbabilityOperatorFormula().getSubformula();
524 storm::automata::DeterministicAutomaton::ptr da3;
525 STORM_SILENT_EXPECT_THROW(da3 = nested3.asHOAPathFormula().readAutomaton(), storm::exceptions::ExpressionEvaluationException);
526}
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::asProbabilityOperatorFormula
ProbabilityOperatorFormula & asProbabilityOperatorFormula()
Definition Formula.cpp:476
storm::logic::Formula::asMultiObjectiveFormula
MultiObjectiveFormula & asMultiObjectiveFormula()
Definition Formula.cpp:237
storm::logic::Formula::isConditionalProbabilityFormula
virtual bool isConditionalProbabilityFormula() const
Definition Formula.cpp:112
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