Storm
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
308#ifdef WINDOWS
309 storm::expressions::Expression twopointseven = manager->rational(2.7);
310 std::map<storm::expressions::Variable, storm::expressions::Expression> substution = {std::make_pair(manager->getVariable("y"), twopointseven),
311 std::make_pair(manager->getVariable("x"), manager->boolean(true))};
312#else
313 std::map<storm::expressions::Variable, storm::expressions::Expression> substution = {std::make_pair(manager->getVariable("y"), manager->rational(2.7)),
314 std::make_pair(manager->getVariable("x"), manager->boolean(true))};
315#endif
316 storm::expressions::Expression substitutedExpression;
317 ASSERT_NO_THROW(substitutedExpression = tempExpression.substitute(substution));
318 EXPECT_TRUE(substitutedExpression.simplify().isTrue());
319}
320
321TEST(Expression, SimplificationTest) {
322 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
323
324 storm::expressions::Expression trueExpression;
325 storm::expressions::Expression falseExpression;
326 storm::expressions::Expression threeExpression;
327 storm::expressions::Expression intVarExpression;
328
329 ASSERT_NO_THROW(trueExpression = manager->boolean(true));
330 ASSERT_NO_THROW(falseExpression = manager->boolean(false));
331 ASSERT_NO_THROW(threeExpression = manager->integer(3));
332 ASSERT_NO_THROW(intVarExpression = manager->declareIntegerVariable("y"));
333
334 storm::expressions::Expression tempExpression;
335 storm::expressions::Expression simplifiedExpression;
336
337 ASSERT_NO_THROW(tempExpression = trueExpression || intVarExpression > threeExpression);
338 ASSERT_NO_THROW(simplifiedExpression = tempExpression.simplify());
339 EXPECT_TRUE(simplifiedExpression.isTrue());
340
341 ASSERT_NO_THROW(tempExpression = falseExpression && intVarExpression > threeExpression);
342 ASSERT_NO_THROW(simplifiedExpression = tempExpression.simplify());
343 EXPECT_TRUE(simplifiedExpression.isFalse());
344}
345
346TEST(Expression, SimpleEvaluationTest) {
347 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
348
349 storm::expressions::Expression trueExpression;
350 storm::expressions::Expression falseExpression;
351 storm::expressions::Expression threeExpression;
352 storm::expressions::Expression piExpression;
353 storm::expressions::Expression boolVarExpression;
354 storm::expressions::Expression intVarExpression;
355 storm::expressions::Expression rationalVarExpression;
356
357 ASSERT_NO_THROW(trueExpression = manager->boolean(true));
358 ASSERT_NO_THROW(falseExpression = manager->boolean(false));
359 ASSERT_NO_THROW(threeExpression = manager->integer(3));
360 ASSERT_NO_THROW(piExpression = manager->rational(3.14));
361 ASSERT_NO_THROW(boolVarExpression = manager->declareBooleanVariable("x"));
362 ASSERT_NO_THROW(intVarExpression = manager->declareIntegerVariable("y"));
363 ASSERT_NO_THROW(rationalVarExpression = manager->declareRationalVariable("z"));
364
365 storm::expressions::Expression tempExpression;
366
367 ASSERT_NO_THROW(tempExpression = (intVarExpression < threeExpression || boolVarExpression) && boolVarExpression);
368
369 ASSERT_NO_THROW(storm::expressions::SimpleValuation valuation(manager));
370 storm::expressions::SimpleValuation valuation(manager);
371 ASSERT_NO_THROW(valuation.setBooleanValue(manager->getVariable("x"), false));
372 ASSERT_NO_THROW(valuation.setIntegerValue(manager->getVariable("y"), 0));
373 ASSERT_NO_THROW(valuation.setRationalValue(manager->getVariable("z"), 0));
374
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 ASSERT_NO_THROW(valuation.setIntegerValue(manager->getVariable("y"), 3));
379 EXPECT_FALSE(tempExpression.evaluateAsBool(&valuation));
380
381 ASSERT_NO_THROW(tempExpression = storm::expressions::ite(intVarExpression < threeExpression, trueExpression, falseExpression));
382 STORM_SILENT_ASSERT_THROW(tempExpression.evaluateAsDouble(&valuation), storm::exceptions::InvalidTypeException);
383 STORM_SILENT_ASSERT_THROW(tempExpression.evaluateAsInt(&valuation), storm::exceptions::InvalidTypeException);
384 EXPECT_FALSE(tempExpression.evaluateAsBool(&valuation));
385}
386
387TEST(Expression, VisitorTest) {
388 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
389
390 storm::expressions::Expression threeExpression;
391 storm::expressions::Expression piExpression;
392 storm::expressions::Expression intVarExpression;
393 storm::expressions::Expression rationalVarExpression;
394
395 ASSERT_NO_THROW(threeExpression = manager->integer(3));
396 ASSERT_NO_THROW(piExpression = manager->rational(3.14));
397 ASSERT_NO_THROW(intVarExpression = manager->declareIntegerVariable("y"));
398 ASSERT_NO_THROW(rationalVarExpression = manager->declareRationalVariable("z"));
399
400 storm::expressions::Expression tempExpression = intVarExpression + rationalVarExpression * threeExpression;
401 storm::expressions::LinearityCheckVisitor visitor;
402 EXPECT_TRUE(visitor.check(tempExpression));
403}
404
405TEST(Expression, RationalFunctionToExpressionTest) {
406 storm::parser::ValueParser<storm::RationalFunction> parser;
407 parser.addParameter("p");
408 parser.addParameter("q");
409 auto rationalFunction = parser.parseValue("((5*p^(3))+(q*p*7)+2)/2");
410
411 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
412 auto transformer = storm::expressions::RationalFunctionToExpression<storm::RationalFunction>(manager);
413
414 storm::expressions::Expression expr;
415 EXPECT_NO_THROW(expr = transformer.toExpression(rationalFunction));
416 auto base = storm::expressions::ExpressionEvaluator<storm::RationalFunction>(*manager);
417 storm::expressions::ToRationalFunctionVisitor<storm::RationalFunction> visitor(base);
418 ASSERT_NO_THROW(rationalFunction.simplify());
419 storm::RationalFunction result;
420 ASSERT_NO_THROW(result = visitor.toRationalFunction(expr));
421 ASSERT_NO_THROW(result.simplify());
422 EXPECT_EQ(rationalFunction.toString(), result.toString());
423
424 rationalFunction = parser.parseValue("(5*((p^(3))+(q*p)))/2");
425 transformer = storm::expressions::RationalFunctionToExpression<storm::RationalFunction>(manager);
426 EXPECT_NO_THROW(expr = transformer.toExpression(rationalFunction));
427 ASSERT_NO_THROW(rationalFunction.simplify());
428 ASSERT_NO_THROW(result = visitor.toRationalFunction(expr));
429 ASSERT_NO_THROW(result.simplify());
430 EXPECT_EQ(rationalFunction.toString(), result.toString());
431}
432
433TEST(Expression, RationalFunctionToExpressionTest_no_params) {
434 storm::parser::ValueParser<storm::RationalFunction> parser;
435 parser.addParameter("p");
436 auto rationalFunction1 = parser.parseValue("(p + 380)/3125");
437 auto rationalFunction2 = parser.parseValue("(p)/3125");
438 auto rationalFunction = rationalFunction1 - rationalFunction2;
439
440 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
441 auto transformer = storm::expressions::RationalFunctionToExpression<storm::RationalFunction>(manager);
442
443 storm::expressions::Expression expr;
444 EXPECT_NO_THROW(expr = transformer.toExpression(rationalFunction));
445 auto base = storm::expressions::ExpressionEvaluator<storm::RationalFunction>(*manager);
446 storm::expressions::ToRationalFunctionVisitor<storm::RationalFunction> visitor(base);
447 ASSERT_NO_THROW(rationalFunction.simplify());
448 storm::RationalFunction result;
449 ASSERT_NO_THROW(result = visitor.toRationalFunction(expr));
450 ASSERT_NO_THROW(result.simplify());
451 EXPECT_EQ(rationalFunction.toString(), result.toString());
452}
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