Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
ExpressionTest.cpp
Go to the documentation of this file.
1#include <map>
2#include <string>
3
4#include "storm-parsers/parser/ValueParser.h"
5#include "storm/adapters/RationalFunctionAdapter.h"
6#include "storm/exceptions/InvalidTypeException.h"
7#include "storm/storage/expressions/Expression.h"
8#include "storm/storage/expressions/ExpressionEvaluator.h"
9#include "storm/storage/expressions/ExpressionManager.h"
10#include "storm/storage/expressions/LinearityCheckVisitor.h"
11#include "storm/storage/expressions/RationalFunctionToExpression.h"
12#include "storm/storage/expressions/SimpleValuation.h"
13#include "storm/storage/expressions/ToRationalFunctionVisitor.h"
14#include "test/storm_gtest.h"
15
16TEST(Expression, FactoryMethodTest) {
17 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
18 EXPECT_NO_THROW(manager->boolean(true));
19 EXPECT_NO_THROW(manager->boolean(false));
20 EXPECT_NO_THROW(manager->integer(3));
21 EXPECT_NO_THROW(manager->rational(3.14));
22 EXPECT_NO_THROW(manager->declareBooleanVariable("x"));
23 EXPECT_NO_THROW(manager->declareIntegerVariable("y"));
24 EXPECT_NO_THROW(manager->declareRationalVariable("z"));
25}
26
27TEST(Expression, AccessorTest) {
28 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
29
30 storm::expressions::Expression trueExpression;
31 storm::expressions::Expression falseExpression;
32 storm::expressions::Expression threeExpression;
33 storm::expressions::Expression piExpression;
34 storm::expressions::Expression boolVarExpression;
35 storm::expressions::Expression intVarExpression;
36 storm::expressions::Expression rationalVarExpression;
37
38 ASSERT_NO_THROW(trueExpression = manager->boolean(true));
39 ASSERT_NO_THROW(falseExpression = manager->boolean(false));
40 ASSERT_NO_THROW(threeExpression = manager->integer(3));
41 ASSERT_NO_THROW(piExpression = manager->rational(3.14));
42 ASSERT_NO_THROW(boolVarExpression = manager->declareBooleanVariable("x"));
43 ASSERT_NO_THROW(intVarExpression = manager->declareIntegerVariable("y"));
44 ASSERT_NO_THROW(rationalVarExpression = manager->declareRationalVariable("z"));
45
46 EXPECT_TRUE(trueExpression.hasBooleanType());
47 EXPECT_TRUE(trueExpression.isLiteral());
48 EXPECT_TRUE(trueExpression.isTrue());
49 EXPECT_FALSE(trueExpression.isFalse());
50 EXPECT_TRUE(trueExpression.getVariables() == std::set<storm::expressions::Variable>());
51
52 EXPECT_TRUE(falseExpression.hasBooleanType());
53 EXPECT_TRUE(falseExpression.isLiteral());
54 EXPECT_FALSE(falseExpression.isTrue());
55 EXPECT_TRUE(falseExpression.isFalse());
56 EXPECT_TRUE(falseExpression.getVariables() == std::set<storm::expressions::Variable>());
57
58 EXPECT_TRUE(threeExpression.hasIntegerType());
59 EXPECT_TRUE(threeExpression.isLiteral());
60 EXPECT_FALSE(threeExpression.isTrue());
61 EXPECT_FALSE(threeExpression.isFalse());
62 EXPECT_TRUE(threeExpression.getVariables() == std::set<storm::expressions::Variable>());
63
64 EXPECT_TRUE(piExpression.hasRationalType());
65 EXPECT_TRUE(piExpression.isLiteral());
66 EXPECT_FALSE(piExpression.isTrue());
67 EXPECT_FALSE(piExpression.isFalse());
68 EXPECT_TRUE(piExpression.getVariables() == std::set<storm::expressions::Variable>());
69
70 EXPECT_TRUE(boolVarExpression.hasBooleanType());
71 EXPECT_FALSE(boolVarExpression.isLiteral());
72 EXPECT_FALSE(boolVarExpression.isTrue());
73 EXPECT_FALSE(boolVarExpression.isFalse());
74 EXPECT_TRUE(boolVarExpression.getVariables() == std::set<storm::expressions::Variable>({manager->getVariable("x")}));
75
76 EXPECT_TRUE(intVarExpression.hasIntegerType());
77 EXPECT_FALSE(intVarExpression.isLiteral());
78 EXPECT_FALSE(intVarExpression.isTrue());
79 EXPECT_FALSE(intVarExpression.isFalse());
80 EXPECT_TRUE(intVarExpression.getVariables() == std::set<storm::expressions::Variable>({manager->getVariable("y")}));
81
82 EXPECT_TRUE(rationalVarExpression.hasRationalType());
83 EXPECT_FALSE(rationalVarExpression.isLiteral());
84 EXPECT_FALSE(rationalVarExpression.isTrue());
85 EXPECT_FALSE(rationalVarExpression.isFalse());
86 EXPECT_TRUE(rationalVarExpression.getVariables() == std::set<storm::expressions::Variable>({manager->getVariable("z")}));
87}
88
89TEST(Expression, OperatorTest) {
90 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
91
92 storm::expressions::Expression trueExpression;
93 storm::expressions::Expression falseExpression;
94 storm::expressions::Expression threeExpression;
95 storm::expressions::Expression piExpression;
96 storm::expressions::Expression boolVarExpression;
97 storm::expressions::Expression intVarExpression;
98 storm::expressions::Expression rationalVarExpression;
99
100 ASSERT_NO_THROW(trueExpression = manager->boolean(true));
101 ASSERT_NO_THROW(falseExpression = manager->boolean(false));
102 ASSERT_NO_THROW(threeExpression = manager->integer(3));
103 ASSERT_NO_THROW(piExpression = manager->rational(3.14));
104 ASSERT_NO_THROW(boolVarExpression = manager->declareBooleanVariable("x"));
105 ASSERT_NO_THROW(intVarExpression = manager->declareIntegerVariable("y"));
106 ASSERT_NO_THROW(rationalVarExpression = manager->declareRationalVariable("z"));
107
108 storm::expressions::Expression tempExpression;
109
110 STORM_SILENT_ASSERT_THROW(tempExpression = storm::expressions::ite(trueExpression, falseExpression, piExpression), storm::exceptions::InvalidTypeException);
111 ASSERT_NO_THROW(tempExpression = storm::expressions::ite(boolVarExpression, threeExpression, rationalVarExpression));
112 EXPECT_TRUE(tempExpression.hasRationalType());
113 ASSERT_NO_THROW(tempExpression = storm::expressions::ite(boolVarExpression, threeExpression, intVarExpression));
114 EXPECT_TRUE(tempExpression.hasIntegerType());
115 ASSERT_NO_THROW(tempExpression = storm::expressions::ite(boolVarExpression, trueExpression, falseExpression));
116 EXPECT_TRUE(tempExpression.hasBooleanType());
117
118 STORM_SILENT_ASSERT_THROW(tempExpression = trueExpression + piExpression, storm::exceptions::InvalidTypeException);
119 ASSERT_NO_THROW(tempExpression = threeExpression + threeExpression);
120 EXPECT_TRUE(tempExpression.hasIntegerType());
121 ASSERT_NO_THROW(tempExpression = threeExpression + piExpression);
122 EXPECT_TRUE(tempExpression.hasRationalType());
123 ASSERT_NO_THROW(tempExpression = rationalVarExpression + rationalVarExpression);
124 EXPECT_TRUE(tempExpression.hasRationalType());
125
126 STORM_SILENT_ASSERT_THROW(tempExpression = trueExpression - piExpression, storm::exceptions::InvalidTypeException);
127 ASSERT_NO_THROW(tempExpression = threeExpression - threeExpression);
128 EXPECT_TRUE(tempExpression.hasIntegerType());
129 ASSERT_NO_THROW(tempExpression = threeExpression - piExpression);
130 EXPECT_TRUE(tempExpression.hasRationalType());
131 ASSERT_NO_THROW(tempExpression = rationalVarExpression - rationalVarExpression);
132 EXPECT_TRUE(tempExpression.hasRationalType());
133
134 STORM_SILENT_ASSERT_THROW(tempExpression = -trueExpression, storm::exceptions::InvalidTypeException);
135 ASSERT_NO_THROW(tempExpression = -threeExpression);
136 EXPECT_TRUE(tempExpression.hasIntegerType());
137 ASSERT_NO_THROW(tempExpression = -piExpression);
138 EXPECT_TRUE(tempExpression.hasRationalType());
139 ASSERT_NO_THROW(tempExpression = -rationalVarExpression);
140 EXPECT_TRUE(tempExpression.hasRationalType());
141
142 STORM_SILENT_ASSERT_THROW(tempExpression = trueExpression * piExpression, storm::exceptions::InvalidTypeException);
143 ASSERT_NO_THROW(tempExpression = threeExpression * threeExpression);
144 EXPECT_TRUE(tempExpression.hasIntegerType());
145 ASSERT_NO_THROW(tempExpression = threeExpression * piExpression);
146 EXPECT_TRUE(tempExpression.hasRationalType());
147 ASSERT_NO_THROW(tempExpression = intVarExpression * intVarExpression);
148 EXPECT_TRUE(tempExpression.hasIntegerType());
149
150 STORM_SILENT_ASSERT_THROW(tempExpression = trueExpression / piExpression, storm::exceptions::InvalidTypeException);
151 ASSERT_NO_THROW(tempExpression = threeExpression / threeExpression);
152 EXPECT_TRUE(tempExpression.hasIntegerType());
153 ASSERT_NO_THROW(tempExpression = threeExpression / piExpression);
154 EXPECT_TRUE(tempExpression.hasRationalType());
155 ASSERT_NO_THROW(tempExpression = rationalVarExpression / intVarExpression);
156 EXPECT_TRUE(tempExpression.hasRationalType());
157
158 STORM_SILENT_ASSERT_THROW(tempExpression = trueExpression && piExpression, storm::exceptions::InvalidTypeException);
159 ASSERT_NO_THROW(tempExpression = trueExpression && falseExpression);
160 EXPECT_TRUE(tempExpression.hasBooleanType());
161 ASSERT_NO_THROW(tempExpression = boolVarExpression && boolVarExpression);
162 EXPECT_TRUE(tempExpression.hasBooleanType());
163
164 STORM_SILENT_ASSERT_THROW(tempExpression = trueExpression || piExpression, storm::exceptions::InvalidTypeException);
165 ASSERT_NO_THROW(tempExpression = trueExpression || falseExpression);
166 EXPECT_TRUE(tempExpression.hasBooleanType());
167 ASSERT_NO_THROW(tempExpression = boolVarExpression || boolVarExpression);
168 EXPECT_TRUE(tempExpression.hasBooleanType());
169
170 STORM_SILENT_ASSERT_THROW(tempExpression = !threeExpression, storm::exceptions::InvalidTypeException);
171 ASSERT_NO_THROW(tempExpression = !trueExpression);
172 EXPECT_TRUE(tempExpression.hasBooleanType());
173 ASSERT_NO_THROW(tempExpression = !boolVarExpression);
174 EXPECT_TRUE(tempExpression.hasBooleanType());
175
176 STORM_SILENT_ASSERT_THROW(tempExpression = trueExpression == piExpression, storm::exceptions::InvalidTypeException);
177 ASSERT_NO_THROW(tempExpression = threeExpression == threeExpression);
178 EXPECT_TRUE(tempExpression.hasBooleanType());
179 ASSERT_NO_THROW(tempExpression = intVarExpression == rationalVarExpression);
180 EXPECT_TRUE(tempExpression.hasBooleanType());
181
182 STORM_SILENT_ASSERT_THROW(tempExpression = trueExpression != piExpression, storm::exceptions::InvalidTypeException);
183 ASSERT_NO_THROW(tempExpression = threeExpression != threeExpression);
184 EXPECT_TRUE(tempExpression.hasBooleanType());
185 ASSERT_NO_THROW(tempExpression = intVarExpression != rationalVarExpression);
186 EXPECT_TRUE(tempExpression.hasBooleanType());
187
188 STORM_SILENT_ASSERT_THROW(tempExpression = trueExpression > piExpression, storm::exceptions::InvalidTypeException);
189 ASSERT_NO_THROW(tempExpression = threeExpression > threeExpression);
190 EXPECT_TRUE(tempExpression.hasBooleanType());
191 ASSERT_NO_THROW(tempExpression = intVarExpression > rationalVarExpression);
192 EXPECT_TRUE(tempExpression.hasBooleanType());
193
194 STORM_SILENT_ASSERT_THROW(tempExpression = trueExpression >= piExpression, storm::exceptions::InvalidTypeException);
195 ASSERT_NO_THROW(tempExpression = threeExpression >= threeExpression);
196 EXPECT_TRUE(tempExpression.hasBooleanType());
197 ASSERT_NO_THROW(tempExpression = intVarExpression >= rationalVarExpression);
198 EXPECT_TRUE(tempExpression.hasBooleanType());
199
200 STORM_SILENT_ASSERT_THROW(tempExpression = trueExpression < piExpression, storm::exceptions::InvalidTypeException);
201 ASSERT_NO_THROW(tempExpression = threeExpression < threeExpression);
202 EXPECT_TRUE(tempExpression.hasBooleanType());
203 ASSERT_NO_THROW(tempExpression = intVarExpression < rationalVarExpression);
204 EXPECT_TRUE(tempExpression.hasBooleanType());
205
206 STORM_SILENT_ASSERT_THROW(tempExpression = trueExpression <= piExpression, storm::exceptions::InvalidTypeException);
207 ASSERT_NO_THROW(tempExpression = threeExpression <= threeExpression);
208 EXPECT_TRUE(tempExpression.hasBooleanType());
209 ASSERT_NO_THROW(tempExpression = intVarExpression <= rationalVarExpression);
210 EXPECT_TRUE(tempExpression.hasBooleanType());
211
212 STORM_SILENT_ASSERT_THROW(tempExpression = trueExpression % piExpression, storm::exceptions::InvalidTypeException);
213 ASSERT_NO_THROW(tempExpression = threeExpression % threeExpression);
214 EXPECT_TRUE(tempExpression.hasIntegerType());
215 ASSERT_NO_THROW(tempExpression = threeExpression % piExpression);
216 EXPECT_TRUE(tempExpression.hasRationalType());
217 ASSERT_NO_THROW(tempExpression = piExpression % threeExpression);
218 EXPECT_TRUE(tempExpression.hasRationalType());
219 ASSERT_NO_THROW(tempExpression = piExpression % piExpression);
220 EXPECT_TRUE(tempExpression.hasRationalType());
221
222 STORM_SILENT_ASSERT_THROW(tempExpression = storm::expressions::modulo(trueExpression, piExpression), storm::exceptions::InvalidTypeException);
223 ASSERT_NO_THROW(tempExpression = storm::expressions::modulo(threeExpression, threeExpression));
224 EXPECT_TRUE(tempExpression.hasIntegerType());
225 ASSERT_NO_THROW(tempExpression = storm::expressions::modulo(threeExpression, piExpression));
226 EXPECT_TRUE(tempExpression.hasRationalType());
227 ASSERT_NO_THROW(tempExpression = storm::expressions::modulo(piExpression, threeExpression));
228 EXPECT_TRUE(tempExpression.hasRationalType());
229 ASSERT_NO_THROW(tempExpression = storm::expressions::modulo(piExpression, piExpression));
230 EXPECT_TRUE(tempExpression.hasRationalType());
231
232 STORM_SILENT_ASSERT_THROW(tempExpression = storm::expressions::minimum(trueExpression, piExpression), storm::exceptions::InvalidTypeException);
233 ASSERT_NO_THROW(tempExpression = storm::expressions::minimum(threeExpression, threeExpression));
234 EXPECT_TRUE(tempExpression.hasIntegerType());
235 ASSERT_NO_THROW(tempExpression = storm::expressions::minimum(intVarExpression, rationalVarExpression));
236 EXPECT_TRUE(tempExpression.hasRationalType());
237
238 STORM_SILENT_ASSERT_THROW(tempExpression = storm::expressions::maximum(trueExpression, piExpression), storm::exceptions::InvalidTypeException);
239 ASSERT_NO_THROW(tempExpression = storm::expressions::maximum(threeExpression, threeExpression));
240 EXPECT_TRUE(tempExpression.hasIntegerType());
241 ASSERT_NO_THROW(tempExpression = storm::expressions::maximum(intVarExpression, rationalVarExpression));
242 EXPECT_TRUE(tempExpression.hasRationalType());
243
244 STORM_SILENT_ASSERT_THROW(tempExpression = storm::expressions::implies(trueExpression, piExpression), storm::exceptions::InvalidTypeException);
245 ASSERT_NO_THROW(tempExpression = storm::expressions::implies(trueExpression, falseExpression));
246 EXPECT_TRUE(tempExpression.hasBooleanType());
247 ASSERT_NO_THROW(tempExpression = storm::expressions::implies(boolVarExpression, boolVarExpression));
248 EXPECT_TRUE(tempExpression.hasBooleanType());
249
250 STORM_SILENT_ASSERT_THROW(tempExpression = storm::expressions::iff(trueExpression, piExpression), storm::exceptions::InvalidTypeException);
251 ASSERT_NO_THROW(tempExpression = storm::expressions::iff(trueExpression, falseExpression));
252 EXPECT_TRUE(tempExpression.hasBooleanType());
253 ASSERT_NO_THROW(tempExpression = storm::expressions::iff(boolVarExpression, boolVarExpression));
254 EXPECT_TRUE(tempExpression.hasBooleanType());
255
256 STORM_SILENT_ASSERT_THROW(tempExpression = trueExpression != piExpression, storm::exceptions::InvalidTypeException);
257 ASSERT_NO_THROW(tempExpression = trueExpression != falseExpression);
258 EXPECT_TRUE(tempExpression.hasBooleanType());
259 ASSERT_NO_THROW(tempExpression = boolVarExpression != boolVarExpression);
260 EXPECT_TRUE(tempExpression.hasBooleanType());
261
262 STORM_SILENT_ASSERT_THROW(tempExpression = storm::expressions::floor(trueExpression), storm::exceptions::InvalidTypeException);
263 ASSERT_NO_THROW(tempExpression = storm::expressions::floor(threeExpression));
264 EXPECT_TRUE(tempExpression.hasIntegerType());
265 ASSERT_NO_THROW(tempExpression = storm::expressions::floor(rationalVarExpression));
266 EXPECT_TRUE(tempExpression.hasIntegerType());
267
268 STORM_SILENT_ASSERT_THROW(tempExpression = storm::expressions::ceil(trueExpression), storm::exceptions::InvalidTypeException);
269 ASSERT_NO_THROW(tempExpression = storm::expressions::ceil(threeExpression));
270 EXPECT_TRUE(tempExpression.hasIntegerType());
271 ASSERT_NO_THROW(tempExpression = storm::expressions::ceil(rationalVarExpression));
272 EXPECT_TRUE(tempExpression.hasIntegerType());
273
274 STORM_SILENT_ASSERT_THROW(tempExpression = storm::expressions::pow(trueExpression, piExpression), storm::exceptions::InvalidTypeException);
275 ASSERT_NO_THROW(tempExpression = storm::expressions::pow(threeExpression, threeExpression, true));
276 EXPECT_TRUE(tempExpression.hasIntegerType());
277 ASSERT_NO_THROW(tempExpression = storm::expressions::pow(threeExpression, threeExpression, false));
278 EXPECT_TRUE(tempExpression.hasRationalType());
279 ASSERT_NO_THROW(tempExpression = storm::expressions::pow(intVarExpression, rationalVarExpression));
280 EXPECT_TRUE(tempExpression.hasRationalType());
281
282 ASSERT_NO_THROW(tempExpression = storm::expressions::maximum(threeExpression, threeExpression));
283 EXPECT_TRUE(tempExpression.hasIntegerType());
284}
285
286TEST(Expression, SubstitutionTest) {
287 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
288
289 storm::expressions::Expression trueExpression;
290 storm::expressions::Expression falseExpression;
291 storm::expressions::Expression threeExpression;
292 storm::expressions::Expression piExpression;
293 storm::expressions::Expression boolVarExpression;
294 storm::expressions::Expression intVarExpression;
295 storm::expressions::Expression rationalVarExpression;
296
297 ASSERT_NO_THROW(trueExpression = manager->boolean(true));
298 ASSERT_NO_THROW(falseExpression = manager->boolean(false));
299 ASSERT_NO_THROW(threeExpression = manager->integer(3));
300 ASSERT_NO_THROW(piExpression = manager->rational(3.14));
301 ASSERT_NO_THROW(boolVarExpression = manager->declareBooleanVariable("x"));
302 ASSERT_NO_THROW(intVarExpression = manager->declareIntegerVariable("y"));
303 ASSERT_NO_THROW(rationalVarExpression = manager->declareRationalVariable("z"));
304
305 storm::expressions::Expression tempExpression;
306 ASSERT_NO_THROW(tempExpression = (intVarExpression < threeExpression || boolVarExpression) && boolVarExpression);
307 std::map<storm::expressions::Variable, storm::expressions::Expression> substution = {std::make_pair(manager->getVariable("y"), manager->rational(2.7)),
308 std::make_pair(manager->getVariable("x"), manager->boolean(true))};
309 storm::expressions::Expression substitutedExpression;
310 ASSERT_NO_THROW(substitutedExpression = tempExpression.substitute(substution));
311 EXPECT_TRUE(substitutedExpression.simplify().isTrue());
312}
313
314TEST(Expression, SimplificationTest) {
315 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
316
317 storm::expressions::Expression trueExpression;
318 storm::expressions::Expression falseExpression;
319 storm::expressions::Expression threeExpression;
320 storm::expressions::Expression intVarExpression;
321
322 ASSERT_NO_THROW(trueExpression = manager->boolean(true));
323 ASSERT_NO_THROW(falseExpression = manager->boolean(false));
324 ASSERT_NO_THROW(threeExpression = manager->integer(3));
325 ASSERT_NO_THROW(intVarExpression = manager->declareIntegerVariable("y"));
326
327 storm::expressions::Expression tempExpression;
328 storm::expressions::Expression simplifiedExpression;
329
330 ASSERT_NO_THROW(tempExpression = trueExpression || intVarExpression > threeExpression);
331 ASSERT_NO_THROW(simplifiedExpression = tempExpression.simplify());
332 EXPECT_TRUE(simplifiedExpression.isTrue());
333
334 ASSERT_NO_THROW(tempExpression = falseExpression && intVarExpression > threeExpression);
335 ASSERT_NO_THROW(simplifiedExpression = tempExpression.simplify());
336 EXPECT_TRUE(simplifiedExpression.isFalse());
337}
338
339TEST(Expression, SimpleEvaluationTest) {
340 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
341
342 storm::expressions::Expression trueExpression;
343 storm::expressions::Expression falseExpression;
344 storm::expressions::Expression threeExpression;
345 storm::expressions::Expression piExpression;
346 storm::expressions::Expression boolVarExpression;
347 storm::expressions::Expression intVarExpression;
348 storm::expressions::Expression rationalVarExpression;
349
350 ASSERT_NO_THROW(trueExpression = manager->boolean(true));
351 ASSERT_NO_THROW(falseExpression = manager->boolean(false));
352 ASSERT_NO_THROW(threeExpression = manager->integer(3));
353 ASSERT_NO_THROW(piExpression = manager->rational(3.14));
354 ASSERT_NO_THROW(boolVarExpression = manager->declareBooleanVariable("x"));
355 ASSERT_NO_THROW(intVarExpression = manager->declareIntegerVariable("y"));
356 ASSERT_NO_THROW(rationalVarExpression = manager->declareRationalVariable("z"));
357
358 storm::expressions::Expression tempExpression;
359
360 ASSERT_NO_THROW(tempExpression = (intVarExpression < threeExpression || boolVarExpression) && boolVarExpression);
361
362 ASSERT_NO_THROW(storm::expressions::SimpleValuation valuation(manager));
363 storm::expressions::SimpleValuation valuation(manager);
364 ASSERT_NO_THROW(valuation.setBooleanValue(manager->getVariable("x"), false));
365 ASSERT_NO_THROW(valuation.setIntegerValue(manager->getVariable("y"), 0));
366 ASSERT_NO_THROW(valuation.setRationalValue(manager->getVariable("z"), 0));
367
368 STORM_SILENT_ASSERT_THROW(tempExpression.evaluateAsDouble(&valuation), storm::exceptions::InvalidTypeException);
369 STORM_SILENT_ASSERT_THROW(tempExpression.evaluateAsInt(&valuation), storm::exceptions::InvalidTypeException);
370 EXPECT_FALSE(tempExpression.evaluateAsBool(&valuation));
371 ASSERT_NO_THROW(valuation.setIntegerValue(manager->getVariable("y"), 3));
372 EXPECT_FALSE(tempExpression.evaluateAsBool(&valuation));
373
374 ASSERT_NO_THROW(tempExpression = storm::expressions::ite(intVarExpression < threeExpression, trueExpression, falseExpression));
375 STORM_SILENT_ASSERT_THROW(tempExpression.evaluateAsDouble(&valuation), storm::exceptions::InvalidTypeException);
376 STORM_SILENT_ASSERT_THROW(tempExpression.evaluateAsInt(&valuation), storm::exceptions::InvalidTypeException);
377 EXPECT_FALSE(tempExpression.evaluateAsBool(&valuation));
378}
379
380TEST(Expression, VisitorTest) {
381 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
382
383 storm::expressions::Expression threeExpression;
384 storm::expressions::Expression piExpression;
385 storm::expressions::Expression intVarExpression;
386 storm::expressions::Expression rationalVarExpression;
387
388 ASSERT_NO_THROW(threeExpression = manager->integer(3));
389 ASSERT_NO_THROW(piExpression = manager->rational(3.14));
390 ASSERT_NO_THROW(intVarExpression = manager->declareIntegerVariable("y"));
391 ASSERT_NO_THROW(rationalVarExpression = manager->declareRationalVariable("z"));
392
393 storm::expressions::Expression tempExpression = intVarExpression + rationalVarExpression * threeExpression;
394 storm::expressions::LinearityCheckVisitor visitor;
395 EXPECT_TRUE(visitor.check(tempExpression));
396}
397
398TEST(Expression, RationalFunctionToExpressionTest) {
399 storm::parser::ValueParser<storm::RationalFunction> parser;
400 parser.addParameter("p");
401 parser.addParameter("q");
402 auto rationalFunction = parser.parseValue("((5*p^(3))+(q*p*7)+2)/2");
403
404 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
405 auto transformer = storm::expressions::RationalFunctionToExpression<storm::RationalFunction>(manager);
406
407 storm::expressions::Expression expr;
408 EXPECT_NO_THROW(expr = transformer.toExpression(rationalFunction));
409 auto base = storm::expressions::ExpressionEvaluator<storm::RationalFunction>(*manager);
410 storm::expressions::ToRationalFunctionVisitor<storm::RationalFunction> visitor(base);
411 ASSERT_NO_THROW(rationalFunction.simplify());
412 storm::RationalFunction result;
413 ASSERT_NO_THROW(result = visitor.toRationalFunction(expr));
414 ASSERT_NO_THROW(result.simplify());
415 EXPECT_EQ(rationalFunction.toString(), result.toString());
416
417 rationalFunction = parser.parseValue("(5*((p^(3))+(q*p)))/2");
418 transformer = storm::expressions::RationalFunctionToExpression<storm::RationalFunction>(manager);
419 EXPECT_NO_THROW(expr = transformer.toExpression(rationalFunction));
420 ASSERT_NO_THROW(rationalFunction.simplify());
421 ASSERT_NO_THROW(result = visitor.toRationalFunction(expr));
422 ASSERT_NO_THROW(result.simplify());
423 EXPECT_EQ(rationalFunction.toString(), result.toString());
424}
425
426TEST(Expression, RationalFunctionToExpressionTest_no_params) {
427 storm::parser::ValueParser<storm::RationalFunction> parser;
428 parser.addParameter("p");
429 auto rationalFunction1 = parser.parseValue("(p + 380)/3125");
430 auto rationalFunction2 = parser.parseValue("(p)/3125");
431 auto rationalFunction = rationalFunction1 - rationalFunction2;
432
433 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
434 auto transformer = storm::expressions::RationalFunctionToExpression<storm::RationalFunction>(manager);
435
436 storm::expressions::Expression expr;
437 EXPECT_NO_THROW(expr = transformer.toExpression(rationalFunction));
438 auto base = storm::expressions::ExpressionEvaluator<storm::RationalFunction>(*manager);
439 storm::expressions::ToRationalFunctionVisitor<storm::RationalFunction> visitor(base);
440 ASSERT_NO_THROW(rationalFunction.simplify());
441 storm::RationalFunction result;
442 ASSERT_NO_THROW(result = visitor.toRationalFunction(expr));
443 ASSERT_NO_THROW(result.simplify());
444 EXPECT_EQ(rationalFunction.toString(), result.toString());
445}
TEST
TEST(Expression, FactoryMethodTest)
Definition ExpressionTest.cpp:16
storm::expressions::Expression::simplify
Expression simplify() const
Simplifies the expression according to some basic rules.
Definition Expression.cpp:78
storm::expressions::Expression::evaluateAsInt
int_fast64_t evaluateAsInt(Valuation const *valuation=nullptr) const
Evaluates the expression under the valuation of variables given by the valuation and returns the resu...
Definition Expression.cpp:66
storm::expressions::Expression::evaluateAsBool
bool evaluateAsBool(Valuation const *valuation=nullptr) const
Evaluates the expression under the valuation of variables given by the valuation and returns the resu...
Definition Expression.cpp:62
storm::expressions::Expression::evaluateAsDouble
double evaluateAsDouble(Valuation const *valuation=nullptr) const
Evaluates the expression under the valuation of variables given by the valuation and returns the resu...
Definition Expression.cpp:70
storm::expressions::Expression::hasBooleanType
bool hasBooleanType() const
Retrieves whether the expression has a boolean return type.
Definition Expression.cpp:193
storm::expressions::Expression::isFalse
bool isFalse() const
Checks if the expression is equal to the boolean literal false.
Definition Expression.cpp:122
storm::expressions::Expression::getVariables
std::set< storm::expressions::Variable > getVariables() const
Retrieves the set of all variables that appear in the expression.
Definition Expression.cpp:130
storm::expressions::Expression::hasIntegerType
bool hasIntegerType() const
Retrieves whether the expression has an integral return type.
Definition Expression.cpp:197
storm::expressions::Expression::isLiteral
bool isLiteral() const
Retrieves whether the expression is a literal.
Definition Expression.cpp:110
storm::expressions::Expression::substitute
Expression substitute(std::map< Variable, Expression > const &variableToExpressionMap) const
Substitutes all occurrences of the variables according to the given map.
Definition Expression.cpp:50
storm::expressions::Expression::hasRationalType
bool hasRationalType() const
Retrieves whether the expression has a rational return type.
Definition Expression.cpp:189
storm::expressions::Expression::isTrue
bool isTrue() const
Checks if the expression is equal to the boolean literal true.
Definition Expression.cpp:118
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::expressions::LinearityCheckVisitor::check
bool check(Expression const &expression, bool booleanIsLinear=false)
Checks that the given expression is linear.
Definition LinearityCheckVisitor.cpp:15
storm::expressions::SimpleValuation
A simple implementation of the valuation interface.
Definition SimpleValuation.h:18
storm::expressions::SimpleValuation::setIntegerValue
virtual void setIntegerValue(Variable const &integerVariable, int_fast64_t value) override
Sets the value of the given integer variable to the provided value.
Definition SimpleValuation.cpp:89
storm::expressions::SimpleValuation::setBooleanValue
virtual void setBooleanValue(Variable const &booleanVariable, bool value) override
Sets the value of the given boolean variable to the provided value.
Definition SimpleValuation.cpp:85
storm::expressions::SimpleValuation::setRationalValue
virtual void setRationalValue(Variable const &rationalVariable, double value) override
Sets the value of the given boolean variable to the provided value.
Definition SimpleValuation.cpp:97
storm::parser::ValueParser
Parser for values according to their ValueType.
Definition ValueParser.h:23
storm::parser::ValueParser::addParameter
void addParameter(std::string const &parameter)
Add declaration of parameter.
Definition ValueParser.cpp:28
storm::parser::ValueParser::parseValue
ValueType parseValue(std::string const &value) const
Parse ValueType from string.
Definition ValueParser.cpp:48
storm::expressions::maximum
Expression maximum(Expression const &first, Expression const &second)
Definition Expression.cpp:418
storm::expressions::ceil
Expression ceil(Expression const &first)
Definition Expression.cpp:468
storm::expressions::ite
Expression ite(Expression const &condition, Expression const &thenExpression, Expression const &elseExpression)
Definition Expression.cpp:425
storm::expressions::iff
Expression iff(Expression const &first, Expression const &second)
Definition Expression.cpp:440
storm::expressions::minimum
Expression minimum(Expression const &first, Expression const &second)
Definition Expression.cpp:411
storm::expressions::floor
Expression floor(Expression const &first)
Definition Expression.cpp:461
storm::expressions::pow
Expression pow(Expression const &base, Expression const &exponent, bool allowIntegerType)
The type of the resulting expression is.
Definition Expression.cpp:454
storm::expressions::implies
Expression implies(Expression const &first, Expression const &second)
Definition Expression.cpp:433
storm::expressions::modulo
Expression modulo(Expression const &first, Expression const &second)
Definition Expression.cpp:540
storm_gtest.h
STORM_SILENT_ASSERT_THROW
#define STORM_SILENT_ASSERT_THROW(statement, expected_exception)
Definition storm_gtest.h:99