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