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