Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
ExpressionParser.cpp
Go to the documentation of this file.
5
9
11
12namespace boost {
13namespace spirit {
14namespace traits {
15template<>
16bool scale(int exp, storm::RationalNumber& r, storm::RationalNumber acc) {
17 if (exp >= 0) {
18 r = acc * storm::utility::pow(storm::RationalNumber(10), static_cast<uint_fast64_t>(exp));
19 } else {
20 r = acc / storm::utility::pow(storm::RationalNumber(10), static_cast<uint_fast64_t>(-exp));
21 }
22 return true;
23}
24
25#if BOOST_VERSION < 107000
26template<>
27bool is_equal_to_one(storm::RationalNumber const& value) {
28 return storm::utility::isOne(value);
29}
30#endif
31
32template<>
33storm::RationalNumber negate(bool neg, storm::RationalNumber const& number) {
34 return neg ? storm::RationalNumber(-number) : number;
35}
36} // namespace traits
37} // namespace spirit
38} // namespace boost
39
40namespace storm {
41namespace parser {
42ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols<char, uint_fast64_t> const& invalidIdentifiers_,
43 bool enableErrorHandling, bool allowBacktracking)
44 : ExpressionParser::base_type(expression),
45 orOperator_(),
46 andOperator_(),
47 equalityOperator_(),
48 relationalOperator_(),
49 plusOperator_(),
50 multiplicationOperator_(),
51 infixPowerModuloOperator_(),
52 unaryOperator_(),
53 floorCeilOperator_(),
54 minMaxOperator_(),
55 prefixPowerModuloLogarithmOperator_(),
56 invalidIdentifiers_(invalidIdentifiers_) {
57 expressionCreator = std::make_unique<ExpressionCreator>(manager);
58
59 identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_') | qi::char_('.')) >> *(qi::alnum | qi::char_('_')))]]]
60 [qi::_pass = phoenix::bind(&ExpressionParser::isValidIdentifier, phoenix::ref(*this), qi::_1)];
61 identifier.name("identifier");
62
63 if (allowBacktracking) {
64 predicateExpression =
65 ((predicateOperator_ >> qi::lit("(")) >> (expression % qi::lit(",")) >>
66 qi::lit(
67 ")"))[qi::_val = phoenix::bind(&ExpressionCreator::createPredicateExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_2, qi::_pass)];
68 } else {
69 predicateExpression =
70 ((predicateOperator_ >> qi::lit("(")) > (expression % qi::lit(",")) >
71 qi::lit(
72 ")"))[qi::_val = phoenix::bind(&ExpressionCreator::createPredicateExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_2, qi::_pass)];
73 }
74 predicateExpression.name("predicate expression");
75
76 if (allowBacktracking) {
77 floorCeilExpression =
78 ((floorCeilOperator_ >> qi::lit("(")) >> expression >>
79 qi::lit(
80 ")"))[qi::_val = phoenix::bind(&ExpressionCreator::createFloorCeilExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_2, qi::_pass)];
81 } else {
82 floorCeilExpression =
83 ((floorCeilOperator_ >> qi::lit("(")) > expression >
84 qi::lit(
85 ")"))[qi::_val = phoenix::bind(&ExpressionCreator::createFloorCeilExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_2, qi::_pass)];
86 }
87 floorCeilExpression.name("floor/ceil expression");
88
89 if (allowBacktracking) {
90 roundExpression =
91 ((qi::lit("round") >> qi::lit("(")) >> expression >>
92 qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionCreator::createRoundExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_pass)];
93 } else {
94 roundExpression =
95 ((qi::lit("round") >> qi::lit("(")) > expression >
96 qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionCreator::createRoundExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_pass)];
97 }
98 roundExpression.name("round expression");
99
100 if (allowBacktracking) {
101 minMaxExpression =
102 ((minMaxOperator_[qi::_a = qi::_1] >> qi::lit("(")) >> expression[qi::_val = qi::_1] >>
103 +(qi::lit(",") >> expression)[qi::_b = phoenix::bind(&ExpressionCreator::createMinimumMaximumExpression, phoenix::ref(*expressionCreator),
104 qi::_val, qi::_a, qi::_1, qi::_pass)][qi::_val = qi::_b]) >>
105 qi::lit(")");
106 } else {
107 minMaxExpression =
108 ((minMaxOperator_[qi::_a = qi::_1] >> qi::lit("(")) > expression[qi::_val = qi::_1] >
109 +(qi::lit(",") > expression)[qi::_val = phoenix::bind(&ExpressionCreator::createMinimumMaximumExpression, phoenix::ref(*expressionCreator),
110 qi::_val, qi::_a, qi::_1, qi::_pass)]) > qi::lit(")");
111 }
112 minMaxExpression.name("min/max expression");
113
114 if (allowBacktracking) {
115 prefixPowerModuloLogarithmExpression =
116 ((prefixPowerModuloLogarithmOperator_ >> qi::lit("(")) >> expression >> qi::lit(",") >> expression >>
117 qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionCreator::createPowerModuloLogarithmExpression, phoenix::ref(*expressionCreator), qi::_2, qi::_1,
118 qi::_3, qi::_pass)] |
119 (qi::lit("func") >> qi::lit("(") >> prefixPowerModuloLogarithmOperator_ >> qi::lit(",") >> expression >> qi::lit(",") >> expression >>
120 qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionCreator::createPowerModuloLogarithmExpression, phoenix::ref(*expressionCreator), qi::_2, qi::_1,
121 qi::_3, qi::_pass)];
122 } else {
123 prefixPowerModuloLogarithmExpression =
124 ((prefixPowerModuloLogarithmOperator_ >> qi::lit("(")) > expression > qi::lit(",") > expression >
125 qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionCreator::createPowerModuloLogarithmExpression, phoenix::ref(*expressionCreator), qi::_2, qi::_1,
126 qi::_3, qi::_pass)] |
127 ((qi::lit("func") >> qi::lit("(")) > prefixPowerModuloLogarithmOperator_ > qi::lit(",") > expression > qi::lit(",") > expression >
128 qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionCreator::createPowerModuloLogarithmExpression, phoenix::ref(*expressionCreator), qi::_2, qi::_1,
129 qi::_3, qi::_pass)];
130 }
131 prefixPowerModuloLogarithmExpression.name("(prefix) power/modulo/logarithm expression");
132
133 identifierExpression =
134 identifier[qi::_val = phoenix::bind(&ExpressionCreator::getIdentifierExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_pass)];
135 identifierExpression.name("identifier expression");
136
137 literalExpression =
138 qi::lit("true")[qi::_val = phoenix::bind(&ExpressionCreator::createBooleanLiteralExpression, phoenix::ref(*expressionCreator), true, qi::_pass)] |
139 qi::lit("false")[qi::_val = phoenix::bind(&ExpressionCreator::createBooleanLiteralExpression, phoenix::ref(*expressionCreator), false, qi::_pass)] |
140 rationalLiteral_[qi::_val = phoenix::bind(&ExpressionCreator::createRationalLiteralExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_pass)] |
141 qi::long_long[qi::_val = phoenix::bind(&ExpressionCreator::createIntegerLiteralExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_pass)];
142 literalExpression.name("literal expression");
143
144 atomicExpression = predicateExpression | floorCeilExpression | roundExpression | prefixPowerModuloLogarithmExpression | minMaxExpression |
145 (qi::lit("(") >> expression >> qi::lit(")")) | identifierExpression | literalExpression;
146 atomicExpression.name("atomic expression");
147
148 unaryExpression =
149 (*unaryOperator_ >>
150 atomicExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createUnaryExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_2, qi::_pass)];
151 unaryExpression.name("unary expression");
152
153 if (allowBacktracking) {
154 infixPowerModuloExpression =
155 unaryExpression[qi::_val = qi::_1] >>
156 -(infixPowerModuloOperator_ >>
157 unaryExpression)[qi::_a = phoenix::bind(&ExpressionCreator::createPowerModuloLogarithmExpression, phoenix::ref(*expressionCreator), qi::_val,
158 qi::_1, qi::_2, qi::_pass)][qi::_val = qi::_a];
159 } else {
160 infixPowerModuloExpression =
161 unaryExpression[qi::_val = qi::_1] >
162 -(infixPowerModuloOperator_ >> unaryExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createPowerModuloLogarithmExpression,
163 phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)];
164 }
165 infixPowerModuloExpression.name("(infix) power/modulo expression");
166
167 if (allowBacktracking) {
168 multiplicationExpression =
169 infixPowerModuloExpression[qi::_val = qi::_1] >>
170 *(multiplicationOperator_ >>
171 infixPowerModuloExpression)[qi::_a = phoenix::bind(&ExpressionCreator::createMultExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1,
172 qi::_2, qi::_pass)][qi::_val = qi::_a];
173 } else {
174 multiplicationExpression =
175 infixPowerModuloExpression[qi::_val = qi::_1] >
176 *(multiplicationOperator_ >
177 infixPowerModuloExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createMultExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1,
178 qi::_2, qi::_pass)];
179 }
180 multiplicationExpression.name("multiplication expression");
181
182 if (allowBacktracking) {
183 plusExpression =
184 multiplicationExpression[qi::_val = qi::_1] >>
185 *(plusOperator_ >> multiplicationExpression)[qi::_a = phoenix::bind(&ExpressionCreator::createPlusExpression, phoenix::ref(*expressionCreator),
186 qi::_val, qi::_1, qi::_2, qi::_pass)][qi::_val = qi::_a];
187 } else {
188 plusExpression =
189 multiplicationExpression[qi::_val = qi::_1] >
190 *(plusOperator_ >> multiplicationExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createPlusExpression, phoenix::ref(*expressionCreator),
191 qi::_val, qi::_1, qi::_2, qi::_pass)];
192 }
193 plusExpression.name("plus expression");
194
195 if (allowBacktracking) {
196 relativeExpression =
197 plusExpression[qi::_val = qi::_1] >>
198 -(relationalOperator_ >> plusExpression)[qi::_a = phoenix::bind(&ExpressionCreator::createRelationalExpression, phoenix::ref(*expressionCreator),
199 qi::_val, qi::_1, qi::_2, qi::_pass)][qi::_val = qi::_a];
200 } else {
201 relativeExpression =
202 plusExpression[qi::_val = qi::_1] >
203 -(relationalOperator_ > plusExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createRelationalExpression, phoenix::ref(*expressionCreator),
204 qi::_val, qi::_1, qi::_2, qi::_pass)];
205 }
206 relativeExpression.name("relative expression");
207
208 if (allowBacktracking) {
209 equalityExpression =
210 relativeExpression[qi::_val = qi::_1] >>
211 *(equalityOperator_ >> relativeExpression)[qi::_a = phoenix::bind(&ExpressionCreator::createEqualsExpression, phoenix::ref(*expressionCreator),
212 qi::_val, qi::_1, qi::_2, qi::_pass)][qi::_val = qi::_a];
213 } else {
214 equalityExpression =
215 relativeExpression[qi::_val = qi::_1] >>
216 *(equalityOperator_ >> relativeExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createEqualsExpression, phoenix::ref(*expressionCreator),
217 qi::_val, qi::_1, qi::_2, qi::_pass)];
218 }
219 equalityExpression.name("equality expression");
220
221 if (allowBacktracking) {
222 andExpression = equalityExpression[qi::_val = qi::_1] >>
223 *(andOperator_ >> equalityExpression)[qi::_a = phoenix::bind(&ExpressionCreator::createAndExpression, phoenix::ref(*expressionCreator),
224 qi::_val, qi::_1, qi::_2, qi::_pass)][qi::_val = qi::_a];
225 } else {
226 andExpression = equalityExpression[qi::_val = qi::_1] >>
227 *(andOperator_ > equalityExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createAndExpression, phoenix::ref(*expressionCreator),
228 qi::_val, qi::_1, qi::_2, qi::_pass)];
229 }
230 andExpression.name("and expression");
231
232 if (allowBacktracking) {
233 orExpression = andExpression[qi::_val = qi::_1] >>
234 *(orOperator_ >> andExpression)[qi::_a = phoenix::bind(&ExpressionCreator::createOrExpression, phoenix::ref(*expressionCreator),
235 qi::_val, qi::_1, qi::_2, qi::_pass)][qi::_val = qi::_a];
236 } else {
237 orExpression = andExpression[qi::_val = qi::_1] >
238 *(orOperator_ > andExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createOrExpression, phoenix::ref(*expressionCreator),
239 qi::_val, qi::_1, qi::_2, qi::_pass)];
240 }
241 orExpression.name("or expression");
242
243 if (allowBacktracking) {
244 iteExpression = orExpression[qi::_val = qi::_1] >>
245 -(qi::lit("?") >> iteExpression >> qi::lit(":") >>
246 iteExpression)[qi::_a = phoenix::bind(&ExpressionCreator::createIteExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1,
247 qi::_2, qi::_pass)][qi::_val = qi::_a];
248 } else {
249 iteExpression =
250 orExpression[qi::_val = qi::_1] > -(qi::lit("?") > iteExpression > qi::lit(":") >
251 iteExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createIteExpression,
252 phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)];
253 }
254 iteExpression.name("if-then-else expression");
255
256 expression %= iteExpression;
257 expression.name("expression");
258
276 if (enableErrorHandling) {
277 // Enable error reporting.
278 qi::on_error<qi::fail>(expression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
279 qi::on_error<qi::fail>(iteExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
280 qi::on_error<qi::fail>(orExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
281 qi::on_error<qi::fail>(andExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
282 qi::on_error<qi::fail>(equalityExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
283 qi::on_error<qi::fail>(relativeExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
284 qi::on_error<qi::fail>(plusExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
285 qi::on_error<qi::fail>(multiplicationExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
286 qi::on_error<qi::fail>(unaryExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
287 qi::on_error<qi::fail>(atomicExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
288 qi::on_error<qi::fail>(literalExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
289 qi::on_error<qi::fail>(identifierExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
290 qi::on_error<qi::fail>(minMaxExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
291 qi::on_error<qi::fail>(floorCeilExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
292 qi::on_error<qi::fail>(roundExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
293 }
294}
295
297 // Needed, because auto-generated destructor requires ExpressionCreator to be a complete type in the header.
298}
299
300void ExpressionParser::setIdentifierMapping(qi::symbols<char, storm::expressions::Expression> const* identifiers_) {
301 expressionCreator->setIdentifierMapping(identifiers_);
302}
303
304void ExpressionParser::setIdentifierMapping(std::unordered_map<std::string, storm::expressions::Expression> const& identifierMapping) {
305 expressionCreator->setIdentifierMapping(identifierMapping);
306}
307
309 expressionCreator->unsetIdentifierMapping();
310}
311
313 expressionCreator->setAcceptDoubleLiterals(flag);
314}
315
316bool ExpressionParser::isValidIdentifier(std::string const& identifier) {
317 if (this->invalidIdentifiers_.find(identifier) != nullptr) {
318 return false;
319 }
320 return true;
321}
322
323storm::expressions::Expression ExpressionParser::parseFromString(std::string const& expressionString, bool ignoreError) const {
324 PositionIteratorType first(expressionString.begin());
325 PositionIteratorType iter = first;
326 PositionIteratorType last(expressionString.end());
327
328 // Create empty result;
330
331 try {
332 // Start parsing.
333 bool succeeded = qi::phrase_parse(
334 iter, last, *this, storm::spirit_encoding::space_type() | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), result);
335 succeeded &= (iter == last);
336 if (!succeeded) {
337 STORM_LOG_THROW(ignoreError, storm::exceptions::WrongFormatException, "Could not parse expression '" << expressionString << "'.");
339 }
340 STORM_LOG_DEBUG("Parsed expression successfully.");
341 } catch (qi::expectation_failure<PositionIteratorType> const& e) {
342 STORM_LOG_THROW(ignoreError, storm::exceptions::WrongFormatException, e.what_);
344 }
345 return result;
346}
347} // namespace parser
348} // namespace storm
boost::spirit::line_pos_iterator< BaseIteratorType > PositionIteratorType
This class is responsible for managing a set of typed variables and all expressions using these varia...
storm::expressions::Expression getIdentifierExpression(std::string const &identifier, bool &pass) const
storm::expressions::Expression createRationalLiteralExpression(storm::RationalNumber const &value, bool &pass) const
storm::expressions::Expression createPredicateExpression(storm::expressions::OperatorType const &opTyp, std::vector< storm::expressions::Expression > const &operands, bool &pass) const
storm::expressions::Expression createIteExpression(storm::expressions::Expression const &e1, storm::expressions::Expression const &e2, storm::expressions::Expression const &e3, bool &pass) const
storm::expressions::Expression createMultExpression(storm::expressions::Expression const &e1, storm::expressions::OperatorType const &operatorType, storm::expressions::Expression const &e2, bool &pass) const
storm::expressions::Expression createPlusExpression(storm::expressions::Expression const &e1, storm::expressions::OperatorType const &operatorType, storm::expressions::Expression const &e2, bool &pass) const
storm::expressions::Expression createEqualsExpression(storm::expressions::Expression const &e1, storm::expressions::OperatorType const &operatorType, storm::expressions::Expression const &e2, bool &pass) const
storm::expressions::Expression createFloorCeilExpression(storm::expressions::OperatorType const &operatorType, storm::expressions::Expression const &e1, bool &pass) const
storm::expressions::Expression createOrExpression(storm::expressions::Expression const &e1, storm::expressions::OperatorType const &operatorType, storm::expressions::Expression const &e2, bool &pass) const
storm::expressions::Expression createIntegerLiteralExpression(int64_t value, bool &pass) const
storm::expressions::Expression createRelationalExpression(storm::expressions::Expression const &e1, storm::expressions::OperatorType const &operatorType, storm::expressions::Expression const &e2, bool &pass) const
storm::expressions::Expression createRoundExpression(storm::expressions::Expression const &e1, bool &pass) const
storm::expressions::Expression createBooleanLiteralExpression(bool value, bool &pass) const
storm::expressions::Expression createUnaryExpression(std::vector< storm::expressions::OperatorType > const &operatorType, storm::expressions::Expression const &e1, bool &pass) const
storm::expressions::Expression createPowerModuloLogarithmExpression(storm::expressions::Expression const &e1, storm::expressions::OperatorType const &operatorType, storm::expressions::Expression const &e2, bool &pass) const
storm::expressions::Expression createAndExpression(storm::expressions::Expression const &e1, storm::expressions::OperatorType const &operatorType, storm::expressions::Expression const &e2, bool &pass) const
storm::expressions::Expression createMinimumMaximumExpression(storm::expressions::Expression const &e1, storm::expressions::OperatorType const &operatorType, storm::expressions::Expression const &e2, bool &pass) const
storm::expressions::Expression parseFromString(std::string const &expressionString, bool ignoreError=false) const
Parses an expression from the given string.
void setIdentifierMapping(qi::symbols< char, storm::expressions::Expression > const *identifiers_)
Sets an identifier mapping that is used to determine valid variables in the expression.
void unsetIdentifierMapping()
Unsets a previously set identifier mapping.
void setAcceptDoubleLiterals(bool flag)
Sets whether double literals are to be accepted or not.
ExpressionParser(storm::expressions::ExpressionManager const &manager, qi::symbols< char, uint_fast64_t > const &invalidIdentifiers_=qi::symbols< char, uint_fast64_t >(), bool enableErrorHandling=true, bool allowBacktracking=false)
Creates an expression parser.
#define STORM_LOG_DEBUG(message)
Definition logging.h:23
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
bool is_equal_to_one(storm::RationalNumber const &value)
storm::RationalNumber negate(bool neg, storm::RationalNumber const &number)
bool scale(int exp, storm::RationalNumber &r, storm::RationalNumber acc)
bool isOne(ValueType const &a)
Definition constants.cpp:36
ValueType pow(ValueType const &value, int_fast64_t exponent)
LabParser.cpp.
Definition cli.cpp:18