Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
PrismParserGrammar.cpp
Go to the documentation of this file.
1#include "storm-parsers/parser/PrismParserGrammar.h"
2
3#include <unordered_set>
4#include "storm/storage/prism/Compositions.h"
5
6#include "storm/exceptions/InvalidArgumentException.h"
7#include "storm/exceptions/InvalidTypeException.h"
8#include "storm/exceptions/UnexpectedException.h"
9#include "storm/exceptions/WrongFormatException.h"
10#include "storm/io/file.h"
11#include "storm/utility/macros.h"
12
13#include "storm/storage/BitVector.h"
14#include "storm/storage/expressions/ExpressionManager.h"
15#include "storm/storage/expressions/VariableExpression.h"
16
17#include "storm-parsers/parser/ExpressionParser.h"
18
19namespace storm {
20namespace parser {
21storm::prism::Program PrismParserGrammar::parse(std::string const& filename, bool prismCompatibility) {
22 // Open file and initialize result.
23 std::ifstream inputFileStream;
24 storm::io::openFile(filename, inputFileStream);
25 storm::prism::Program result;
26
27 // Now try to parse the contents of the file.
28 try {
29 std::string fileContent((std::istreambuf_iterator<char>(inputFileStream)), (std::istreambuf_iterator<char>()));
30 result = parseFromString(fileContent, filename, prismCompatibility);
31 } catch (storm::exceptions::WrongFormatException& e) {
32 // In case of an exception properly close the file before passing exception.
33 storm::io::closeFile(inputFileStream);
34 throw e;
35 } catch (std::exception& e) {
36 // In case of an exception properly close the file before passing exception.
37 storm::io::closeFile(inputFileStream);
38 throw e;
39 }
40
41 // Close the stream in case everything went smoothly and return result.
42 storm::io::closeFile(inputFileStream);
43 return result;
44}
45
46storm::prism::Program PrismParserGrammar::parseFromString(std::string const& input, std::string const& filename, bool prismCompatibility) {
47 bool hasByteOrderMark = input.size() >= 3 && input[0] == '\xEF' && input[1] == '\xBB' && input[2] == '\xBF';
48
49 PositionIteratorType first(hasByteOrderMark ? input.begin() + 3 : input.begin());
50 PositionIteratorType iter = first;
51 PositionIteratorType last(input.end());
52 STORM_LOG_ASSERT(first != last, "Illegal input to PRISM parser.");
53
54 // Create empty result;
55 storm::prism::Program result;
56
57 // Create grammar.
58 storm::parser::PrismParserGrammar grammar(filename, first, prismCompatibility);
59 try {
60 // Start first run.
61 storm::spirit_encoding::space_type space;
62 bool succeeded = qi::phrase_parse(iter, last, grammar, space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), result);
63 STORM_LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Parsing failed in first pass.");
64 STORM_LOG_DEBUG("First pass of parsing PRISM input finished.");
65
66 // Start second run.
67 first = PositionIteratorType(input.begin());
68 iter = first;
69 last = PositionIteratorType(input.end());
70 grammar.moveToSecondRun();
71 succeeded = qi::phrase_parse(iter, last, grammar, space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), result);
72 STORM_LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Parsing failed in second pass.");
73 } catch (qi::expectation_failure<PositionIteratorType> const& e) {
74 // If the parser expected content different than the one provided, display information about the location of the error.
75 std::size_t lineNumber = boost::spirit::get_line(e.first);
76
77 // Now propagate exception.
78 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << lineNumber << " of file " << filename << ".");
79 }
80
81 STORM_LOG_TRACE("Parsed PRISM input: " << result);
82
83 return result;
84}
85
86PrismParserGrammar::PrismParserGrammar(std::string const& filename, Iterator first, bool prismCompatibility)
87 : PrismParserGrammar::base_type(start),
88 secondRun(false),
89 prismCompatibility(prismCompatibility),
90 filename(filename),
91 annotate(first),
92 manager(new storm::expressions::ExpressionManager()),
93 expressionParser(new ExpressionParser(*manager, expressionKeywords_, false, false)) {
94 ExpressionParser& expression_ = *expressionParser;
95 boolExpression = (expression_[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParserGrammar::isOfBoolType, phoenix::ref(*this), qi::_val)];
96 boolExpression.name("boolean expression");
97
98 intExpression = (expression_[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParserGrammar::isOfIntType, phoenix::ref(*this), qi::_val)];
99 intExpression.name("integer expression");
100
101 numericalExpression = (expression_[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParserGrammar::isOfNumericalType, phoenix::ref(*this), qi::_val)];
102 numericalExpression.name("numerical expression");
103
104 // Parse simple identifier.
105 identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]]
106 [qi::_pass = phoenix::bind(&PrismParserGrammar::isValidIdentifier, phoenix::ref(*this), qi::_1)];
107 identifier.name("identifier");
108
109 // Fail if the identifier has been used before
110 freshIdentifier = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParserGrammar::isFreshIdentifier, phoenix::ref(*this), qi::_1)];
111 freshIdentifier.name("fresh identifier");
112
113 modelTypeDefinition %= modelType_;
114 modelTypeDefinition.name("model type");
115
116 // Defined constants. Will be checked before undefined constants.
117 // ">>" before literal '=' because we can still parse an undefined constant afterwards.
118 definedBooleanConstantDefinition =
119 (((qi::lit("const") >> qi::lit("bool")) > freshIdentifier) >>
120 (qi::lit("=") > boolExpression >
121 qi::lit(";")))[qi::_val = phoenix::bind(&PrismParserGrammar::createDefinedBooleanConstant, phoenix::ref(*this), qi::_1, qi::_2)];
122 definedBooleanConstantDefinition.name("defined boolean constant declaration");
123
124 definedIntegerConstantDefinition =
125 (((qi::lit("const") >> -qi::lit("int")) >> freshIdentifier) >>
126 (qi::lit("=") > intExpression > qi::lit(";")))[qi::_val = phoenix::bind(&PrismParserGrammar::createDefinedIntegerConstant, phoenix::ref(*this), qi::_1,
127 qi::_2)]; // '>>' before freshIdentifier because of the optional 'int'.
128 // Otherwise, undefined constant 'const bool b;' would not parse.
129 definedIntegerConstantDefinition.name("defined integer constant declaration");
130
131 definedDoubleConstantDefinition =
132 (((qi::lit("const") >> qi::lit("double")) > freshIdentifier) >>
133 (qi::lit("=") > numericalExpression >
134 qi::lit(";")))[qi::_val = phoenix::bind(&PrismParserGrammar::createDefinedDoubleConstant, phoenix::ref(*this), qi::_1, qi::_2)];
135 definedDoubleConstantDefinition.name("defined double constant declaration");
136
137 definedConstantDefinition %= (definedBooleanConstantDefinition | definedDoubleConstantDefinition | definedIntegerConstantDefinition);
138 definedConstantDefinition.name("defined constant definition");
139
140 // Undefined constants. At this point we already checked for a defined constant, therefore a ";" is required after the identifier;
141 undefinedBooleanConstantDefinition =
142 (((qi::lit("const") >> qi::lit("bool")) > freshIdentifier) >
143 qi::lit(";"))[qi::_val = phoenix::bind(&PrismParserGrammar::createUndefinedBooleanConstant, phoenix::ref(*this), qi::_1)];
144 undefinedBooleanConstantDefinition.name("undefined boolean constant declaration");
145
146 undefinedIntegerConstantDefinition =
147 (((qi::lit("const") >> -qi::lit("int")) > freshIdentifier) >
148 qi::lit(";"))[qi::_val = phoenix::bind(&PrismParserGrammar::createUndefinedIntegerConstant, phoenix::ref(*this), qi::_1)];
149 undefinedIntegerConstantDefinition.name("undefined integer constant declaration");
150
151 undefinedDoubleConstantDefinition =
152 (((qi::lit("const") >> qi::lit("double")) > freshIdentifier) >
153 qi::lit(";"))[qi::_val = phoenix::bind(&PrismParserGrammar::createUndefinedDoubleConstant, phoenix::ref(*this), qi::_1)];
154 undefinedDoubleConstantDefinition.name("undefined double constant definition");
155
156 undefinedConstantDefinition = (undefinedBooleanConstantDefinition | undefinedDoubleConstantDefinition |
157 undefinedIntegerConstantDefinition); // Due to the 'const N;' syntax, it is important to have integer constants last
158
159 undefinedConstantDefinition.name("undefined constant definition");
160
161 // formula definitions. This will be changed for the second run.
162 formulaDefinitionRhs = (qi::lit("=") > qi::as_string[(+(qi::char_ - (qi::lit(";") | qi::lit("endmodule"))))][qi::_val = qi::_1] > qi::lit(";"));
163 formulaDefinitionRhs.name("formula defining expression");
164
165 formulaDefinition = (qi::lit("formula") > freshIdentifier >
166 formulaDefinitionRhs)[qi::_val = phoenix::bind(&PrismParserGrammar::createFormulaFirstRun, phoenix::ref(*this), qi::_1, qi::_2)];
167 formulaDefinition.name("formula definition");
168
169 booleanVariableDefinition =
170 (((freshIdentifier > qi::lit(":")) >> qi::lit("bool")) > -((qi::lit("init") > boolExpression[qi::_a = qi::_1]) | qi::attr(manager->boolean(false))) >
171 qi::lit(";"))[qi::_val = phoenix::bind(&PrismParserGrammar::createBooleanVariable, phoenix::ref(*this), qi::_1, qi::_a)];
172 booleanVariableDefinition.name("boolean variable definition");
173
174 boundedIntegerVariableDefinition =
175 (((freshIdentifier > qi::lit(":")) >> qi::lit("[")) > intExpression > qi::lit("..") > intExpression > qi::lit("]") >
176 -(qi::lit("init") > intExpression[qi::_a = qi::_1]) >
177 qi::lit(";"))[qi::_val = phoenix::bind(&PrismParserGrammar::createIntegerVariable, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_a)];
178 boundedIntegerVariableDefinition.name("bounded integer variable definition");
179
180 unboundedIntegerVariableDefinition = (((freshIdentifier > qi::lit(":")) >> qi::lit("int")) > -(qi::lit("init") > intExpression[qi::_a = qi::_1]) >
181 qi::lit(";"))[qi::_val = phoenix::bind(&PrismParserGrammar::createIntegerVariable, phoenix::ref(*this), qi::_1,
182 storm::expressions::Expression(), storm::expressions::Expression(), qi::_a)];
183 unboundedIntegerVariableDefinition.name("unbounded integer variable definition");
184
185 integerVariableDefinition = boundedIntegerVariableDefinition | unboundedIntegerVariableDefinition;
186 integerVariableDefinition.name("integer variable definition");
187
188 clockVariableDefinition = (((freshIdentifier > qi::lit(":")) >> qi::lit("clock")) >
189 qi::lit(";"))[qi::_val = phoenix::bind(&PrismParserGrammar::createClockVariable, phoenix::ref(*this), qi::_1)];
190 clockVariableDefinition.name("clock variable definition");
191
192 variableDefinition = (booleanVariableDefinition[phoenix::push_back(qi::_r1, qi::_1)] | integerVariableDefinition[phoenix::push_back(qi::_r2, qi::_1)] |
193 clockVariableDefinition[phoenix::push_back(qi::_r3, qi::_1)]);
194 variableDefinition.name("variable declaration");
195
196 globalVariableDefinition =
197 (qi::lit("global") >
198 (booleanVariableDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::globalBooleanVariables, qi::_r1), qi::_1)] |
199 integerVariableDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::globalIntegerVariables, qi::_r1), qi::_1)]));
200 globalVariableDefinition.name("global variable declaration list");
201
202 stateRewardDefinition = (boolExpression > qi::lit(":") > numericalExpression >
203 qi::lit(";"))[qi::_val = phoenix::bind(&PrismParserGrammar::createStateReward, phoenix::ref(*this), qi::_1, qi::_2)];
204 stateRewardDefinition.name("state reward definition");
205
206 stateActionRewardDefinition =
207 (qi::lit("[") > -identifier > qi::lit("]") > boolExpression > qi::lit(":") > numericalExpression >
208 qi::lit(";"))[qi::_val = phoenix::bind(&PrismParserGrammar::createStateActionReward, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_r1)];
209 stateActionRewardDefinition.name("state action reward definition");
210
211 transitionRewardDefinition =
212 ((qi::lit("[") > -identifier[qi::_a = qi::_1] > qi::lit("]") > boolExpression[qi::_b = qi::_1]) >>
213 (qi::lit("->") > boolExpression[qi::_c = qi::_1] > qi::lit(":") > numericalExpression[qi::_d = qi::_1] >
214 qi::lit(";")))[qi::_val = phoenix::bind(&PrismParserGrammar::createTransitionReward, phoenix::ref(*this), qi::_a, qi::_b, qi::_c, qi::_d, qi::_r1)];
215 transitionRewardDefinition.name("transition reward definition");
216
217 freshRewardModelName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParserGrammar::isFreshRewardModelName, phoenix::ref(*this), qi::_1)];
218 freshRewardModelName.name("fresh reward model name");
219
220 rewardModelDefinition =
221 (qi::lit("rewards") > -(qi::lit("\"") > freshRewardModelName[qi::_a = qi::_1] > qi::lit("\"")) >
222 +(transitionRewardDefinition(qi::_r1)[phoenix::push_back(qi::_d, qi::_1)] | stateActionRewardDefinition(qi::_r1)[phoenix::push_back(qi::_c, qi::_1)] |
223 stateRewardDefinition[phoenix::push_back(qi::_b, qi::_1)]) >
224 qi::lit("endrewards"))[qi::_val = phoenix::bind(&PrismParserGrammar::createRewardModel, phoenix::ref(*this), qi::_a, qi::_b, qi::_c, qi::_d)];
225 rewardModelDefinition.name("reward model definition");
226
227 initialStatesConstruct =
228 (qi::lit("init") > boolExpression >
229 qi::lit("endinit"))[qi::_pass = phoenix::bind(&PrismParserGrammar::addInitialStatesConstruct, phoenix::ref(*this), qi::_1, qi::_r1)];
230 initialStatesConstruct.name("initial construct");
231
232 observablesConstruct =
233 (qi::lit("observables") > (identifier % qi::lit(",")) >
234 qi::lit("endobservables"))[qi::_pass = phoenix::bind(&PrismParserGrammar::addObservablesConstruct, phoenix::ref(*this), qi::_1, qi::_r1)];
235 observablesConstruct.name("observables construct");
236
237 invariantConstruct = (qi::lit("invariant") > boolExpression > qi::lit("endinvariant"))[qi::_val = qi::_1];
238 invariantConstruct.name("invariant construct");
239
240 knownModuleName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParserGrammar::isKnownModuleName, phoenix::ref(*this), qi::_1, false)];
241 knownModuleName.name("existing module name");
242
243 freshModuleName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParserGrammar::isFreshModuleName, phoenix::ref(*this), qi::_1)];
244 freshModuleName.name("fresh module name");
245
246 systemCompositionConstruct =
247 (qi::lit("system") > parallelComposition >
248 qi::lit("endsystem"))[phoenix::bind(&PrismParserGrammar::addSystemCompositionConstruct, phoenix::ref(*this), qi::_1, qi::_r1)];
249 systemCompositionConstruct.name("system composition construct");
250
251 actionNameList %= identifier[phoenix::insert(qi::_val, qi::_1)] >> *("," >> identifier[phoenix::insert(qi::_val, qi::_1)]);
252 actionNameList.name("action list");
253
254 parallelComposition =
255 hidingOrRenamingComposition[qi::_val = qi::_1] >>
256 *((interleavingParallelComposition > hidingOrRenamingComposition)[qi::_val = phoenix::bind(&PrismParserGrammar::createInterleavingParallelComposition,
257 phoenix::ref(*this), qi::_val, qi::_1)] |
258 (synchronizingParallelComposition > hidingOrRenamingComposition)[qi::_val = phoenix::bind(&PrismParserGrammar::createSynchronizingParallelComposition,
259 phoenix::ref(*this), qi::_val, qi::_1)] |
260 (restrictedParallelComposition > hidingOrRenamingComposition)[qi::_val = phoenix::bind(&PrismParserGrammar::createRestrictedParallelComposition,
261 phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]);
262 parallelComposition.name("parallel composition");
263
264 synchronizingParallelComposition = qi::lit("||");
265 synchronizingParallelComposition.name("synchronizing parallel composition");
266
267 interleavingParallelComposition = qi::lit("|||");
268 interleavingParallelComposition.name("interleaving parallel composition");
269
270 restrictedParallelComposition = qi::lit("|[") > actionNameList > qi::lit("]|");
271 restrictedParallelComposition.name("restricted parallel composition");
272
273 hidingOrRenamingComposition = hidingComposition | renamingComposition | atomicComposition;
274 hidingOrRenamingComposition.name("hiding/renaming composition");
275
276 hidingComposition =
277 (atomicComposition >>
278 (qi::lit("/") > (qi::lit("{") > actionNameList >
279 qi::lit("}"))))[qi::_val = phoenix::bind(&PrismParserGrammar::createHidingComposition, phoenix::ref(*this), qi::_1, qi::_2)];
280 hidingComposition.name("hiding composition");
281
282 actionRenamingList =
283 +(identifier >> (qi::lit("<-") >> identifier))[phoenix::insert(qi::_val, phoenix::construct<std::pair<std::string, std::string>>(qi::_1, qi::_2))];
284 actionRenamingList.name("action renaming list");
285
286 renamingComposition =
287 (atomicComposition >>
288 (qi::lit("{") >
289 (actionRenamingList > qi::lit("}"))))[qi::_val = phoenix::bind(&PrismParserGrammar::createRenamingComposition, phoenix::ref(*this), qi::_1, qi::_2)];
290 renamingComposition.name("renaming composition");
291
292 atomicComposition = (qi::lit("(") > parallelComposition > qi::lit(")")) | moduleComposition;
293 atomicComposition.name("atomic composition");
294
295 moduleComposition = identifier[qi::_val = phoenix::bind(&PrismParserGrammar::createModuleComposition, phoenix::ref(*this), qi::_1)];
296 moduleComposition.name("module composition");
297
298 freshLabelName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParserGrammar::isFreshLabelName, phoenix::ref(*this), qi::_1)];
299 freshLabelName.name("fresh label name");
300
301 labelDefinition = (qi::lit("label") > -qi::lit("\"") > freshLabelName > -qi::lit("\"") > qi::lit("=") > boolExpression >
302 qi::lit(";"))[qi::_val = phoenix::bind(&PrismParserGrammar::createLabel, phoenix::ref(*this), qi::_1, qi::_2)];
303 labelDefinition.name("label definition");
304
305 freshObservationLabelName =
306 (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParserGrammar::isFreshObservationLabelName, phoenix::ref(*this), qi::_1)];
307 freshObservationLabelName.name("fresh observable name");
308
309 observableDefinition =
310 (qi::lit("observable") > -qi::lit("\"") > freshObservationLabelName > -qi::lit("\"") > qi::lit("=") > (intExpression | boolExpression) >
311 qi::lit(";"))[qi::_val = phoenix::bind(&PrismParserGrammar::createObservationLabel, phoenix::ref(*this), qi::_1, qi::_2)];
312 observableDefinition.name("observable definition");
313
314 assignmentDefinition = ((qi::lit("(") >> identifier >> qi::lit("'")) > qi::lit("=") > expression_ >
315 qi::lit(")"))[qi::_val = phoenix::bind(&PrismParserGrammar::createAssignment, phoenix::ref(*this), qi::_1, qi::_2)];
316 assignmentDefinition.name("assignment");
317
318 assignmentDefinitionList =
319 (assignmentDefinition % "&")[qi::_val = qi::_1] | (qi::lit("true"))[qi::_val = phoenix::construct<std::vector<storm::prism::Assignment>>()];
320 assignmentDefinitionList.name("assignment list");
321
322 likelihoodDefinition =
323 (numericalExpression >
324 qi::lit(":"))[qi::_val = phoenix::construct<typename storm::prism::Update::ExpressionPair>(qi::_1, storm::expressions::Expression())] |
325 (qi::lit("[") > numericalExpression > qi::lit(",") > numericalExpression > qi::lit("]") >
326 qi::lit(":"))[qi::_val = phoenix::construct<typename storm::prism::Update::ExpressionPair>(qi::_1, qi::_2)];
327
328 updateDefinition =
329 (assignmentDefinitionList[qi::_val = phoenix::bind(&PrismParserGrammar::createUpdate, phoenix::ref(*this),
330 typename storm::prism::Update::ExpressionPair(), qi::_1, qi::_r1)] |
331 ((likelihoodDefinition >
332 assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParserGrammar::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)]));
333 updateDefinition.name("update");
334
335 updateListDefinition %= +updateDefinition(qi::_r1) % "+";
336 updateListDefinition.name("update list");
337
338 // This is a dummy command-definition (it ignores the actual contents of the command) that is overwritten when the parser is moved to the second run.
339 commandDefinition = (((qi::lit("[") > -identifier > qi::lit("]")) | (qi::lit("<") > -identifier > qi::lit(">")[qi::_a = true])) >
340 +(qi::char_ - (qi::lit(";") | qi::lit("endmodule"))) >
341 qi::lit(";"))[qi::_val = phoenix::bind(&PrismParserGrammar::createDummyCommand, phoenix::ref(*this), qi::_1, qi::_r1)];
342 commandDefinition.name("command definition");
343
344 // We first check for a module renaming, i.e., for this rule we certainly have to see a module definition
345 moduleDefinition =
346 ((qi::lit("module") > freshModuleName > *(variableDefinition(qi::_a, qi::_b, qi::_c))) > -invariantConstruct > (*commandDefinition(qi::_r1)) >
347 qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParserGrammar::createModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_c, qi::_2, qi::_3,
348 qi::_r1)];
349 moduleDefinition.name("module definition");
350
351 freshPlayerName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParserGrammar::isFreshPlayerName, phoenix::ref(*this), qi::_1)];
352 freshPlayerName.name("fresh player name");
353
354 playerControlledActionName =
355 ((qi::lit("[") > identifier >
356 qi::lit("]"))[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParserGrammar::isKnownActionName, phoenix::ref(*this), qi::_1, true)];
357 playerControlledActionName.name("player controlled action name");
358
359 playerControlledModuleName =
360 (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParserGrammar::isKnownModuleName, phoenix::ref(*this), qi::_1, true)];
361 playerControlledModuleName.name("player controlled module name");
362
363 playerConstruct =
364 (qi::lit("player") > freshPlayerName[qi::_a = qi::_1] >
365 +((playerControlledActionName[phoenix::push_back(qi::_c, qi::_1)] | playerControlledModuleName[phoenix::push_back(qi::_b, qi::_1)]) % ',') >
366 qi::lit("endplayer"))[qi::_val = phoenix::bind(&PrismParserGrammar::createPlayer, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)];
367 playerConstruct.name("player construct");
368
369 moduleRenaming =
370 (qi::lit("[") >
371 ((identifier > qi::lit("=") > identifier)[phoenix::insert(qi::_a, phoenix::construct<std::pair<std::string, std::string>>(qi::_1, qi::_2))] % ",") >
372 qi::lit("]"))[qi::_val = phoenix::bind(&PrismParserGrammar::createModuleRenaming, phoenix::ref(*this), qi::_a)];
373 moduleRenaming.name("Module renaming list");
374
375 renamedModule =
376 (((qi::lit("module") > freshModuleName) >> qi::lit("=")) > knownModuleName[qi::_a = qi::_1] >
377 (moduleRenaming[qi::_b = qi::_1])[qi::_pass =
378 phoenix::bind(&PrismParserGrammar::isValidModuleRenaming, phoenix::ref(*this), qi::_a, qi::_b, qi::_r1)] >
379 qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParserGrammar::createRenamedModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_r1)];
380 renamedModule.name("module definition via renaming");
381
382 start =
383 (qi::eps[phoenix::bind(&PrismParserGrammar::removeInitialConstruct, phoenix::ref(*this), phoenix::ref(globalProgramInformation))] >
384 modelTypeDefinition[phoenix::bind(&PrismParserGrammar::setModelType, phoenix::ref(*this), phoenix::ref(globalProgramInformation), qi::_1)] >
385 *(observablesConstruct(phoenix::ref(globalProgramInformation)) |
386 definedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, phoenix::ref(globalProgramInformation)), qi::_1)] |
387 undefinedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, phoenix::ref(globalProgramInformation)),
388 qi::_1)] |
389 formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, phoenix::ref(globalProgramInformation)), qi::_1)] |
390 globalVariableDefinition(phoenix::ref(globalProgramInformation)) |
391 (renamedModule(phoenix::ref(globalProgramInformation)) | moduleDefinition(phoenix::ref(globalProgramInformation)))[phoenix::push_back(
392 phoenix::bind(&GlobalProgramInformation::modules, phoenix::ref(globalProgramInformation)), qi::_1)] |
393 initialStatesConstruct(phoenix::ref(globalProgramInformation)) |
394 rewardModelDefinition(phoenix::ref(globalProgramInformation))[phoenix::push_back(
395 phoenix::bind(&GlobalProgramInformation::rewardModels, phoenix::ref(globalProgramInformation)), qi::_1)] |
396 labelDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::labels, phoenix::ref(globalProgramInformation)), qi::_1)] |
397 observableDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::observationLabels, phoenix::ref(globalProgramInformation)),
398 qi::_1)] |
399 formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, phoenix::ref(globalProgramInformation)), qi::_1)] |
400 playerConstruct(phoenix::ref(globalProgramInformation))[phoenix::push_back(
401 phoenix::bind(&GlobalProgramInformation::players, phoenix::ref(globalProgramInformation)), qi::_1)]) >
402 -(systemCompositionConstruct(phoenix::ref(globalProgramInformation))) >
403 qi::eoi)[qi::_val = phoenix::bind(&PrismParserGrammar::createProgram, phoenix::ref(*this), phoenix::ref(globalProgramInformation))];
404 start.name("probabilistic program");
405
406 // Enable location tracking for important entities.
407 auto setLocationInfoFunction = this->annotate(qi::_val, qi::_1, qi::_3);
408 qi::on_success(undefinedBooleanConstantDefinition, setLocationInfoFunction);
409 qi::on_success(undefinedIntegerConstantDefinition, setLocationInfoFunction);
410 qi::on_success(undefinedDoubleConstantDefinition, setLocationInfoFunction);
411 qi::on_success(definedBooleanConstantDefinition, setLocationInfoFunction);
412 qi::on_success(definedIntegerConstantDefinition, setLocationInfoFunction);
413 qi::on_success(definedDoubleConstantDefinition, setLocationInfoFunction);
414 qi::on_success(booleanVariableDefinition, setLocationInfoFunction);
415 qi::on_success(integerVariableDefinition, setLocationInfoFunction);
416 qi::on_success(clockVariableDefinition, setLocationInfoFunction);
417 qi::on_success(moduleDefinition, setLocationInfoFunction);
418 qi::on_success(moduleRenaming, setLocationInfoFunction);
419 qi::on_success(renamedModule, setLocationInfoFunction);
420 qi::on_success(formulaDefinition, setLocationInfoFunction);
421 qi::on_success(rewardModelDefinition, setLocationInfoFunction);
422 qi::on_success(labelDefinition, setLocationInfoFunction);
423 qi::on_success(observableDefinition, setLocationInfoFunction);
424 qi::on_success(commandDefinition, setLocationInfoFunction);
425 qi::on_success(updateDefinition, setLocationInfoFunction);
426 qi::on_success(assignmentDefinition, setLocationInfoFunction);
427
428 // Enable error reporting.
429 qi::on_error<qi::fail>(start,
430 (phoenix::bind(&PrismParserGrammar::reportRejectedKeywordIdentifier, phoenix::ref(*this)), handler(qi::_1, qi::_2, qi::_3, qi::_4)));
431}
432
433void PrismParserGrammar::moveToSecondRun() {
434 {
435 auto const undeclaredObsIt = std::find_if(observables.begin(), observables.end(), [](auto const& pair) { return !pair.second; });
436 STORM_LOG_THROW(undeclaredObsIt == observables.end(), storm::exceptions::WrongFormatException,
437 "Some variables marked as observable, but never declared, e.g. " << undeclaredObsIt->first);
438 }
439
440 // In the second run, we actually need to parse the commands instead of just skipping them,
441 // so we adapt the rule for parsing commands.
442 commandDefinition =
443 (((qi::lit("[") > -identifier > qi::lit("]")) | (qi::lit("<") > -identifier > qi::lit(">")[qi::_a = true])) > *expressionParser > qi::lit("->") >
444 updateListDefinition(qi::_r1) >
445 qi::lit(";"))[qi::_val = phoenix::bind(&PrismParserGrammar::createCommand, phoenix::ref(*this), qi::_a, qi::_1, qi::_2, qi::_3, qi::_r1)];
446
447 auto setLocationInfoFunction = this->annotate(qi::_val, qi::_1, qi::_3);
448 qi::on_success(commandDefinition, setLocationInfoFunction);
449
450 formulaDefinition = (qi::lit("formula") > identifier > qi::lit("=") > *expressionParser >
451 qi::lit(";"))[qi::_val = phoenix::bind(&PrismParserGrammar::createFormulaSecondRun, phoenix::ref(*this), qi::_1, qi::_2)];
452 formulaDefinition.name("formula definition");
453 this->secondRun = true;
454 this->expressionParser->setIdentifierMapping(&this->identifiers_);
455
456 // We need to parse the formula rhs between the first run and the second run, because
457 // * in the first run, the type of the formula (int, bool, clock) is not known
458 // * in the second run, formulas might be used before they are declared
459 createFormulaIdentifiers(this->globalProgramInformation.formulas);
460
461 this->globalProgramInformation.moveToSecondRun();
462}
463
464void PrismParserGrammar::createFormulaIdentifiers(std::vector<storm::prism::Formula> const& formulas) {
465 STORM_LOG_THROW(formulas.size() == this->formulaExpressions.size(), storm::exceptions::UnexpectedException,
466 "Unexpected number of formulas and formula expressions.");
467 this->formulaOrder.clear();
468 storm::storage::BitVector unprocessed(formulas.size(), true);
469 // It might be that formulas are declared in a weird order.
470 // We follow a trial-and-error approach: If we can not parse the expression for one formula,
471 // we assume a subsequent formula has to be evaluated first.
472 // We cycle through the formulas until no further progress is made
473 bool progress = true;
474 while (progress) {
475 progress = false;
476 for (uint64_t formulaIndex = unprocessed.getNextSetIndex(0); formulaIndex < formulas.size();
477 formulaIndex = unprocessed.getNextSetIndex(formulaIndex + 1)) {
478 storm::expressions::Expression expression = this->expressionParser->parseFromString(formulaExpressions[formulaIndex], true);
479 if (expression.isInitialized()) {
480 progress = true;
481 unprocessed.set(formulaIndex, false);
482 formulaOrder.push_back(formulaIndex);
483 storm::expressions::Variable variable;
484 try {
485 if (expression.hasIntegerType()) {
486 variable = manager->declareIntegerVariable(formulas[formulaIndex].getName());
487 } else if (expression.hasBooleanType()) {
488 variable = manager->declareBooleanVariable(formulas[formulaIndex].getName());
489 } else {
490 STORM_LOG_ASSERT(expression.hasNumericalType(),
491 "Unexpected type for formula expression of formula " << formulas[formulaIndex].getName());
492 variable = manager->declareRationalVariable(formulas[formulaIndex].getName());
493 }
494 this->identifiers_.add(formulas[formulaIndex].getName(), variable.getExpression());
495 } catch (storm::exceptions::InvalidArgumentException const&) {
496 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
497 "Parsing error in " << this->getFilename() << ": illegal identifier '" << formulas[formulaIndex].getName() << "' at line '"
498 << formulas[formulaIndex].getLineNumber() << ".");
499 }
500 this->expressionParser->setIdentifierMapping(&this->identifiers_);
501 }
502 }
503 }
504 if (!unprocessed.empty()) {
505 for (uint64_t formulaIndex : unprocessed) {
506 STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Invalid expression for formula '" << formulas[formulaIndex].getName()
507 << "' at line '" << formulas[formulaIndex].getLineNumber() << "':\n\t" << formulaExpressions[formulaIndex]);
508 }
509 STORM_LOG_THROW(unprocessed.getNumberOfSetBits() == 1, storm::exceptions::WrongFormatException,
510 "Unable to parse expressions for " << unprocessed.getNumberOfSetBits() << " formulas. This could be due to circular dependencies.");
511 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
512 "Unable to parse expression for formula '" << formulas[unprocessed.getNextSetIndex(0)].getName() << "'.");
513 }
514}
515
516void PrismParserGrammar::allowDoubleLiterals(bool flag) {
517 this->expressionParser->setAcceptDoubleLiterals(flag);
518}
519
520std::string const& PrismParserGrammar::getFilename() const {
521 return this->filename;
522}
523
524bool PrismParserGrammar::isValidIdentifier(std::string const& identifier) {
525 if (this->keywords_.find(identifier) != nullptr) {
526 // "player"/"endplayer" and "invariant"/"endinvariant" are only meaningful (and thus only reserved) for
527 // SMGs resp. PTAs; the model type is already known at this point since it is always the first thing
528 // parsed in the file.
529 auto const modelType = this->globalProgramInformation.modelType;
530 bool const isExemptSmgKeyword = (identifier == "player" || identifier == "endplayer") && modelType != storm::prism::Program::ModelType::SMG;
531 bool const isExemptPtaKeyword = (identifier == "invariant" || identifier == "endinvariant") && modelType != storm::prism::Program::ModelType::PTA;
532 if (isExemptSmgKeyword || isExemptPtaKeyword) {
533 return true;
534 }
535 // Do not log here: this check also fires on harmless speculative backtracking during a successful parse.
536 // Recorded for diagnostics in case parsing ultimately fails, see reportRejectedKeywordIdentifier.
537 this->lastRejectedKeywordIdentifier = identifier;
538 return false;
539 }
540 return true;
541}
542
543void PrismParserGrammar::reportRejectedKeywordIdentifier() {
544 if (!this->lastRejectedKeywordIdentifier.empty()) {
545 STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": '" << this->lastRejectedKeywordIdentifier
546 << "' is a reserved keyword and cannot be used as an identifier.");
547 }
548}
549
550bool PrismParserGrammar::isKnownModuleName(std::string const& moduleName, bool inSecondRun) {
551 if ((this->secondRun == inSecondRun) && this->globalProgramInformation.moduleToIndexMap.count(moduleName) == 0) {
552 STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Unknown module '" << moduleName << "'.");
553 return false;
554 }
555 return true;
556}
557
558bool PrismParserGrammar::isFreshModuleName(std::string const& moduleName) {
559 if (!this->secondRun && this->globalProgramInformation.moduleToIndexMap.count(moduleName) != 0) {
560 STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Duplicate module name '" << moduleName << "'.");
561 return false;
562 }
563 return true;
564}
565
566bool PrismParserGrammar::isKnownActionName(std::string const& actionName, bool inSecondRun) {
567 if ((this->secondRun == inSecondRun) && this->globalProgramInformation.actionIndices.count(actionName) == 0) {
568 STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Unknown action label '" << actionName << "'.");
569 return false;
570 }
571 return true;
572}
573
574bool PrismParserGrammar::isFreshIdentifier(std::string const& identifier) {
575 if (!this->secondRun && this->manager->hasVariable(identifier)) {
576 STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Duplicate identifier '" << identifier << "'.");
577 return false;
578 }
579 return true;
580}
581
582bool PrismParserGrammar::isFreshLabelName(std::string const& labelName) {
583 if (!this->secondRun) {
584 for (auto const& existingLabel : this->globalProgramInformation.labels) {
585 if (labelName == existingLabel.getName()) {
586 STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Duplicate label name '" << identifier << "'.");
587 return false;
588 }
589 }
590 }
591 return true;
592}
593
594bool PrismParserGrammar::isFreshObservationLabelName(std::string const& labelName) {
595 if (!this->secondRun) {
596 // In the first run, check if we already know such an observation label
597 if (std::any_of(this->globalProgramInformation.observationLabels.begin(), this->globalProgramInformation.observationLabels.end(),
598 [&labelName](auto const& existingLabel) { return labelName == existingLabel.getName(); })) {
599 STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Duplicate observation label name '" << labelName << "'.");
600 return false;
601 }
602 } else {
603 // In the second run, check if there is a clash between observation label and known observable variable.
604 if (std::any_of(this->observables.begin(), this->observables.end(),
605 [&labelName](auto const& observableVariable) { return labelName == observableVariable.first; })) {
606 STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Observation label name '" << labelName
607 << "' coincides with the name of an observable variable.");
608 return false;
609 }
610 }
611 return true;
612}
613
614bool PrismParserGrammar::isFreshRewardModelName(std::string const& rewardModelName) {
615 if (!this->secondRun) {
616 for (auto const& existingRewardModel : this->globalProgramInformation.rewardModels) {
617 if (rewardModelName == existingRewardModel.getName()) {
618 STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Duplicate reward model name '" << identifier << "'.");
619 return false;
620 }
621 }
622 }
623 return true;
624}
625
626bool PrismParserGrammar::isFreshPlayerName(std::string const& playerName) {
627 return true;
628}
629
630bool PrismParserGrammar::isOfBoolType(storm::expressions::Expression const& expression) {
631 return !this->secondRun || expression.hasBooleanType();
632}
633
634bool PrismParserGrammar::isOfIntType(storm::expressions::Expression const& expression) {
635 return !this->secondRun || expression.hasIntegerType();
636}
637
638bool PrismParserGrammar::isOfNumericalType(storm::expressions::Expression const& expression) {
639 return !this->secondRun || expression.hasNumericalType();
640}
641
642bool PrismParserGrammar::addInitialStatesConstruct(storm::expressions::Expression const& initialStatesExpression,
643 GlobalProgramInformation& globalProgramInformation) {
644 STORM_LOG_THROW(!globalProgramInformation.hasInitialConstruct, storm::exceptions::WrongFormatException,
645 "Parsing error in " << this->getFilename() << ": Program must not define two initial constructs.");
646 if (globalProgramInformation.hasInitialConstruct) {
647 return false;
648 }
649 globalProgramInformation.hasInitialConstruct = true;
650 globalProgramInformation.initialConstruct = storm::prism::InitialConstruct(initialStatesExpression, this->getFilename(), get_line(qi::_3));
651 return true;
652}
653
654bool PrismParserGrammar::addSystemCompositionConstruct(std::shared_ptr<storm::prism::Composition> const& composition,
655 GlobalProgramInformation& globalProgramInformation) {
656 globalProgramInformation.systemCompositionConstruct = storm::prism::SystemCompositionConstruct(composition, this->getFilename(), get_line(qi::_3));
657 return true;
658}
659
660void PrismParserGrammar::setModelType(GlobalProgramInformation& globalProgramInformation, storm::prism::Program::ModelType const& modelType) {
661 STORM_LOG_THROW(globalProgramInformation.modelType == storm::prism::Program::ModelType::UNDEFINED, storm::exceptions::WrongFormatException,
662 "Parsing error in " << this->getFilename() << ": Program must not set model type multiple times.");
663 globalProgramInformation.modelType = modelType;
664}
665
666std::shared_ptr<storm::prism::Composition> PrismParserGrammar::createModuleComposition(std::string const& moduleName) const {
667 return std::make_shared<storm::prism::ModuleComposition>(moduleName);
668}
669
670std::shared_ptr<storm::prism::Composition> PrismParserGrammar::createRenamingComposition(std::shared_ptr<storm::prism::Composition> const& subcomposition,
671 std::map<std::string, std::string> const& renaming) const {
672 return std::make_shared<storm::prism::RenamingComposition>(subcomposition, renaming);
673}
674
675std::shared_ptr<storm::prism::Composition> PrismParserGrammar::createHidingComposition(std::shared_ptr<storm::prism::Composition> const& subcomposition,
676 std::set<std::string> const& actionsToHide) const {
677 return std::make_shared<storm::prism::HidingComposition>(subcomposition, actionsToHide);
678}
679
680std::shared_ptr<storm::prism::Composition> PrismParserGrammar::createSynchronizingParallelComposition(
681 std::shared_ptr<storm::prism::Composition> const& left, std::shared_ptr<storm::prism::Composition> const& right) const {
682 return std::make_shared<storm::prism::SynchronizingParallelComposition>(left, right);
683}
684
685std::shared_ptr<storm::prism::Composition> PrismParserGrammar::createInterleavingParallelComposition(
686 std::shared_ptr<storm::prism::Composition> const& left, std::shared_ptr<storm::prism::Composition> const& right) const {
687 return std::make_shared<storm::prism::InterleavingParallelComposition>(left, right);
688}
689
690std::shared_ptr<storm::prism::Composition> PrismParserGrammar::createRestrictedParallelComposition(
691 std::shared_ptr<storm::prism::Composition> const& left, std::set<std::string> const& synchronizingActions,
692 std::shared_ptr<storm::prism::Composition> const& right) const {
693 return std::make_shared<storm::prism::RestrictedParallelComposition>(left, synchronizingActions, right);
694}
695
696storm::prism::Constant PrismParserGrammar::createUndefinedBooleanConstant(std::string const& newConstant) const {
697 if (!this->secondRun) {
698 try {
699 storm::expressions::Variable newVariable = manager->declareBooleanVariable(newConstant, true);
700 this->identifiers_.add(newConstant, newVariable.getExpression());
701 } catch (storm::exceptions::InvalidArgumentException const&) {
702 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
703 "Parsing error in " << this->getFilename() << ": illegal identifier '" << newConstant << "'.");
704 }
705 }
706 return storm::prism::Constant(manager->getVariable(newConstant), this->getFilename());
707}
708
709storm::prism::Constant PrismParserGrammar::createUndefinedIntegerConstant(std::string const& newConstant) const {
710 if (!this->secondRun) {
711 try {
712 storm::expressions::Variable newVariable = manager->declareIntegerVariable(newConstant, true);
713 this->identifiers_.add(newConstant, newVariable.getExpression());
714 } catch (storm::exceptions::InvalidArgumentException const&) {
715 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
716 "Parsing error in " << this->getFilename() << ": illegal identifier '" << newConstant << "'.");
717 }
718 }
719 return storm::prism::Constant(manager->getVariable(newConstant), this->getFilename());
720}
721
722storm::prism::Constant PrismParserGrammar::createUndefinedDoubleConstant(std::string const& newConstant) const {
723 if (!this->secondRun) {
724 try {
725 storm::expressions::Variable newVariable = manager->declareRationalVariable(newConstant, true);
726 this->identifiers_.add(newConstant, newVariable.getExpression());
727 } catch (storm::exceptions::InvalidArgumentException const&) {
728 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
729 "Parsing error in " << this->getFilename() << ": illegal identifier '" << newConstant << "'.");
730 }
731 }
732 return storm::prism::Constant(manager->getVariable(newConstant), this->getFilename());
733}
734
735storm::prism::Constant PrismParserGrammar::createDefinedBooleanConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
736 if (!this->secondRun) {
737 try {
738 storm::expressions::Variable newVariable = manager->declareBooleanVariable(newConstant, true);
739 this->identifiers_.add(newConstant, newVariable.getExpression());
740 } catch (storm::exceptions::InvalidArgumentException const&) {
741 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
742 "Parsing error in " << this->getFilename() << ": illegal identifier '" << newConstant << "'.");
743 }
744 }
745 return storm::prism::Constant(manager->getVariable(newConstant), expression, this->getFilename());
746}
747
748storm::prism::Constant PrismParserGrammar::createDefinedIntegerConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
749 if (!this->secondRun) {
750 try {
751 storm::expressions::Variable newVariable = manager->declareIntegerVariable(newConstant, true);
752 this->identifiers_.add(newConstant, newVariable.getExpression());
753 } catch (storm::exceptions::InvalidArgumentException const&) {
754 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
755 "Parsing error in " << this->getFilename() << ": illegal identifier '" << newConstant << "'.");
756 }
757 }
758 return storm::prism::Constant(manager->getVariable(newConstant), expression, this->getFilename());
759}
760
761storm::prism::Constant PrismParserGrammar::createDefinedDoubleConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
762 if (!this->secondRun) {
763 try {
764 storm::expressions::Variable newVariable = manager->declareRationalVariable(newConstant, true);
765 this->identifiers_.add(newConstant, newVariable.getExpression());
766 } catch (storm::exceptions::InvalidArgumentException const&) {
767 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
768 "Parsing error in " << this->getFilename() << ": illegal identifier '" << newConstant << "'.");
769 }
770 }
771 return storm::prism::Constant(manager->getVariable(newConstant), expression, this->getFilename());
772}
773
774storm::prism::Formula PrismParserGrammar::createFormulaFirstRun(std::string const& formulaName, std::string const& expression) {
775 // Only store the expression as a string. It will be parsed between first and second run
776 // This is necessary because the resulting type of the formula is only known after the first run.
777 STORM_LOG_ASSERT(!this->secondRun, "This constructor should have only been called during the first run.");
778 formulaExpressions.push_back(expression);
779 return storm::prism::Formula(formulaName, this->getFilename());
780}
781
782storm::prism::Formula PrismParserGrammar::createFormulaSecondRun(std::string const& formulaName, storm::expressions::Expression const& expression) {
783 // This is necessary because the resulting type of the formula is only known after the first run.
784 STORM_LOG_ASSERT(this->secondRun, "This constructor should have only been called during the second run.");
785 storm::expressions::Expression lhsExpression = *this->identifiers_.find(formulaName);
786 return storm::prism::Formula(lhsExpression.getBaseExpression().asVariableExpression().getVariable(), expression, this->getFilename());
787}
788
789storm::prism::Label PrismParserGrammar::createLabel(std::string const& labelName, storm::expressions::Expression expression) const {
790 return storm::prism::Label(labelName, expression, this->getFilename());
791}
792
793storm::prism::ObservationLabel PrismParserGrammar::createObservationLabel(std::string const& labelName, storm::expressions::Expression expression) const {
794 return storm::prism::ObservationLabel(labelName, expression, this->getFilename());
795}
796
797storm::prism::RewardModel PrismParserGrammar::createRewardModel(std::string const& rewardModelName, std::vector<storm::prism::StateReward> const& stateRewards,
798 std::vector<storm::prism::StateActionReward> const& stateActionRewards,
799 std::vector<storm::prism::TransitionReward> const& transitionRewards) const {
800 return storm::prism::RewardModel(rewardModelName, stateRewards, stateActionRewards, transitionRewards, this->getFilename());
801}
802
803storm::prism::StateReward PrismParserGrammar::createStateReward(storm::expressions::Expression statePredicateExpression,
804 storm::expressions::Expression rewardValueExpression) const {
805 if (this->secondRun) {
806 return storm::prism::StateReward(statePredicateExpression, rewardValueExpression, this->getFilename());
807 } else {
808 return storm::prism::StateReward();
809 }
810}
811
812storm::prism::StateActionReward PrismParserGrammar::createStateActionReward(boost::optional<std::string> const& actionName,
813 storm::expressions::Expression statePredicateExpression,
814 storm::expressions::Expression rewardValueExpression,
815 GlobalProgramInformation& globalProgramInformation) const {
816 if (this->secondRun) {
817 std::string realActionName = actionName ? actionName.get() : "";
818
819 auto const& nameIndexPair = globalProgramInformation.actionIndices.find(realActionName);
820 STORM_LOG_THROW(nameIndexPair != globalProgramInformation.actionIndices.end(), storm::exceptions::WrongFormatException,
821 "Action reward refers to illegal action '" << realActionName << "'.");
822 return storm::prism::StateActionReward(nameIndexPair->second, realActionName, statePredicateExpression, rewardValueExpression, this->getFilename());
823 } else {
824 return storm::prism::StateActionReward();
825 }
826}
827
828storm::prism::TransitionReward PrismParserGrammar::createTransitionReward(boost::optional<std::string> const& actionName,
829 storm::expressions::Expression sourceStatePredicateExpression,
830 storm::expressions::Expression targetStatePredicateExpression,
831 storm::expressions::Expression rewardValueExpression,
832 GlobalProgramInformation& globalProgramInformation) const {
833 if (this->secondRun) {
834 std::string realActionName = actionName ? actionName.get() : "";
835
836 auto const& nameIndexPair = globalProgramInformation.actionIndices.find(realActionName);
837 STORM_LOG_THROW(nameIndexPair != globalProgramInformation.actionIndices.end(), storm::exceptions::WrongFormatException,
838 "Transition reward refers to illegal action '" << realActionName << "'.");
839 return storm::prism::TransitionReward(nameIndexPair->second, realActionName, sourceStatePredicateExpression, targetStatePredicateExpression,
840 rewardValueExpression, this->getFilename());
841 } else {
842 return storm::prism::TransitionReward();
843 }
844}
845
846storm::prism::Assignment PrismParserGrammar::createAssignment(std::string const& variableName, storm::expressions::Expression assignedExpression) const {
847 return storm::prism::Assignment(manager->getVariable(variableName), assignedExpression, this->getFilename());
848}
849
850storm::prism::Update PrismParserGrammar::createUpdate(typename storm::prism::Update::ExpressionPair likelihoodExpressions,
851 std::vector<storm::prism::Assignment> const& assignments,
852 GlobalProgramInformation& globalProgramInformation) const {
853 ++globalProgramInformation.currentUpdateIndex;
854 if (!likelihoodExpressions.first.isInitialized()) {
855 likelihoodExpressions.first = manager->rational(1);
856 }
857 return storm::prism::Update(globalProgramInformation.currentUpdateIndex - 1, likelihoodExpressions, assignments, this->getFilename());
858}
859
860storm::prism::Command PrismParserGrammar::createCommand(bool markovian, boost::optional<std::string> const& actionName,
861 storm::expressions::Expression guardExpression, std::vector<storm::prism::Update> const& updates,
862 GlobalProgramInformation& globalProgramInformation) const {
863 ++globalProgramInformation.currentCommandIndex;
864 std::string realActionName = actionName ? actionName.get() : "";
865
866 uint_fast64_t actionIndex = 0;
867
868 // If the action name was not yet seen, record it.
869 auto nameIndexPair = globalProgramInformation.actionIndices.find(realActionName);
870 if (nameIndexPair == globalProgramInformation.actionIndices.end()) {
871 std::size_t nextIndex = globalProgramInformation.actionIndices.size();
872 globalProgramInformation.actionIndices.emplace(realActionName, nextIndex);
873 actionIndex = nextIndex;
874 } else {
875 actionIndex = nameIndexPair->second;
876 }
877 return storm::prism::Command(globalProgramInformation.currentCommandIndex - 1, markovian, actionIndex, realActionName, guardExpression, updates,
878 this->getFilename());
879}
880
881storm::prism::Command PrismParserGrammar::createDummyCommand(boost::optional<std::string> const& actionName,
882 GlobalProgramInformation& globalProgramInformation) const {
883 STORM_LOG_ASSERT(!this->secondRun, "Dummy procedure must not be called in second run.");
884 std::string realActionName = actionName ? actionName.get() : "";
885
886 // Register the action name if it has not appeared earlier.
887 auto nameIndexPair = globalProgramInformation.actionIndices.find(realActionName);
888 if (nameIndexPair == globalProgramInformation.actionIndices.end()) {
889 std::size_t nextIndex = globalProgramInformation.actionIndices.size();
890 globalProgramInformation.actionIndices.emplace(realActionName, nextIndex);
891 }
892
893 return storm::prism::Command();
894}
895
896storm::prism::BooleanVariable PrismParserGrammar::createBooleanVariable(std::string const& variableName,
897 storm::expressions::Expression initialValueExpression) const {
898 if (!this->secondRun) {
899 try {
900 storm::expressions::Variable newVariable = manager->declareBooleanVariable(variableName);
901 this->identifiers_.add(variableName, newVariable.getExpression());
902 } catch (storm::exceptions::InvalidArgumentException const&) {
903 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
904 "Parsing error in " << this->getFilename() << ": illegal identifier '" << variableName << "'.");
905 }
906 }
907 bool const observable = this->observables.count(variableName) > 0;
908 if (observable) {
909 this->observables.at(variableName) = true;
910 }
911 return storm::prism::BooleanVariable(manager->getVariable(variableName), initialValueExpression, observable, this->getFilename());
912}
913
914storm::prism::IntegerVariable PrismParserGrammar::createIntegerVariable(std::string const& variableName, storm::expressions::Expression lowerBoundExpression,
915 storm::expressions::Expression upperBoundExpression,
916 storm::expressions::Expression initialValueExpression) const {
917 if (!this->secondRun) {
918 try {
919 storm::expressions::Variable newVariable = manager->declareIntegerVariable(variableName);
920 this->identifiers_.add(variableName, newVariable.getExpression());
921 } catch (storm::exceptions::InvalidArgumentException const&) {
922 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
923 "Parsing error in " << this->getFilename() << ": illegal identifier '" << variableName << "'.");
924 }
925 }
926 bool const observable = this->observables.count(variableName) > 0;
927 if (observable) {
928 this->observables.at(variableName) = true;
929 }
930
931 return storm::prism::IntegerVariable(manager->getVariable(variableName), lowerBoundExpression, upperBoundExpression, initialValueExpression, observable,
932 this->getFilename());
933}
934
935storm::prism::ClockVariable PrismParserGrammar::createClockVariable(std::string const& variableName) const {
936 if (!this->secondRun) {
937 try {
938 storm::expressions::Variable newVariable = manager->declareRationalVariable(variableName);
939 this->identifiers_.add(variableName, newVariable.getExpression());
940 } catch (storm::exceptions::InvalidArgumentException const&) {
941 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
942 "Parsing error in " << this->getFilename() << ": illegal identifier '" << variableName << "'.");
943 }
944 }
945 bool const observable = this->observables.count(variableName) > 0;
946 if (observable) {
947 this->observables.at(variableName) = true;
948 }
949
950 return storm::prism::ClockVariable(manager->getVariable(variableName), observable, this->getFilename());
951}
952
953bool PrismParserGrammar::addObservablesConstruct(std::vector<std::string> const& observables, GlobalProgramInformation& globalProgramInformation) {
954 STORM_LOG_THROW(!globalProgramInformation.hasObservablesConstruct, storm::exceptions::WrongFormatException,
955 "Parsing error in " << this->getFilename() << ": Program must not define two observables constructs.");
956 if (globalProgramInformation.hasObservablesConstruct) {
957 return false;
958 }
959 globalProgramInformation.hasObservablesConstruct = true;
960 for (auto const& observable : observables) {
961 this->observables[observable] = false;
962 }
963 return true;
964}
965
966storm::prism::Player PrismParserGrammar::createPlayer(std::string const& playerName, std::vector<std::string> const& moduleNames,
967 std::vector<std::string> const& actionNames) {
968 if (this->secondRun) {
969 std::unordered_set<std::string> controlledModules;
970 std::unordered_set<std::string> controlledActions;
971 for (auto const& moduleName : moduleNames) {
972 auto moduleIndexPair = globalProgramInformation.moduleToIndexMap.find(moduleName);
973 STORM_LOG_ASSERT(moduleIndexPair != globalProgramInformation.moduleToIndexMap.end(),
974 "Parsing error in " << this->getFilename() << " for player " << playerName << ": No module named '" << moduleName << "' present.");
975 controlledModules.insert(moduleIndexPair->first);
976 bool moduleNotYetControlled = globalProgramInformation.playerControlledModules.insert(moduleIndexPair->second).second;
977 STORM_LOG_THROW(moduleNotYetControlled, storm::exceptions::WrongFormatException,
978 "Parsing error in " << this->getFilename() << " for player " << playerName << ": Module '" << moduleName
979 << "' already controlled by another player.");
980 }
981 for (std::string actionName : actionNames) {
982 auto actionIndexPair = globalProgramInformation.actionIndices.find(actionName);
983 STORM_LOG_ASSERT(actionIndexPair != globalProgramInformation.actionIndices.end(),
984 "Parsing error in " << this->getFilename() << " for player " << playerName << ": No action named '" << actionName << "' present.");
985 controlledActions.insert(actionIndexPair->first);
986 bool actionNotYetControlled = globalProgramInformation.playerControlledActions.insert(actionIndexPair->second).second;
987 STORM_LOG_THROW(actionNotYetControlled, storm::exceptions::WrongFormatException,
988 "Parsing error in " << this->getFilename() << " for player " << playerName << ": Command '" << actionName
989 << "' already controlled by another player.");
990 }
991 return storm::prism::Player(playerName, controlledModules, controlledActions);
992 } else {
993 return storm::prism::Player();
994 }
995}
996
997storm::prism::Module PrismParserGrammar::createModule(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables,
998 std::vector<storm::prism::IntegerVariable> const& integerVariables,
999 std::vector<storm::prism::ClockVariable> const& clockVariables,
1000 boost::optional<storm::expressions::Expression> const& invariant,
1001 std::vector<storm::prism::Command> const& commands,
1002 GlobalProgramInformation& globalProgramInformation) const {
1003 if (!this->secondRun) {
1004 globalProgramInformation.moduleToIndexMap[moduleName] = globalProgramInformation.modules.size();
1005 }
1006 // Assert that the module name is already known and has the expected index.
1007 STORM_LOG_ASSERT(!this->secondRun || globalProgramInformation.moduleToIndexMap.count(moduleName) > 0, "Module name '" << moduleName << "' was not found.");
1008 STORM_LOG_ASSERT(!this->secondRun || globalProgramInformation.moduleToIndexMap[moduleName] == globalProgramInformation.modules.size(),
1009 "The index for module '" << moduleName << "' does not match the index from the first parsing run.");
1010 return storm::prism::Module(moduleName, booleanVariables, integerVariables, clockVariables,
1011 invariant.is_initialized() ? invariant.get() : storm::expressions::Expression(), commands, this->getFilename());
1012}
1013
1014bool PrismParserGrammar::isValidModuleRenaming(std::string const& oldModuleName, storm::prism::ModuleRenaming const& moduleRenaming,
1015 GlobalProgramInformation const& globalProgramInformation) const {
1016 if (!this->secondRun) {
1017 auto const& renaming = moduleRenaming.getRenaming();
1018 auto const& moduleIndexPair = globalProgramInformation.moduleToIndexMap.find(oldModuleName);
1019 if (moduleIndexPair == globalProgramInformation.moduleToIndexMap.end()) {
1020 STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": No module named '" << oldModuleName << "' to rename.");
1021 return false;
1022 }
1023 storm::prism::Module const& moduleToRename = globalProgramInformation.modules[moduleIndexPair->second];
1024 // Check whether all varialbes are renamed.
1025 for (auto const& variable : moduleToRename.getBooleanVariables()) {
1026 auto const& renamingPair = renaming.find(variable.getName());
1027 if (renamingPair == renaming.end()) {
1028 STORM_LOG_ERROR("Parsing error in renaming of module '" << oldModuleName << "': Boolean variable '" << variable.getName()
1029 << "' was not renamed.");
1030 return false;
1031 }
1032 }
1033 for (auto const& variable : moduleToRename.getIntegerVariables()) {
1034 auto const& renamingPair = renaming.find(variable.getName());
1035 if (renamingPair == renaming.end()) {
1036 STORM_LOG_ERROR("Parsing error in renaming of module '" << oldModuleName << "': Integer variable '" << variable.getName()
1037 << "' was not renamed.");
1038 return false;
1039 }
1040 }
1041 for (auto const& variable : moduleToRename.getClockVariables()) {
1042 auto const& renamingPair = renaming.find(variable.getName());
1043 if (renamingPair == renaming.end()) {
1044 STORM_LOG_ERROR("Parsing error in renaming of module '" << oldModuleName << "': Clock variable '" << variable.getName()
1045 << "' was not renamed.");
1046 return false;
1047 }
1048 }
1049 }
1050 return true;
1051}
1052
1053storm::prism::ModuleRenaming PrismParserGrammar::createModuleRenaming(std::map<std::string, std::string> const& renaming) const {
1054 return storm::prism::ModuleRenaming(renaming);
1055}
1056
1057storm::prism::Module PrismParserGrammar::createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName,
1058 storm::prism::ModuleRenaming const& moduleRenaming,
1059 GlobalProgramInformation& globalProgramInformation) const {
1060 // Check whether the module to rename actually exists.
1061 auto const& moduleIndexPair = globalProgramInformation.moduleToIndexMap.find(oldModuleName);
1062 STORM_LOG_THROW(moduleIndexPair != globalProgramInformation.moduleToIndexMap.end(), storm::exceptions::WrongFormatException,
1063 "Parsing error in " << this->getFilename() << ": No module named '" << oldModuleName << "' to rename.");
1064 storm::prism::Module const& moduleToRename = globalProgramInformation.modules[moduleIndexPair->second];
1065 STORM_LOG_THROW(!moduleToRename.isRenamedFromModule(), storm::exceptions::WrongFormatException,
1066 "Parsing error in " << this->getFilename() << ": The module '" << newModuleName << "' can not be created from module '" << oldModuleName
1067 << "' through module renaming because '" << oldModuleName << "' is also a renamed module. Create '" << newModuleName
1068 << "' via a renaming from base module '" << moduleToRename.getBaseModule() << "' instead.");
1069 auto const& renaming = moduleRenaming.getRenaming();
1070 if (!this->secondRun) {
1071 // Add a mapping from the new module name to its (future) index.
1072 globalProgramInformation.moduleToIndexMap[newModuleName] = globalProgramInformation.modules.size();
1073
1074 // Register all (renamed) variables for later use.
1075 // We already checked before, whether the renaiming is valid.
1076 for (auto const& variable : moduleToRename.getBooleanVariables()) {
1077 auto const& renamingPair = renaming.find(variable.getName());
1078 STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException,
1079 "Parsing error in " << this->getFilename() << ": Boolean variable '" << variable.getName() << " was not renamed.");
1080 storm::expressions::Variable renamedVariable = manager->declareBooleanVariable(renamingPair->second);
1081 this->identifiers_.add(renamingPair->second, renamedVariable.getExpression());
1082 if (this->observables.count(renamingPair->second) > 0) {
1083 this->observables.at(renamingPair->second) = true;
1084 }
1085 }
1086 for (auto const& variable : moduleToRename.getIntegerVariables()) {
1087 auto const& renamingPair = renaming.find(variable.getName());
1088 STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException,
1089 "Parsing error in " << this->getFilename() << ": Integer variable '" << variable.getName() << " was not renamed.");
1090 storm::expressions::Variable renamedVariable = manager->declareIntegerVariable(renamingPair->second);
1091 this->identifiers_.add(renamingPair->second, renamedVariable.getExpression());
1092 if (this->observables.count(renamingPair->second) > 0) {
1093 this->observables.at(renamingPair->second) = true;
1094 }
1095 }
1096 for (auto const& variable : moduleToRename.getClockVariables()) {
1097 auto const& renamingPair = renaming.find(variable.getName());
1098 STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException,
1099 "Parsing error in " << this->getFilename() << ": Clock variable '" << variable.getName() << " was not renamed.");
1100 storm::expressions::Variable renamedVariable = manager->declareRationalVariable(renamingPair->second);
1101 this->identifiers_.add(renamingPair->second, renamedVariable.getExpression());
1102 if (this->observables.count(renamingPair->second) > 0) {
1103 this->observables.at(renamingPair->second) = true;
1104 }
1105 }
1106
1107 for (auto const& command : moduleToRename.getCommands()) {
1108 std::string newActionName = command.getActionName();
1109 auto const& renamingPair = renaming.find(command.getActionName());
1110 if (renamingPair != renaming.end()) {
1111 newActionName = renamingPair->second;
1112 }
1113
1114 // Record any newly occurring action names/indices.
1115 auto nameIndexPair = globalProgramInformation.actionIndices.find(newActionName);
1116 if (nameIndexPair == globalProgramInformation.actionIndices.end()) {
1117 std::size_t nextIndex = globalProgramInformation.actionIndices.size();
1118 globalProgramInformation.actionIndices.emplace(newActionName, nextIndex);
1119 }
1120 }
1121
1122 // Return a dummy module in the first pass.
1123 return storm::prism::Module();
1124 } else {
1125 // Assert that the module name is already known and has the expected index.
1126 STORM_LOG_ASSERT(globalProgramInformation.moduleToIndexMap.count(newModuleName) > 0, "Module name '" << newModuleName << "' was not found.");
1127 STORM_LOG_ASSERT(globalProgramInformation.moduleToIndexMap[newModuleName] == globalProgramInformation.modules.size(),
1128 "The index for module " << newModuleName << " does not match the index from the first parsing run.");
1129
1130 // Create a mapping from identifiers to the expressions they need to be replaced with.
1131 std::map<storm::expressions::Variable, storm::expressions::Expression> expressionRenaming;
1132 for (auto const& namePair : renaming) {
1133 storm::expressions::Expression const* substitutedExpression = this->identifiers_.find(namePair.second);
1134 // If the mapped-to-value is an expression, we need to replace it.
1135 if (substitutedExpression != nullptr) {
1136 expressionRenaming.emplace(manager->getVariable(namePair.first), *substitutedExpression);
1137 }
1138 }
1139
1140 // Rename the boolean variables.
1141 std::vector<storm::prism::BooleanVariable> booleanVariables;
1142 for (auto const& variable : moduleToRename.getBooleanVariables()) {
1143 auto const& renamingPair = renaming.find(variable.getName());
1144 STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException,
1145 "Parsing error in " << this->getFilename() << ": Boolean variable '" << variable.getName() << " was not renamed.");
1146 bool const observable = this->observables.count(renamingPair->second) > 0;
1147 if (observable) {
1148 this->observables.at(renamingPair->second) = true;
1149 }
1150 booleanVariables.push_back(storm::prism::BooleanVariable(
1151 manager->getVariable(renamingPair->second),
1152 variable.hasInitialValue() ? variable.getInitialValueExpression().substitute(expressionRenaming) : variable.getInitialValueExpression(),
1153 observable, this->getFilename(), moduleRenaming.getLineNumber()));
1154 }
1155
1156 // Rename the integer variables.
1157 std::vector<storm::prism::IntegerVariable> integerVariables;
1158 for (auto const& variable : moduleToRename.getIntegerVariables()) {
1159 auto const& renamingPair = renaming.find(variable.getName());
1160 STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException,
1161 "Parsing error in " << this->getFilename() << ": Integer variable '" << variable.getName() << " was not renamed.");
1162 bool const observable = this->observables.count(renamingPair->second) > 0;
1163 if (observable) {
1164 this->observables.at(renamingPair->second) = true;
1165 }
1166 integerVariables.push_back(storm::prism::IntegerVariable(
1167 manager->getVariable(renamingPair->second), variable.getLowerBoundExpression().substitute(expressionRenaming),
1168 variable.getUpperBoundExpression().substitute(expressionRenaming),
1169 variable.hasInitialValue() ? variable.getInitialValueExpression().substitute(expressionRenaming) : variable.getInitialValueExpression(),
1170 observable, this->getFilename(), moduleRenaming.getLineNumber()));
1171 }
1172
1173 // Rename the clock variables.
1174 std::vector<storm::prism::ClockVariable> clockVariables;
1175 for (auto const& variable : moduleToRename.getClockVariables()) {
1176 auto const& renamingPair = renaming.find(variable.getName());
1177 STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException,
1178 "Parsing error in " << this->getFilename() << ": Clock variable '" << variable.getName() << " was not renamed.");
1179 bool const observable = this->observables.count(renamingPair->second) > 0;
1180 if (observable) {
1181 this->observables.at(renamingPair->second) = true;
1182 }
1183 clockVariables.push_back(
1184 storm::prism::ClockVariable(manager->getVariable(renamingPair->second), observable, this->getFilename(), moduleRenaming.getLineNumber()));
1185 }
1186
1187 // Rename invariant (if present)
1188 storm::expressions::Expression invariant;
1189 if (moduleToRename.hasInvariant()) {
1190 invariant = moduleToRename.getInvariant().substitute(expressionRenaming);
1191 }
1192
1193 // Rename commands.
1194 std::vector<storm::prism::Command> commands;
1195 for (auto const& command : moduleToRename.getCommands()) {
1196 std::vector<storm::prism::Update> updates;
1197 for (auto const& update : command.getUpdates()) {
1198 std::vector<storm::prism::Assignment> assignments;
1199 for (auto const& assignment : update.getAssignments()) {
1200 auto const& renamingPair = renaming.find(assignment.getVariableName());
1201 if (renamingPair != renaming.end()) {
1202 assignments.emplace_back(manager->getVariable(renamingPair->second), assignment.getExpression().substitute(expressionRenaming),
1203 this->getFilename(), moduleRenaming.getLineNumber());
1204 } else {
1205 assignments.emplace_back(assignment.getVariable(), assignment.getExpression().substitute(expressionRenaming), this->getFilename(),
1206 moduleRenaming.getLineNumber());
1207 }
1208 }
1209 if (update.isLikelihoodInterval()) {
1210 typename storm::prism::Update::ExpressionPair likelihoodInterval{
1211 update.getLikelihoodExpressionInterval().first.substitute(expressionRenaming),
1212 update.getLikelihoodExpressionInterval().second.substitute(expressionRenaming)};
1213 updates.emplace_back(globalProgramInformation.currentUpdateIndex, likelihoodInterval, assignments, this->getFilename(),
1214 moduleRenaming.getLineNumber());
1215 } else {
1216 updates.emplace_back(globalProgramInformation.currentUpdateIndex, update.getLikelihoodExpression().substitute(expressionRenaming),
1217 assignments, this->getFilename(), moduleRenaming.getLineNumber());
1218 }
1219 ++globalProgramInformation.currentUpdateIndex;
1220 }
1221
1222 std::string newActionName = command.getActionName();
1223 auto const& renamingPair = renaming.find(command.getActionName());
1224 if (renamingPair != renaming.end()) {
1225 newActionName = renamingPair->second;
1226 }
1227
1228 uint_fast64_t actionIndex = 0;
1229 auto nameIndexPair = globalProgramInformation.actionIndices.find(newActionName);
1230 if (nameIndexPair == globalProgramInformation.actionIndices.end()) {
1231 std::size_t nextIndex = globalProgramInformation.actionIndices.size();
1232 globalProgramInformation.actionIndices.emplace(newActionName, nextIndex);
1233 actionIndex = nextIndex;
1234 } else {
1235 actionIndex = nameIndexPair->second;
1236 }
1237
1238 commands.emplace_back(globalProgramInformation.currentCommandIndex, command.isMarkovian(), actionIndex, newActionName,
1239 command.getGuardExpression().substitute(expressionRenaming), updates, this->getFilename(), moduleRenaming.getLineNumber());
1240 ++globalProgramInformation.currentCommandIndex;
1241 }
1242
1243 return storm::prism::Module(newModuleName, booleanVariables, integerVariables, clockVariables, invariant, commands, oldModuleName, renaming);
1244 }
1245}
1246
1247storm::prism::Program PrismParserGrammar::createProgram(GlobalProgramInformation const& globalProgramInformation) const {
1248 storm::prism::Program::ModelType finalModelType = globalProgramInformation.modelType;
1249 if (globalProgramInformation.modelType == storm::prism::Program::ModelType::UNDEFINED) {
1250 STORM_LOG_WARN("Program does not specify model type. Implicitly assuming 'mdp'.");
1251 finalModelType = storm::prism::Program::ModelType::MDP;
1252 }
1253
1254 // make sure formulas are stored in a proper order.
1255 std::vector<storm::prism::Formula> orderedFormulas;
1256 if (this->secondRun) {
1257 orderedFormulas.reserve(globalProgramInformation.formulas.size());
1258 for (uint64_t const& i : formulaOrder) {
1259 orderedFormulas.push_back(std::move(globalProgramInformation.formulas[i]));
1260 }
1261 }
1262
1263 return storm::prism::Program(
1264 manager, finalModelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables,
1265 globalProgramInformation.globalIntegerVariables, orderedFormulas, globalProgramInformation.players, globalProgramInformation.modules,
1266 globalProgramInformation.actionIndices, globalProgramInformation.rewardModels, globalProgramInformation.labels,
1267 globalProgramInformation.observationLabels,
1268 secondRun && !globalProgramInformation.hasInitialConstruct ? boost::none : boost::make_optional(globalProgramInformation.initialConstruct),
1269 globalProgramInformation.systemCompositionConstruct, prismCompatibility, this->getFilename(), 1, this->secondRun);
1270}
1271
1272void PrismParserGrammar::removeInitialConstruct(GlobalProgramInformation& globalProgramInformation) const {
1273 globalProgramInformation.hasInitialConstruct = false;
1274}
1275} // namespace parser
1276} // namespace storm
PositionIteratorType
boost::spirit::line_pos_iterator< BaseIteratorType > PositionIteratorType
Definition SpiritParserDefinitions.h:21
Iterator
PositionIteratorType Iterator
Definition SpiritParserDefinitions.h:22
storm::expressions::BaseExpression::asVariableExpression
VariableExpression const & asVariableExpression() const
Definition BaseExpression.cpp:193
storm::expressions::Expression::hasNumericalType
bool hasNumericalType() const
Retrieves whether the expression has a numerical return type, i.e., integer or double.
Definition Expression.cpp:185
storm::expressions::Expression::hasBooleanType
bool hasBooleanType() const
Retrieves whether the expression has a boolean return type.
Definition Expression.cpp:193
storm::expressions::Expression::hasIntegerType
bool hasIntegerType() const
Retrieves whether the expression has an integral return type.
Definition Expression.cpp:197
storm::expressions::Expression::getBaseExpression
BaseExpression const & getBaseExpression() const
Retrieves the base expression underlying this expression object.
Definition Expression.cpp:169
storm::expressions::Expression::substitute
Expression substitute(std::map< Variable, Expression > const &variableToExpressionMap) const
Substitutes all occurrences of the variables according to the given map.
Definition Expression.cpp:50
storm::expressions::Expression::isInitialized
bool isInitialized() const
Checks whether the object encapsulates a base-expression.
Definition Expression.cpp:209
storm::expressions::VariableExpression::getVariable
Variable const & getVariable() const
Retrieves the variable associated with this expression.
Definition VariableExpression.cpp:17
storm::expressions::Variable::getExpression
storm::expressions::Expression getExpression() const
Retrieves an expression that represents the variable.
Definition Variable.cpp:34
storm::expressions::Variable::getName
std::string const & getName() const
Retrieves the name of the variable.
Definition Variable.cpp:46
storm::parser::GlobalProgramInformation::observationLabels
std::vector< storm::prism::ObservationLabel > observationLabels
Definition PrismParserGrammar.h:82
storm::parser::GlobalProgramInformation::modules
std::vector< storm::prism::Module > modules
Definition PrismParserGrammar.h:79
storm::parser::GlobalProgramInformation::constants
std::vector< storm::prism::Constant > constants
Definition PrismParserGrammar.h:73
storm::parser::GlobalProgramInformation::labels
std::vector< storm::prism::Label > labels
Definition PrismParserGrammar.h:81
storm::parser::GlobalProgramInformation::players
std::vector< storm::prism::Player > players
Definition PrismParserGrammar.h:83
storm::parser::GlobalProgramInformation::globalBooleanVariables
std::vector< storm::prism::BooleanVariable > globalBooleanVariables
Definition PrismParserGrammar.h:75
storm::parser::GlobalProgramInformation::formulas
std::vector< storm::prism::Formula > formulas
Definition PrismParserGrammar.h:74
storm::parser::GlobalProgramInformation::rewardModels
std::vector< storm::prism::RewardModel > rewardModels
Definition PrismParserGrammar.h:80
storm::parser::GlobalProgramInformation::globalIntegerVariables
std::vector< storm::prism::IntegerVariable > globalIntegerVariables
Definition PrismParserGrammar.h:76
storm::parser::PrismParserGrammar::parseFromString
static storm::prism::Program parseFromString(std::string const &input, std::string const &filename, bool prismCompatability=false)
Parses the given input stream into the PRISM storage classes assuming it complies with the PRISM synt...
Definition PrismParserGrammar.cpp:46
storm::parser::PrismParserGrammar::parse
static storm::prism::Program parse(std::string const &filename, bool prismCompatability=false)
Parses the given file into the PRISM storage classes assuming it complies with the PRISM syntax.
Definition PrismParserGrammar.cpp:21
storm::prism::Module::getCommands
std::vector< storm::prism::Command > const & getCommands() const
Retrieves the commands of the module.
Definition Module.cpp:133
storm::prism::Module::getBaseModule
std::string const & getBaseModule() const
If the module was created via renaming, this method retrieves the name of the module that was used as...
Definition Module.cpp:167
storm::prism::Module::getIntegerVariables
std::vector< storm::prism::IntegerVariable > const & getIntegerVariables() const
Retrieves the integer variables of the module.
Definition Module.cpp:74
storm::prism::Module::getBooleanVariables
std::vector< storm::prism::BooleanVariable > const & getBooleanVariables() const
Retrieves the boolean variables of the module.
Definition Module.cpp:63
storm::prism::Module::getInvariant
storm::expressions::Expression const & getInvariant() const
Returns the specified invariant (only relevant for PTA models).
Definition Module.cpp:388
storm::prism::Module::isRenamedFromModule
bool isRenamedFromModule() const
Retrieves whether this module was created from another module via renaming.
Definition Module.cpp:163
storm::prism::Module::hasInvariant
bool hasInvariant() const
Returns true, if an invariant was specified (only relevant for PTA models).
Definition Module.cpp:384
storm::prism::Module::getClockVariables
std::vector< storm::prism::ClockVariable > const & getClockVariables() const
Retrieves the clock variables of the module.
Definition Module.cpp:89
storm::prism::Program::ModelType
ModelType
An enum for the different model types.
Definition Program.h:35
storm::prism::Update::ExpressionPair
std::pair< storm::expressions::Expression, storm::expressions::Expression > ExpressionPair
Definition Update.h:12
STORM_LOG_WARN
#define STORM_LOG_WARN(message)
Definition logging.h:28
STORM_LOG_DEBUG
#define STORM_LOG_DEBUG(message)
Definition logging.h:21
STORM_LOG_TRACE
#define STORM_LOG_TRACE(message)
Definition logging.h:15
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_THROW
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:28
storm::io::closeFile
void closeFile(std::ofstream &stream)
Close the given file after writing.
Definition file.h:47
storm::io::openFile
void openFile(std::string const &filepath, std::ofstream &filestream, bool append=false, bool silent=false)
Open the given file for writing.
Definition file.h:18
storm::parser
Contains all file parsers and helper classes.
Definition DFTGalileoParser.h:6