Storm 1.10.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, keywords_, 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 = (qi::lit("observables") > (identifier % qi::lit(",")) >
233 qi::lit("endobservables"))[phoenix::bind(&PrismParserGrammar::createObservablesList, phoenix::ref(*this), qi::_1)];
234 observablesConstruct.name("observables construct");
235
236 invariantConstruct = (qi::lit("invariant") > boolExpression > qi::lit("endinvariant"))[qi::_val = qi::_1];
237 invariantConstruct.name("invariant construct");
238
239 knownModuleName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParserGrammar::isKnownModuleName, phoenix::ref(*this), qi::_1, false)];
240 knownModuleName.name("existing module name");
241
242 freshModuleName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParserGrammar::isFreshModuleName, phoenix::ref(*this), qi::_1)];
243 freshModuleName.name("fresh module name");
244
245 systemCompositionConstruct =
246 (qi::lit("system") > parallelComposition >
247 qi::lit("endsystem"))[phoenix::bind(&PrismParserGrammar::addSystemCompositionConstruct, phoenix::ref(*this), qi::_1, qi::_r1)];
248 systemCompositionConstruct.name("system composition construct");
249
250 actionNameList %= identifier[phoenix::insert(qi::_val, qi::_1)] >> *("," >> identifier[phoenix::insert(qi::_val, qi::_1)]);
251 actionNameList.name("action list");
252
253 parallelComposition =
254 hidingOrRenamingComposition[qi::_val = qi::_1] >>
255 *((interleavingParallelComposition > hidingOrRenamingComposition)[qi::_val = phoenix::bind(&PrismParserGrammar::createInterleavingParallelComposition,
256 phoenix::ref(*this), qi::_val, qi::_1)] |
257 (synchronizingParallelComposition > hidingOrRenamingComposition)[qi::_val = phoenix::bind(&PrismParserGrammar::createSynchronizingParallelComposition,
258 phoenix::ref(*this), qi::_val, qi::_1)] |
259 (restrictedParallelComposition > hidingOrRenamingComposition)[qi::_val = phoenix::bind(&PrismParserGrammar::createRestrictedParallelComposition,
260 phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]);
261 parallelComposition.name("parallel composition");
262
263 synchronizingParallelComposition = qi::lit("||");
264 synchronizingParallelComposition.name("synchronizing parallel composition");
265
266 interleavingParallelComposition = qi::lit("|||");
267 interleavingParallelComposition.name("interleaving parallel composition");
268
269 restrictedParallelComposition = qi::lit("|[") > actionNameList > qi::lit("]|");
270 restrictedParallelComposition.name("restricted parallel composition");
271
272 hidingOrRenamingComposition = hidingComposition | renamingComposition | atomicComposition;
273 hidingOrRenamingComposition.name("hiding/renaming composition");
274
275 hidingComposition =
276 (atomicComposition >>
277 (qi::lit("/") > (qi::lit("{") > actionNameList >
278 qi::lit("}"))))[qi::_val = phoenix::bind(&PrismParserGrammar::createHidingComposition, phoenix::ref(*this), qi::_1, qi::_2)];
279 hidingComposition.name("hiding composition");
280
281 actionRenamingList =
282 +(identifier >> (qi::lit("<-") >> identifier))[phoenix::insert(qi::_val, phoenix::construct<std::pair<std::string, std::string>>(qi::_1, qi::_2))];
283 actionRenamingList.name("action renaming list");
284
285 renamingComposition =
286 (atomicComposition >>
287 (qi::lit("{") >
288 (actionRenamingList > qi::lit("}"))))[qi::_val = phoenix::bind(&PrismParserGrammar::createRenamingComposition, phoenix::ref(*this), qi::_1, qi::_2)];
289 renamingComposition.name("renaming composition");
290
291 atomicComposition = (qi::lit("(") > parallelComposition > qi::lit(")")) | moduleComposition;
292 atomicComposition.name("atomic composition");
293
294 moduleComposition = identifier[qi::_val = phoenix::bind(&PrismParserGrammar::createModuleComposition, phoenix::ref(*this), qi::_1)];
295 moduleComposition.name("module composition");
296
297 freshLabelName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParserGrammar::isFreshLabelName, phoenix::ref(*this), qi::_1)];
298 freshLabelName.name("fresh label name");
299
300 labelDefinition = (qi::lit("label") > -qi::lit("\"") > freshLabelName > -qi::lit("\"") > qi::lit("=") > boolExpression >
301 qi::lit(";"))[qi::_val = phoenix::bind(&PrismParserGrammar::createLabel, phoenix::ref(*this), qi::_1, qi::_2)];
302 labelDefinition.name("label definition");
303
304 freshObservationLabelName =
305 (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParserGrammar::isFreshObservationLabelName, phoenix::ref(*this), qi::_1)];
306 freshObservationLabelName.name("fresh observable name");
307
308 observableDefinition =
309 (qi::lit("observable") > -qi::lit("\"") > freshObservationLabelName > -qi::lit("\"") > qi::lit("=") > (intExpression | boolExpression) >
310 qi::lit(";"))[qi::_val = phoenix::bind(&PrismParserGrammar::createObservationLabel, phoenix::ref(*this), qi::_1, qi::_2)];
311 observableDefinition.name("observable definition");
312
313 assignmentDefinition = ((qi::lit("(") >> identifier >> qi::lit("'")) > qi::lit("=") > expression_ >
314 qi::lit(")"))[qi::_val = phoenix::bind(&PrismParserGrammar::createAssignment, phoenix::ref(*this), qi::_1, qi::_2)];
315 assignmentDefinition.name("assignment");
316
317 assignmentDefinitionList =
318 (assignmentDefinition % "&")[qi::_val = qi::_1] | (qi::lit("true"))[qi::_val = phoenix::construct<std::vector<storm::prism::Assignment>>()];
319 assignmentDefinitionList.name("assignment list");
320
321 likelihoodDefinition =
322 (numericalExpression >
323 qi::lit(":"))[qi::_val = phoenix::construct<typename storm::prism::Update::ExpressionPair>(qi::_1, storm::expressions::Expression())] |
324 (qi::lit("[") > numericalExpression > qi::lit(",") > numericalExpression > qi::lit("]") >
325 qi::lit(":"))[qi::_val = phoenix::construct<typename storm::prism::Update::ExpressionPair>(qi::_1, qi::_2)];
326
327 updateDefinition =
328 (assignmentDefinitionList[qi::_val = phoenix::bind(&PrismParserGrammar::createUpdate, phoenix::ref(*this),
329 typename storm::prism::Update::ExpressionPair(), qi::_1, qi::_r1)] |
330 ((likelihoodDefinition >
331 assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParserGrammar::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)]));
332 updateDefinition.name("update");
333
334 updateListDefinition %= +updateDefinition(qi::_r1) % "+";
335 updateListDefinition.name("update list");
336
337 // 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.
338 commandDefinition = (((qi::lit("[") > -identifier > qi::lit("]")) | (qi::lit("<") > -identifier > qi::lit(">")[qi::_a = true])) >
339 +(qi::char_ - (qi::lit(";") | qi::lit("endmodule"))) >
340 qi::lit(";"))[qi::_val = phoenix::bind(&PrismParserGrammar::createDummyCommand, phoenix::ref(*this), qi::_1, qi::_r1)];
341 commandDefinition.name("command definition");
342
343 // We first check for a module renaming, i.e., for this rule we certainly have to see a module definition
344 moduleDefinition =
345 ((qi::lit("module") > freshModuleName > *(variableDefinition(qi::_a, qi::_b, qi::_c))) > -invariantConstruct > (*commandDefinition(qi::_r1)) >
346 qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParserGrammar::createModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_c, qi::_2, qi::_3,
347 qi::_r1)];
348 moduleDefinition.name("module definition");
349
350 freshPlayerName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParserGrammar::isFreshPlayerName, phoenix::ref(*this), qi::_1)];
351 freshPlayerName.name("fresh player name");
352
353 playerControlledActionName =
354 ((qi::lit("[") > identifier >
355 qi::lit("]"))[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParserGrammar::isKnownActionName, phoenix::ref(*this), qi::_1, true)];
356 playerControlledActionName.name("player controlled action name");
357
358 playerControlledModuleName =
359 (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParserGrammar::isKnownModuleName, phoenix::ref(*this), qi::_1, true)];
360 playerControlledModuleName.name("player controlled module name");
361
362 playerConstruct =
363 (qi::lit("player") > freshPlayerName[qi::_a = qi::_1] >
364 +((playerControlledActionName[phoenix::push_back(qi::_c, qi::_1)] | playerControlledModuleName[phoenix::push_back(qi::_b, qi::_1)]) % ',') >
365 qi::lit("endplayer"))[qi::_val = phoenix::bind(&PrismParserGrammar::createPlayer, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)];
366 playerConstruct.name("player construct");
367
368 moduleRenaming =
369 (qi::lit("[") >
370 ((identifier > qi::lit("=") > identifier)[phoenix::insert(qi::_a, phoenix::construct<std::pair<std::string, std::string>>(qi::_1, qi::_2))] % ",") >
371 qi::lit("]"))[qi::_val = phoenix::bind(&PrismParserGrammar::createModuleRenaming, phoenix::ref(*this), qi::_a)];
372 moduleRenaming.name("Module renaming list");
373
374 renamedModule =
375 (((qi::lit("module") > freshModuleName) >> qi::lit("=")) > knownModuleName[qi::_a = qi::_1] >
376 (moduleRenaming[qi::_b = qi::_1])[qi::_pass =
377 phoenix::bind(&PrismParserGrammar::isValidModuleRenaming, phoenix::ref(*this), qi::_a, qi::_b, qi::_r1)] >
378 qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParserGrammar::createRenamedModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_r1)];
379 renamedModule.name("module definition via renaming");
380
381 start =
382 (qi::eps[phoenix::bind(&PrismParserGrammar::removeInitialConstruct, phoenix::ref(*this), phoenix::ref(globalProgramInformation))] >
383 modelTypeDefinition[phoenix::bind(&PrismParserGrammar::setModelType, phoenix::ref(*this), phoenix::ref(globalProgramInformation), qi::_1)] >
384 -observablesConstruct >
385 *(definedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, phoenix::ref(globalProgramInformation)), qi::_1)] |
386 undefinedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, phoenix::ref(globalProgramInformation)),
387 qi::_1)] |
388 formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, phoenix::ref(globalProgramInformation)), qi::_1)] |
389 globalVariableDefinition(phoenix::ref(globalProgramInformation)) |
390 (renamedModule(phoenix::ref(globalProgramInformation)) | moduleDefinition(phoenix::ref(globalProgramInformation)))[phoenix::push_back(
391 phoenix::bind(&GlobalProgramInformation::modules, phoenix::ref(globalProgramInformation)), qi::_1)] |
392 initialStatesConstruct(phoenix::ref(globalProgramInformation)) |
393 rewardModelDefinition(phoenix::ref(globalProgramInformation))[phoenix::push_back(
394 phoenix::bind(&GlobalProgramInformation::rewardModels, phoenix::ref(globalProgramInformation)), qi::_1)] |
395 labelDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::labels, phoenix::ref(globalProgramInformation)), qi::_1)] |
396 observableDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::observationLabels, phoenix::ref(globalProgramInformation)),
397 qi::_1)] |
398 formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, phoenix::ref(globalProgramInformation)), qi::_1)] |
399 playerConstruct(phoenix::ref(globalProgramInformation))[phoenix::push_back(
400 phoenix::bind(&GlobalProgramInformation::players, phoenix::ref(globalProgramInformation)), qi::_1)]) >
401 -(systemCompositionConstruct(phoenix::ref(globalProgramInformation))) >
402 qi::eoi)[qi::_val = phoenix::bind(&PrismParserGrammar::createProgram, phoenix::ref(*this), phoenix::ref(globalProgramInformation))];
403 start.name("probabilistic program");
404
405 // Enable location tracking for important entities.
406 auto setLocationInfoFunction = this->annotate(qi::_val, qi::_1, qi::_3);
407 qi::on_success(undefinedBooleanConstantDefinition, setLocationInfoFunction);
408 qi::on_success(undefinedIntegerConstantDefinition, setLocationInfoFunction);
409 qi::on_success(undefinedDoubleConstantDefinition, setLocationInfoFunction);
410 qi::on_success(definedBooleanConstantDefinition, setLocationInfoFunction);
411 qi::on_success(definedIntegerConstantDefinition, setLocationInfoFunction);
412 qi::on_success(definedDoubleConstantDefinition, setLocationInfoFunction);
413 qi::on_success(booleanVariableDefinition, setLocationInfoFunction);
414 qi::on_success(integerVariableDefinition, setLocationInfoFunction);
415 qi::on_success(clockVariableDefinition, setLocationInfoFunction);
416 qi::on_success(moduleDefinition, setLocationInfoFunction);
417 qi::on_success(moduleRenaming, setLocationInfoFunction);
418 qi::on_success(renamedModule, setLocationInfoFunction);
419 qi::on_success(formulaDefinition, setLocationInfoFunction);
420 qi::on_success(rewardModelDefinition, setLocationInfoFunction);
421 qi::on_success(labelDefinition, setLocationInfoFunction);
422 qi::on_success(observableDefinition, setLocationInfoFunction);
423 qi::on_success(commandDefinition, setLocationInfoFunction);
424 qi::on_success(updateDefinition, setLocationInfoFunction);
425 qi::on_success(assignmentDefinition, setLocationInfoFunction);
426
427 // Enable error reporting.
428 qi::on_error<qi::fail>(start, handler(qi::_1, qi::_2, qi::_3, qi::_4));
429}
430
431void PrismParserGrammar::moveToSecondRun() {
432 // In the second run, we actually need to parse the commands instead of just skipping them,
433 // so we adapt the rule for parsing commands.
434 STORM_LOG_THROW(observables.empty(), storm::exceptions::WrongFormatException,
435 "Some variables marked as observable, but never declared, e.g. " << *observables.begin());
436
437 commandDefinition =
438 (((qi::lit("[") > -identifier > qi::lit("]")) | (qi::lit("<") > -identifier > qi::lit(">")[qi::_a = true])) > *expressionParser > qi::lit("->") >
439 updateListDefinition(qi::_r1) >
440 qi::lit(";"))[qi::_val = phoenix::bind(&PrismParserGrammar::createCommand, phoenix::ref(*this), qi::_a, qi::_1, qi::_2, qi::_3, qi::_r1)];
441
442 auto setLocationInfoFunction = this->annotate(qi::_val, qi::_1, qi::_3);
443 qi::on_success(commandDefinition, setLocationInfoFunction);
444
445 formulaDefinition = (qi::lit("formula") > identifier > qi::lit("=") > *expressionParser >
446 qi::lit(";"))[qi::_val = phoenix::bind(&PrismParserGrammar::createFormulaSecondRun, phoenix::ref(*this), qi::_1, qi::_2)];
447 formulaDefinition.name("formula definition");
448 this->secondRun = true;
449 this->expressionParser->setIdentifierMapping(&this->identifiers_);
450
451 // We need to parse the formula rhs between the first run and the second run, because
452 // * in the first run, the type of the formula (int, bool, clock) is not known
453 // * in the second run, formulas might be used before they are declared
454 createFormulaIdentifiers(this->globalProgramInformation.formulas);
455
456 this->globalProgramInformation.moveToSecondRun();
457}
458
459void PrismParserGrammar::createFormulaIdentifiers(std::vector<storm::prism::Formula> const& formulas) {
460 STORM_LOG_THROW(formulas.size() == this->formulaExpressions.size(), storm::exceptions::UnexpectedException,
461 "Unexpected number of formulas and formula expressions");
462 this->formulaOrder.clear();
463 storm::storage::BitVector unprocessed(formulas.size(), true);
464 // It might be that formulas are declared in a weird order.
465 // We follow a trial-and-error approach: If we can not parse the expression for one formula,
466 // we assume a subsequent formula has to be evaluated first.
467 // We cycle through the formulas until no further progress is made
468 bool progress = true;
469 while (progress) {
470 progress = false;
471 for (uint64_t formulaIndex = unprocessed.getNextSetIndex(0); formulaIndex < formulas.size();
472 formulaIndex = unprocessed.getNextSetIndex(formulaIndex + 1)) {
473 storm::expressions::Expression expression = this->expressionParser->parseFromString(formulaExpressions[formulaIndex], true);
474 if (expression.isInitialized()) {
475 progress = true;
476 unprocessed.set(formulaIndex, false);
477 formulaOrder.push_back(formulaIndex);
478 storm::expressions::Variable variable;
479 try {
480 if (expression.hasIntegerType()) {
481 variable = manager->declareIntegerVariable(formulas[formulaIndex].getName());
482 } else if (expression.hasBooleanType()) {
483 variable = manager->declareBooleanVariable(formulas[formulaIndex].getName());
484 } else {
485 STORM_LOG_ASSERT(expression.hasNumericalType(),
486 "Unexpected type for formula expression of formula " << formulas[formulaIndex].getName());
487 variable = manager->declareRationalVariable(formulas[formulaIndex].getName());
488 }
489 this->identifiers_.add(formulas[formulaIndex].getName(), variable.getExpression());
490 } catch (storm::exceptions::InvalidArgumentException const& e) {
491 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
492 "Parsing error in " << this->getFilename() << ": illegal identifier '" << formulas[formulaIndex].getName() << "' at line '"
493 << formulas[formulaIndex].getLineNumber());
494 }
495 this->expressionParser->setIdentifierMapping(&this->identifiers_);
496 }
497 }
498 }
499 if (!unprocessed.empty()) {
500 for (auto formulaIndex : unprocessed) {
501 STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Invalid expression for formula '" << formulas[formulaIndex].getName()
502 << "' at line '" << formulas[formulaIndex].getLineNumber() << "':\n\t" << formulaExpressions[formulaIndex]);
503 }
504 STORM_LOG_THROW(unprocessed.getNumberOfSetBits() == 1, storm::exceptions::WrongFormatException,
505 "Unable to parse expressions for " << unprocessed.getNumberOfSetBits() << " formulas. This could be due to circular dependencies");
506 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
507 "Unable to parse expression for formula '" << formulas[unprocessed.getNextSetIndex(0)].getName() << "'.");
508 }
509}
510
511void PrismParserGrammar::allowDoubleLiterals(bool flag) {
512 this->expressionParser->setAcceptDoubleLiterals(flag);
513}
514
515std::string const& PrismParserGrammar::getFilename() const {
516 return this->filename;
517}
518
519bool PrismParserGrammar::isValidIdentifier(std::string const& identifier) {
520 if (this->keywords_.find(identifier) != nullptr) {
521 return false;
522 }
523 return true;
524}
525
526bool PrismParserGrammar::isKnownModuleName(std::string const& moduleName, bool inSecondRun) {
527 if ((this->secondRun == inSecondRun) && this->globalProgramInformation.moduleToIndexMap.count(moduleName) == 0) {
528 STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Unknown module '" << moduleName << "'.");
529 return false;
530 }
531 return true;
532}
533
534bool PrismParserGrammar::isFreshModuleName(std::string const& moduleName) {
535 if (!this->secondRun && this->globalProgramInformation.moduleToIndexMap.count(moduleName) != 0) {
536 STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Duplicate module name '" << moduleName << "'.");
537 return false;
538 }
539 return true;
540}
541
542bool PrismParserGrammar::isKnownActionName(std::string const& actionName, bool inSecondRun) {
543 if ((this->secondRun == inSecondRun) && this->globalProgramInformation.actionIndices.count(actionName) == 0) {
544 STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Unknown action label '" << actionName << "'.");
545 return false;
546 }
547 return true;
548}
549
550bool PrismParserGrammar::isFreshIdentifier(std::string const& identifier) {
551 if (!this->secondRun && this->manager->hasVariable(identifier)) {
552 STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Duplicate identifier '" << identifier << "'.");
553 return false;
554 }
555 return true;
556}
557
558bool PrismParserGrammar::isFreshLabelName(std::string const& labelName) {
559 if (!this->secondRun) {
560 for (auto const& existingLabel : this->globalProgramInformation.labels) {
561 if (labelName == existingLabel.getName()) {
562 STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Duplicate label name '" << identifier << "'.");
563 return false;
564 }
565 }
566 }
567 return true;
568}
569
570bool PrismParserGrammar::isFreshObservationLabelName(std::string const& labelName) {
571 if (!this->secondRun) {
572 for (auto const& existingLabel : this->globalProgramInformation.observationLabels) {
573 if (labelName == existingLabel.getName()) {
574 STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Duplicate observable name '" << identifier << "'.");
575 return false;
576 }
577 }
578 }
579 return true;
580}
581
582bool PrismParserGrammar::isFreshRewardModelName(std::string const& rewardModelName) {
583 if (!this->secondRun) {
584 for (auto const& existingRewardModel : this->globalProgramInformation.rewardModels) {
585 if (rewardModelName == existingRewardModel.getName()) {
586 STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Duplicate reward model name '" << identifier << "'.");
587 return false;
588 }
589 }
590 }
591 return true;
592}
593
594bool PrismParserGrammar::isFreshPlayerName(std::string const& playerName) {
595 return true;
596}
597
598bool PrismParserGrammar::isOfBoolType(storm::expressions::Expression const& expression) {
599 return !this->secondRun || expression.hasBooleanType();
600}
601
602bool PrismParserGrammar::isOfIntType(storm::expressions::Expression const& expression) {
603 return !this->secondRun || expression.hasIntegerType();
604}
605
606bool PrismParserGrammar::isOfNumericalType(storm::expressions::Expression const& expression) {
607 return !this->secondRun || expression.hasNumericalType();
608}
609
610bool PrismParserGrammar::addInitialStatesConstruct(storm::expressions::Expression const& initialStatesExpression,
611 GlobalProgramInformation& globalProgramInformation) {
612 STORM_LOG_THROW(!globalProgramInformation.hasInitialConstruct, storm::exceptions::WrongFormatException,
613 "Parsing error in " << this->getFilename() << ": Program must not define two initial constructs.");
614 if (globalProgramInformation.hasInitialConstruct) {
615 return false;
616 }
617 globalProgramInformation.hasInitialConstruct = true;
618 globalProgramInformation.initialConstruct = storm::prism::InitialConstruct(initialStatesExpression, this->getFilename(), get_line(qi::_3));
619 return true;
620}
621
622bool PrismParserGrammar::addSystemCompositionConstruct(std::shared_ptr<storm::prism::Composition> const& composition,
623 GlobalProgramInformation& globalProgramInformation) {
624 globalProgramInformation.systemCompositionConstruct = storm::prism::SystemCompositionConstruct(composition, this->getFilename(), get_line(qi::_3));
625 return true;
626}
627
628void PrismParserGrammar::setModelType(GlobalProgramInformation& globalProgramInformation, storm::prism::Program::ModelType const& modelType) {
629 STORM_LOG_THROW(globalProgramInformation.modelType == storm::prism::Program::ModelType::UNDEFINED, storm::exceptions::WrongFormatException,
630 "Parsing error in " << this->getFilename() << ": Program must not set model type multiple times.");
631 globalProgramInformation.modelType = modelType;
632}
633
634std::shared_ptr<storm::prism::Composition> PrismParserGrammar::createModuleComposition(std::string const& moduleName) const {
635 return std::make_shared<storm::prism::ModuleComposition>(moduleName);
636}
637
638std::shared_ptr<storm::prism::Composition> PrismParserGrammar::createRenamingComposition(std::shared_ptr<storm::prism::Composition> const& subcomposition,
639 std::map<std::string, std::string> const& renaming) const {
640 return std::make_shared<storm::prism::RenamingComposition>(subcomposition, renaming);
641}
642
643std::shared_ptr<storm::prism::Composition> PrismParserGrammar::createHidingComposition(std::shared_ptr<storm::prism::Composition> const& subcomposition,
644 std::set<std::string> const& actionsToHide) const {
645 return std::make_shared<storm::prism::HidingComposition>(subcomposition, actionsToHide);
646}
647
648std::shared_ptr<storm::prism::Composition> PrismParserGrammar::createSynchronizingParallelComposition(
649 std::shared_ptr<storm::prism::Composition> const& left, std::shared_ptr<storm::prism::Composition> const& right) const {
650 return std::make_shared<storm::prism::SynchronizingParallelComposition>(left, right);
651}
652
653std::shared_ptr<storm::prism::Composition> PrismParserGrammar::createInterleavingParallelComposition(
654 std::shared_ptr<storm::prism::Composition> const& left, std::shared_ptr<storm::prism::Composition> const& right) const {
655 return std::make_shared<storm::prism::InterleavingParallelComposition>(left, right);
656}
657
658std::shared_ptr<storm::prism::Composition> PrismParserGrammar::createRestrictedParallelComposition(
659 std::shared_ptr<storm::prism::Composition> const& left, std::set<std::string> const& synchronizingActions,
660 std::shared_ptr<storm::prism::Composition> const& right) const {
661 return std::make_shared<storm::prism::RestrictedParallelComposition>(left, synchronizingActions, right);
662}
663
664storm::prism::Constant PrismParserGrammar::createUndefinedBooleanConstant(std::string const& newConstant) const {
665 if (!this->secondRun) {
666 try {
667 storm::expressions::Variable newVariable = manager->declareBooleanVariable(newConstant, true);
668 this->identifiers_.add(newConstant, newVariable.getExpression());
669 } catch (storm::exceptions::InvalidArgumentException const& e) {
670 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
671 "Parsing error in " << this->getFilename() << ": illegal identifier '" << newConstant << "'.");
672 }
673 }
674 return storm::prism::Constant(manager->getVariable(newConstant), this->getFilename());
675}
676
677storm::prism::Constant PrismParserGrammar::createUndefinedIntegerConstant(std::string const& newConstant) const {
678 if (!this->secondRun) {
679 try {
680 storm::expressions::Variable newVariable = manager->declareIntegerVariable(newConstant, true);
681 this->identifiers_.add(newConstant, newVariable.getExpression());
682 } catch (storm::exceptions::InvalidArgumentException const& e) {
683 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
684 "Parsing error in " << this->getFilename() << ": illegal identifier '" << newConstant << "'.");
685 }
686 }
687 return storm::prism::Constant(manager->getVariable(newConstant), this->getFilename());
688}
689
690storm::prism::Constant PrismParserGrammar::createUndefinedDoubleConstant(std::string const& newConstant) const {
691 if (!this->secondRun) {
692 try {
693 storm::expressions::Variable newVariable = manager->declareRationalVariable(newConstant, true);
694 this->identifiers_.add(newConstant, newVariable.getExpression());
695 } catch (storm::exceptions::InvalidArgumentException const& e) {
696 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
697 "Parsing error in " << this->getFilename() << ": illegal identifier '" << newConstant << "'.");
698 }
699 }
700 return storm::prism::Constant(manager->getVariable(newConstant), this->getFilename());
701}
702
703storm::prism::Constant PrismParserGrammar::createDefinedBooleanConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
704 if (!this->secondRun) {
705 try {
706 storm::expressions::Variable newVariable = manager->declareBooleanVariable(newConstant, true);
707 this->identifiers_.add(newConstant, newVariable.getExpression());
708 } catch (storm::exceptions::InvalidArgumentException const& e) {
709 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
710 "Parsing error in " << this->getFilename() << ": illegal identifier '" << newConstant << "'.");
711 }
712 }
713 return storm::prism::Constant(manager->getVariable(newConstant), expression, this->getFilename());
714}
715
716storm::prism::Constant PrismParserGrammar::createDefinedIntegerConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
717 if (!this->secondRun) {
718 try {
719 storm::expressions::Variable newVariable = manager->declareIntegerVariable(newConstant, true);
720 this->identifiers_.add(newConstant, newVariable.getExpression());
721 } catch (storm::exceptions::InvalidArgumentException const& e) {
722 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
723 "Parsing error in " << this->getFilename() << ": illegal identifier '" << newConstant << "'.");
724 }
725 }
726 return storm::prism::Constant(manager->getVariable(newConstant), expression, this->getFilename());
727}
728
729storm::prism::Constant PrismParserGrammar::createDefinedDoubleConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
730 if (!this->secondRun) {
731 try {
732 storm::expressions::Variable newVariable = manager->declareRationalVariable(newConstant, true);
733 this->identifiers_.add(newConstant, newVariable.getExpression());
734 } catch (storm::exceptions::InvalidArgumentException const& e) {
735 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
736 "Parsing error in " << this->getFilename() << ": illegal identifier '" << newConstant << "'.");
737 }
738 }
739 return storm::prism::Constant(manager->getVariable(newConstant), expression, this->getFilename());
740}
741
742storm::prism::Formula PrismParserGrammar::createFormulaFirstRun(std::string const& formulaName, std::string const& expression) {
743 // Only store the expression as a string. It will be parsed between first and second run
744 // This is necessary because the resulting type of the formula is only known after the first run.
745 STORM_LOG_ASSERT(!this->secondRun, "This constructor should have only been called during the first run.");
746 formulaExpressions.push_back(expression);
747 return storm::prism::Formula(formulaName, this->getFilename());
748}
749
750storm::prism::Formula PrismParserGrammar::createFormulaSecondRun(std::string const& formulaName, storm::expressions::Expression const& expression) {
751 // This is necessary because the resulting type of the formula is only known after the first run.
752 STORM_LOG_ASSERT(this->secondRun, "This constructor should have only been called during the second run.");
753 storm::expressions::Expression lhsExpression = *this->identifiers_.find(formulaName);
754 return storm::prism::Formula(lhsExpression.getBaseExpression().asVariableExpression().getVariable(), expression, this->getFilename());
755}
756
757storm::prism::Label PrismParserGrammar::createLabel(std::string const& labelName, storm::expressions::Expression expression) const {
758 return storm::prism::Label(labelName, expression, this->getFilename());
759}
760
761storm::prism::ObservationLabel PrismParserGrammar::createObservationLabel(std::string const& labelName, storm::expressions::Expression expression) const {
762 return storm::prism::ObservationLabel(labelName, expression, this->getFilename());
763}
764
765storm::prism::RewardModel PrismParserGrammar::createRewardModel(std::string const& rewardModelName, std::vector<storm::prism::StateReward> const& stateRewards,
766 std::vector<storm::prism::StateActionReward> const& stateActionRewards,
767 std::vector<storm::prism::TransitionReward> const& transitionRewards) const {
768 return storm::prism::RewardModel(rewardModelName, stateRewards, stateActionRewards, transitionRewards, this->getFilename());
769}
770
771storm::prism::StateReward PrismParserGrammar::createStateReward(storm::expressions::Expression statePredicateExpression,
772 storm::expressions::Expression rewardValueExpression) const {
773 if (this->secondRun) {
774 return storm::prism::StateReward(statePredicateExpression, rewardValueExpression, this->getFilename());
775 } else {
776 return storm::prism::StateReward();
777 }
778}
779
780storm::prism::StateActionReward PrismParserGrammar::createStateActionReward(boost::optional<std::string> const& actionName,
781 storm::expressions::Expression statePredicateExpression,
782 storm::expressions::Expression rewardValueExpression,
783 GlobalProgramInformation& globalProgramInformation) const {
784 if (this->secondRun) {
785 std::string realActionName = actionName ? actionName.get() : "";
786
787 auto const& nameIndexPair = globalProgramInformation.actionIndices.find(realActionName);
788 STORM_LOG_THROW(nameIndexPair != globalProgramInformation.actionIndices.end(), storm::exceptions::WrongFormatException,
789 "Action reward refers to illegal action '" << realActionName << "'.");
790 return storm::prism::StateActionReward(nameIndexPair->second, realActionName, statePredicateExpression, rewardValueExpression, this->getFilename());
791 } else {
792 return storm::prism::StateActionReward();
793 }
794}
795
796storm::prism::TransitionReward PrismParserGrammar::createTransitionReward(boost::optional<std::string> const& actionName,
797 storm::expressions::Expression sourceStatePredicateExpression,
798 storm::expressions::Expression targetStatePredicateExpression,
799 storm::expressions::Expression rewardValueExpression,
800 GlobalProgramInformation& globalProgramInformation) const {
801 if (this->secondRun) {
802 std::string realActionName = actionName ? actionName.get() : "";
803
804 auto const& nameIndexPair = globalProgramInformation.actionIndices.find(realActionName);
805 STORM_LOG_THROW(nameIndexPair != globalProgramInformation.actionIndices.end(), storm::exceptions::WrongFormatException,
806 "Transition reward refers to illegal action '" << realActionName << "'.");
807 return storm::prism::TransitionReward(nameIndexPair->second, realActionName, sourceStatePredicateExpression, targetStatePredicateExpression,
808 rewardValueExpression, this->getFilename());
809 } else {
810 return storm::prism::TransitionReward();
811 }
812}
813
814storm::prism::Assignment PrismParserGrammar::createAssignment(std::string const& variableName, storm::expressions::Expression assignedExpression) const {
815 return storm::prism::Assignment(manager->getVariable(variableName), assignedExpression, this->getFilename());
816}
817
818storm::prism::Update PrismParserGrammar::createUpdate(typename storm::prism::Update::ExpressionPair likelihoodExpressions,
819 std::vector<storm::prism::Assignment> const& assignments,
820 GlobalProgramInformation& globalProgramInformation) const {
821 ++globalProgramInformation.currentUpdateIndex;
822 if (!likelihoodExpressions.first.isInitialized()) {
823 likelihoodExpressions.first = manager->rational(1);
824 }
825 return storm::prism::Update(globalProgramInformation.currentUpdateIndex - 1, likelihoodExpressions, assignments, this->getFilename());
826}
827
828storm::prism::Command PrismParserGrammar::createCommand(bool markovian, boost::optional<std::string> const& actionName,
829 storm::expressions::Expression guardExpression, std::vector<storm::prism::Update> const& updates,
830 GlobalProgramInformation& globalProgramInformation) const {
831 ++globalProgramInformation.currentCommandIndex;
832 std::string realActionName = actionName ? actionName.get() : "";
833
834 uint_fast64_t actionIndex = 0;
835
836 // If the action name was not yet seen, record it.
837 auto nameIndexPair = globalProgramInformation.actionIndices.find(realActionName);
838 if (nameIndexPair == globalProgramInformation.actionIndices.end()) {
839 std::size_t nextIndex = globalProgramInformation.actionIndices.size();
840 globalProgramInformation.actionIndices.emplace(realActionName, nextIndex);
841 actionIndex = nextIndex;
842 } else {
843 actionIndex = nameIndexPair->second;
844 }
845 return storm::prism::Command(globalProgramInformation.currentCommandIndex - 1, markovian, actionIndex, realActionName, guardExpression, updates,
846 this->getFilename());
847}
848
849storm::prism::Command PrismParserGrammar::createDummyCommand(boost::optional<std::string> const& actionName,
850 GlobalProgramInformation& globalProgramInformation) const {
851 STORM_LOG_ASSERT(!this->secondRun, "Dummy procedure must not be called in second run.");
852 std::string realActionName = actionName ? actionName.get() : "";
853
854 // Register the action name if it has not appeared earlier.
855 auto nameIndexPair = globalProgramInformation.actionIndices.find(realActionName);
856 if (nameIndexPair == globalProgramInformation.actionIndices.end()) {
857 std::size_t nextIndex = globalProgramInformation.actionIndices.size();
858 globalProgramInformation.actionIndices.emplace(realActionName, nextIndex);
859 }
860
861 return storm::prism::Command();
862}
863
864storm::prism::BooleanVariable PrismParserGrammar::createBooleanVariable(std::string const& variableName,
865 storm::expressions::Expression initialValueExpression) const {
866 if (!this->secondRun) {
867 try {
868 storm::expressions::Variable newVariable = manager->declareBooleanVariable(variableName);
869 this->identifiers_.add(variableName, newVariable.getExpression());
870 } catch (storm::exceptions::InvalidArgumentException const& e) {
871 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
872 "Parsing error in " << this->getFilename() << ": illegal identifier '" << variableName << "'.");
873 }
874 }
875 bool observable = this->observables.count(variableName) > 0;
876 if (observable) {
877 this->observables.erase(variableName);
878 }
879 return storm::prism::BooleanVariable(manager->getVariable(variableName), initialValueExpression, observable, this->getFilename());
880}
881
882storm::prism::IntegerVariable PrismParserGrammar::createIntegerVariable(std::string const& variableName, storm::expressions::Expression lowerBoundExpression,
883 storm::expressions::Expression upperBoundExpression,
884 storm::expressions::Expression initialValueExpression) const {
885 if (!this->secondRun) {
886 try {
887 storm::expressions::Variable newVariable = manager->declareIntegerVariable(variableName);
888 this->identifiers_.add(variableName, newVariable.getExpression());
889 } catch (storm::exceptions::InvalidArgumentException const& e) {
890 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
891 "Parsing error in " << this->getFilename() << ": illegal identifier '" << variableName << "'.");
892 }
893 }
894 bool observable = this->observables.count(variableName) > 0;
895 if (observable) {
896 this->observables.erase(variableName);
897 }
898
899 return storm::prism::IntegerVariable(manager->getVariable(variableName), lowerBoundExpression, upperBoundExpression, initialValueExpression, observable,
900 this->getFilename());
901}
902
903storm::prism::ClockVariable PrismParserGrammar::createClockVariable(std::string const& variableName) const {
904 if (!this->secondRun) {
905 try {
906 storm::expressions::Variable newVariable = manager->declareRationalVariable(variableName);
907 this->identifiers_.add(variableName, newVariable.getExpression());
908 } catch (storm::exceptions::InvalidArgumentException const& e) {
909 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
910 "Parsing error in " << this->getFilename() << ": illegal identifier '" << variableName << "'.");
911 }
912 }
913 bool observable = this->observables.count(variableName) > 0;
914 if (observable) {
915 this->observables.erase(variableName);
916 }
917
918 return storm::prism::ClockVariable(manager->getVariable(variableName), observable, this->getFilename());
919}
920
921void PrismParserGrammar::createObservablesList(std::vector<std::string> const& observables) {
922 this->observables.insert(observables.begin(), observables.end());
923 // We need this list to be filled in both runs.
924}
925
926storm::prism::Player PrismParserGrammar::createPlayer(std::string const& playerName, std::vector<std::string> const& moduleNames,
927 std::vector<std::string> const& actionNames) {
928 if (this->secondRun) {
929 std::unordered_set<std::string> controlledModules;
930 std::unordered_set<std::string> controlledActions;
931 for (auto const& moduleName : moduleNames) {
932 auto moduleIndexPair = globalProgramInformation.moduleToIndexMap.find(moduleName);
933 STORM_LOG_ASSERT(moduleIndexPair != globalProgramInformation.moduleToIndexMap.end(),
934 "Parsing error in " << this->getFilename() << " for player " << playerName << ": No module named '" << moduleName << "' present.");
935 controlledModules.insert(moduleIndexPair->first);
936 bool moduleNotYetControlled = globalProgramInformation.playerControlledModules.insert(moduleIndexPair->second).second;
937 STORM_LOG_THROW(moduleNotYetControlled, storm::exceptions::WrongFormatException,
938 "Parsing error in " << this->getFilename() << " for player " << playerName << ": Module '" << moduleName
939 << "' already controlled by another player.");
940 }
941 for (std::string actionName : actionNames) {
942 auto actionIndexPair = globalProgramInformation.actionIndices.find(actionName);
943 STORM_LOG_ASSERT(actionIndexPair != globalProgramInformation.actionIndices.end(),
944 "Parsing error in " << this->getFilename() << " for player " << playerName << ": No action named '" << actionName << "' present.");
945 controlledActions.insert(actionIndexPair->first);
946 bool actionNotYetControlled = globalProgramInformation.playerControlledActions.insert(actionIndexPair->second).second;
947 STORM_LOG_THROW(actionNotYetControlled, storm::exceptions::WrongFormatException,
948 "Parsing error in " << this->getFilename() << " for player " << playerName << ": Command '" << actionName
949 << "' already controlled by another player.");
950 }
951 return storm::prism::Player(playerName, controlledModules, controlledActions);
952 } else {
953 return storm::prism::Player();
954 }
955}
956
957storm::prism::Module PrismParserGrammar::createModule(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables,
958 std::vector<storm::prism::IntegerVariable> const& integerVariables,
959 std::vector<storm::prism::ClockVariable> const& clockVariables,
960 boost::optional<storm::expressions::Expression> const& invariant,
961 std::vector<storm::prism::Command> const& commands,
962 GlobalProgramInformation& globalProgramInformation) const {
963 if (!this->secondRun) {
964 globalProgramInformation.moduleToIndexMap[moduleName] = globalProgramInformation.modules.size();
965 }
966 // Assert that the module name is already known and has the expected index.
967 STORM_LOG_ASSERT(!this->secondRun || globalProgramInformation.moduleToIndexMap.count(moduleName) > 0, "Module name '" << moduleName << "' was not found.");
968 STORM_LOG_ASSERT(!this->secondRun || globalProgramInformation.moduleToIndexMap[moduleName] == globalProgramInformation.modules.size(),
969 "The index for module '" << moduleName << "' does not match the index from the first parsing run.");
970 return storm::prism::Module(moduleName, booleanVariables, integerVariables, clockVariables,
971 invariant.is_initialized() ? invariant.get() : storm::expressions::Expression(), commands, this->getFilename());
972}
973
974bool PrismParserGrammar::isValidModuleRenaming(std::string const& oldModuleName, storm::prism::ModuleRenaming const& moduleRenaming,
975 GlobalProgramInformation const& globalProgramInformation) const {
976 if (!this->secondRun) {
977 auto const& renaming = moduleRenaming.getRenaming();
978 auto const& moduleIndexPair = globalProgramInformation.moduleToIndexMap.find(oldModuleName);
979 if (moduleIndexPair == globalProgramInformation.moduleToIndexMap.end()) {
980 STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": No module named '" << oldModuleName << "' to rename.");
981 return false;
982 }
983 storm::prism::Module const& moduleToRename = globalProgramInformation.modules[moduleIndexPair->second];
984 // Check whether all varialbes are renamed.
985 for (auto const& variable : moduleToRename.getBooleanVariables()) {
986 auto const& renamingPair = renaming.find(variable.getName());
987 if (renamingPair == renaming.end()) {
988 STORM_LOG_ERROR("Parsing error in renaming of module '" << oldModuleName << "': Boolean variable '" << variable.getName()
989 << "' was not renamed.");
990 return false;
991 }
992 }
993 for (auto const& variable : moduleToRename.getIntegerVariables()) {
994 auto const& renamingPair = renaming.find(variable.getName());
995 if (renamingPair == renaming.end()) {
996 STORM_LOG_ERROR("Parsing error in renaming of module '" << oldModuleName << "': Integer variable '" << variable.getName()
997 << "' was not renamed.");
998 return false;
999 }
1000 }
1001 for (auto const& variable : moduleToRename.getClockVariables()) {
1002 auto const& renamingPair = renaming.find(variable.getName());
1003 if (renamingPair == renaming.end()) {
1004 STORM_LOG_ERROR("Parsing error in renaming of module '" << oldModuleName << "': Clock variable '" << variable.getName()
1005 << "' was not renamed.");
1006 return false;
1007 }
1008 }
1009 }
1010 return true;
1011}
1012
1013storm::prism::ModuleRenaming PrismParserGrammar::createModuleRenaming(std::map<std::string, std::string> const& renaming) const {
1014 return storm::prism::ModuleRenaming(renaming);
1015}
1016
1017storm::prism::Module PrismParserGrammar::createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName,
1018 storm::prism::ModuleRenaming const& moduleRenaming,
1019 GlobalProgramInformation& globalProgramInformation) const {
1020 // Check whether the module to rename actually exists.
1021 auto const& moduleIndexPair = globalProgramInformation.moduleToIndexMap.find(oldModuleName);
1022 STORM_LOG_THROW(moduleIndexPair != globalProgramInformation.moduleToIndexMap.end(), storm::exceptions::WrongFormatException,
1023 "Parsing error in " << this->getFilename() << ": No module named '" << oldModuleName << "' to rename.");
1024 storm::prism::Module const& moduleToRename = globalProgramInformation.modules[moduleIndexPair->second];
1025 STORM_LOG_THROW(!moduleToRename.isRenamedFromModule(), storm::exceptions::WrongFormatException,
1026 "Parsing error in " << this->getFilename() << ": The module '" << newModuleName << "' can not be created from module '" << oldModuleName
1027 << "' through module renaming because '" << oldModuleName << "' is also a renamed module. Create '" << newModuleName
1028 << "' via a renaming from base module '" << moduleToRename.getBaseModule() << "' instead.");
1029 auto const& renaming = moduleRenaming.getRenaming();
1030 if (!this->secondRun) {
1031 // Add a mapping from the new module name to its (future) index.
1032 globalProgramInformation.moduleToIndexMap[newModuleName] = globalProgramInformation.modules.size();
1033
1034 // Register all (renamed) variables for later use.
1035 // We already checked before, whether the renaiming is valid.
1036 for (auto const& variable : moduleToRename.getBooleanVariables()) {
1037 auto const& renamingPair = renaming.find(variable.getName());
1038 STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException,
1039 "Parsing error in " << this->getFilename() << ": Boolean variable '" << variable.getName() << " was not renamed.");
1040 storm::expressions::Variable renamedVariable = manager->declareBooleanVariable(renamingPair->second);
1041 this->identifiers_.add(renamingPair->second, renamedVariable.getExpression());
1042 if (this->observables.count(renamingPair->second) > 0) {
1043 this->observables.erase(renamingPair->second);
1044 }
1045 }
1046 for (auto const& variable : moduleToRename.getIntegerVariables()) {
1047 auto const& renamingPair = renaming.find(variable.getName());
1048 STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException,
1049 "Parsing error in " << this->getFilename() << ": Integer variable '" << variable.getName() << " was not renamed.");
1050 storm::expressions::Variable renamedVariable = manager->declareIntegerVariable(renamingPair->second);
1051 this->identifiers_.add(renamingPair->second, renamedVariable.getExpression());
1052 if (this->observables.count(renamingPair->second) > 0) {
1053 this->observables.erase(renamingPair->second);
1054 }
1055 }
1056 for (auto const& variable : moduleToRename.getClockVariables()) {
1057 auto const& renamingPair = renaming.find(variable.getName());
1058 STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException,
1059 "Parsing error in " << this->getFilename() << ": Clock variable '" << variable.getName() << " was not renamed.");
1060 storm::expressions::Variable renamedVariable = manager->declareRationalVariable(renamingPair->second);
1061 this->identifiers_.add(renamingPair->second, renamedVariable.getExpression());
1062 if (this->observables.count(renamingPair->second) > 0) {
1063 this->observables.erase(renamingPair->second);
1064 }
1065 }
1066
1067 for (auto const& command : moduleToRename.getCommands()) {
1068 std::string newActionName = command.getActionName();
1069 auto const& renamingPair = renaming.find(command.getActionName());
1070 if (renamingPair != renaming.end()) {
1071 newActionName = renamingPair->second;
1072 }
1073
1074 // Record any newly occurring action names/indices.
1075 auto nameIndexPair = globalProgramInformation.actionIndices.find(newActionName);
1076 if (nameIndexPair == globalProgramInformation.actionIndices.end()) {
1077 std::size_t nextIndex = globalProgramInformation.actionIndices.size();
1078 globalProgramInformation.actionIndices.emplace(newActionName, nextIndex);
1079 }
1080 }
1081
1082 // Return a dummy module in the first pass.
1083 return storm::prism::Module();
1084 } else {
1085 // Assert that the module name is already known and has the expected index.
1086 STORM_LOG_ASSERT(globalProgramInformation.moduleToIndexMap.count(newModuleName) > 0, "Module name '" << newModuleName << "' was not found.");
1087 STORM_LOG_ASSERT(globalProgramInformation.moduleToIndexMap[newModuleName] == globalProgramInformation.modules.size(),
1088 "The index for module " << newModuleName << " does not match the index from the first parsing run.");
1089
1090 // Create a mapping from identifiers to the expressions they need to be replaced with.
1091 std::map<storm::expressions::Variable, storm::expressions::Expression> expressionRenaming;
1092 for (auto const& namePair : renaming) {
1093 storm::expressions::Expression const* substitutedExpression = this->identifiers_.find(namePair.second);
1094 // If the mapped-to-value is an expression, we need to replace it.
1095 if (substitutedExpression != nullptr) {
1096 expressionRenaming.emplace(manager->getVariable(namePair.first), *substitutedExpression);
1097 }
1098 }
1099
1100 // Rename the boolean variables.
1101 std::vector<storm::prism::BooleanVariable> booleanVariables;
1102 for (auto const& variable : moduleToRename.getBooleanVariables()) {
1103 auto const& renamingPair = renaming.find(variable.getName());
1104 STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException,
1105 "Parsing error in " << this->getFilename() << ": Boolean variable '" << variable.getName() << " was not renamed.");
1106 bool observable = this->observables.count(renamingPair->second) > 0;
1107 if (observable) {
1108 this->observables.erase(renamingPair->second);
1109 }
1110 booleanVariables.push_back(storm::prism::BooleanVariable(
1111 manager->getVariable(renamingPair->second),
1112 variable.hasInitialValue() ? variable.getInitialValueExpression().substitute(expressionRenaming) : variable.getInitialValueExpression(),
1113 observable, this->getFilename(), moduleRenaming.getLineNumber()));
1114 }
1115
1116 // Rename the integer variables.
1117 std::vector<storm::prism::IntegerVariable> integerVariables;
1118 for (auto const& variable : moduleToRename.getIntegerVariables()) {
1119 auto const& renamingPair = renaming.find(variable.getName());
1120 STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException,
1121 "Parsing error in " << this->getFilename() << ": Integer variable '" << variable.getName() << " was not renamed.");
1122 bool observable = this->observables.count(renamingPair->second) > 0;
1123 if (observable) {
1124 this->observables.erase(renamingPair->second);
1125 }
1126 integerVariables.push_back(storm::prism::IntegerVariable(
1127 manager->getVariable(renamingPair->second), variable.getLowerBoundExpression().substitute(expressionRenaming),
1128 variable.getUpperBoundExpression().substitute(expressionRenaming),
1129 variable.hasInitialValue() ? variable.getInitialValueExpression().substitute(expressionRenaming) : variable.getInitialValueExpression(),
1130 observable, this->getFilename(), moduleRenaming.getLineNumber()));
1131 }
1132
1133 // Rename the clock variables.
1134 std::vector<storm::prism::ClockVariable> clockVariables;
1135 for (auto const& variable : moduleToRename.getClockVariables()) {
1136 auto const& renamingPair = renaming.find(variable.getName());
1137 STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException,
1138 "Parsing error in " << this->getFilename() << ": Clock variable '" << variable.getName() << " was not renamed.");
1139 bool observable = this->observables.count(renamingPair->second) > 0;
1140 if (observable) {
1141 this->observables.erase(renamingPair->second);
1142 }
1143 clockVariables.push_back(
1144 storm::prism::ClockVariable(manager->getVariable(renamingPair->second), observable, this->getFilename(), moduleRenaming.getLineNumber()));
1145 }
1146
1147 // Rename invariant (if present)
1148 storm::expressions::Expression invariant;
1149 if (moduleToRename.hasInvariant()) {
1150 invariant = moduleToRename.getInvariant().substitute(expressionRenaming);
1151 }
1152
1153 // Rename commands.
1154 std::vector<storm::prism::Command> commands;
1155 for (auto const& command : moduleToRename.getCommands()) {
1156 std::vector<storm::prism::Update> updates;
1157 for (auto const& update : command.getUpdates()) {
1158 std::vector<storm::prism::Assignment> assignments;
1159 for (auto const& assignment : update.getAssignments()) {
1160 auto const& renamingPair = renaming.find(assignment.getVariableName());
1161 if (renamingPair != renaming.end()) {
1162 assignments.emplace_back(manager->getVariable(renamingPair->second), assignment.getExpression().substitute(expressionRenaming),
1163 this->getFilename(), moduleRenaming.getLineNumber());
1164 } else {
1165 assignments.emplace_back(assignment.getVariable(), assignment.getExpression().substitute(expressionRenaming), this->getFilename(),
1166 moduleRenaming.getLineNumber());
1167 }
1168 }
1169 if (update.isLikelihoodInterval()) {
1170 typename storm::prism::Update::ExpressionPair likelihoodInterval{
1171 update.getLikelihoodExpressionInterval().first.substitute(expressionRenaming),
1172 update.getLikelihoodExpressionInterval().second.substitute(expressionRenaming)};
1173 updates.emplace_back(globalProgramInformation.currentUpdateIndex, likelihoodInterval, assignments, this->getFilename(),
1174 moduleRenaming.getLineNumber());
1175 } else {
1176 updates.emplace_back(globalProgramInformation.currentUpdateIndex, update.getLikelihoodExpression().substitute(expressionRenaming),
1177 assignments, this->getFilename(), moduleRenaming.getLineNumber());
1178 }
1179 ++globalProgramInformation.currentUpdateIndex;
1180 }
1181
1182 std::string newActionName = command.getActionName();
1183 auto const& renamingPair = renaming.find(command.getActionName());
1184 if (renamingPair != renaming.end()) {
1185 newActionName = renamingPair->second;
1186 }
1187
1188 uint_fast64_t actionIndex = 0;
1189 auto nameIndexPair = globalProgramInformation.actionIndices.find(newActionName);
1190 if (nameIndexPair == globalProgramInformation.actionIndices.end()) {
1191 std::size_t nextIndex = globalProgramInformation.actionIndices.size();
1192 globalProgramInformation.actionIndices.emplace(newActionName, nextIndex);
1193 actionIndex = nextIndex;
1194 } else {
1195 actionIndex = nameIndexPair->second;
1196 }
1197
1198 commands.emplace_back(globalProgramInformation.currentCommandIndex, command.isMarkovian(), actionIndex, newActionName,
1199 command.getGuardExpression().substitute(expressionRenaming), updates, this->getFilename(), moduleRenaming.getLineNumber());
1200 ++globalProgramInformation.currentCommandIndex;
1201 }
1202
1203 return storm::prism::Module(newModuleName, booleanVariables, integerVariables, clockVariables, invariant, commands, oldModuleName, renaming);
1204 }
1205}
1206
1207storm::prism::Program PrismParserGrammar::createProgram(GlobalProgramInformation const& globalProgramInformation) const {
1208 storm::prism::Program::ModelType finalModelType = globalProgramInformation.modelType;
1209 if (globalProgramInformation.modelType == storm::prism::Program::ModelType::UNDEFINED) {
1210 STORM_LOG_WARN("Program does not specify model type. Implicitly assuming 'mdp'.");
1211 finalModelType = storm::prism::Program::ModelType::MDP;
1212 }
1213
1214 // make sure formulas are stored in a proper order.
1215 std::vector<storm::prism::Formula> orderedFormulas;
1216 if (this->secondRun) {
1217 orderedFormulas.reserve(globalProgramInformation.formulas.size());
1218 for (uint64_t const& i : formulaOrder) {
1219 orderedFormulas.push_back(std::move(globalProgramInformation.formulas[i]));
1220 }
1221 }
1222
1223 return storm::prism::Program(
1224 manager, finalModelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables,
1225 globalProgramInformation.globalIntegerVariables, orderedFormulas, globalProgramInformation.players, globalProgramInformation.modules,
1226 globalProgramInformation.actionIndices, globalProgramInformation.rewardModels, globalProgramInformation.labels,
1227 globalProgramInformation.observationLabels,
1228 secondRun && !globalProgramInformation.hasInitialConstruct ? boost::none : boost::make_optional(globalProgramInformation.initialConstruct),
1229 globalProgramInformation.systemCompositionConstruct, prismCompatibility, this->getFilename(), 1, this->secondRun);
1230}
1231
1232void PrismParserGrammar::removeInitialConstruct(GlobalProgramInformation& globalProgramInformation) const {
1233 globalProgramInformation.hasInitialConstruct = false;
1234}
1235} // namespace parser
1236} // namespace storm
PositionIteratorType
boost::spirit::line_pos_iterator< BaseIteratorType > PositionIteratorType
Definition SpiritParserDefinitions.h:22
Iterator
PositionIteratorType Iterator
Definition SpiritParserDefinitions.h:23
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:80
storm::parser::GlobalProgramInformation::modules
std::vector< storm::prism::Module > modules
Definition PrismParserGrammar.h:77
storm::parser::GlobalProgramInformation::constants
std::vector< storm::prism::Constant > constants
Definition PrismParserGrammar.h:71
storm::parser::GlobalProgramInformation::labels
std::vector< storm::prism::Label > labels
Definition PrismParserGrammar.h:79
storm::parser::GlobalProgramInformation::players
std::vector< storm::prism::Player > players
Definition PrismParserGrammar.h:81
storm::parser::GlobalProgramInformation::globalBooleanVariables
std::vector< storm::prism::BooleanVariable > globalBooleanVariables
Definition PrismParserGrammar.h:73
storm::parser::GlobalProgramInformation::formulas
std::vector< storm::prism::Formula > formulas
Definition PrismParserGrammar.h:72
storm::parser::GlobalProgramInformation::actionIndices
std::map< std::string, uint_fast64_t > actionIndices
Definition PrismParserGrammar.h:76
storm::parser::GlobalProgramInformation::rewardModels
std::vector< storm::prism::RewardModel > rewardModels
Definition PrismParserGrammar.h:78
storm::parser::GlobalProgramInformation::moduleToIndexMap
std::map< std::string, uint_fast64_t > moduleToIndexMap
Definition PrismParserGrammar.h:75
storm::parser::GlobalProgramInformation::globalIntegerVariables
std::vector< storm::prism::IntegerVariable > globalIntegerVariables
Definition PrismParserGrammar.h:74
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::LocatedInformation::getLineNumber
uint_fast64_t getLineNumber() const
Retrieves the line number in which the information was found.
Definition LocatedInformation.cpp:17
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::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::ModuleRenaming::getRenaming
std::map< std::string, std::string > const & getRenaming() const
If the module was created via renaming, this method returns the applied renaming of identifiers used ...
Definition ModuleRenaming.cpp:13
storm::prism::Program::ModelType
ModelType
An enum for the different model types.
Definition Program.h:36
storm::prism::Program::hasInitialConstruct
bool hasInitialConstruct() const
Retrieves whether the program specifies an initial construct.
Definition Program.cpp:645
storm::prism::Update::ExpressionPair
std::pair< storm::expressions::Expression, storm::expressions::Expression > ExpressionPair
Definition Update.h:13
storm::storage::BitVector
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:16
STORM_LOG_WARN
#define STORM_LOG_WARN(message)
Definition logging.h:25
STORM_LOG_DEBUG
#define STORM_LOG_DEBUG(message)
Definition logging.h:18
STORM_LOG_TRACE
#define STORM_LOG_TRACE(message)
Definition logging.h:12
STORM_LOG_ERROR
#define STORM_LOG_ERROR(message)
Definition logging.h:26
STORM_LOG_ASSERT
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
STORM_LOG_THROW
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
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
LabParser.cpp.
Definition AutomaticSettings.cpp:13