Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
FormulaParserGrammar.cpp
Go to the documentation of this file.
1#include "FormulaParserGrammar.h"
2
3#include <memory>
4
5#include "storm/storage/expressions/ExpressionManager.h"
6
7namespace storm {
8namespace parser {
9
10FormulaParserGrammar::FormulaParserGrammar(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager)
11 : FormulaParserGrammar::base_type(start), constManager(manager), manager(nullptr), expressionParser(*manager, keywords_, true, true), propertyCount(0) {
12 initialize();
13}
14
15FormulaParserGrammar::FormulaParserGrammar(std::shared_ptr<storm::expressions::ExpressionManager> const& manager)
16 : FormulaParserGrammar::base_type(start), constManager(manager), manager(manager), expressionParser(*manager, keywords_, true, true), propertyCount(0) {
17 initialize();
18}
19
20qi::symbols<char, storm::expressions::Expression> const& FormulaParserGrammar::getIdentifiers() const {
21 return identifiers_;
22}
23
24void FormulaParserGrammar::initialize() {
25 // Register all variables so we can parse them in the expressions.
26 for (auto variableTypePair : *constManager) {
27 addIdentifierExpression(variableTypePair.first.getName(), variableTypePair.first);
28 }
29 // Set the identifier mapping to actually generate expressions.
30 expressionParser.setIdentifierMapping(&identifiers_);
31
32 keywords_.name("keyword");
33 nonStandardKeywords_.name("non-standard Storm-specific keyword");
34 relationalOperator_.name("relational operator");
35 optimalityOperator_.name("optimality operator");
36 operatorKeyword_.name("Operator keyword");
37 filterType_.name("filter type");
38
39 // Auxiliary helpers
40 isPathFormula = qi::eps(qi::_r1 == FormulaKind::Path);
41 noAmbiguousNonAssociativeOperator =
42 !(qi::lit(qi::_r2)[qi::_pass = phoenix::bind(&FormulaParserGrammar::raiseAmbiguousNonAssociativeOperatorError, phoenix::ref(*this), qi::_r1, qi::_r2)]);
43 noAmbiguousNonAssociativeOperator.name("no ambiguous non-associative operator");
44 identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_') | qi::char_('.')) >> *(qi::alnum | qi::char_('_')))]]];
45 identifier.name("identifier");
46 label %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]];
47 label.name("label");
48 quotedString %= qi::as_string[qi::lexeme[qi::omit[qi::char_('"')] > qi::raw[*(!qi::char_('"') >> qi::char_)] > qi::omit[qi::lit('"')]]];
49 quotedString.name("quoted string");
50
51 // PCTL-like Operator Formulas
52 operatorInformation =
53 (-optimalityOperator_)[qi::_a = qi::_1] >>
54 ((qi::lit("=") >
55 qi::lit("?"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createOperatorInformation, phoenix::ref(*this), qi::_a, boost::none, boost::none)] |
56 (relationalOperator_ >
57 expressionParser)[qi::_val = phoenix::bind(&FormulaParserGrammar::createOperatorInformation, phoenix::ref(*this), qi::_a, qi::_1, qi::_2)]);
58 operatorInformation.name("operator information");
59 operatorSubFormula =
60 (((qi::eps(qi::_r1 == storm::logic::FormulaContext::Probability) > formula(FormulaKind::Path, qi::_r1)) |
61 (qi::eps(qi::_r1 == storm::logic::FormulaContext::Reward) >
62 (longRunAverageRewardFormula | eventuallyFormula(qi::_r1) | discountedCumulativeRewardFormula | discountedTotalRewardFormula |
63 cumulativeRewardFormula | instantaneousRewardFormula | totalRewardFormula)) |
64 (qi::eps(qi::_r1 == storm::logic::FormulaContext::Time) > eventuallyFormula(qi::_r1)) |
65 (qi::eps(qi::_r1 == storm::logic::FormulaContext::LongRunAverage) > formula(FormulaKind::State, storm::logic::FormulaContext::LongRunAverage))) >>
66 -(qi::lit("||") >
67 formula(FormulaKind::Path, storm::logic::FormulaContext::Probability)))[qi::_val = phoenix::bind(&FormulaParserGrammar::createConditionalFormula,
68 phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)];
69 operatorSubFormula.name("operator subformula");
70 rewardModelName = qi::eps(qi::_r1 == storm::logic::FormulaContext::Reward) >> (qi::lit("{\"") > label > qi::lit("\"}"));
71 rewardModelName.name("reward model name");
72 operatorFormula =
73 (operatorKeyword_[qi::_a = qi::_1] > -rewardModelName(qi::_a) > operatorInformation > qi::lit("[") > operatorSubFormula(qi::_a) >
74 qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createOperatorFormula, phoenix::ref(*this), qi::_a, qi::_2, qi::_3, qi::_4)];
75 operatorFormula.name("operator formula");
76
77 // Atomic propositions
78 labelFormula =
79 (qi::lit("\"") >> label >> qi::lit("\""))[qi::_val = phoenix::bind(&FormulaParserGrammar::createAtomicLabelFormula, phoenix::ref(*this), qi::_1)];
80 labelFormula.name("label formula");
81 expressionFormula = expressionParser[qi::_val = phoenix::bind(&FormulaParserGrammar::createAtomicExpressionFormula, phoenix::ref(*this), qi::_1)];
82 expressionFormula.name("expression formula");
83
84 basicPropositionalFormula =
85 expressionFormula // try as expression first, e.g. '(false)=false' is an atomic expression formula. Also should be checked before operator formulas and
86 // others. Otherwise, e.g. variable "Random" would be parsed as reward operator 'R' (followed by andom)
87 | (qi::lit("(") >>
88 (formula(qi::_r1, qi::_r2) > qi::lit(")"))) // If we're starting with '(' but this is not an expression, we must have a formula inside the brackets
89 | labelFormula | negationPropositionalFormula(qi::_r1, qi::_r2) | operatorFormula |
90 (isPathFormula(qi::_r1) >> prefixOperatorPathFormula(qi::_r2)) // Needed for e.g. F "a" & X "a" = F ("a" & (X "a"))
91 | multiLexOperatorFormula // Has to come after prefixOperatorPathFormula to avoid confusion with multiBoundedPathFormula
92 | multiOperatorFormula // Has to come after multilex to avoid failing to parse multilex
93 | quantileFormula | gameFormula;
94
95 // Propositional Logic operators
96 // To correctly parse the operator precedences (! binds stronger than & binds stronger than |), we run through different "precedence levels" starting with
97 // the strongest binding operator.
98 negationPropositionalFormula =
99 (qi::lit("!") >
100 basicPropositionalFormula(qi::_r1, qi::_r2))[qi::_val = phoenix::bind(&FormulaParserGrammar::createUnaryBooleanStateOrPathFormula, phoenix::ref(*this),
101 qi::_1, storm::logic::UnaryBooleanOperatorType::Not)];
102 basicPropositionalFormula.name("basic propositional formula");
103 andLevelPropositionalFormula =
104 basicPropositionalFormula(qi::_r1, qi::_r2)[qi::_val = qi::_1] >>
105 *(qi::lit("&") > basicPropositionalFormula(
106 qi::_r1, qi::_r2)[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateOrPathFormula, phoenix::ref(*this),
107 qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::And)]);
108 andLevelPropositionalFormula.name("and precedence level propositional formula");
109 orLevelPropositionalFormula =
110 andLevelPropositionalFormula(qi::_r1, qi::_r2)[qi::_val = qi::_1] >>
111 *((!qi::lit("||") >> qi::lit("|")) // Make sure to not confuse with conditional operator "||"
112 > andLevelPropositionalFormula(
113 qi::_r1, qi::_r2)[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateOrPathFormula, phoenix::ref(*this), qi::_val, qi::_1,
114 storm::logic::BinaryBooleanStateFormula::OperatorType::Or)]);
115 orLevelPropositionalFormula.name("or precedence level propositional formula");
116 propositionalFormula = orLevelPropositionalFormula(qi::_r1, qi::_r2);
117
118 // Path operators
119 // Again need to parse precedences correctly. Propositional formulae bind stronger than temporal operators.
120 basicPathFormula = propositionalFormula(FormulaKind::Path, qi::_r1) // Bracketed case is handled here as well
121 | prefixOperatorPathFormula(
122 qi::_r1); // Needs to be checked *after* atomic expression formulas. Otherwise e.g. variable Fail would be parsed as "F (ail)"
123 prefixOperatorPathFormula =
124 eventuallyFormula(qi::_r1) | nextFormula(qi::_r1) | globallyFormula(qi::_r1) | hoaPathFormula(qi::_r1) | multiBoundedPathFormula(qi::_r1);
125 basicPathFormula.name("basic path formula");
126 timeBoundReference =
127 (-qi::lit("rew") >>
128 rewardModelName(storm::logic::FormulaContext::Reward))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundReference, phoenix::ref(*this),
129 storm::logic::TimeBoundType::Reward, qi::_1)] |
130 (qi::lit("rew") >>
131 -rewardModelName(storm::logic::FormulaContext::Reward))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundReference, phoenix::ref(*this),
132 storm::logic::TimeBoundType::Reward, qi::_1)] |
133 (qi::lit("steps"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundReference, phoenix::ref(*this), storm::logic::TimeBoundType::Steps,
134 boost::none)] |
135 (-qi::lit("time"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundReference, phoenix::ref(*this), storm::logic::TimeBoundType::Time,
136 boost::none)];
137 timeBoundReference.name("time bound reference");
138 timeBound = ((timeBoundReference >> qi::lit("[")) > expressionParser > qi::lit(",") > expressionParser >
139 qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromInterval, phoenix::ref(*this), qi::_2, qi::_3, qi::_1)] |
140 (timeBoundReference >> (qi::lit("<=")[(qi::_a = true, qi::_b = false)] | qi::lit("<")[(qi::_a = true, qi::_b = true)] |
141 qi::lit(">=")[(qi::_a = false, qi::_b = false)] | qi::lit(">")[(qi::_a = false, qi::_b = true)]) >>
142 expressionParser)[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromSingleBound, phoenix::ref(*this), qi::_2, qi::_a, qi::_b,
143 qi::_1)] |
144 (timeBoundReference >> qi::lit("=") >>
145 expressionParser)[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromInterval, phoenix::ref(*this), qi::_2, qi::_2, qi::_1)];
146 timeBound.name("time bound");
147 timeBounds = (timeBound % qi::lit(",")) | (((-qi::lit("^") >> qi::lit("{")) >> (timeBound % qi::lit(","))) >> qi::lit("}"));
148 timeBounds.name("time bounds");
149 eventuallyFormula =
150 (qi::lit("F") > (-timeBounds) >
151 basicPathFormula(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createEventuallyFormula, phoenix::ref(*this), qi::_1, qi::_r1, qi::_2)];
152 eventuallyFormula.name("eventually formula");
153 nextFormula = (qi::lit("X") > basicPathFormula(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createNextFormula, phoenix::ref(*this), qi::_1)];
154 nextFormula.name("next formula");
155 globallyFormula =
156 (qi::lit("G") > basicPathFormula(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createGloballyFormula, phoenix::ref(*this), qi::_1)];
157 globallyFormula.name("globally formula");
158 hoaPathFormula =
159 qi::lit("HOA:") > qi::lit("{") > quotedString[qi::_val = phoenix::bind(&FormulaParserGrammar::createHOAPathFormula, phoenix::ref(*this), qi::_1)] >>
160 *(qi::lit(",") > quotedString > qi::lit("->") >
161 formula(FormulaKind::State, qi::_r1))[phoenix::bind(&FormulaParserGrammar::addHoaAPMapping, phoenix::ref(*this), *qi::_val, qi::_1, qi::_2)] >
162 qi::lit("}");
163 multiBoundedPathFormulaOperand = pathFormula(
164 qi::_r1)[qi::_pass = phoenix::bind(&FormulaParserGrammar::isValidMultiBoundedPathFormulaOperand, phoenix::ref(*this), qi::_1)][qi::_val = qi::_1];
165 multiBoundedPathFormulaOperand.name("multi bounded path formula operand");
166 multiBoundedPathFormula = ((qi::lit("multi") > qi::lit("(")) >> (multiBoundedPathFormulaOperand(qi::_r1) % qi::lit(",")) >>
167 qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createMultiBoundedPathFormula, phoenix::ref(*this), qi::_1)];
168 multiBoundedPathFormula.name("multi bounded path formula");
169 untilLevelPathFormula =
170 basicPathFormula(qi::_r1)[qi::_val = qi::_1] >>
171 -((qi::lit("U") > (-timeBounds) >
172 basicPathFormula(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createUntilFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]) >>
173 (qi::eps > noAmbiguousNonAssociativeOperator(qi::_val, std::string("U"))); // Do not parse a U b U c
174 untilLevelPathFormula.name("until precedence level path formula");
175 pathFormula = untilLevelPathFormula(qi::_r1);
176 pathFormula.name("path formula");
177
178 // Quantitative path formulae (reward)
179 discountedTotalRewardFormula =
180 (qi::lit("Cdiscount=") >>
181 expressionParser)[qi::_val = phoenix::bind(&FormulaParserGrammar::createDiscountedTotalRewardFormula, phoenix::ref(*this), qi::_1)];
182 discountedTotalRewardFormula.name("discounted total reward formula");
183 discountedCumulativeRewardFormula =
184 (qi::lit("C") >> timeBounds >> qi::lit("discount=") >>
185 expressionParser)[qi::_val = phoenix::bind(&FormulaParserGrammar::createDiscountedCumulativeRewardFormula, phoenix::ref(*this), qi::_2, qi::_1)];
186 discountedCumulativeRewardFormula.name("discounted cumulative reward formula");
187 longRunAverageRewardFormula = (qi::lit("LRA") | qi::lit("S") |
188 qi::lit("MP"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageRewardFormula, phoenix::ref(*this))];
189 longRunAverageRewardFormula.name("long run average reward formula");
190 instantaneousRewardFormula =
191 (qi::lit("I=") > expressionParser)[qi::_val = phoenix::bind(&FormulaParserGrammar::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)];
192 instantaneousRewardFormula.name("instantaneous reward formula");
193 cumulativeRewardFormula =
194 (qi::lit("C") >> timeBounds)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)];
195 cumulativeRewardFormula.name("cumulative reward formula");
196 totalRewardFormula = (qi::lit("C"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTotalRewardFormula, phoenix::ref(*this))];
197 totalRewardFormula.name("total reward formula");
198
199 // Game Formulae
200 playerCoalition = (-((identifier[phoenix::push_back(qi::_a, qi::_1)] | qi::uint_[phoenix::push_back(qi::_a, qi::_1)]) %
201 ','))[qi::_val = phoenix::bind(&FormulaParserGrammar::createPlayerCoalition, phoenix::ref(*this), qi::_a)];
202 playerCoalition.name("player coalition");
203 gameFormula = (qi::lit("<<") > playerCoalition > qi::lit(">>") >
204 operatorFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createGameFormula, phoenix::ref(*this), qi::_1, qi::_2)];
205 gameFormula.name("game formula");
206
207 // Multi-objective, quantiles
208 multiOperatorFormula = (qi::lit("multi") > qi::lit("(") > (operatorFormula % qi::lit(",")) >
209 qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createMultiOperatorFormula, phoenix::ref(*this), qi::_1,
210 storm::logic::MultiObjectiveFormula::Type::Tradeoff)];
211 multiOperatorFormula.name("multi-objective operator formula");
212 multiLexOperatorFormula = (qi::lit("multilex") > qi::lit("(") > (operatorFormula % qi::lit(",")) >
213 qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createMultiOperatorFormula, phoenix::ref(*this), qi::_1,
214 storm::logic::MultiObjectiveFormula::Type::Lexicographic)];
215 multiLexOperatorFormula.name("multi-objective lexicographic operator formula");
216 quantileBoundVariable = (-optimalityOperator_ >> identifier >>
217 qi::lit(","))[qi::_val = phoenix::bind(&FormulaParserGrammar::createQuantileBoundVariables, phoenix::ref(*this), qi::_1, qi::_2)];
218 quantileBoundVariable.name("quantile bound variable");
219 quantileFormula = (qi::lit("quantile") > qi::lit("(") > *(quantileBoundVariable) >
220 operatorFormula[qi::_pass = phoenix::bind(&FormulaParserGrammar::isBooleanReturnType, phoenix::ref(*this), qi::_1, true)] >
221 qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createQuantileFormula, phoenix::ref(*this), qi::_1, qi::_2)];
222 quantileFormula.name("Quantile formula");
223
224 // General formulae
225 formula = (isPathFormula(qi::_r1) >> pathFormula(qi::_r2) | propositionalFormula(qi::_r1, qi::_r2));
226 formula.name("formula");
227
228 topLevelFormula = formula(FormulaKind::State, storm::logic::FormulaContext::Undefined);
229 topLevelFormula.name("top-level formula");
230
231 formulaName = qi::lit("\"") >> identifier >> qi::lit("\"") >> qi::lit(":");
232 formulaName.name("formula name");
233
234 constantDefinition =
235 (qi::lit("const") > -(qi::lit("int")[qi::_a = ConstantDataType::Integer] | qi::lit("bool")[qi::_a = ConstantDataType::Bool] |
236 qi::lit("double")[qi::_a = ConstantDataType::Rational]) >>
237 identifier >> -(qi::lit("=") > expressionParser))[phoenix::bind(&FormulaParserGrammar::addConstant, phoenix::ref(*this), qi::_1, qi::_a, qi::_2)];
238 constantDefinition.name("constant definition");
239
240#pragma clang diagnostic push
241#pragma clang diagnostic ignored "-Woverloaded-shift-op-parentheses"
242
243 filterProperty =
244 (-formulaName >> qi::lit("filter") > qi::lit("(") > filterType_ > qi::lit(",") > topLevelFormula > qi::lit(",") >
245 formula(FormulaKind::State, storm::logic::FormulaContext::Undefined) >
246 qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProperty, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)] |
247 (-formulaName >>
248 topLevelFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates, phoenix::ref(*this), qi::_1, qi::_2)];
249 filterProperty.name("filter property");
250
251#pragma clang diagnostic pop
252
253 start = (qi::eps >> filterProperty[phoenix::push_back(qi::_val, qi::_1)] |
254 qi::eps(phoenix::bind(&FormulaParserGrammar::areConstantDefinitionsAllowed, phoenix::ref(*this))) >> constantDefinition | qi::eps) %
255 +(qi::char_("\n;")) >>
256 qi::skip(storm::spirit_encoding::space_type() | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)))[qi::eps] >> qi::eoi;
257 start.name("start");
258
259 // Enable the following lines to print debug output for most the rules.
260 // debug(rewardModelName)
261 // debug(operatorFormula)
262 // debug(labelFormula)
263 // debug(expressionFormula)
264 // debug(basicPropositionalFormula)
265 // debug(negationPropositionalFormula)
266 // debug(andLevelPropositionalFormula)
267 // debug(orLevelPropositionalFormula)
268 // debug(propositionalFormula)
269 // debug(timeBoundReference)
270 // debug(timeBound)
271 // debug(timeBounds)
272 // debug(eventuallyFormula)
273 // debug(nextFormula)
274 // debug(globallyFormula)
275 // debug(hoaPathFormula)
276 // debug(multiBoundedPathFormula)
277 // debug(prefixOperatorPathFormula)
278 // debug(basicPathFormula)
279 // debug(untilLevelPathFormula)
280 // debug(pathFormula)
281 // debug(longRunAverageRewardFormula)
282 // debug(instantaneousRewardFormula)
283 // debug(cumulativeRewardFormula)
284 // debug(totalRewardFormula)
285 // debug(playerCoalition)
286 // debug(gameFormula)
287 // debug(multiOperatorFormula)
288 // debug(multiLexOperatorFormula)
289 // debug(quantileBoundVariable)
290 // debug(quantileFormula)
291 // debug(formula)
292 // debug(topLevelFormula)
293 // debug(formulaName)
294 // debug(filterProperty)
295 // debug(constantDefinition )
296 // debug(start)
297 // debug(discountedCumulativeRewardFormula)
298 // debug(discountedTotalRewardFormula)
299
300 // Enable error reporting.
301 qi::on_error<qi::fail>(rewardModelName, handler(qi::_1, qi::_2, qi::_3, qi::_4));
302 qi::on_error<qi::fail>(operatorFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
303 qi::on_error<qi::fail>(labelFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
304 qi::on_error<qi::fail>(expressionFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
305 qi::on_error<qi::fail>(basicPropositionalFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
306 qi::on_error<qi::fail>(negationPropositionalFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
307 qi::on_error<qi::fail>(andLevelPropositionalFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
308 qi::on_error<qi::fail>(orLevelPropositionalFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
309 qi::on_error<qi::fail>(propositionalFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
310 qi::on_error<qi::fail>(timeBoundReference, handler(qi::_1, qi::_2, qi::_3, qi::_4));
311 qi::on_error<qi::fail>(timeBound, handler(qi::_1, qi::_2, qi::_3, qi::_4));
312 qi::on_error<qi::fail>(timeBounds, handler(qi::_1, qi::_2, qi::_3, qi::_4));
313 qi::on_error<qi::fail>(eventuallyFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
314 qi::on_error<qi::fail>(nextFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
315 qi::on_error<qi::fail>(globallyFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
316 qi::on_error<qi::fail>(hoaPathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
317 qi::on_error<qi::fail>(multiBoundedPathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
318 qi::on_error<qi::fail>(prefixOperatorPathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
319 qi::on_error<qi::fail>(basicPathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
320 qi::on_error<qi::fail>(untilLevelPathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
321 qi::on_error<qi::fail>(pathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
322 qi::on_error<qi::fail>(longRunAverageRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
323 qi::on_error<qi::fail>(instantaneousRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
324 qi::on_error<qi::fail>(cumulativeRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
325 qi::on_error<qi::fail>(totalRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
326 qi::on_error<qi::fail>(discountedCumulativeRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
327 qi::on_error<qi::fail>(discountedTotalRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
328 qi::on_error<qi::fail>(playerCoalition, handler(qi::_1, qi::_2, qi::_3, qi::_4));
329 qi::on_error<qi::fail>(gameFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
330 qi::on_error<qi::fail>(multiOperatorFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
331 qi::on_error<qi::fail>(multiLexOperatorFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
332 qi::on_error<qi::fail>(quantileBoundVariable, handler(qi::_1, qi::_2, qi::_3, qi::_4));
333 qi::on_error<qi::fail>(quantileFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
334 qi::on_error<qi::fail>(formula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
335 qi::on_error<qi::fail>(topLevelFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
336 qi::on_error<qi::fail>(formulaName, handler(qi::_1, qi::_2, qi::_3, qi::_4));
337 qi::on_error<qi::fail>(filterProperty, handler(qi::_1, qi::_2, qi::_3, qi::_4));
338 qi::on_error<qi::fail>(constantDefinition, handler(qi::_1, qi::_2, qi::_3, qi::_4));
339 qi::on_error<qi::fail>(start, handler(qi::_1, qi::_2, qi::_3, qi::_4));
340}
341
342void FormulaParserGrammar::addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression) {
343 STORM_LOG_WARN_COND(keywords_.find(identifier) == nullptr,
344 "Identifier `" << identifier << "' coincides with a reserved keyword or operator. Property expressions using the variable or constant '"
345 << identifier << "' will not be parsed correctly.");
346 STORM_LOG_WARN_COND(nonStandardKeywords_.find(identifier) == nullptr,
347 "Identifier `" << identifier << "' coincides with a reserved keyword or operator. Property expressions using the variable or constant '"
348 << identifier << "' might not be parsed correctly.");
349 this->identifiers_.add(identifier, expression);
350}
351
352void FormulaParserGrammar::addConstant(std::string const& name, ConstantDataType type, boost::optional<storm::expressions::Expression> const& expression) {
353 STORM_LOG_ASSERT(manager, "Mutable expression manager required to define new constants.");
354 storm::expressions::Variable newVariable;
355 STORM_LOG_THROW(!manager->hasVariable(name), storm::exceptions::WrongFormatException,
356 "Invalid constant definition '" << name << "' in property: variable already exists.");
357
358 if (type == ConstantDataType::Bool) {
359 newVariable = manager->declareBooleanVariable(name);
360 } else if (type == ConstantDataType::Integer) {
361 newVariable = manager->declareIntegerVariable(name);
362 } else {
363 newVariable = manager->declareRationalVariable(name);
364 }
365
366 if (expression) {
367 addIdentifierExpression(name, expression.get());
368 } else {
369 undefinedConstants.insert(newVariable);
370 addIdentifierExpression(name, newVariable);
371 }
372}
373
374bool FormulaParserGrammar::areConstantDefinitionsAllowed() const {
375 return static_cast<bool>(manager);
376}
377
378std::shared_ptr<storm::logic::TimeBoundReference> FormulaParserGrammar::createTimeBoundReference(storm::logic::TimeBoundType const& type,
379 boost::optional<std::string> const& rewardModelName) const {
380 if (type == storm::logic::TimeBoundType::Reward) {
381 return std::make_shared<storm::logic::TimeBoundReference>(rewardModelName);
382 } else {
383 return std::make_shared<storm::logic::TimeBoundReference>(type);
384 }
385}
386
387std::tuple<boost::optional<storm::logic::TimeBound>, boost::optional<storm::logic::TimeBound>, std::shared_ptr<storm::logic::TimeBoundReference>>
388FormulaParserGrammar::createTimeBoundFromInterval(storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound,
389 std::shared_ptr<storm::logic::TimeBoundReference> const& timeBoundReference) const {
390 // As soon as it somehow does not break everything anymore, I will change return types here.
391
392 storm::logic::TimeBound lower(false, lowerBound);
393 storm::logic::TimeBound upper(false, upperBound);
394 return std::make_tuple(lower, upper, timeBoundReference);
395}
396
397std::tuple<boost::optional<storm::logic::TimeBound>, boost::optional<storm::logic::TimeBound>, std::shared_ptr<storm::logic::TimeBoundReference>>
398FormulaParserGrammar::createTimeBoundFromSingleBound(storm::expressions::Expression const& bound, bool upperBound, bool strict,
399 std::shared_ptr<storm::logic::TimeBoundReference> const& timeBoundReference) const {
400 // As soon as it somehow does not break everything anymore, I will change return types here.
401 if (upperBound) {
402 return std::make_tuple(boost::none, storm::logic::TimeBound(strict, bound), timeBoundReference);
403 } else {
404 return std::make_tuple(storm::logic::TimeBound(strict, bound), boost::none, timeBoundReference);
405 }
406}
407
408std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createInstantaneousRewardFormula(storm::expressions::Expression const& timeBound) const {
409 return std::shared_ptr<storm::logic::Formula const>(new storm::logic::InstantaneousRewardFormula(timeBound));
410}
411
412std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createCumulativeRewardFormula(
413 std::vector<std::tuple<boost::optional<storm::logic::TimeBound>, boost::optional<storm::logic::TimeBound>,
414 std::shared_ptr<storm::logic::TimeBoundReference>>> const& timeBounds) const {
415 std::vector<storm::logic::TimeBound> bounds;
416 std::vector<storm::logic::TimeBoundReference> timeBoundReferences;
417 for (auto const& timeBound : timeBounds) {
418 STORM_LOG_THROW(!std::get<0>(timeBound), storm::exceptions::WrongFormatException, "Cumulative reward formulas with lower time bound are not allowed.");
419 STORM_LOG_THROW(std::get<1>(timeBound), storm::exceptions::WrongFormatException, "Cumulative reward formulas require an upper bound.");
420 bounds.push_back(std::get<1>(timeBound).get());
421 timeBoundReferences.emplace_back(*std::get<2>(timeBound));
422 }
423 return std::shared_ptr<storm::logic::Formula const>(new storm::logic::CumulativeRewardFormula(bounds, timeBoundReferences));
424}
425
426std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createDiscountedCumulativeRewardFormula(
427 storm::expressions::Expression const& discountFactor,
428 std::vector<std::tuple<boost::optional<storm::logic::TimeBound>, boost::optional<storm::logic::TimeBound>,
429 std::shared_ptr<storm::logic::TimeBoundReference>>> const& timeBounds) const {
430 std::vector<storm::logic::TimeBound> bounds;
431 std::vector<storm::logic::TimeBoundReference> timeBoundReferences;
432 for (auto const& timeBound : timeBounds) {
433 STORM_LOG_THROW(!std::get<0>(timeBound), storm::exceptions::WrongFormatException, "Cumulative reward formulas with lower time bound are not allowed.");
434 STORM_LOG_THROW(std::get<1>(timeBound), storm::exceptions::WrongFormatException, "Cumulative reward formulas require an upper bound.");
435 bounds.push_back(std::get<1>(timeBound).get());
436 timeBoundReferences.emplace_back(*std::get<2>(timeBound));
437 }
438 return std::shared_ptr<storm::logic::Formula const>(new storm::logic::DiscountedCumulativeRewardFormula(discountFactor, bounds, timeBoundReferences));
439}
440
441std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createTotalRewardFormula() const {
442 return std::shared_ptr<storm::logic::Formula const>(new storm::logic::TotalRewardFormula());
443}
444
445std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createDiscountedTotalRewardFormula(
446 storm::expressions::Expression const& discountFactor) const {
447 return std::shared_ptr<storm::logic::Formula const>(new storm::logic::DiscountedTotalRewardFormula(discountFactor));
448}
449
450std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createLongRunAverageRewardFormula() const {
451 return std::shared_ptr<storm::logic::Formula const>(new storm::logic::LongRunAverageRewardFormula());
452}
453
454std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createAtomicExpressionFormula(storm::expressions::Expression const& expression) const {
455 STORM_LOG_THROW(expression.hasBooleanType(), storm::exceptions::WrongFormatException,
456 "Expected expression " + expression.toString() + " to be of boolean type.");
457 if (expression.isLiteral()) {
458 return createBooleanLiteralFormula(expression.evaluateAsBool());
459 }
460 return std::shared_ptr<storm::logic::Formula const>(new storm::logic::AtomicExpressionFormula(expression));
461}
462
463std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createBooleanLiteralFormula(bool literal) const {
464 return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BooleanLiteralFormula(literal));
465}
466
467std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createAtomicLabelFormula(std::string const& label) const {
468 return std::shared_ptr<storm::logic::Formula const>(new storm::logic::AtomicLabelFormula(label));
469}
470
471std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createEventuallyFormula(
472 boost::optional<std::vector<std::tuple<boost::optional<storm::logic::TimeBound>, boost::optional<storm::logic::TimeBound>,
473 std::shared_ptr<storm::logic::TimeBoundReference>>>> const& timeBounds,
474 storm::logic::FormulaContext context, std::shared_ptr<storm::logic::Formula const> const& subformula) const {
475 if (timeBounds && !timeBounds.get().empty()) {
476 std::vector<boost::optional<storm::logic::TimeBound>> lowerBounds, upperBounds;
477 std::vector<storm::logic::TimeBoundReference> timeBoundReferences;
478 for (auto const& timeBound : timeBounds.get()) {
479 lowerBounds.push_back(std::get<0>(timeBound));
480 upperBounds.push_back(std::get<1>(timeBound));
481 timeBoundReferences.emplace_back(*std::get<2>(timeBound));
482 }
483 return std::shared_ptr<storm::logic::Formula const>(
484 new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, lowerBounds, upperBounds, timeBoundReferences));
485 } else {
486 return std::shared_ptr<storm::logic::Formula const>(new storm::logic::EventuallyFormula(subformula, context));
487 }
488}
489
490std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createGloballyFormula(std::shared_ptr<storm::logic::Formula const> const& subformula) const {
491 return std::shared_ptr<storm::logic::Formula const>(new storm::logic::GloballyFormula(subformula));
492}
493
494std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createNextFormula(std::shared_ptr<storm::logic::Formula const> const& subformula) const {
495 return std::shared_ptr<storm::logic::Formula const>(new storm::logic::NextFormula(subformula));
496}
497
498std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createUntilFormula(
499 std::shared_ptr<storm::logic::Formula const> const& leftSubformula,
500 boost::optional<std::vector<std::tuple<boost::optional<storm::logic::TimeBound>, boost::optional<storm::logic::TimeBound>,
501 std::shared_ptr<storm::logic::TimeBoundReference>>>> const& timeBounds,
502 std::shared_ptr<storm::logic::Formula const> const& rightSubformula) {
503 if (timeBounds && !timeBounds.get().empty()) {
504 std::vector<boost::optional<storm::logic::TimeBound>> lowerBounds, upperBounds;
505 std::vector<storm::logic::TimeBoundReference> timeBoundReferences;
506 for (auto const& timeBound : timeBounds.get()) {
507 lowerBounds.push_back(std::get<0>(timeBound));
508 upperBounds.push_back(std::get<1>(timeBound));
509 timeBoundReferences.emplace_back(*std::get<2>(timeBound));
510 }
511 return std::shared_ptr<storm::logic::Formula const>(
512 new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, lowerBounds, upperBounds, timeBoundReferences));
513 } else {
514 return std::shared_ptr<storm::logic::Formula const>(new storm::logic::UntilFormula(leftSubformula, rightSubformula));
515 }
516}
517
518std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createHOAPathFormula(std::string const& automatonFile) const {
519 return std::shared_ptr<storm::logic::Formula const>(new storm::logic::HOAPathFormula(automatonFile));
520}
521
522void FormulaParserGrammar::addHoaAPMapping(storm::logic::Formula const& hoaFormula, const std::string& ap,
523 std::shared_ptr<storm::logic::Formula const>& expression) const {
524 // taking a const Formula reference and doing static_ and const_cast from Formula to allow non-const access to
525 // qi::_val of the hoaPathFormula rule
526 storm::logic::HOAPathFormula& hoaFormula_ = static_cast<storm::logic::HOAPathFormula&>(const_cast<storm::logic::Formula&>(hoaFormula));
527 hoaFormula_.addAPMapping(ap, expression);
528}
529
530std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createConditionalFormula(
531 std::shared_ptr<storm::logic::Formula const> const& leftSubformula, boost::optional<std::shared_ptr<storm::logic::Formula const>> const& rightSubformula,
532 storm::logic::FormulaContext context) const {
533 if (rightSubformula) {
534 return std::shared_ptr<storm::logic::Formula const>(new storm::logic::ConditionalFormula(leftSubformula, rightSubformula.get(), context));
535 } else {
536 // If there is no rhs, just return the lhs
537 return leftSubformula;
538 }
539}
540
541storm::logic::OperatorInformation FormulaParserGrammar::createOperatorInformation(boost::optional<storm::OptimizationDirection> const& optimizationDirection,
542 boost::optional<storm::logic::ComparisonType> const& comparisonType,
543 boost::optional<storm::expressions::Expression> const& threshold) const {
544 if (comparisonType && threshold) {
545 storm::expressions::ExpressionEvaluator<storm::RationalNumber> evaluator(*constManager);
546 return storm::logic::OperatorInformation(optimizationDirection, storm::logic::Bound(comparisonType.get(), threshold.get()));
547 } else {
548 return storm::logic::OperatorInformation(optimizationDirection, boost::none);
549 }
550}
551
552std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createOperatorFormula(storm::logic::FormulaContext const& context,
553 boost::optional<std::string> const& rewardModelName,
554 storm::logic::OperatorInformation const& operatorInformation,
555 std::shared_ptr<storm::logic::Formula const> const& subformula) {
556 switch (context) {
557 case storm::logic::FormulaContext::Probability:
558 STORM_LOG_ASSERT(!rewardModelName, "Probability operator with reward information parsed");
559 return createProbabilityOperatorFormula(operatorInformation, subformula);
560 case storm::logic::FormulaContext::Reward:
561 return createRewardOperatorFormula(rewardModelName, operatorInformation, subformula);
562 case storm::logic::FormulaContext::LongRunAverage:
563 STORM_LOG_ASSERT(!rewardModelName, "LRA operator with reward information parsed");
564 return createLongRunAverageOperatorFormula(operatorInformation, subformula);
565 case storm::logic::FormulaContext::Time:
566 STORM_LOG_ASSERT(!rewardModelName, "Time operator with reward model name parsed");
567 return createTimeOperatorFormula(operatorInformation, subformula);
568 default:
569 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Unexpected formula context.");
570 }
571}
572
573std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createLongRunAverageOperatorFormula(
574 storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula const> const& subformula) const {
575 return std::shared_ptr<storm::logic::Formula const>(new storm::logic::LongRunAverageOperatorFormula(subformula, operatorInformation));
576}
577
578std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createRewardOperatorFormula(
579 boost::optional<std::string> const& rewardModelName, storm::logic::OperatorInformation const& operatorInformation,
580 std::shared_ptr<storm::logic::Formula const> const& subformula) const {
581 return std::shared_ptr<storm::logic::Formula const>(new storm::logic::RewardOperatorFormula(subformula, rewardModelName, operatorInformation));
582}
583
584std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createTimeOperatorFormula(
585 storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula const> const& subformula) const {
586 return std::shared_ptr<storm::logic::Formula const>(new storm::logic::TimeOperatorFormula(subformula, operatorInformation));
587}
588
589std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createProbabilityOperatorFormula(
590 storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula const> const& subformula) {
591 return std::shared_ptr<storm::logic::Formula const>(new storm::logic::ProbabilityOperatorFormula(subformula, operatorInformation));
592}
593
594std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createBinaryBooleanStateFormula(
595 std::shared_ptr<storm::logic::Formula const> const& leftSubformula, std::shared_ptr<storm::logic::Formula const> const& rightSubformula,
596 storm::logic::BinaryBooleanStateFormula::OperatorType operatorType) {
597 return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BinaryBooleanStateFormula(operatorType, leftSubformula, rightSubformula));
598}
599
600std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createUnaryBooleanStateFormula(
601 std::shared_ptr<storm::logic::Formula const> const& subformula, boost::optional<storm::logic::UnaryBooleanStateFormula::OperatorType> const& operatorType) {
602 if (operatorType) {
603 return std::shared_ptr<storm::logic::Formula const>(new storm::logic::UnaryBooleanStateFormula(operatorType.get(), subformula));
604 } else {
605 return subformula;
606 }
607}
608
609std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createBinaryBooleanPathFormula(
610 std::shared_ptr<storm::logic::Formula const> const& leftSubformula, std::shared_ptr<storm::logic::Formula const> const& rightSubformula,
611 storm::logic::BinaryBooleanPathFormula::OperatorType operatorType) {
612 return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BinaryBooleanPathFormula(operatorType, leftSubformula, rightSubformula));
613}
614
615std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createUnaryBooleanPathFormula(
616 std::shared_ptr<storm::logic::Formula const> const& subformula, boost::optional<storm::logic::UnaryBooleanPathFormula::OperatorType> const& operatorType) {
617 if (operatorType) {
618 return std::shared_ptr<storm::logic::Formula const>(new storm::logic::UnaryBooleanPathFormula(operatorType.get(), subformula));
619 } else {
620 return subformula;
621 }
622}
623
624std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createBinaryBooleanStateOrPathFormula(
625 std::shared_ptr<storm::logic::Formula const> const& leftSubformula, std::shared_ptr<storm::logic::Formula const> const& rightSubformula,
626 storm::logic::BinaryBooleanOperatorType operatorType) {
627 if (leftSubformula->isStateFormula() && rightSubformula->isStateFormula()) {
628 return createBinaryBooleanStateFormula(leftSubformula, rightSubformula, operatorType);
629 } else if (leftSubformula->isPathFormula() || rightSubformula->isPathFormula()) {
630 return createBinaryBooleanPathFormula(leftSubformula, rightSubformula, operatorType);
631 }
632 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Subformulas have unexpected type.");
633}
634
635std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createUnaryBooleanStateOrPathFormula(
636 std::shared_ptr<storm::logic::Formula const> const& subformula, boost::optional<storm::logic::UnaryBooleanOperatorType> const& operatorType) {
637 if (subformula->isStateFormula()) {
638 return createUnaryBooleanStateFormula(subformula, operatorType);
639 } else if (subformula->isPathFormula()) {
640 return createUnaryBooleanPathFormula(subformula, operatorType);
641 }
642 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Subformulas have unexpected type.");
643}
644
645bool FormulaParserGrammar::isValidMultiBoundedPathFormulaOperand(std::shared_ptr<storm::logic::Formula const> const& operand) {
646 if (operand->isBoundedUntilFormula()) {
647 if (!operand->asBoundedUntilFormula().isMultiDimensional()) {
648 return true;
649 }
650 STORM_LOG_ERROR("Composition of multidimensional bounded until formula must consist of single dimension subformulas. Got '" << *operand
651 << "' instead.");
652 }
653 return false;
654}
655
656std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createMultiBoundedPathFormula(
657 std::vector<std::shared_ptr<storm::logic::Formula const>> const& subformulas) {
658 std::vector<std::shared_ptr<storm::logic::Formula const>> leftSubformulas, rightSubformulas;
659 std::vector<boost::optional<storm::logic::TimeBound>> lowerBounds, upperBounds;
660 std::vector<storm::logic::TimeBoundReference> timeBoundReferences;
661 for (auto const& subformula : subformulas) {
662 STORM_LOG_THROW(subformula->isBoundedUntilFormula(), storm::exceptions::WrongFormatException,
663 "multi-path formulas require bounded until (or eventually) subformulae. Got '" << *subformula << "' instead.");
664 auto const& f = subformula->asBoundedUntilFormula();
665 STORM_LOG_THROW(!f.isMultiDimensional(), storm::exceptions::WrongFormatException,
666 "Composition of multidimensional bounded until formula must consist of single dimension subformulas. Got '" << f << "' instead.");
667 leftSubformulas.push_back(f.getLeftSubformula().asSharedPointer());
668 rightSubformulas.push_back(f.getRightSubformula().asSharedPointer());
669 if (f.hasLowerBound()) {
670 lowerBounds.emplace_back(storm::logic::TimeBound(f.isLowerBoundStrict(), f.getLowerBound()));
671 } else {
672 lowerBounds.emplace_back();
673 }
674 if (f.hasUpperBound()) {
675 upperBounds.emplace_back(storm::logic::TimeBound(f.isUpperBoundStrict(), f.getUpperBound()));
676 } else {
677 upperBounds.emplace_back();
678 }
679 timeBoundReferences.push_back(f.getTimeBoundReference());
680 }
681 return std::shared_ptr<storm::logic::Formula const>(
682 new storm::logic::BoundedUntilFormula(leftSubformulas, rightSubformulas, lowerBounds, upperBounds, timeBoundReferences));
683}
684
685std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createMultiOperatorFormula(
686 std::vector<std::shared_ptr<storm::logic::Formula const>> const& subformulas, storm::logic::MultiObjectiveFormula::Type type) {
687 return std::shared_ptr<storm::logic::Formula const>(new storm::logic::MultiObjectiveFormula(subformulas, type));
688}
689
690storm::expressions::Variable FormulaParserGrammar::createQuantileBoundVariables(boost::optional<storm::solver::OptimizationDirection> const& dir,
691 std::string const& variableName) {
692 STORM_LOG_ASSERT(manager, "Mutable expression manager required to define quantile bound variable.");
693 storm::expressions::Variable var;
694 if (manager->hasVariable(variableName)) {
695 var = manager->getVariable(variableName);
696 STORM_LOG_THROW(quantileFormulaVariables.count(var) > 0, storm::exceptions::WrongFormatException,
697 "Invalid quantile variable name '" << variableName << "' in quantile formula: variable already exists.");
698 } else {
699 var = manager->declareRationalVariable(variableName);
700 quantileFormulaVariables.insert(var);
701 }
702 STORM_LOG_WARN_COND(!dir.is_initialized(), "Optimization direction '"
703 << dir.get() << "' for quantile variable " << variableName
704 << " is ignored. This information will be derived from the subformula of the quantile.");
705 addIdentifierExpression(variableName, var);
706 return var;
707}
708
709std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createQuantileFormula(std::vector<storm::expressions::Variable> const& boundVariables,
710 std::shared_ptr<storm::logic::Formula const> const& subformula) {
711 return std::shared_ptr<storm::logic::Formula const>(new storm::logic::QuantileFormula(boundVariables, subformula));
712}
713
714std::set<storm::expressions::Variable> FormulaParserGrammar::getUndefinedConstants(std::shared_ptr<storm::logic::Formula const> const& formula) const {
715 std::set<storm::expressions::Variable> result;
716 std::set<storm::expressions::Variable> usedVariables = formula->getUsedVariables();
717 std::set_intersection(usedVariables.begin(), usedVariables.end(), undefinedConstants.begin(), undefinedConstants.end(),
718 std::inserter(result, result.begin()));
719 return result;
720}
721
722storm::jani::Property FormulaParserGrammar::createProperty(boost::optional<std::string> const& propertyName, storm::modelchecker::FilterType const& filterType,
723 std::shared_ptr<storm::logic::Formula const> const& formula,
724 std::shared_ptr<storm::logic::Formula const> const& states) {
725 storm::jani::FilterExpression filterExpression(formula, filterType, states);
726
727 ++propertyCount;
728 if (propertyName) {
729 return storm::jani::Property(propertyName.get(), filterExpression, this->getUndefinedConstants(formula));
730 } else {
731 return storm::jani::Property(std::to_string(propertyCount - 1), filterExpression, this->getUndefinedConstants(formula));
732 }
733}
734
735storm::jani::Property FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates(boost::optional<std::string> const& propertyName,
736 std::shared_ptr<storm::logic::Formula const> const& formula) {
737 ++propertyCount;
738 if (propertyName) {
739 return storm::jani::Property(propertyName.get(), formula, this->getUndefinedConstants(formula));
740 } else {
741 return storm::jani::Property(std::to_string(propertyCount), formula, this->getUndefinedConstants(formula));
742 }
743}
744
745storm::logic::PlayerCoalition FormulaParserGrammar::createPlayerCoalition(
746 std::vector<std::variant<std::string, storm::storage::PlayerIndex>> const& playerIds) const {
747 return storm::logic::PlayerCoalition(playerIds);
748}
749
750std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createGameFormula(storm::logic::PlayerCoalition const& coalition,
751 std::shared_ptr<storm::logic::Formula const> const& subformula) const {
752 return std::shared_ptr<storm::logic::Formula const>(new storm::logic::GameFormula(coalition, subformula));
753}
754
755bool FormulaParserGrammar::isBooleanReturnType(std::shared_ptr<storm::logic::Formula const> const& formula, bool raiseErrorMessage) {
756 if (formula->hasQualitativeResult()) {
757 return true;
758 }
759 STORM_LOG_ERROR_COND(!raiseErrorMessage, "Formula " << *formula << " does not have a Boolean return type.");
760 return false;
761}
762
763bool FormulaParserGrammar::raiseAmbiguousNonAssociativeOperatorError(std::shared_ptr<storm::logic::Formula const> const& formula, std::string const& op) {
764 STORM_LOG_ERROR("Ambiguous use of non-associative operator '" << op << "' in formula '" << *formula << " U ... '");
765 return true;
766}
767
768} // namespace parser
769} // namespace storm
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::hasBooleanType
bool hasBooleanType() const
Retrieves whether the expression has a boolean return type.
Definition Expression.cpp:193
storm::expressions::Expression::isLiteral
bool isLiteral() const
Retrieves whether the expression is a literal.
Definition Expression.cpp:110
storm::expressions::Expression::toString
std::string toString() const
Converts the expression into a string.
Definition Expression.cpp:236
storm::logic::HOAPathFormula::addAPMapping
void addAPMapping(const std::string &ap, const std::shared_ptr< Formula const > &formula)
Definition HOAPathFormula.cpp:32
storm::parser::ExpressionParser::setIdentifierMapping
void setIdentifierMapping(qi::symbols< char, storm::expressions::Expression > const *identifiers_)
Sets an identifier mapping that is used to determine valid variables in the expression.
Definition ExpressionParser.cpp:312
storm::parser::FormulaParserGrammar::getIdentifiers
qi::symbols< char, storm::expressions::Expression > const & getIdentifiers() const
Definition FormulaParserGrammar.cpp:20
storm::parser::FormulaParserGrammar::FormulaParserGrammar
FormulaParserGrammar(std::shared_ptr< storm::expressions::ExpressionManager const > const &manager)
Definition FormulaParserGrammar.cpp:10
storm::parser::FormulaParserGrammar::addIdentifierExpression
void addIdentifierExpression(std::string const &identifier, storm::expressions::Expression const &expression)
Adds an identifier and the expression it is supposed to be replaced with.
Definition FormulaParserGrammar.cpp:342
STORM_LOG_ERROR
#define STORM_LOG_ERROR(message)
Definition logging.h:26
STORM_LOG_ASSERT
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
STORM_LOG_WARN_COND
#define STORM_LOG_WARN_COND(cond, message)
Definition macros.h:38
STORM_LOG_ERROR_COND
#define STORM_LOG_ERROR_COND(cond, message)
Definition macros.h:52
STORM_LOG_THROW
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30