Storm 1.14.0.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/JsonAdapter.h"
9#include "storm/adapters/RationalFunctionAdapter.h"
10#include "storm/exceptions/InvalidArgumentException.h"
11#include "storm/exceptions/InvalidTypeException.h"
12#include "storm/storage/expressions/Expression.h"
13#include "storm/storage/expressions/ExpressionEvaluator.h"
14#include "storm/storage/expressions/ExpressionManager.h"
15#include "storm/storage/expressions/LinearCoefficientVisitor.h"
16#include "storm/storage/expressions/LinearityCheckVisitor.h"
17#include "storm/storage/expressions/RationalFunctionToExpression.h"
18#include "storm/storage/expressions/SimpleValuation.h"
19#include "storm/storage/expressions/ToRationalFunctionVisitor.h"
20
21TEST(Expression, FactoryMethodTest) {
22 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
23 EXPECT_NO_THROW(manager->boolean(true));
24 EXPECT_NO_THROW(manager->boolean(false));
25 EXPECT_NO_THROW(manager->integer(3));
26 EXPECT_NO_THROW(manager->rational(3.14));
27 EXPECT_NO_THROW(manager->declareBooleanVariable("x"));
28 EXPECT_NO_THROW(manager->declareIntegerVariable("y"));
29 EXPECT_NO_THROW(manager->declareRationalVariable("z"));
30}
31
32TEST(Expression, AccessorTest) {
33 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
34
35 storm::expressions::Expression trueExpression;
36 storm::expressions::Expression falseExpression;
37 storm::expressions::Expression threeExpression;
38 storm::expressions::Expression piExpression;
39 storm::expressions::Expression boolVarExpression;
40 storm::expressions::Expression intVarExpression;
41 storm::expressions::Expression rationalVarExpression;
42
43 ASSERT_NO_THROW(trueExpression = manager->boolean(true));
44 ASSERT_NO_THROW(falseExpression = manager->boolean(false));
45 ASSERT_NO_THROW(threeExpression = manager->integer(3));
46 ASSERT_NO_THROW(piExpression = manager->rational(3.14));
47 ASSERT_NO_THROW(boolVarExpression = manager->declareBooleanVariable("x"));
48 ASSERT_NO_THROW(intVarExpression = manager->declareIntegerVariable("y"));
49 ASSERT_NO_THROW(rationalVarExpression = manager->declareRationalVariable("z"));
50
51 EXPECT_TRUE(trueExpression.hasBooleanType());
52 EXPECT_TRUE(trueExpression.isLiteral());
53 EXPECT_TRUE(trueExpression.isTrue());
54 EXPECT_FALSE(trueExpression.isFalse());
55 EXPECT_TRUE(trueExpression.getVariables() == std::set<storm::expressions::Variable>());
56
57 EXPECT_TRUE(falseExpression.hasBooleanType());
58 EXPECT_TRUE(falseExpression.isLiteral());
59 EXPECT_FALSE(falseExpression.isTrue());
60 EXPECT_TRUE(falseExpression.isFalse());
61 EXPECT_TRUE(falseExpression.getVariables() == std::set<storm::expressions::Variable>());
62
63 EXPECT_TRUE(threeExpression.hasIntegerType());
64 EXPECT_TRUE(threeExpression.isLiteral());
65 EXPECT_FALSE(threeExpression.isTrue());
66 EXPECT_FALSE(threeExpression.isFalse());
67 EXPECT_TRUE(threeExpression.getVariables() == std::set<storm::expressions::Variable>());
68
69 EXPECT_TRUE(piExpression.hasRationalType());
70 EXPECT_TRUE(piExpression.isLiteral());
71 EXPECT_FALSE(piExpression.isTrue());
72 EXPECT_FALSE(piExpression.isFalse());
73 EXPECT_TRUE(piExpression.getVariables() == std::set<storm::expressions::Variable>());
74
75 EXPECT_TRUE(boolVarExpression.hasBooleanType());
76 EXPECT_FALSE(boolVarExpression.isLiteral());
77 EXPECT_FALSE(boolVarExpression.isTrue());
78 EXPECT_FALSE(boolVarExpression.isFalse());
79 EXPECT_TRUE(boolVarExpression.getVariables() == std::set<storm::expressions::Variable>({manager->getVariable("x")}));
80
81 EXPECT_TRUE(intVarExpression.hasIntegerType());
82 EXPECT_FALSE(intVarExpression.isLiteral());
83 EXPECT_FALSE(intVarExpression.isTrue());
84 EXPECT_FALSE(intVarExpression.isFalse());
85 EXPECT_TRUE(intVarExpression.getVariables() == std::set<storm::expressions::Variable>({manager->getVariable("y")}));
86
87 EXPECT_TRUE(rationalVarExpression.hasRationalType());
88 EXPECT_FALSE(rationalVarExpression.isLiteral());
89 EXPECT_FALSE(rationalVarExpression.isTrue());
90 EXPECT_FALSE(rationalVarExpression.isFalse());
91 EXPECT_TRUE(rationalVarExpression.getVariables() == std::set<storm::expressions::Variable>({manager->getVariable("z")}));
92}
93
94TEST(Expression, OperatorTest) {
95 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
96
97 storm::expressions::Expression trueExpression;
98 storm::expressions::Expression falseExpression;
99 storm::expressions::Expression threeExpression;
100 storm::expressions::Expression piExpression;
101 storm::expressions::Expression boolVarExpression;
102 storm::expressions::Expression intVarExpression;
103 storm::expressions::Expression rationalVarExpression;
104
105 ASSERT_NO_THROW(trueExpression = manager->boolean(true));
106 ASSERT_NO_THROW(falseExpression = manager->boolean(false));
107 ASSERT_NO_THROW(threeExpression = manager->integer(3));
108 ASSERT_NO_THROW(piExpression = manager->rational(3.14));
109 ASSERT_NO_THROW(boolVarExpression = manager->declareBooleanVariable("x"));
110 ASSERT_NO_THROW(intVarExpression = manager->declareIntegerVariable("y"));
111 ASSERT_NO_THROW(rationalVarExpression = manager->declareRationalVariable("z"));
112
113 storm::expressions::Expression tempExpression;
114
115 STORM_SILENT_ASSERT_THROW(tempExpression = storm::expressions::ite(trueExpression, falseExpression, piExpression), storm::exceptions::InvalidTypeException);
116 ASSERT_NO_THROW(tempExpression = storm::expressions::ite(boolVarExpression, threeExpression, rationalVarExpression));
117 EXPECT_TRUE(tempExpression.hasRationalType());
118 ASSERT_NO_THROW(tempExpression = storm::expressions::ite(boolVarExpression, threeExpression, intVarExpression));
119 EXPECT_TRUE(tempExpression.hasIntegerType());
120 ASSERT_NO_THROW(tempExpression = storm::expressions::ite(boolVarExpression, trueExpression, falseExpression));
121 EXPECT_TRUE(tempExpression.hasBooleanType());
122
123 STORM_SILENT_ASSERT_THROW(tempExpression = trueExpression + piExpression, storm::exceptions::InvalidTypeException);
124 ASSERT_NO_THROW(tempExpression = threeExpression + threeExpression);
125 EXPECT_TRUE(tempExpression.hasIntegerType());
126 ASSERT_NO_THROW(tempExpression = threeExpression + piExpression);
127 EXPECT_TRUE(tempExpression.hasRationalType());
128 ASSERT_NO_THROW(tempExpression = rationalVarExpression + rationalVarExpression);
129 EXPECT_TRUE(tempExpression.hasRationalType());
130
131 STORM_SILENT_ASSERT_THROW(tempExpression = trueExpression - piExpression, storm::exceptions::InvalidTypeException);
132 ASSERT_NO_THROW(tempExpression = threeExpression - threeExpression);
133 EXPECT_TRUE(tempExpression.hasIntegerType());
134 ASSERT_NO_THROW(tempExpression = threeExpression - piExpression);
135 EXPECT_TRUE(tempExpression.hasRationalType());
136 ASSERT_NO_THROW(tempExpression = rationalVarExpression - rationalVarExpression);
137 EXPECT_TRUE(tempExpression.hasRationalType());
138
139 STORM_SILENT_ASSERT_THROW(tempExpression = -trueExpression, storm::exceptions::InvalidTypeException);
140 ASSERT_NO_THROW(tempExpression = -threeExpression);
141 EXPECT_TRUE(tempExpression.hasIntegerType());
142 ASSERT_NO_THROW(tempExpression = -piExpression);
143 EXPECT_TRUE(tempExpression.hasRationalType());
144 ASSERT_NO_THROW(tempExpression = -rationalVarExpression);
145 EXPECT_TRUE(tempExpression.hasRationalType());
146
147 STORM_SILENT_ASSERT_THROW(tempExpression = trueExpression * piExpression, storm::exceptions::InvalidTypeException);
148 ASSERT_NO_THROW(tempExpression = threeExpression * threeExpression);
149 EXPECT_TRUE(tempExpression.hasIntegerType());
150 ASSERT_NO_THROW(tempExpression = threeExpression * piExpression);
151 EXPECT_TRUE(tempExpression.hasRationalType());
152 ASSERT_NO_THROW(tempExpression = intVarExpression * intVarExpression);
153 EXPECT_TRUE(tempExpression.hasIntegerType());
154
155 STORM_SILENT_ASSERT_THROW(tempExpression = trueExpression / piExpression, storm::exceptions::InvalidTypeException);
156 ASSERT_NO_THROW(tempExpression = threeExpression / threeExpression);
157 EXPECT_TRUE(tempExpression.hasIntegerType());
158 ASSERT_NO_THROW(tempExpression = threeExpression / piExpression);
159 EXPECT_TRUE(tempExpression.hasRationalType());
160 ASSERT_NO_THROW(tempExpression = rationalVarExpression / intVarExpression);
161 EXPECT_TRUE(tempExpression.hasRationalType());
162
163 STORM_SILENT_ASSERT_THROW(tempExpression = trueExpression && piExpression, storm::exceptions::InvalidTypeException);
164 ASSERT_NO_THROW(tempExpression = trueExpression && falseExpression);
165 EXPECT_TRUE(tempExpression.hasBooleanType());
166 ASSERT_NO_THROW(tempExpression = boolVarExpression && boolVarExpression);
167 EXPECT_TRUE(tempExpression.hasBooleanType());
168
169 STORM_SILENT_ASSERT_THROW(tempExpression = trueExpression || piExpression, storm::exceptions::InvalidTypeException);
170 ASSERT_NO_THROW(tempExpression = trueExpression || falseExpression);
171 EXPECT_TRUE(tempExpression.hasBooleanType());
172 ASSERT_NO_THROW(tempExpression = boolVarExpression || boolVarExpression);
173 EXPECT_TRUE(tempExpression.hasBooleanType());
174
175 STORM_SILENT_ASSERT_THROW(tempExpression = !threeExpression, storm::exceptions::InvalidTypeException);
176 ASSERT_NO_THROW(tempExpression = !trueExpression);
177 EXPECT_TRUE(tempExpression.hasBooleanType());
178 ASSERT_NO_THROW(tempExpression = !boolVarExpression);
179 EXPECT_TRUE(tempExpression.hasBooleanType());
180
181 STORM_SILENT_ASSERT_THROW(tempExpression = trueExpression == piExpression, storm::exceptions::InvalidTypeException);
182 ASSERT_NO_THROW(tempExpression = threeExpression == threeExpression);
183 EXPECT_TRUE(tempExpression.hasBooleanType());
184 ASSERT_NO_THROW(tempExpression = intVarExpression == rationalVarExpression);
185 EXPECT_TRUE(tempExpression.hasBooleanType());
186
187 STORM_SILENT_ASSERT_THROW(tempExpression = trueExpression != piExpression, storm::exceptions::InvalidTypeException);
188 ASSERT_NO_THROW(tempExpression = threeExpression != threeExpression);
189 EXPECT_TRUE(tempExpression.hasBooleanType());
190 ASSERT_NO_THROW(tempExpression = intVarExpression != rationalVarExpression);
191 EXPECT_TRUE(tempExpression.hasBooleanType());
192
193 STORM_SILENT_ASSERT_THROW(tempExpression = trueExpression > piExpression, storm::exceptions::InvalidTypeException);
194 ASSERT_NO_THROW(tempExpression = threeExpression > threeExpression);
195 EXPECT_TRUE(tempExpression.hasBooleanType());
196 ASSERT_NO_THROW(tempExpression = intVarExpression > rationalVarExpression);
197 EXPECT_TRUE(tempExpression.hasBooleanType());
198
199 STORM_SILENT_ASSERT_THROW(tempExpression = trueExpression >= piExpression, storm::exceptions::InvalidTypeException);
200 ASSERT_NO_THROW(tempExpression = threeExpression >= threeExpression);
201 EXPECT_TRUE(tempExpression.hasBooleanType());
202 ASSERT_NO_THROW(tempExpression = intVarExpression >= rationalVarExpression);
203 EXPECT_TRUE(tempExpression.hasBooleanType());
204
205 STORM_SILENT_ASSERT_THROW(tempExpression = trueExpression < piExpression, storm::exceptions::InvalidTypeException);
206 ASSERT_NO_THROW(tempExpression = threeExpression < threeExpression);
207 EXPECT_TRUE(tempExpression.hasBooleanType());
208 ASSERT_NO_THROW(tempExpression = intVarExpression < rationalVarExpression);
209 EXPECT_TRUE(tempExpression.hasBooleanType());
210
211 STORM_SILENT_ASSERT_THROW(tempExpression = trueExpression <= piExpression, storm::exceptions::InvalidTypeException);
212 ASSERT_NO_THROW(tempExpression = threeExpression <= threeExpression);
213 EXPECT_TRUE(tempExpression.hasBooleanType());
214 ASSERT_NO_THROW(tempExpression = intVarExpression <= rationalVarExpression);
215 EXPECT_TRUE(tempExpression.hasBooleanType());
216
217 STORM_SILENT_ASSERT_THROW(tempExpression = trueExpression % piExpression, storm::exceptions::InvalidTypeException);
218 ASSERT_NO_THROW(tempExpression = threeExpression % threeExpression);
219 EXPECT_TRUE(tempExpression.hasIntegerType());
220 ASSERT_NO_THROW(tempExpression = threeExpression % piExpression);
221 EXPECT_TRUE(tempExpression.hasRationalType());
222 ASSERT_NO_THROW(tempExpression = piExpression % threeExpression);
223 EXPECT_TRUE(tempExpression.hasRationalType());
224 ASSERT_NO_THROW(tempExpression = piExpression % piExpression);
225 EXPECT_TRUE(tempExpression.hasRationalType());
226
227 STORM_SILENT_ASSERT_THROW(tempExpression = storm::expressions::modulo(trueExpression, piExpression), storm::exceptions::InvalidTypeException);
228 ASSERT_NO_THROW(tempExpression = storm::expressions::modulo(threeExpression, threeExpression));
229 EXPECT_TRUE(tempExpression.hasIntegerType());
230 ASSERT_NO_THROW(tempExpression = storm::expressions::modulo(threeExpression, piExpression));
231 EXPECT_TRUE(tempExpression.hasRationalType());
232 ASSERT_NO_THROW(tempExpression = storm::expressions::modulo(piExpression, threeExpression));
233 EXPECT_TRUE(tempExpression.hasRationalType());
234 ASSERT_NO_THROW(tempExpression = storm::expressions::modulo(piExpression, piExpression));
235 EXPECT_TRUE(tempExpression.hasRationalType());
236
237 STORM_SILENT_ASSERT_THROW(tempExpression = storm::expressions::minimum(trueExpression, piExpression), storm::exceptions::InvalidTypeException);
238 ASSERT_NO_THROW(tempExpression = storm::expressions::minimum(threeExpression, threeExpression));
239 EXPECT_TRUE(tempExpression.hasIntegerType());
240 ASSERT_NO_THROW(tempExpression = storm::expressions::minimum(intVarExpression, rationalVarExpression));
241 EXPECT_TRUE(tempExpression.hasRationalType());
242
243 STORM_SILENT_ASSERT_THROW(tempExpression = storm::expressions::maximum(trueExpression, piExpression), storm::exceptions::InvalidTypeException);
244 ASSERT_NO_THROW(tempExpression = storm::expressions::maximum(threeExpression, threeExpression));
245 EXPECT_TRUE(tempExpression.hasIntegerType());
246 ASSERT_NO_THROW(tempExpression = storm::expressions::maximum(intVarExpression, rationalVarExpression));
247 EXPECT_TRUE(tempExpression.hasRationalType());
248
249 STORM_SILENT_ASSERT_THROW(tempExpression = storm::expressions::implies(trueExpression, piExpression), storm::exceptions::InvalidTypeException);
250 ASSERT_NO_THROW(tempExpression = storm::expressions::implies(trueExpression, falseExpression));
251 EXPECT_TRUE(tempExpression.hasBooleanType());
252 ASSERT_NO_THROW(tempExpression = storm::expressions::implies(boolVarExpression, boolVarExpression));
253 EXPECT_TRUE(tempExpression.hasBooleanType());
254
255 STORM_SILENT_ASSERT_THROW(tempExpression = storm::expressions::iff(trueExpression, piExpression), storm::exceptions::InvalidTypeException);
256 ASSERT_NO_THROW(tempExpression = storm::expressions::iff(trueExpression, falseExpression));
257 EXPECT_TRUE(tempExpression.hasBooleanType());
258 ASSERT_NO_THROW(tempExpression = storm::expressions::iff(boolVarExpression, boolVarExpression));
259 EXPECT_TRUE(tempExpression.hasBooleanType());
260
261 STORM_SILENT_ASSERT_THROW(tempExpression = trueExpression != piExpression, storm::exceptions::InvalidTypeException);
262 ASSERT_NO_THROW(tempExpression = trueExpression != falseExpression);
263 EXPECT_TRUE(tempExpression.hasBooleanType());
264 ASSERT_NO_THROW(tempExpression = boolVarExpression != boolVarExpression);
265 EXPECT_TRUE(tempExpression.hasBooleanType());
266
267 STORM_SILENT_ASSERT_THROW(tempExpression = storm::expressions::floor(trueExpression), storm::exceptions::InvalidTypeException);
268 ASSERT_NO_THROW(tempExpression = storm::expressions::floor(threeExpression));
269 EXPECT_TRUE(tempExpression.hasIntegerType());
270 ASSERT_NO_THROW(tempExpression = storm::expressions::floor(rationalVarExpression));
271 EXPECT_TRUE(tempExpression.hasIntegerType());
272
273 STORM_SILENT_ASSERT_THROW(tempExpression = storm::expressions::ceil(trueExpression), storm::exceptions::InvalidTypeException);
274 ASSERT_NO_THROW(tempExpression = storm::expressions::ceil(threeExpression));
275 EXPECT_TRUE(tempExpression.hasIntegerType());
276 ASSERT_NO_THROW(tempExpression = storm::expressions::ceil(rationalVarExpression));
277 EXPECT_TRUE(tempExpression.hasIntegerType());
278
279 STORM_SILENT_ASSERT_THROW(tempExpression = storm::expressions::pow(trueExpression, piExpression), storm::exceptions::InvalidTypeException);
280 ASSERT_NO_THROW(tempExpression = storm::expressions::pow(threeExpression, threeExpression, true));
281 EXPECT_TRUE(tempExpression.hasIntegerType());
282 ASSERT_NO_THROW(tempExpression = storm::expressions::pow(threeExpression, threeExpression, false));
283 EXPECT_TRUE(tempExpression.hasRationalType());
284 ASSERT_NO_THROW(tempExpression = storm::expressions::pow(intVarExpression, rationalVarExpression));
285 EXPECT_TRUE(tempExpression.hasRationalType());
286
287 ASSERT_NO_THROW(tempExpression = storm::expressions::maximum(threeExpression, threeExpression));
288 EXPECT_TRUE(tempExpression.hasIntegerType());
289}
290
291TEST(Expression, SubstitutionTest) {
292 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
293
294 storm::expressions::Expression trueExpression;
295 storm::expressions::Expression falseExpression;
296 storm::expressions::Expression threeExpression;
297 storm::expressions::Expression piExpression;
298 storm::expressions::Expression boolVarExpression;
299 storm::expressions::Expression intVarExpression;
300 storm::expressions::Expression rationalVarExpression;
301
302 ASSERT_NO_THROW(trueExpression = manager->boolean(true));
303 ASSERT_NO_THROW(falseExpression = manager->boolean(false));
304 ASSERT_NO_THROW(threeExpression = manager->integer(3));
305 ASSERT_NO_THROW(piExpression = manager->rational(3.14));
306 ASSERT_NO_THROW(boolVarExpression = manager->declareBooleanVariable("x"));
307 ASSERT_NO_THROW(intVarExpression = manager->declareIntegerVariable("y"));
308 ASSERT_NO_THROW(rationalVarExpression = manager->declareRationalVariable("z"));
309
310 storm::expressions::Expression tempExpression;
311 ASSERT_NO_THROW(tempExpression = (intVarExpression < threeExpression || boolVarExpression) && boolVarExpression);
312 std::map<storm::expressions::Variable, storm::expressions::Expression> substution = {std::make_pair(manager->getVariable("y"), manager->rational(2.7)),
313 std::make_pair(manager->getVariable("x"), manager->boolean(true))};
314 storm::expressions::Expression substitutedExpression;
315 ASSERT_NO_THROW(substitutedExpression = tempExpression.substitute(substution));
316 EXPECT_TRUE(substitutedExpression.simplify().isTrue());
317}
318
319TEST(Expression, SumAndProductTest) {
320 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
321 storm::expressions::Variable xVar = manager->declareIntegerVariable("x");
322 storm::expressions::Variable yVar = manager->declareIntegerVariable("y");
323 storm::expressions::Variable zVar = manager->declareRationalVariable("z");
324 storm::expressions::Expression x = xVar.getExpression();
325 storm::expressions::Expression y = yVar.getExpression();
326 storm::expressions::Expression z = zVar.getExpression();
327 storm::expressions::Expression four = manager->integer(4);
328
329 EXPECT_TRUE(storm::expressions::sum({x}).isVariable());
330 EXPECT_TRUE(storm::expressions::product({x}).isVariable());
331
332 storm::expressions::SimpleValuation valuation(manager);
333 valuation.setIntegerValue(xVar, 2);
334 valuation.setIntegerValue(yVar, 3);
335 valuation.setRationalValue(zVar, 0.5);
336
337 auto const intSum = storm::expressions::sum({x, y, four, x, y});
338 auto const intProduct = storm::expressions::product({x, y, four, x, y});
339 EXPECT_TRUE(intSum.hasIntegerType());
340 EXPECT_TRUE(intProduct.hasIntegerType());
341 EXPECT_EQ(14, intSum.evaluateAsInt(&valuation));
342 EXPECT_EQ(144, intProduct.evaluateAsInt(&valuation));
343
344 auto const mixedSum = storm::expressions::sum({x, y, four, z});
345 auto const mixedProduct = storm::expressions::product({x, y, four, z});
346 EXPECT_TRUE(mixedSum.hasRationalType());
347 EXPECT_TRUE(mixedProduct.hasRationalType());
348 EXPECT_NEAR(9.5, mixedSum.evaluateAsDouble(&valuation), 1e-12);
349 EXPECT_NEAR(12.0, mixedProduct.evaluateAsDouble(&valuation), 1e-12);
350
351 EXPECT_THROW(storm::expressions::sum({}), storm::exceptions::InvalidArgumentException);
352 EXPECT_THROW(storm::expressions::product({}), storm::exceptions::InvalidArgumentException);
353}
354
355TEST(Expression, SimplificationTest) {
356 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
357
358 storm::expressions::Expression trueExpression;
359 storm::expressions::Expression falseExpression;
360 storm::expressions::Expression threeExpression;
361 storm::expressions::Expression intVarExpression;
362
363 ASSERT_NO_THROW(trueExpression = manager->boolean(true));
364 ASSERT_NO_THROW(falseExpression = manager->boolean(false));
365 ASSERT_NO_THROW(threeExpression = manager->integer(3));
366 ASSERT_NO_THROW(intVarExpression = manager->declareIntegerVariable("y"));
367
368 storm::expressions::Expression tempExpression;
369 storm::expressions::Expression simplifiedExpression;
370
371 ASSERT_NO_THROW(tempExpression = trueExpression || intVarExpression > threeExpression);
372 ASSERT_NO_THROW(simplifiedExpression = tempExpression.simplify());
373 EXPECT_TRUE(simplifiedExpression.isTrue());
374
375 ASSERT_NO_THROW(tempExpression = falseExpression && intVarExpression > threeExpression);
376 ASSERT_NO_THROW(simplifiedExpression = tempExpression.simplify());
377 EXPECT_TRUE(simplifiedExpression.isFalse());
378}
379
380TEST(Expression, SimpleEvaluationTest) {
381 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
382
383 storm::expressions::Expression trueExpression;
384 storm::expressions::Expression falseExpression;
385 storm::expressions::Expression threeExpression;
386 storm::expressions::Expression piExpression;
387 storm::expressions::Expression boolVarExpression;
388 storm::expressions::Expression intVarExpression;
389 storm::expressions::Expression rationalVarExpression;
390
391 ASSERT_NO_THROW(trueExpression = manager->boolean(true));
392 ASSERT_NO_THROW(falseExpression = manager->boolean(false));
393 ASSERT_NO_THROW(threeExpression = manager->integer(3));
394 ASSERT_NO_THROW(piExpression = manager->rational(3.14));
395 ASSERT_NO_THROW(boolVarExpression = manager->declareBooleanVariable("x"));
396 ASSERT_NO_THROW(intVarExpression = manager->declareIntegerVariable("y"));
397 ASSERT_NO_THROW(rationalVarExpression = manager->declareRationalVariable("z"));
398
399 storm::expressions::Expression tempExpression;
400
401 ASSERT_NO_THROW(tempExpression = (intVarExpression < threeExpression || boolVarExpression) && boolVarExpression);
402
403 ASSERT_NO_THROW(storm::expressions::SimpleValuation valuation(manager));
404 storm::expressions::SimpleValuation valuation(manager);
405 ASSERT_NO_THROW(valuation.setBooleanValue(manager->getVariable("x"), false));
406 ASSERT_NO_THROW(valuation.setIntegerValue(manager->getVariable("y"), 0));
407 ASSERT_NO_THROW(valuation.setRationalValue(manager->getVariable("z"), 0));
408
409 STORM_SILENT_ASSERT_THROW(tempExpression.evaluateAsDouble(&valuation), storm::exceptions::InvalidTypeException);
410 STORM_SILENT_ASSERT_THROW(tempExpression.evaluateAsInt(&valuation), storm::exceptions::InvalidTypeException);
411 EXPECT_FALSE(tempExpression.evaluateAsBool(&valuation));
412 ASSERT_NO_THROW(valuation.setIntegerValue(manager->getVariable("y"), 3));
413 EXPECT_FALSE(tempExpression.evaluateAsBool(&valuation));
414
415 ASSERT_NO_THROW(tempExpression = storm::expressions::ite(intVarExpression < threeExpression, trueExpression, falseExpression));
416 STORM_SILENT_ASSERT_THROW(tempExpression.evaluateAsDouble(&valuation), storm::exceptions::InvalidTypeException);
417 STORM_SILENT_ASSERT_THROW(tempExpression.evaluateAsInt(&valuation), storm::exceptions::InvalidTypeException);
418 EXPECT_FALSE(tempExpression.evaluateAsBool(&valuation));
419}
420
421TEST(Expression, VisitorTest) {
422 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
423
424 storm::expressions::Expression threeExpression;
425 storm::expressions::Expression piExpression;
426 storm::expressions::Expression intVarExpression;
427 storm::expressions::Expression rationalVarExpression;
428
429 ASSERT_NO_THROW(threeExpression = manager->integer(3));
430 ASSERT_NO_THROW(piExpression = manager->rational(3.14));
431 ASSERT_NO_THROW(intVarExpression = manager->declareIntegerVariable("y"));
432 ASSERT_NO_THROW(rationalVarExpression = manager->declareRationalVariable("z"));
433
434 storm::expressions::Expression tempExpression = intVarExpression + rationalVarExpression * threeExpression;
435 storm::expressions::LinearityCheckVisitor visitor;
436 EXPECT_TRUE(visitor.check(tempExpression));
437}
438
439TEST(Expression, RationalFunctionToExpressionTest) {
440 storm::parser::ValueParser<storm::RationalFunction> parser;
441 parser.addParameter("p");
442 parser.addParameter("q");
443 auto rationalFunction = parser.parseValue("((5*p^(3))+(q*p*7)+2)/2");
444
445 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
446 auto transformer = storm::expressions::RationalFunctionToExpression<storm::RationalFunction>(manager);
447
448 storm::expressions::Expression expr;
449 EXPECT_NO_THROW(expr = transformer.toExpression(rationalFunction));
450 auto base = storm::expressions::ExpressionEvaluator<storm::RationalFunction>(*manager);
451 storm::expressions::ToRationalFunctionVisitor<storm::RationalFunction> visitor(base);
452 ASSERT_NO_THROW(rationalFunction.simplify());
453 storm::RationalFunction result;
454 ASSERT_NO_THROW(result = visitor.toRationalFunction(expr));
455 ASSERT_NO_THROW(result.simplify());
456 EXPECT_EQ(rationalFunction.toString(), result.toString());
457
458 rationalFunction = parser.parseValue("(5*((p^(3))+(q*p)))/2");
459 transformer = storm::expressions::RationalFunctionToExpression<storm::RationalFunction>(manager);
460 EXPECT_NO_THROW(expr = transformer.toExpression(rationalFunction));
461 ASSERT_NO_THROW(rationalFunction.simplify());
462 ASSERT_NO_THROW(result = visitor.toRationalFunction(expr));
463 ASSERT_NO_THROW(result.simplify());
464 EXPECT_EQ(rationalFunction.toString(), result.toString());
465}
466
467TEST(Expression, RationalFunctionToExpressionTest_no_params) {
468 storm::parser::ValueParser<storm::RationalFunction> parser;
469 parser.addParameter("p");
470 auto rationalFunction1 = parser.parseValue("(p + 380)/3125");
471 auto rationalFunction2 = parser.parseValue("(p)/3125");
472 auto rationalFunction = rationalFunction1 - rationalFunction2;
473
474 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
475 auto transformer = storm::expressions::RationalFunctionToExpression<storm::RationalFunction>(manager);
476
477 storm::expressions::Expression expr;
478 EXPECT_NO_THROW(expr = transformer.toExpression(rationalFunction));
479 auto base = storm::expressions::ExpressionEvaluator<storm::RationalFunction>(*manager);
480 storm::expressions::ToRationalFunctionVisitor<storm::RationalFunction> visitor(base);
481 ASSERT_NO_THROW(rationalFunction.simplify());
482 storm::RationalFunction result;
483 ASSERT_NO_THROW(result = visitor.toRationalFunction(expr));
484 ASSERT_NO_THROW(result.simplify());
485 EXPECT_EQ(rationalFunction.toString(), result.toString());
486}
487
488// The valuation checks the variables it is accessed with by assertions, which are disabled in release mode.
489#ifndef NDEBUG
490#define EXPECT_REJECTED(statement) EXPECT_DEATH_IF_SUPPORTED(statement, "")
491#else
492#define EXPECT_REJECTED(statement) (void)0
493#endif
494
495TEST(ExpressionDeathTest, SimpleValuationContainsOnlyItsSnapshotVariables) {
496 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
497
498 storm::expressions::Variable x = manager->declareBooleanVariable("x");
499 storm::expressions::Variable y = manager->declareIntegerVariable("y");
500 storm::expressions::Variable z = manager->declareRationalVariable("z");
501
502 storm::expressions::SimpleValuation valuation(manager);
503 valuation.setBooleanValue(x, true);
504 valuation.setIntegerValue(y, 42);
505 valuation.setRationalValue(z, 1.5);
506
507 EXPECT_TRUE(valuation.contains(x));
508 EXPECT_TRUE(valuation.contains(y));
509 EXPECT_TRUE(valuation.contains(z));
510
511 // Declare further variables after the snapshot has been taken.
512 storm::expressions::Variable freshBoolean = manager->declareBooleanVariable("freshBoolean");
513 storm::expressions::Variable freshInteger = manager->declareIntegerVariable("freshInteger");
514 storm::expressions::Variable freshRational = manager->declareRationalVariable("freshRational");
515 storm::expressions::Variable freshBitVector = manager->declareBitVectorVariable("freshBitVector", 8);
516
517 EXPECT_FALSE(valuation.contains(freshBoolean));
518 EXPECT_FALSE(valuation.contains(freshInteger));
519 EXPECT_FALSE(valuation.contains(freshRational));
520 EXPECT_FALSE(valuation.contains(freshBitVector));
521
522 EXPECT_REJECTED(valuation.getBooleanValue(freshBoolean));
523 EXPECT_REJECTED(valuation.setBooleanValue(freshBoolean, false));
524 EXPECT_REJECTED(valuation.getIntegerValue(freshInteger));
525 EXPECT_REJECTED(valuation.setIntegerValue(freshInteger, 1));
526 EXPECT_REJECTED(valuation.getRationalValue(freshRational));
527 EXPECT_REJECTED(valuation.setRationalValue(freshRational, 2.5));
528 EXPECT_REJECTED(valuation.getBitVectorValue(freshBitVector));
529 EXPECT_REJECTED(valuation.setBitVectorValue(freshBitVector, 1));
530
531 // The variables the valuation was created for remain accessible.
532 EXPECT_TRUE(valuation.getBooleanValue(x));
533 EXPECT_EQ(42, valuation.getIntegerValue(y));
534 EXPECT_DOUBLE_EQ(1.5, valuation.getRationalValue(z));
535
536 // Printing must skip the variables that have no value in this snapshot.
537 std::string printed;
538 ASSERT_NO_THROW(printed = valuation.toString());
539 EXPECT_NE(std::string::npos, printed.find("x=true"));
540 EXPECT_EQ(std::string::npos, printed.find("freshBoolean"));
541 EXPECT_NO_THROW(printed = valuation.toString(false));
542
543 // Serialization must skip the variables that have no value in this snapshot.
544 auto const serialized = valuation.toJson();
545 EXPECT_TRUE(serialized.contains("x"));
546 EXPECT_TRUE(serialized.contains("y"));
547 EXPECT_TRUE(serialized.contains("z"));
548 EXPECT_FALSE(serialized.contains("freshBoolean"));
549 EXPECT_FALSE(serialized.contains("freshInteger"));
550 EXPECT_FALSE(serialized.contains("freshRational"));
551 EXPECT_FALSE(serialized.contains("freshBitVector"));
552}
553
554TEST(ExpressionDeathTest, SimpleValuationRejectsForeignVariables) {
555 std::shared_ptr<storm::expressions::ExpressionManager> managerA(new storm::expressions::ExpressionManager());
556 std::shared_ptr<storm::expressions::ExpressionManager> managerB(new storm::expressions::ExpressionManager());
557
558 storm::expressions::Variable own = managerA->declareBooleanVariable("flag");
559 storm::expressions::Variable foreign = managerB->declareBooleanVariable("flag");
560
561 storm::expressions::SimpleValuation valuation(managerA);
562 valuation.setBooleanValue(own, true);
563
564 // Both variables have offset zero, so only the manager distinguishes them.
565 ASSERT_EQ(own.getOffset(), foreign.getOffset());
566 EXPECT_FALSE(valuation.contains(foreign));
567 EXPECT_REJECTED(valuation.getBooleanValue(foreign));
568 EXPECT_REJECTED(valuation.setBooleanValue(foreign, false));
569 EXPECT_TRUE(valuation.getBooleanValue(own));
570}
571
572TEST(ExpressionDeathTest, SimpleValuationRejectsVariablesItDoesNotStore) {
573 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
574
575 storm::expressions::Variable flag = manager->declareBooleanVariable("flag");
576 storm::expressions::Variable array = manager->declareArrayVariable("array", manager->getIntegerType());
577
578 storm::expressions::SimpleValuation valuation(manager);
579 valuation.setBooleanValue(flag, true);
580
581 EXPECT_FALSE(valuation.contains(array));
582 EXPECT_REJECTED(valuation.getBooleanValue(array));
583
584 // Array variables share the offset space of no stored type, but they are never contained.
585 ASSERT_NO_THROW(valuation.toString());
586}
587
588TEST(ExpressionDeathTest, SimpleValuationRejectsVariablesOfDefaultConstructedValuation) {
589 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
590 storm::expressions::Variable x = manager->declareBooleanVariable("x");
591
592 storm::expressions::SimpleValuation valuation;
593 EXPECT_FALSE(valuation.contains(x));
594 EXPECT_REJECTED(valuation.getBooleanValue(x));
595 EXPECT_REJECTED(valuation.setBooleanValue(x, true));
596}
597TEST(Expression, LinearCoefficientsTest) {
598 auto manager = std::make_shared<storm::expressions::ExpressionManager>();
599 auto x = manager->declareRationalVariable("x");
600 auto y = manager->declareRationalVariable("y");
601
602 // 1/3 * x + (x - y) / 2 - 1 is linear with exact rational coefficients.
603 auto linear = manager->rational(storm::utility::convertNumber<storm::RationalNumber>(1) / storm::utility::convertNumber<storm::RationalNumber>(3)) *
604 x.getExpression() +
605 (x.getExpression() - y.getExpression()) / manager->integer(2) - manager->integer(1);
606 auto coefficients = storm::expressions::LinearCoefficientVisitor<storm::RationalNumber>().getLinearCoefficients(linear);
607 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(5) / storm::utility::convertNumber<storm::RationalNumber>(6),
608 coefficients.getCoefficient(x));
609 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(-1) / storm::utility::convertNumber<storm::RationalNumber>(2),
610 coefficients.getCoefficient(y));
611 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(-1), coefficients.getConstantPart());
612
613 // Variables that cancel out are not part of the coefficients.
614 auto cancelled = storm::expressions::LinearCoefficientVisitor<double>().getLinearCoefficients(x.getExpression() + y.getExpression() - x.getExpression());
615 EXPECT_EQ(1ul, cancelled.size());
616
617 // Non-linear expressions and divisions by zero are rejected.
618 storm::expressions::LinearCoefficientVisitor<storm::RationalNumber> visitor;
619 EXPECT_FALSE(visitor.tryGetLinearCoefficients(x.getExpression() * y.getExpression()).has_value());
620 EXPECT_FALSE(visitor.tryGetLinearCoefficients(x.getExpression() / manager->integer(0)).has_value());
621 EXPECT_FALSE(visitor.tryGetLinearCoefficients(x.getExpression() <= y.getExpression()).has_value());
622 EXPECT_THROW(visitor.getLinearCoefficients(x.getExpression() * y.getExpression()), storm::exceptions::InvalidArgumentException);
623}
EXPECT_REJECTED
#define EXPECT_REJECTED(statement)
Definition ExpressionTest.cpp:490
TEST
TEST(Expression, FactoryMethodTest)
Definition ExpressionTest.cpp:21
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:71
storm::expressions::LinearCoefficientVisitor
Computes the coefficients of a linear expression.
Definition LinearCoefficientVisitor.h:17
storm::expressions::LinearCoefficientVisitor::tryGetLinearCoefficients
std::optional< VariableCoefficients > tryGetLinearCoefficients(Expression const &expression)
As getLinearCoefficients, but returns std::nullopt instead of throwing if the expression is not linea...
Definition LinearCoefficientVisitor.cpp:132
storm::expressions::LinearCoefficientVisitor::getLinearCoefficients
VariableCoefficients getLinearCoefficients(Expression const &expression)
Computes the coefficients of all identifiers appearing in the expression if the expression was rewrit...
Definition LinearCoefficientVisitor.cpp:138
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:17
storm::expressions::SimpleValuation::contains
bool contains(Variable const &variable) const
Checks whether this valuation stores a value for the given variable.
Definition SimpleValuation.cpp:69
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:115
storm::expressions::SimpleValuation::getIntegerValue
virtual int_fast64_t getIntegerValue(Variable const &integerVariable) const override
Retrieves the value of the given integer variable.
Definition SimpleValuation.cpp:95
storm::expressions::SimpleValuation::getRationalValue
virtual double getRationalValue(Variable const &rationalVariable) const override
Retrieves the value of the given rational variable.
Definition SimpleValuation.cpp:105
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:110
storm::expressions::SimpleValuation::toJson
storm::json< storm::RationalNumber > toJson() const
Definition SimpleValuation.cpp:186
storm::expressions::SimpleValuation::toString
virtual std::string toString(bool pretty=true) const
Definition SimpleValuation.cpp:149
storm::expressions::SimpleValuation::getBooleanValue
virtual bool getBooleanValue(Variable const &booleanVariable) const override
Retrieves the value of the given boolean variable.
Definition SimpleValuation.cpp:90
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:125
storm::expressions::SimpleValuation::getBitVectorValue
virtual int_fast64_t getBitVectorValue(Variable const &bitVectorVariable) const override
Retrieves the value of the given bit vector variable.
Definition SimpleValuation.cpp:100
storm::expressions::SimpleValuation::setBitVectorValue
virtual void setBitVectorValue(Variable const &bitVectorVariable, int_fast64_t value) override
Sets the value of the given bit vector variable to the provided value.
Definition SimpleValuation.cpp:120
storm::expressions::ToRationalFunctionVisitor::toRationalFunction
RationalFunctionType toRationalFunction(Expression const &expression)
Definition ToRationalFunctionVisitor.cpp:18
storm::expressions::Variable::getExpression
storm::expressions::Expression getExpression() const
Retrieves an expression that represents the variable.
Definition Variable.cpp:34
storm::expressions::Variable::getOffset
uint_fast64_t getOffset() const
Retrieves the offset of the variable in the group of all equally typed variables.
Definition Variable.cpp:42
storm::parser::ValueParser
Parser for values according to their ValueType.
Definition ValueParser.h:24
storm::parser::ValueParser::addParameter
void addParameter(std::string const &parameter)
Add declaration of parameter.
Definition ValueParser.cpp:30
storm::parser::ValueParser::parseValue
ValueType parseValue(std::string const &value) const
Parse ValueType from string.
Definition ValueParser.cpp:50
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::sum
Expression sum(std::vector< storm::expressions::Expression > const &expressions)
Definition Expression.cpp:536
storm::expressions::product
Expression product(std::vector< storm::expressions::Expression > const &expressions)
Definition Expression.cpp:540
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::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::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:544
storm::utility::convertNumber
TargetType convertNumber(SourceType const &number)
Definition constants.cpp:145
storm::RationalFunction
carl::RationalFunction< Polynomial, true > RationalFunction
Definition RationalFunctionForward.h:47
storm_gtest.h
STORM_SILENT_ASSERT_THROW
#define STORM_SILENT_ASSERT_THROW(statement, expected_exception)
Definition storm_gtest.h:16