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