Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Program.cpp
Go to the documentation of this file.
2
3#include <algorithm>
4#include <boost/algorithm/string/join.hpp>
5#include <sstream>
6
9
22
26
28
29namespace storm {
30namespace prism {
32 public:
33 CompositionValidityChecker(storm::prism::Program const& program) : program(program) {
34 // Intentionally left empty.
35 }
36
37 void check(Composition const& composition) {
38 composition.accept(*this, boost::any());
39 if (appearingModules.size() != program.getNumberOfModules()) {
40 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Not every module is used in the system composition.");
41 }
42 }
43
44 virtual boost::any visit(ModuleComposition const& composition, boost::any const&) override {
45 bool isValid = program.hasModule(composition.getModuleName());
46 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
47 "The module \"" << composition.getModuleName() << "\" referred to in the system composition does not exist.");
48 isValid = appearingModules.find(composition.getModuleName()) == appearingModules.end();
49 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
50 "The module \"" << composition.getModuleName() << "\" is referred to more than once in the system composition.");
51 appearingModules.insert(composition.getModuleName());
52 std::set<uint_fast64_t> synchronizingActionIndices = program.getModule(composition.getModuleName()).getSynchronizingActionIndices();
53 return synchronizingActionIndices;
54 }
55
56 virtual boost::any visit(RenamingComposition const& composition, boost::any const& data) override {
57 std::set<uint_fast64_t> subSynchronizingActionIndices = boost::any_cast<std::set<uint_fast64_t>>(composition.getSubcomposition().accept(*this, data));
58
59 std::set<uint_fast64_t> newSynchronizingActionIndices = subSynchronizingActionIndices;
60 for (auto const& namePair : composition.getActionRenaming()) {
61 if (!program.hasAction(namePair.first)) {
62 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "System composition refers to unknown action '" << namePair.first << "'.");
63 } else if (!program.hasAction(namePair.second)) {
64 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "System composition refers to unknown action '" << namePair.second << "'.");
65 } else {
66 uint_fast64_t fromIndex = program.getActionIndex(namePair.first);
67 uint_fast64_t toIndex = program.getActionIndex(namePair.second);
68 auto it = subSynchronizingActionIndices.find(fromIndex);
70 it != subSynchronizingActionIndices.end(), storm::exceptions::WrongFormatException,
71 "Cannot rename action '" << namePair.first << "', because module '" << composition.getSubcomposition() << " does not have this action.");
72 newSynchronizingActionIndices.erase(newSynchronizingActionIndices.find(fromIndex));
73 newSynchronizingActionIndices.insert(toIndex);
74 }
75 }
76
77 return newSynchronizingActionIndices;
78 }
79
80 virtual boost::any visit(HidingComposition const& composition, boost::any const& data) override {
81 std::set<uint_fast64_t> subSynchronizingActionIndices = boost::any_cast<std::set<uint_fast64_t>>(composition.getSubcomposition().accept(*this, data));
82
83 for (auto const& action : composition.getActionsToHide()) {
84 if (!program.hasAction(action)) {
85 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "System composition refers to unknown action '" << action << "'.");
86 } else {
87 uint_fast64_t index = program.getActionIndex(action);
88 auto it = subSynchronizingActionIndices.find(index);
89 STORM_LOG_THROW(it != subSynchronizingActionIndices.end(), storm::exceptions::WrongFormatException,
90 "Cannot hide action '" << action << "', because module '" << composition.getSubcomposition() << " does not have this action.");
91 subSynchronizingActionIndices.erase(it);
92 }
93 }
94
95 return subSynchronizingActionIndices;
96 }
97
98 virtual boost::any visit(SynchronizingParallelComposition const& composition, boost::any const& data) override {
99 std::set<uint_fast64_t> leftSynchronizingActionIndices =
100 boost::any_cast<std::set<uint_fast64_t>>(composition.getLeftSubcomposition().accept(*this, data));
101 std::set<uint_fast64_t> rightSynchronizingActionIndices =
102 boost::any_cast<std::set<uint_fast64_t>>(composition.getRightSubcomposition().accept(*this, data));
103
104 std::set<uint_fast64_t> synchronizingActionIndices;
105 std::set_union(leftSynchronizingActionIndices.begin(), leftSynchronizingActionIndices.end(), rightSynchronizingActionIndices.begin(),
106 rightSynchronizingActionIndices.end(), std::inserter(synchronizingActionIndices, synchronizingActionIndices.begin()));
107
108 return synchronizingActionIndices;
109 }
110
111 virtual boost::any visit(InterleavingParallelComposition const& composition, boost::any const& data) override {
112 std::set<uint_fast64_t> leftSynchronizingActionIndices =
113 boost::any_cast<std::set<uint_fast64_t>>(composition.getLeftSubcomposition().accept(*this, data));
114 std::set<uint_fast64_t> rightSynchronizingActionIndices =
115 boost::any_cast<std::set<uint_fast64_t>>(composition.getRightSubcomposition().accept(*this, data));
116
117 std::set<uint_fast64_t> synchronizingActionIndices;
118 std::set_union(leftSynchronizingActionIndices.begin(), leftSynchronizingActionIndices.end(), rightSynchronizingActionIndices.begin(),
119 rightSynchronizingActionIndices.end(), std::inserter(synchronizingActionIndices, synchronizingActionIndices.begin()));
120
121 return synchronizingActionIndices;
122 }
123
124 virtual boost::any visit(RestrictedParallelComposition const& composition, boost::any const& data) override {
125 std::set<uint_fast64_t> leftSynchronizingActionIndices =
126 boost::any_cast<std::set<uint_fast64_t>>(composition.getLeftSubcomposition().accept(*this, data));
127 std::set<uint_fast64_t> rightSynchronizingActionIndices =
128 boost::any_cast<std::set<uint_fast64_t>>(composition.getRightSubcomposition().accept(*this, data));
129
130 for (auto const& action : composition.getSynchronizingActions()) {
131 if (!program.hasAction(action)) {
132 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "System composition refers to unknown action '" << action << "'.");
133 } else {
134 uint_fast64_t index = program.getActionIndex(action);
135 auto it = leftSynchronizingActionIndices.find(index);
136 STORM_LOG_THROW(it != leftSynchronizingActionIndices.end(), storm::exceptions::WrongFormatException,
137 "Cannot synchronize on action '" << action << "', because module '" << composition.getLeftSubcomposition()
138 << " does not have this action.");
139 it = rightSynchronizingActionIndices.find(index);
140 STORM_LOG_THROW(it != rightSynchronizingActionIndices.end(), storm::exceptions::WrongFormatException,
141 "Cannot synchronize on action '" << action << "', because module '" << composition.getRightSubcomposition()
142 << " does not have this action.");
143 }
144 }
145
146 std::set<uint_fast64_t> synchronizingActionIndices;
147 std::set_union(leftSynchronizingActionIndices.begin(), leftSynchronizingActionIndices.end(), rightSynchronizingActionIndices.begin(),
148 rightSynchronizingActionIndices.end(), std::inserter(synchronizingActionIndices, synchronizingActionIndices.begin()));
149
150 return synchronizingActionIndices;
151 }
152
153 private:
154 storm::prism::Program const& program;
155 std::set<std::string> appearingModules;
156};
157
158Program::Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants,
159 std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables,
160 std::vector<Formula> const& formulas, std::vector<Player> const& players, std::vector<Module> const& modules,
161 std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, std::vector<Label> const& labels,
162 std::vector<ObservationLabel> const& observationLabels, boost::optional<InitialConstruct> const& initialConstruct,
163 boost::optional<SystemCompositionConstruct> const& compositionConstruct, bool prismCompatibility, std::string const& filename,
164 uint_fast64_t lineNumber, bool finalModel)
165 : LocatedInformation(filename, lineNumber),
166 manager(manager),
167 modelType(modelType),
168 constants(constants),
169 constantToIndexMap(),
170 globalBooleanVariables(globalBooleanVariables),
171 globalBooleanVariableToIndexMap(),
172 globalIntegerVariables(globalIntegerVariables),
173 globalIntegerVariableToIndexMap(),
174 formulas(formulas),
175 formulaToIndexMap(),
176 players(players),
177 modules(modules),
178 moduleToIndexMap(),
179 rewardModels(rewardModels),
180 rewardModelToIndexMap(),
181 systemCompositionConstruct(compositionConstruct),
182 labels(labels),
183 labelToIndexMap(),
184 observationLabels(observationLabels),
185 actionToIndexMap(actionToIndexMap),
186 indexToActionMap(),
187 actions(),
188 synchronizingActionIndices(),
189 actionIndicesToModuleIndexMap(),
190 variableToModuleIndexMap(),
191 possiblySynchronizingCommands(),
192 prismCompatibility(prismCompatibility) {
193 // Start by creating the necessary mappings from the given ones.
194 this->createMappings();
195
196 // Set the initial construct if given.
197 if (initialConstruct) {
198 this->initialConstruct = initialConstruct.get();
199 } else {
200 // Otherwise, we create the missing initial values.
201 this->createMissingInitialValues();
202 for (auto& modules : this->modules) {
203 modules.createMissingInitialValues();
204 }
205 }
206
207 uint64_t highestGlobalIndex = this->getHighestCommandIndex();
208 possiblySynchronizingCommands = storage::BitVector(highestGlobalIndex + 1);
209 std::set<uint64_t> possiblySynchronizingActionIndices;
210 for (uint64_t syncAction : synchronizingActionIndices) {
213 }
214 }
215 for (auto const& module : getModules()) {
216 for (auto const& command : module.getCommands()) {
217 if (command.isLabeled()) {
218 if (possiblySynchronizingActionIndices.count(command.getActionIndex()) > 0) {
219 possiblySynchronizingCommands.set(command.getGlobalIndex());
220 }
221 }
222 }
223 }
224
225 if (finalModel) {
226 // If the model is supposed to be a CTMC, but contains probabilistic commands, we transform them to Markovian
227 // commands and issue a warning.
228 if (modelType == storm::prism::Program::ModelType::CTMC && prismCompatibility) {
229 bool hasProbabilisticCommands = false;
230 for (auto& module : this->modules) {
231 for (auto& command : module.getCommands()) {
232 if (!command.isMarkovian()) {
233 command.setMarkovian(true);
234 hasProbabilisticCommands = true;
235 }
236 }
237 }
238 STORM_LOG_WARN_COND(!hasProbabilisticCommands,
239 "The input model is a CTMC, but uses probabilistic commands like they are used in PRISM. Consider rewriting the commands to "
240 "use Markovian commands instead.");
241 }
242 // Then check the validity.
243 this->checkValidity(Program::ValidityCheckLevel::VALIDINPUT);
244 }
245}
246
247Program::ModelType Program::getModelType() const {
248 return modelType;
249}
250
251bool Program::isDiscreteTimeModel() const {
252 return modelType == ModelType::DTMC || modelType == ModelType::MDP || modelType == ModelType::POMDP || modelType == ModelType::SMG;
253}
254
255bool Program::isDeterministicModel() const {
256 return modelType == ModelType::DTMC || modelType == ModelType::CTMC;
257}
258
259bool Program::isPartiallyObservable() const {
260 return modelType == ModelType::POMDP;
261}
262
263size_t Program::getNumberOfCommands() const {
264 size_t res = 0;
265 for (auto const& module : this->getModules()) {
266 res += module.getNumberOfCommands();
267 }
268 return res;
269}
270
271bool Program::hasUnboundedVariables() const {
272 for (auto const& globalIntegerVariable : this->globalIntegerVariables) {
273 if (!globalIntegerVariable.hasLowerBoundExpression() || !globalIntegerVariable.hasUpperBoundExpression()) {
274 return true;
275 }
276 }
277 for (auto const& module : modules) {
278 if (module.hasUnboundedVariables()) {
279 return true;
280 }
281 }
282 return false;
283}
284
285bool Program::hasUndefinedConstants() const {
286 for (auto const& constant : this->getConstants()) {
287 if (!constant.isDefined()) {
288 return true;
289 }
290 }
291 return false;
292}
293
294bool Program::undefinedConstantsAreGraphPreserving() const {
295 if (!this->hasUndefinedConstants()) {
296 return true;
297 }
298
299 // Gather the variables of all undefined constants.
300 std::set<storm::expressions::Variable> undefinedConstantVariables;
301 for (auto const& constant : this->getConstants()) {
302 if (!constant.isDefined()) {
303 undefinedConstantVariables.insert(constant.getExpressionVariable());
304 }
305 }
306
307 // Start by checking the defining expressions of all defined constants. If it contains a currently undefined
308 // constant, we need to mark the target constant as undefined as well.
309 for (auto const& constant : this->getConstants()) {
310 if (constant.isDefined()) {
311 if (constant.getExpression().containsVariable(undefinedConstantVariables)) {
312 undefinedConstantVariables.insert(constant.getExpressionVariable());
313 }
314 }
315 }
316
317 // Now check initial value and range expressions of global variables.
318 for (auto const& booleanVariable : this->getGlobalBooleanVariables()) {
319 if (booleanVariable.hasInitialValue()) {
320 if (booleanVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
321 return false;
322 }
323 }
324 }
325 for (auto const& integerVariable : this->getGlobalIntegerVariables()) {
326 if (integerVariable.hasInitialValue()) {
327 if (integerVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
328 return false;
329 }
330 }
331 if (integerVariable.hasLowerBoundExpression() && integerVariable.getLowerBoundExpression().containsVariable(undefinedConstantVariables)) {
332 return false;
333 }
334 if (integerVariable.hasUpperBoundExpression() && integerVariable.getUpperBoundExpression().containsVariable(undefinedConstantVariables)) {
335 return false;
336 }
337 }
338
339 // Proceed by checking each of the modules.
340 for (auto const& module : this->getModules()) {
341 if (!module.containsVariablesOnlyInUpdateProbabilities(undefinedConstantVariables)) {
342 return false;
343 }
344 }
345
346 // Check the reward models.
347 for (auto const& rewardModel : this->getRewardModels()) {
348 rewardModel.containsVariablesOnlyInRewardValueExpressions(undefinedConstantVariables);
349 }
350
351 // Initial construct.
352 if (this->hasInitialConstruct()) {
353 if (this->getInitialConstruct().getInitialStatesExpression().containsVariable(undefinedConstantVariables)) {
354 return false;
355 }
356 }
357
358 // Labels.
359 for (auto const& label : this->getLabels()) {
360 if (label.getStatePredicateExpression().containsVariable(undefinedConstantVariables)) {
361 return false;
362 }
363 }
364
365 return true;
366}
367
368std::vector<std::reference_wrapper<storm::prism::Constant const>> Program::getUndefinedConstants() const {
369 std::vector<std::reference_wrapper<storm::prism::Constant const>> result;
370 for (auto const& constant : this->getConstants()) {
371 if (!constant.isDefined()) {
372 result.push_back(constant);
373 }
374 }
375 return result;
376}
377
378std::string Program::getUndefinedConstantsAsString() const {
379 std::stringstream stream;
380 bool printComma = false;
381 for (auto const& constant : getUndefinedConstants()) {
382 if (printComma) {
383 stream << ", ";
384 } else {
385 printComma = true;
386 }
387 stream << constant.get().getName() << " (" << constant.get().getType() << ")";
388 }
389 stream << ".";
390 return stream.str();
391}
392
393bool Program::hasConstant(std::string const& constantName) const {
394 return this->constantToIndexMap.find(constantName) != this->constantToIndexMap.end();
395}
396
397Constant const& Program::getConstant(std::string const& constantName) const {
398 auto const& constantIndexPair = this->constantToIndexMap.find(constantName);
399 return this->getConstants()[constantIndexPair->second];
400}
401
402std::vector<Constant> const& Program::getConstants() const {
403 return this->constants;
404}
405
406std::map<storm::expressions::Variable, storm::expressions::Expression> Program::getConstantsSubstitution() const {
407 return getConstantsFormulasSubstitution(true, false);
408}
409
410std::map<storm::expressions::Variable, storm::expressions::Expression> Program::getFormulasSubstitution() const {
411 return getConstantsFormulasSubstitution(false, true);
412}
413
414std::map<storm::expressions::Variable, storm::expressions::Expression> Program::getConstantsFormulasSubstitution(bool getConstantsSubstitution,
415 bool getFormulasSubstitution) const {
416 std::map<storm::expressions::Variable, storm::expressions::Expression> result;
417 if (getConstantsSubstitution) {
418 for (auto const& constant : this->getConstants()) {
419 if (constant.isDefined()) {
420 result.emplace(constant.getExpressionVariable(), constant.getExpression().substitute(result));
421 }
422 }
423 }
424 if (getFormulasSubstitution) {
425 for (auto const& formula : this->getFormulas()) {
426 result.emplace(formula.getExpressionVariable(), formula.getExpression().substitute(result));
427 }
428 }
429 return result;
430}
431
432std::map<storm::expressions::Variable, storm::expressions::Expression> Program::getSubstitutionForRenamedModule(
433 Module const& renamedModule, std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
434 auto renaming = getFinalRenamingOfModule(renamedModule);
435 std::map<storm::expressions::Variable, storm::expressions::Expression> renamingAsSubstitution;
436 for (auto const& renamingPair : renaming) {
437 if (getManager().hasVariable(renamingPair.first)) {
438 assert(getManager().hasVariable(renamingPair.second));
439 renamingAsSubstitution.emplace(getManager().getVariable(renamingPair.first), getManager().getVariableExpression(renamingPair.second));
440 }
441 }
442
443 std::map<storm::expressions::Variable, storm::expressions::Expression> newSubstitution;
444 for (auto const& substVarExpr : substitution) {
445 newSubstitution.emplace(substVarExpr.first, storm::jani::substituteJaniExpression(substVarExpr.second, renamingAsSubstitution, false));
446 }
447 return newSubstitution;
448}
449
450std::map<std::string, std::string> Program::getFinalRenamingOfModule(Module const& renamedModule) const {
451 std::vector<Module const*> moduleStack = {&renamedModule};
452 while (moduleStack.back()->isRenamedFromModule()) {
453 moduleStack.push_back(&getModule(moduleStack.back()->getBaseModule()));
454 }
455
456 assert(!moduleStack.back()->isRenamedFromModule());
457 moduleStack.pop_back();
458 assert(moduleStack.empty() || moduleStack.back()->isRenamedFromModule());
459 std::map<std::string, std::string> currentRenaming;
460 while (!moduleStack.empty()) {
461 Module const& currentModule = *moduleStack.back();
462 moduleStack.pop_back();
463 assert(currentModule.isRenamedFromModule());
464 std::map<std::string, std::string> newRenaming = currentModule.getRenaming();
465 for (auto const& renaimingPair : newRenaming) {
466 auto findRes = currentRenaming.find(renaimingPair.second);
467 if (findRes != currentRenaming.end()) {
468 newRenaming[renaimingPair.second] = findRes->second;
469 currentRenaming.erase(findRes);
470 }
471 }
472 newRenaming.insert(currentRenaming.begin(), currentRenaming.end());
473 currentRenaming = std::move(newRenaming);
474 }
475 return currentRenaming;
476}
477
478std::size_t Program::getNumberOfConstants() const {
479 return this->getConstants().size();
480}
481
482std::vector<BooleanVariable> const& Program::getGlobalBooleanVariables() const {
483 return this->globalBooleanVariables;
484}
485
486std::vector<IntegerVariable> const& Program::getGlobalIntegerVariables() const {
487 return this->globalIntegerVariables;
488}
489
490std::set<storm::expressions::Variable> Program::getAllExpressionVariables(bool includeConstants) const {
491 std::set<storm::expressions::Variable> result;
492
493 if (includeConstants) {
494 for (auto const& constant : constants) {
495 result.insert(constant.getExpressionVariable());
496 }
497 }
498 for (auto const& variable : globalBooleanVariables) {
499 result.insert(variable.getExpressionVariable());
500 }
501 for (auto const& variable : globalIntegerVariables) {
502 result.insert(variable.getExpressionVariable());
503 }
504 for (auto const& module : modules) {
505 auto const& moduleVariables = module.getAllExpressionVariables();
506 result.insert(moduleVariables.begin(), moduleVariables.end());
507 }
508
509 return result;
510}
511
512std::vector<storm::expressions::Expression> Program::getAllRangeExpressions() const {
513 std::vector<storm::expressions::Expression> result;
514 for (auto const& globalIntegerVariable : this->globalIntegerVariables) {
515 if (globalIntegerVariable.hasLowerBoundExpression() || globalIntegerVariable.hasUpperBoundExpression()) {
516 result.push_back(globalIntegerVariable.getRangeExpression());
517 }
518 }
519
520 for (auto const& module : modules) {
521 std::vector<storm::expressions::Expression> moduleRangeExpressions = module.getAllRangeExpressions();
522 result.insert(result.end(), moduleRangeExpressions.begin(), moduleRangeExpressions.end());
523 }
524
525 return result;
526}
527
528bool Program::globalBooleanVariableExists(std::string const& variableName) const {
529 return this->globalBooleanVariableToIndexMap.count(variableName) > 0;
530}
531
532bool Program::globalIntegerVariableExists(std::string const& variableName) const {
533 return this->globalIntegerVariableToIndexMap.count(variableName) > 0;
534}
535
536BooleanVariable const& Program::getGlobalBooleanVariable(std::string const& variableName) const {
537 auto const& nameIndexPair = this->globalBooleanVariableToIndexMap.find(variableName);
538 STORM_LOG_THROW(nameIndexPair != this->globalBooleanVariableToIndexMap.end(), storm::exceptions::OutOfRangeException,
539 "Unknown boolean variable '" << variableName << "'.");
540 return this->getGlobalBooleanVariables()[nameIndexPair->second];
541}
542
543IntegerVariable const& Program::getGlobalIntegerVariable(std::string const& variableName) const {
544 auto const& nameIndexPair = this->globalIntegerVariableToIndexMap.find(variableName);
545 STORM_LOG_THROW(nameIndexPair != this->globalIntegerVariableToIndexMap.end(), storm::exceptions::OutOfRangeException,
546 "Unknown integer variable '" << variableName << "'.");
547 return this->getGlobalIntegerVariables()[nameIndexPair->second];
548}
549
550std::size_t Program::getNumberOfGlobalBooleanVariables() const {
551 return this->getGlobalBooleanVariables().size();
552}
553
554std::size_t Program::getNumberOfGlobalIntegerVariables() const {
555 return this->getGlobalIntegerVariables().size();
556}
557
558std::vector<Formula> const& Program::getFormulas() const {
559 return this->formulas;
560}
561
562std::vector<Player> const& Program::getPlayers() const {
563 return this->players;
564}
565
566std::size_t Program::getNumberOfPlayers() const {
567 return this->getPlayers().size();
568}
569
570storm::storage::PlayerIndex const& Program::getIndexOfPlayer(std::string const& playerName) const {
571 return this->playerToIndexMap.at(playerName);
572}
573
574std::map<std::string, storm::storage::PlayerIndex> const& Program::getPlayerNameToIndexMapping() const {
575 return playerToIndexMap;
576}
577
578std::vector<storm::storage::PlayerIndex> Program::buildModuleIndexToPlayerIndexMap() const {
579 std::vector<storm::storage::PlayerIndex> result(this->getModules().size(), storm::storage::INVALID_PLAYER_INDEX);
580 for (storm::storage::PlayerIndex i = 0; i < this->getPlayers().size(); ++i) {
581 for (auto const& module : this->getPlayers()[i].getModules()) {
582 STORM_LOG_ASSERT(hasModule(module), "Module " << module << " not found.");
583 STORM_LOG_ASSERT(moduleToIndexMap.at(module) < this->getModules().size(), "module index " << moduleToIndexMap.at(module) << " out of range.");
584 result[moduleToIndexMap.at(module)] = i;
585 }
586 }
587 return result;
588}
589
590std::map<uint64_t, storm::storage::PlayerIndex> Program::buildActionIndexToPlayerIndexMap() const {
591 std::map<uint64_t, storm::storage::PlayerIndex> result;
592 // First insert an invalid player index for all available actions
593 for (auto const& action : indexToActionMap) {
594 result.emplace_hint(result.end(), action.first, storm::storage::INVALID_PLAYER_INDEX);
595 }
596 // Now set the actual player indices.
597 // Note that actions that are not assigned to a player will still have INVALID_PLAYER_INDEX afterwards
598 for (storm::storage::PlayerIndex i = 0; i < this->getPlayers().size(); ++i) {
599 for (auto const& act : this->getPlayers()[i].getActions()) {
600 STORM_LOG_ASSERT(hasAction(act), "Action " << act << " not found.");
601 result[actionToIndexMap.at(act)] = i;
602 }
603 }
604 return result;
605}
606
607std::size_t Program::getNumberOfFormulas() const {
608 return this->getFormulas().size();
609}
610
611std::size_t Program::getNumberOfModules() const {
612 return this->getModules().size();
613}
614
615storm::prism::Module const& Program::getModule(uint_fast64_t index) const {
616 return this->modules[index];
617}
618
619bool Program::hasModule(std::string const& moduleName) const {
620 return this->moduleToIndexMap.find(moduleName) != this->moduleToIndexMap.end();
621}
622
623Module const& Program::getModule(std::string const& moduleName) const {
624 auto const& nameIndexPair = this->moduleToIndexMap.find(moduleName);
625 STORM_LOG_THROW(nameIndexPair != this->moduleToIndexMap.end(), storm::exceptions::OutOfRangeException, "Unknown module '" << moduleName << "'.");
626 return this->getModules()[nameIndexPair->second];
627}
628
629std::vector<storm::prism::Module> const& Program::getModules() const {
630 return this->modules;
631}
632
633std::map<std::string, uint_fast64_t> const& Program::getActionNameToIndexMapping() const {
634 return actionToIndexMap;
635}
636
637uint64_t Program::getNumberOfUnlabeledCommands() const {
638 uint64_t result = 0;
639 for (auto const& m : modules) {
640 result += m.getNumberOfUnlabeledCommands();
641 }
642 return result;
643}
644
645bool Program::hasInitialConstruct() const {
646 return static_cast<bool>(initialConstruct);
647}
648
649storm::prism::InitialConstruct const& Program::getInitialConstruct() const {
650 return this->initialConstruct.get();
651}
652
653boost::optional<InitialConstruct> const& Program::getOptionalInitialConstruct() const {
654 return this->initialConstruct;
655}
656
657void Program::updateInitialStatesExpression(expressions::Expression const& newExpression) {
658 STORM_LOG_THROW(hasInitialConstruct(), exceptions::InvalidOperationException, "We can only update the initial construct, if it already exists.");
659 this->initialConstruct = boost::make_optional(InitialConstruct(newExpression));
660}
661
662storm::expressions::Expression Program::getInitialStatesExpression() const {
663 // If there is an initial construct, return its expression. If not, we construct the expression from the
664 // initial values of the variables (which have to exist).
665 if (this->hasInitialConstruct()) {
666 return this->getInitialConstruct().getInitialStatesExpression();
667 } else {
669
670 for (auto const& variable : this->getGlobalBooleanVariables()) {
671 if (result.isInitialized()) {
672 result = result && storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression());
673 } else {
674 result = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression());
675 }
676 }
677 for (auto const& variable : this->getGlobalIntegerVariables()) {
678 if (result.isInitialized()) {
679 result = result && variable.getExpressionVariable() == variable.getInitialValueExpression();
680 } else {
681 result = variable.getExpressionVariable() == variable.getInitialValueExpression();
682 }
683 }
684 for (auto const& module : this->getModules()) {
685 for (auto const& variable : module.getBooleanVariables()) {
686 if (result.isInitialized()) {
687 result = result && storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression());
688 } else {
689 result = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression());
690 }
691 }
692 for (auto const& variable : module.getIntegerVariables()) {
693 if (result.isInitialized()) {
694 result = result && variable.getExpressionVariable() == variable.getInitialValueExpression();
695 } else {
696 result = variable.getExpressionVariable() == variable.getInitialValueExpression();
697 }
698 }
699 }
700
701 // If there are no variables, there is no restriction on the initial states.
702 if (!result.isInitialized()) {
703 result = manager->boolean(true);
704 }
705
706 return result;
707 }
708}
709
710bool Program::specifiesSystemComposition() const {
711 return static_cast<bool>(systemCompositionConstruct);
712}
713
714SystemCompositionConstruct const& Program::getSystemCompositionConstruct() const {
715 return systemCompositionConstruct.get();
716}
717
718boost::optional<SystemCompositionConstruct> Program::getOptionalSystemCompositionConstruct() const {
719 return systemCompositionConstruct;
720}
721
722std::shared_ptr<Composition> Program::getDefaultSystemComposition() const {
723 std::shared_ptr<Composition> current = std::make_shared<ModuleComposition>(this->modules.front().getName());
724
725 for (uint_fast64_t index = 1; index < this->modules.size(); ++index) {
726 std::shared_ptr<Composition> newComposition =
727 std::make_shared<SynchronizingParallelComposition>(current, std::make_shared<ModuleComposition>(this->modules[index].getName()));
728 current = newComposition;
729 }
730
731 return current;
732}
733
734std::set<std::string> const& Program::getActions() const {
735 return this->actions;
736}
737
738std::set<uint_fast64_t> const& Program::getSynchronizingActionIndices() const {
739 return this->synchronizingActionIndices;
740}
741
742std::string const& Program::getActionName(uint_fast64_t actionIndex) const {
743 auto const& indexNamePair = this->indexToActionMap.find(actionIndex);
744 STORM_LOG_THROW(indexNamePair != this->indexToActionMap.end(), storm::exceptions::InvalidArgumentException, "Unknown action index " << actionIndex << ".");
745 return indexNamePair->second;
746}
747
748uint_fast64_t Program::getActionIndex(std::string const& actionName) const {
749 auto const& nameIndexPair = this->actionToIndexMap.find(actionName);
750 STORM_LOG_THROW(nameIndexPair != this->actionToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Unknown action name '" << actionName << "'.");
751 return nameIndexPair->second;
752}
753
754bool Program::hasAction(std::string const& actionName) const {
755 return this->actionToIndexMap.find(actionName) != this->actionToIndexMap.end();
756}
757
758bool Program::hasAction(uint_fast64_t const& actionIndex) const {
759 return this->indexToActionMap.find(actionIndex) != this->indexToActionMap.end();
760}
761
762std::set<uint_fast64_t> const& Program::getModuleIndicesByAction(std::string const& action) const {
763 auto const& nameIndexPair = this->actionToIndexMap.find(action);
764 STORM_LOG_THROW(nameIndexPair != this->actionToIndexMap.end(), storm::exceptions::OutOfRangeException, "Action name '" << action << "' does not exist.");
765 return this->getModuleIndicesByActionIndex(nameIndexPair->second);
766}
767
768std::set<uint_fast64_t> const& Program::getModuleIndicesByActionIndex(uint_fast64_t actionIndex) const {
769 auto const& actionModuleSetPair = this->actionIndicesToModuleIndexMap.find(actionIndex);
770 STORM_LOG_THROW(actionModuleSetPair != this->actionIndicesToModuleIndexMap.end(), storm::exceptions::OutOfRangeException,
771 "Action with index '" << actionIndex << "' does not exist.");
772 return actionModuleSetPair->second;
773}
774
775uint_fast64_t Program::getModuleIndexByVariable(std::string const& variableName) const {
776 auto const& variableNameToModuleIndexPair = this->variableToModuleIndexMap.find(variableName);
777 STORM_LOG_THROW(variableNameToModuleIndexPair != this->variableToModuleIndexMap.end(), storm::exceptions::OutOfRangeException,
778 "Variable '" << variableName << "' does not exist.");
779 return variableNameToModuleIndexPair->second;
780}
781
782std::pair<uint_fast64_t, uint_fast64_t> Program::getModuleCommandIndexByGlobalCommandIndex(uint_fast64_t globalCommandIndex) const {
783 uint_fast64_t moduleIndex = 0;
784 for (auto const& module : modules) {
785 uint_fast64_t commandIndex = 0;
786 for (auto const& command : module.getCommands()) {
787 if (command.getGlobalIndex() == globalCommandIndex) {
788 return std::pair<uint_fast64_t, uint_fast64_t>(moduleIndex, commandIndex);
789 }
790 ++commandIndex;
791 }
792 ++moduleIndex;
793 }
794 // This point should not be reached if the globalCommandIndex is valid
795 STORM_LOG_THROW(false, storm::exceptions::OutOfRangeException, "Global command index '" << globalCommandIndex << "' does not exist.");
796 return std::pair<uint_fast64_t, uint_fast64_t>(0, 0);
797}
798
799bool Program::hasRewardModel() const {
800 return !this->rewardModels.empty();
801}
802
803bool Program::hasRewardModel(std::string const& name) const {
804 auto const& nameIndexPair = this->rewardModelToIndexMap.find(name);
805 return nameIndexPair != this->rewardModelToIndexMap.end();
806}
807
808std::vector<storm::prism::RewardModel> const& Program::getRewardModels() const {
809 return this->rewardModels;
810}
811
812std::size_t Program::getNumberOfRewardModels() const {
813 return this->getRewardModels().size();
814}
815
816storm::prism::RewardModel const& Program::getRewardModel(std::string const& name) const {
817 auto const& nameIndexPair = this->rewardModelToIndexMap.find(name);
818 STORM_LOG_THROW(nameIndexPair != this->rewardModelToIndexMap.end(), storm::exceptions::OutOfRangeException,
819 "Reward model '" << name << "' does not exist.");
820 return this->getRewardModels()[nameIndexPair->second];
821}
822
823RewardModel const& Program::getRewardModel(uint_fast64_t index) const {
824 STORM_LOG_THROW(this->getNumberOfRewardModels() > index, storm::exceptions::OutOfRangeException, "Reward model with index " << index << " does not exist.");
825 return this->rewardModels[index];
826}
827
828bool Program::hasLabel(std::string const& labelName) const {
829 auto it = std::find_if(labels.begin(), labels.end(), [&labelName](storm::prism::Label const& label) { return label.getName() == labelName; });
830 return it != labels.end();
831}
832
833std::vector<Label> const& Program::getLabels() const {
834 return this->labels;
835}
836
837std::vector<storm::expressions::Expression> Program::getAllGuards(bool negated) const {
838 std::vector<storm::expressions::Expression> allGuards;
839 for (auto const& module : modules) {
840 for (auto const& command : module.getCommands()) {
841 allGuards.push_back(negated ? !command.getGuardExpression() : command.getGuardExpression());
842 }
843 }
844 return allGuards;
845}
846
847storm::expressions::Expression const& Program::getLabelExpression(std::string const& label) const {
848 auto const& labelIndexPair = labelToIndexMap.find(label);
849 STORM_LOG_THROW(labelIndexPair != labelToIndexMap.end(), storm::exceptions::InvalidArgumentException,
850 "Cannot retrieve expression for unknown label '" << label << "'.");
851 return this->labels[labelIndexPair->second].getStatePredicateExpression();
852}
853
854std::map<std::string, storm::expressions::Expression> Program::getLabelToExpressionMapping() const {
855 std::map<std::string, storm::expressions::Expression> result;
856 for (auto const& label : labels) {
857 result.emplace(label.getName(), label.getStatePredicateExpression());
858 }
859 return result;
860}
861
862std::size_t Program::getNumberOfLabels() const {
863 return this->getLabels().size();
864}
865
866void Program::addLabel(std::string const& name, storm::expressions::Expression const& statePredicateExpression) {
867 auto it = std::find_if(this->labels.begin(), this->labels.end(), [&name](storm::prism::Label const& label) { return label.getName() == name; });
868 STORM_LOG_THROW(it == this->labels.end(), storm::exceptions::InvalidArgumentException,
869 "Cannot add a label '" << name << "', because a label with that name already exists.");
870 this->labels.emplace_back(name, statePredicateExpression);
871}
872
873void Program::removeLabel(std::string const& name) {
874 auto it = std::find_if(this->labels.begin(), this->labels.end(), [&name](storm::prism::Label const& label) { return label.getName() == name; });
875 STORM_LOG_THROW(it != this->labels.end(), storm::exceptions::InvalidArgumentException, "Canno remove unknown label '" << name << "'.");
876 this->labels.erase(it);
877}
878
879void Program::removeRewardModels() {
880 this->rewardModels.clear();
881 this->rewardModelToIndexMap.clear();
882}
883
884void Program::filterLabels(std::set<std::string> const& labelSet) {
885 std::vector<storm::prism::Label> newLabels;
886 newLabels.reserve(labelSet.size());
887
888 // Now filter the labels by the criterion whether or not their name appears in the given label set.
889 for (auto it = labels.begin(), ite = labels.end(); it != ite; ++it) {
890 auto setIt = labelSet.find(it->getName());
891 if (setIt != labelSet.end()) {
892 newLabels.emplace_back(*it);
893 }
894 }
895
896 // Move the new labels in place.
897 this->labels = std::move(newLabels);
898}
899
900std::vector<ObservationLabel> const& Program::getObservationLabels() const {
901 return this->observationLabels;
902}
903
904std::size_t Program::getNumberOfObservationLabels() const {
905 return this->observationLabels.size();
906}
907
908storm::storage::BitVector const& Program::getPossiblySynchronizingCommands() const {
909 return possiblySynchronizingCommands;
910}
911
912Program Program::restrictCommands(storm::storage::FlatSet<uint_fast64_t> const& indexSet) const {
913 std::vector<storm::prism::Module> newModules;
914 newModules.reserve(this->getNumberOfModules());
915
916 for (auto const& module : this->getModules()) {
917 newModules.push_back(module.restrictCommands(indexSet));
918 }
919
920 return Program(this->manager, this->getModelType(), this->getConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(),
921 this->getFormulas(), this->getPlayers(), newModules, this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(),
922 this->getObservationLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
923}
924
925void Program::createMappings() {
926 // Build the mappings for constants, global variables, formulas, modules, reward models and labels.
927 for (uint_fast64_t constantIndex = 0; constantIndex < this->getNumberOfConstants(); ++constantIndex) {
928 this->constantToIndexMap[this->getConstants()[constantIndex].getName()] = constantIndex;
929 }
930 for (uint_fast64_t globalVariableIndex = 0; globalVariableIndex < this->getNumberOfGlobalBooleanVariables(); ++globalVariableIndex) {
931 this->globalBooleanVariableToIndexMap[this->getGlobalBooleanVariables()[globalVariableIndex].getName()] = globalVariableIndex;
932 }
933 for (uint_fast64_t globalVariableIndex = 0; globalVariableIndex < this->getNumberOfGlobalIntegerVariables(); ++globalVariableIndex) {
934 this->globalIntegerVariableToIndexMap[this->getGlobalIntegerVariables()[globalVariableIndex].getName()] = globalVariableIndex;
935 }
936 for (uint_fast64_t formulaIndex = 0; formulaIndex < this->getNumberOfFormulas(); ++formulaIndex) {
937 this->formulaToIndexMap[this->getFormulas()[formulaIndex].getName()] = formulaIndex;
938 }
939 for (uint_fast64_t labelIndex = 0; labelIndex < this->getNumberOfLabels(); ++labelIndex) {
940 this->labelToIndexMap[this->getLabels()[labelIndex].getName()] = labelIndex;
941 }
942 for (uint_fast64_t moduleIndex = 0; moduleIndex < this->getNumberOfModules(); ++moduleIndex) {
943 this->moduleToIndexMap[this->getModules()[moduleIndex].getName()] = moduleIndex;
944 }
945 for (storm::storage::PlayerIndex playerIndex = 0; playerIndex < this->getNumberOfPlayers(); ++playerIndex) {
946 this->playerToIndexMap[this->getPlayers()[playerIndex].getName()] = playerIndex;
947 }
948 for (uint_fast64_t rewardModelIndex = 0; rewardModelIndex < this->getNumberOfRewardModels(); ++rewardModelIndex) {
949 this->rewardModelToIndexMap[this->getRewardModels()[rewardModelIndex].getName()] = rewardModelIndex;
950 }
951
952 for (auto const& actionIndexPair : this->getActionNameToIndexMapping()) {
953 this->actions.insert(actionIndexPair.first);
954 this->indexToActionMap.emplace(actionIndexPair.second, actionIndexPair.first);
955
956 // Only let all non-zero indices be synchronizing.
957 if (actionIndexPair.second != 0) {
958 this->synchronizingActionIndices.insert(actionIndexPair.second);
959 this->actionIndicesToModuleIndexMap[actionIndexPair.second] = std::set<uint_fast64_t>();
960 }
961 }
962
963 // Build the mapping from action names to module indices so that the lookup can later be performed quickly.
964 for (unsigned int moduleIndex = 0; moduleIndex < this->getNumberOfModules(); moduleIndex++) {
965 Module const& module = this->getModule(moduleIndex);
966
967 for (auto const& actionIndex : module.getSynchronizingActionIndices()) {
968 this->actionIndicesToModuleIndexMap[actionIndex].insert(moduleIndex);
969 }
970
971 // Put in the appropriate entries for the mapping from variable names to module index.
972 for (auto const& booleanVariable : module.getBooleanVariables()) {
973 this->variableToModuleIndexMap[booleanVariable.getName()] = moduleIndex;
974 }
975 for (auto const& integerVariable : module.getIntegerVariables()) {
976 this->variableToModuleIndexMap[integerVariable.getName()] = moduleIndex;
977 }
978 for (auto const& clockVariable : module.getClockVariables()) {
979 this->variableToModuleIndexMap[clockVariable.getName()] = moduleIndex;
980 }
981 }
982}
983
984Program Program::defineUndefinedConstants(std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) const {
985 // For sanity checking, we keep track of all undefined constants that we define in the course of this procedure.
986 std::set<storm::expressions::Variable> definedUndefinedConstants;
987
988 std::vector<Constant> newConstants;
989 newConstants.reserve(this->getNumberOfConstants());
990 for (auto const& constant : this->getConstants()) {
991 // If the constant is already defined, we need to replace the appearances of undefined constants in its
992 // defining expression
993 if (constant.isDefined()) {
994 // Make sure we are not trying to define an already defined constant.
995 STORM_LOG_THROW(constantDefinitions.find(constant.getExpressionVariable()) == constantDefinitions.end(),
996 storm::exceptions::InvalidArgumentException, "Illegally defining already defined constant '" << constant.getName() << "'.");
997
998 // Now replace the occurrences of undefined constants in its defining expression.
999 newConstants.emplace_back(constant.getExpressionVariable(), constant.getExpression().substitute(constantDefinitions), constant.getFilename(),
1000 constant.getLineNumber());
1001 } else {
1002 auto const& variableExpressionPair = constantDefinitions.find(constant.getExpressionVariable());
1003
1004 // If the constant is not defined by the mapping, we leave it like it is.
1005 if (variableExpressionPair == constantDefinitions.end()) {
1006 newConstants.emplace_back(constant);
1007 } else {
1008 // Otherwise, we add it to the defined constants and assign it the appropriate expression.
1009 definedUndefinedConstants.insert(constant.getExpressionVariable());
1010
1011 // Make sure the type of the constant is correct.
1012 STORM_LOG_THROW(variableExpressionPair->second.getType() == constant.getType(), storm::exceptions::InvalidArgumentException,
1013 "Illegal type of expression defining constant '" << constant.getName() << "'.");
1014
1015 // Now create the defined constant.
1016 newConstants.emplace_back(constant.getExpressionVariable(), variableExpressionPair->second, constant.getFilename(), constant.getLineNumber());
1017 }
1018 }
1019 }
1020
1021 return Program(this->manager, this->getModelType(), newConstants, this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(),
1022 this->getPlayers(), this->getModules(), this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(),
1023 this->getObservationLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
1024}
1025
1026Program Program::substituteConstants() const {
1027 return substituteConstantsFormulas(true, false);
1028}
1029
1030Program Program::substituteFormulas() const {
1031 return substituteConstantsFormulas(false, true);
1032}
1033
1034Program Program::substituteNonStandardPredicates() const {
1035 // TODO support in constants, initial construct, and rewards
1036
1037 std::vector<Formula> newFormulas;
1038 newFormulas.reserve(this->getNumberOfFormulas());
1039 for (auto const& oldFormula : this->getFormulas()) {
1040 newFormulas.emplace_back(oldFormula.substituteNonStandardPredicates());
1041 }
1042
1043 std::vector<BooleanVariable> newBooleanVariables;
1044 newBooleanVariables.reserve(this->getNumberOfGlobalBooleanVariables());
1045 for (auto const& booleanVariable : this->getGlobalBooleanVariables()) {
1046 newBooleanVariables.emplace_back(booleanVariable.substituteNonStandardPredicates());
1047 }
1048
1049 std::vector<IntegerVariable> newIntegerVariables;
1050 newBooleanVariables.reserve(this->getNumberOfGlobalIntegerVariables());
1051 for (auto const& integerVariable : this->getGlobalIntegerVariables()) {
1052 newIntegerVariables.emplace_back(integerVariable.substituteNonStandardPredicates());
1053 }
1054
1055 std::vector<Module> newModules;
1056 newModules.reserve(this->getNumberOfModules());
1057 for (auto const& module : this->getModules()) {
1058 newModules.emplace_back(module.substituteNonStandardPredicates());
1059 }
1060
1061 std::vector<Label> newLabels;
1062 newLabels.reserve(this->getNumberOfLabels());
1063 for (auto const& label : this->getLabels()) {
1064 newLabels.emplace_back(label.substituteNonStandardPredicates());
1065 }
1066
1067 std::vector<ObservationLabel> newObservationLabels;
1068 newObservationLabels.reserve(this->getNumberOfObservationLabels());
1069 for (auto const& label : this->getObservationLabels()) {
1070 newObservationLabels.emplace_back(label.substituteNonStandardPredicates());
1071 }
1072
1073 return Program(this->manager, this->getModelType(), this->getConstants(), newBooleanVariables, newIntegerVariables, newFormulas, this->getPlayers(),
1074 newModules, this->getActionNameToIndexMapping(), this->getRewardModels(), newLabels, newObservationLabels, initialConstruct,
1075 this->getOptionalSystemCompositionConstruct(), prismCompatibility);
1076}
1077
1078Program Program::substituteConstantsFormulas(bool substituteConstants, bool substituteFormulas) const {
1079 // Formulas need to be substituted first. otherwise, constants appearing in formula expressions can not be handled properly
1080 if (substituteConstants && substituteFormulas) {
1081 return this->substituteFormulas().substituteConstants();
1082 }
1083
1084 // We start by creating the appropriate substitution.
1085 std::map<storm::expressions::Variable, storm::expressions::Expression> substitution =
1086 getConstantsFormulasSubstitution(substituteConstants, substituteFormulas);
1087
1088 std::vector<Constant> newConstants;
1089 newConstants.reserve(this->getNumberOfConstants());
1090 for (auto const& oldConstant : this->getConstants()) {
1091 newConstants.push_back(oldConstant.substitute(substitution));
1092 }
1093
1094 std::vector<Formula> newFormulas;
1095 newFormulas.reserve(this->getNumberOfFormulas());
1096 for (auto const& oldFormula : this->getFormulas()) {
1097 newFormulas.emplace_back(oldFormula.substitute(substitution));
1098 }
1099
1100 std::vector<BooleanVariable> newBooleanVariables;
1101 newBooleanVariables.reserve(this->getNumberOfGlobalBooleanVariables());
1102 for (auto const& booleanVariable : this->getGlobalBooleanVariables()) {
1103 newBooleanVariables.emplace_back(booleanVariable.substitute(substitution));
1104 }
1105
1106 std::vector<IntegerVariable> newIntegerVariables;
1107 newBooleanVariables.reserve(this->getNumberOfGlobalIntegerVariables());
1108 for (auto const& integerVariable : this->getGlobalIntegerVariables()) {
1109 newIntegerVariables.emplace_back(integerVariable.substitute(substitution));
1110 }
1111
1112 std::vector<Module> newModules;
1113 newModules.reserve(this->getNumberOfModules());
1114 for (auto const& module : this->getModules()) {
1115 if (module.isRenamedFromModule()) {
1116 // The renaming needs to be applied to the substitution as well.
1117 auto renamedSubstitution = getSubstitutionForRenamedModule(module, substitution);
1118 newModules.emplace_back(module.substitute(renamedSubstitution));
1119 } else {
1120 newModules.emplace_back(module.substitute(substitution));
1121 }
1122 }
1123
1124 std::vector<RewardModel> newRewardModels;
1125 newRewardModels.reserve(this->getNumberOfRewardModels());
1126 for (auto const& rewardModel : this->getRewardModels()) {
1127 newRewardModels.emplace_back(rewardModel.substitute(substitution));
1128 }
1129
1130 boost::optional<storm::prism::InitialConstruct> newInitialConstruct;
1131 if (this->hasInitialConstruct()) {
1132 newInitialConstruct = this->getInitialConstruct().substitute(substitution);
1133 }
1134
1135 std::vector<Label> newLabels;
1136 newLabels.reserve(this->getNumberOfLabels());
1137 for (auto const& label : this->getLabels()) {
1138 newLabels.emplace_back(label.substitute(substitution));
1139 }
1140
1141 std::vector<ObservationLabel> newObservationLabels;
1142 newObservationLabels.reserve(this->getNumberOfObservationLabels());
1143 for (auto const& label : this->getObservationLabels()) {
1144 newObservationLabels.emplace_back(label.substitute(substitution));
1145 }
1146
1147 return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, this->getPlayers(), newModules,
1148 this->getActionNameToIndexMapping(), newRewardModels, newLabels, newObservationLabels, newInitialConstruct,
1149 this->getOptionalSystemCompositionConstruct(), prismCompatibility);
1150}
1151
1152Program Program::labelUnlabelledCommands(std::map<uint64_t, std::string> const& nameSuggestions) const {
1153 for (auto const& entry : nameSuggestions) {
1154 STORM_LOG_THROW(!hasAction(entry.second), storm::exceptions::InvalidArgumentException, "Cannot suggest names already in the program.");
1155 }
1156 std::vector<Module> newModules;
1157 std::vector<RewardModel> newRewardModels;
1158 std::map<std::string, uint64_t> newActionNameToIndexMapping = getActionNameToIndexMapping();
1159
1160 uint64_t oldId = 1;
1161 if (!getSynchronizingActionIndices().empty()) {
1162 oldId = *(getSynchronizingActionIndices().rbegin()) + 1;
1163 }
1164 uint64_t newId = oldId;
1165 for (auto const& module : modules) {
1166 newModules.push_back(module.labelUnlabelledCommands(nameSuggestions, newId, newActionNameToIndexMapping));
1167 }
1168
1169 std::vector<std::pair<uint64_t, std::string>> newActionNames;
1170 for (auto const& entry : newActionNameToIndexMapping) {
1171 if (!hasAction(entry.first)) {
1172 newActionNames.emplace_back(entry.second, entry.first);
1173 }
1174 }
1175 for (auto const& rewardModel : rewardModels) {
1176 newRewardModels.push_back(rewardModel.labelUnlabelledCommands(newActionNames));
1177 }
1178
1179 return Program(this->manager, this->getModelType(), this->getConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(),
1180 this->getFormulas(), this->getPlayers(), newModules, newActionNameToIndexMapping, newRewardModels, this->getLabels(),
1181 this->getObservationLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
1182}
1183
1184Program Program::replaceVariableInitializationByInitExpression() const {
1185 std::vector<BooleanVariable> newBooleanVariables = globalBooleanVariables;
1186 for (auto& newVar : newBooleanVariables) {
1187 newVar.setInitialValueExpression(storm::expressions::Expression());
1188 }
1189
1190 std::vector<IntegerVariable> newIntegerVariables = globalIntegerVariables;
1191 for (auto& newVar : newIntegerVariables) {
1192 newVar.setInitialValueExpression(storm::expressions::Expression());
1193 }
1194
1195 std::vector<Module> newModules = this->getModules();
1196 for (auto& module : newModules) {
1197 module.removeVariableInitialization();
1198 }
1199
1200 return Program(this->manager, this->getModelType(), this->getConstants(), newBooleanVariables, newIntegerVariables, this->getFormulas(), this->getPlayers(),
1201 newModules, this->actionToIndexMap, this->getRewardModels(), this->getLabels(), this->getObservationLabels(),
1202 InitialConstruct(this->getInitialStatesExpression()), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
1203}
1204
1205Program Program::replaceConstantByVariable(Constant const& c, expressions::Expression const& lowerBound, expressions::Expression const& upperBound,
1206 bool observable) const {
1207 STORM_LOG_THROW(this->getModelType() == ModelType::POMDP || observable, storm::exceptions::InvalidArgumentException,
1208 "Variables can only be unobservable in POMDPs");
1209 std::vector<BooleanVariable> newBooleanVariables = globalBooleanVariables;
1210 std::vector<IntegerVariable> newIntegerVariables = globalIntegerVariables;
1211 std::vector<Constant> newConstants = constants;
1212 auto newEnd = std::remove(newConstants.begin(), newConstants.end(), c);
1213 newConstants.erase(newEnd, newConstants.end()); // Erase is necessary based on Erase-remove idiom
1214 // The following throw is moved here as this is cheaper.
1215 STORM_LOG_THROW(newConstants.size() == constants.size() - 1, exceptions::InvalidArgumentException, "Can only replace a constant if it is present.");
1216 if (c.getType().isBooleanType()) {
1217 newBooleanVariables.emplace_back(c.getExpressionVariable(), c.getExpression(), observable);
1218 } else {
1219 newIntegerVariables.emplace_back(c.getExpressionVariable(), lowerBound, upperBound, c.getExpression(), observable);
1220 }
1221 return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, this->getFormulas(), this->getPlayers(),
1222 modules, this->actionToIndexMap, this->getRewardModels(), this->getLabels(), this->getObservationLabels(),
1223 this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
1224}
1225
1226void Program::checkValidity(Program::ValidityCheckLevel lvl) const {
1227 // Start by checking the constant declarations.
1228 std::set<storm::expressions::Variable> all;
1229 std::set<storm::expressions::Variable> allGlobals;
1230 std::set<storm::expressions::Variable> globalVariables;
1231 std::set<storm::expressions::Variable> constants;
1232 for (auto const& constant : this->getConstants()) {
1233 // Check defining expressions of defined constants.
1234 if (constant.isDefined()) {
1235 std::set<storm::expressions::Variable> containedVariables = constant.getExpression().getVariables();
1236 std::set<storm::expressions::Variable> illegalVariables;
1237 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1238 std::inserter(illegalVariables, illegalVariables.begin()));
1239 bool isValid = illegalVariables.empty();
1240
1241 if (!isValid) {
1242 std::vector<std::string> illegalVariableNames;
1243 for (auto const& var : illegalVariables) {
1244 illegalVariableNames.push_back(var.getName());
1245 }
1246 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1247 "Error in " << constant.getFilename() << ", line " << constant.getLineNumber()
1248 << ": defining expression refers to unknown identifiers: " << boost::algorithm::join(illegalVariableNames, ",")
1249 << ".");
1250 }
1251 }
1252
1253 // Record the new identifier for future checks.
1254 constants.insert(constant.getExpressionVariable());
1255 all.insert(constant.getExpressionVariable());
1256 allGlobals.insert(constant.getExpressionVariable());
1257 }
1258
1259 // Now we check the variable declarations. We start with the global variables.
1260 std::set<storm::expressions::Variable> variables;
1261 for (auto const& variable : this->getGlobalBooleanVariables()) {
1262 if (variable.hasInitialValue()) {
1263 STORM_LOG_THROW(!this->hasInitialConstruct(), storm::exceptions::WrongFormatException,
1264 "Error for " << variable.getName() << " (" << variable.getFilename() << ", line " << variable.getLineNumber()
1265 << "): illegal to specify initial value if an initial construct is present.");
1266
1267 // Check the initial value of the variable.
1268 std::set<storm::expressions::Variable> containedVariables = variable.getInitialValueExpression().getVariables();
1269 std::set<storm::expressions::Variable> illegalVariables;
1270 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1271 std::inserter(illegalVariables, illegalVariables.begin()));
1272 bool isValid = illegalVariables.empty();
1273
1274 if (!isValid) {
1275 std::vector<std::string> illegalVariableNames;
1276 for (auto const& var : illegalVariables) {
1277 illegalVariableNames.push_back(var.getName());
1278 }
1279 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1280 "Error in " << variable.getFilename() << ", line " << variable.getLineNumber()
1281 << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",")
1282 << ".");
1283 }
1284 }
1285
1286 // Record the new identifier for future checks.
1287 variables.insert(variable.getExpressionVariable());
1288 all.insert(variable.getExpressionVariable());
1289 allGlobals.insert(variable.getExpressionVariable());
1290 globalVariables.insert(variable.getExpressionVariable());
1291 }
1292 for (auto const& variable : this->getGlobalIntegerVariables()) {
1293 // Check that bound expressions of the range.
1294 if (variable.hasLowerBoundExpression()) {
1295 std::set<storm::expressions::Variable> containedVariables = variable.getLowerBoundExpression().getVariables();
1296 std::set<storm::expressions::Variable> illegalVariables;
1297 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1298 std::inserter(illegalVariables, illegalVariables.begin()));
1299 bool isValid = illegalVariables.empty();
1300
1301 if (!isValid) {
1302 std::vector<std::string> illegalVariableNames;
1303 for (auto const& var : illegalVariables) {
1304 illegalVariableNames.push_back(var.getName());
1305 }
1306 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1307 "Error in " << variable.getFilename() << ", line " << variable.getLineNumber()
1308 << ": lower bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",")
1309 << ".");
1310 }
1311 }
1312
1313 if (variable.hasUpperBoundExpression()) {
1314 std::set<storm::expressions::Variable> containedVariables = variable.getUpperBoundExpression().getVariables();
1315 std::set<storm::expressions::Variable> illegalVariables;
1316 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1317 std::inserter(illegalVariables, illegalVariables.begin()));
1318 bool isValid = illegalVariables.empty();
1319 if (!isValid) {
1320 std::vector<std::string> illegalVariableNames;
1321 for (auto const& var : illegalVariables) {
1322 illegalVariableNames.push_back(var.getName());
1323 }
1324 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1325 "Error in " << variable.getFilename() << ", line " << variable.getLineNumber()
1326 << ": upper bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",")
1327 << ".");
1328 }
1329 }
1330
1331 if (variable.hasInitialValue()) {
1332 STORM_LOG_THROW(!this->hasInitialConstruct(), storm::exceptions::WrongFormatException,
1333 "Error for " << variable.getName() << " (" << variable.getFilename() << ", line " << variable.getLineNumber()
1334 << "): illegal to specify initial value if an initial construct is present.");
1335
1336 // Check the initial value of the variable.
1337 std::set<storm::expressions::Variable> containedVariables = variable.getInitialValueExpression().getVariables();
1338 std::set<storm::expressions::Variable> illegalVariables;
1339 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1340 std::inserter(illegalVariables, illegalVariables.begin()));
1341 bool isValid = illegalVariables.empty();
1342 if (!isValid) {
1343 std::vector<std::string> illegalVariableNames;
1344 for (auto const& var : illegalVariables) {
1345 illegalVariableNames.push_back(var.getName());
1346 }
1347 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1348 "Error in " << variable.getFilename() << ", line " << variable.getLineNumber()
1349 << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",")
1350 << ".");
1351 }
1352 }
1353
1354 // Record the new identifier for future checks.
1355 variables.insert(variable.getExpressionVariable());
1356 all.insert(variable.getExpressionVariable());
1357 allGlobals.insert(variable.getExpressionVariable());
1358 globalVariables.insert(variable.getExpressionVariable());
1359 }
1360
1361 // Now go through the variables of the modules.
1362 for (auto const& module : this->getModules()) {
1363 for (auto const& variable : module.getBooleanVariables()) {
1364 if (variable.hasInitialValue()) {
1365 STORM_LOG_THROW(!this->hasInitialConstruct(), storm::exceptions::WrongFormatException,
1366 "Error for " << module.getName() << "." << variable.getName() << " (" << variable.getFilename() << ", line "
1367 << variable.getLineNumber() << "): illegal to specify initial value if an initial construct is present.");
1368
1369 // Check the initial value of the variable.
1370 std::set<storm::expressions::Variable> containedVariables = variable.getInitialValueExpression().getVariables();
1371 std::set<storm::expressions::Variable> illegalVariables;
1372 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1373 std::inserter(illegalVariables, illegalVariables.begin()));
1374 bool isValid = illegalVariables.empty();
1375 if (!isValid) {
1376 std::vector<std::string> illegalVariableNames;
1377 for (auto const& var : illegalVariables) {
1378 illegalVariableNames.push_back(var.getName());
1379 }
1381 isValid, storm::exceptions::WrongFormatException,
1382 "Error in " << variable.getFilename() << ", line " << variable.getLineNumber()
1383 << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
1384 }
1385 }
1386
1387 // Record the new identifier for future checks.
1388 variables.insert(variable.getExpressionVariable());
1389 all.insert(variable.getExpressionVariable());
1390 }
1391 for (auto const& variable : module.getIntegerVariables()) {
1392 // Check that bound expressions of the range.
1393 if (variable.hasLowerBoundExpression()) {
1394 std::set<storm::expressions::Variable> containedVariables = variable.getLowerBoundExpression().getVariables();
1395 std::set<storm::expressions::Variable> illegalVariables;
1396 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1397 std::inserter(illegalVariables, illegalVariables.begin()));
1398 bool isValid = illegalVariables.empty();
1399 if (!isValid) {
1400 std::vector<std::string> illegalVariableNames;
1401 for (auto const& var : illegalVariables) {
1402 illegalVariableNames.push_back(var.getName());
1403 }
1404 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1405 "Error in " << variable.getFilename() << ", line " << variable.getLineNumber()
1406 << ": lower bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",")
1407 << ".");
1408 }
1409 }
1410
1411 if (variable.hasUpperBoundExpression()) {
1412 std::set<storm::expressions::Variable> containedVariables = variable.getUpperBoundExpression().getVariables();
1413 std::set<storm::expressions::Variable> illegalVariables;
1414
1415 illegalVariables.clear();
1416 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1417 std::inserter(illegalVariables, illegalVariables.begin()));
1418 bool isValid = illegalVariables.empty();
1419 if (!isValid) {
1420 std::vector<std::string> illegalVariableNames;
1421 for (auto const& var : illegalVariables) {
1422 illegalVariableNames.push_back(var.getName());
1423 }
1424 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1425 "Error in " << variable.getFilename() << ", line " << variable.getLineNumber()
1426 << ": upper bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",")
1427 << ".");
1428 }
1429 }
1430
1431 if (variable.hasInitialValue()) {
1432 STORM_LOG_THROW(!this->hasInitialConstruct(), storm::exceptions::WrongFormatException,
1433 "Error for " << module.getName() << "." << variable.getName() << " (" << variable.getFilename() << ", line "
1434 << variable.getLineNumber() << "): illegal to specify initial value if an initial construct is present.");
1435
1436 // Check the initial value of the variable.
1437 std::set<storm::expressions::Variable> containedVariables = variable.getInitialValueExpression().getVariables();
1438 std::set<storm::expressions::Variable> illegalVariables;
1439 illegalVariables.clear();
1440 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1441 std::inserter(illegalVariables, illegalVariables.begin()));
1442 bool isValid = illegalVariables.empty();
1443 if (!isValid) {
1444 std::vector<std::string> illegalVariableNames;
1445 for (auto const& var : illegalVariables) {
1446 illegalVariableNames.push_back(var.getName());
1447 }
1449 isValid, storm::exceptions::WrongFormatException,
1450 "Error in " << variable.getFilename() << ", line " << variable.getLineNumber()
1451 << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
1452 }
1453 }
1454
1455 // Record the new identifier for future checks.
1456 variables.insert(variable.getExpressionVariable());
1457 all.insert(variable.getExpressionVariable());
1458 }
1459
1460 for (auto const& variable : module.getClockVariables()) {
1461 // Record the new identifier for future checks.
1462 variables.insert(variable.getExpressionVariable());
1463 all.insert(variable.getExpressionVariable());
1464 }
1465 }
1466
1467 // Create the set of valid identifiers for future checks.
1468 std::set<storm::expressions::Variable> variablesAndConstants;
1469 std::set_union(variables.begin(), variables.end(), constants.begin(), constants.end(), std::inserter(variablesAndConstants, variablesAndConstants.begin()));
1470
1471 // Collect the formula placeholders and check formulas
1472 for (auto const& formula : this->getFormulas()) {
1473 std::set<storm::expressions::Variable> containedVariables = formula.getExpression().getVariables();
1474 bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1475 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1476 "Error in " << formula.getFilename() << ", line " << formula.getLineNumber() << ": expression '" << formula.getExpression()
1477 << "'of formula '" << formula.getName() << "' refers to unknown identifiers.");
1478 if (formula.hasExpressionVariable()) {
1479 all.insert(formula.getExpressionVariable());
1480 variablesAndConstants.insert(formula.getExpressionVariable());
1481 }
1482 }
1483
1484 // Check the commands and invariants of the modules.
1485 bool hasProbabilisticCommand = false;
1486 bool hasMarkovianCommand = false;
1487 bool hasLabeledMarkovianCommand = false;
1488 std::map<std::pair<storm::expressions::Variable, uint64_t>, std::pair<uint64_t, std::string>> writtenGlobalVariables;
1489 for (auto const& module : this->getModules()) {
1490 std::set<storm::expressions::Variable> legalVariables = globalVariables;
1491 for (auto const& variable : module.getBooleanVariables()) {
1492 legalVariables.insert(variable.getExpressionVariable());
1493 }
1494 for (auto const& variable : module.getIntegerVariables()) {
1495 legalVariables.insert(variable.getExpressionVariable());
1496 }
1497 for (auto const& variable : module.getClockVariables()) {
1498 legalVariables.insert(variable.getExpressionVariable());
1499 }
1500
1501 if (module.hasInvariant()) {
1502 std::set<storm::expressions::Variable> containedVariables = module.getInvariant().getVariables();
1503 std::set<storm::expressions::Variable> illegalVariables;
1504 std::set_difference(containedVariables.begin(), containedVariables.end(), variablesAndConstants.begin(), variablesAndConstants.end(),
1505 std::inserter(illegalVariables, illegalVariables.begin()));
1506 bool isValid = illegalVariables.empty();
1507 if (!isValid) {
1508 std::vector<std::string> illegalVariableNames;
1509 for (auto const& var : illegalVariables) {
1510 illegalVariableNames.push_back(var.getName());
1511 }
1512 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1513 "Error in " << module.getFilename() << ", line " << module.getLineNumber() << ": invariant " << module.getInvariant()
1514 << " refers to unknown identifiers: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
1515 }
1516 STORM_LOG_THROW(module.getInvariant().hasBooleanType(), storm::exceptions::WrongFormatException,
1517 "Error in " << module.getFilename() << ", line " << module.getLineNumber() << ": invariant " << module.getInvariant()
1518 << " must evaluate to type 'bool'.");
1519 }
1520
1521 for (auto& command : module.getCommands()) {
1522 // Check the guard.
1523 std::set<storm::expressions::Variable> containedVariables = command.getGuardExpression().getVariables();
1524 std::set<storm::expressions::Variable> illegalVariables;
1525 std::set_difference(containedVariables.begin(), containedVariables.end(), variablesAndConstants.begin(), variablesAndConstants.end(),
1526 std::inserter(illegalVariables, illegalVariables.begin()));
1527 bool isValid = illegalVariables.empty();
1528 if (!isValid) {
1529 std::vector<std::string> illegalVariableNames;
1530 for (auto const& var : illegalVariables) {
1531 illegalVariableNames.push_back(var.getName());
1532 }
1533 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1534 "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": guard " << command.getGuardExpression()
1535 << " refers to unknown identifiers: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
1536 }
1538 command.getGuardExpression().hasBooleanType(), storm::exceptions::WrongFormatException,
1539 "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": expression for guard must evaluate to type 'bool'.");
1540
1541 // Record which types of commands were seen.
1542 if (command.isMarkovian()) {
1543 hasMarkovianCommand = true;
1544 } else {
1545 hasProbabilisticCommand = true;
1546 }
1547
1548 // If the command is Markovian and labeled, we throw an error or raise a warning, depending on
1549 // whether or not the PRISM compatibility mode was enabled.
1550 if (command.isMarkovian() && command.isLabeled()) {
1551 hasLabeledMarkovianCommand = true;
1552 }
1553
1554 // Check all updates.
1555 for (auto const& update : command.getUpdates()) {
1556 containedVariables = update.getLikelihoodExpression().getVariables();
1557 illegalVariables.clear();
1558 std::set_difference(containedVariables.begin(), containedVariables.end(), variablesAndConstants.begin(), variablesAndConstants.end(),
1559 std::inserter(illegalVariables, illegalVariables.begin()));
1560 isValid = illegalVariables.empty();
1561 if (!isValid) {
1562 std::vector<std::string> illegalVariableNames;
1563 for (auto const& var : illegalVariables) {
1564 illegalVariableNames.push_back(var.getName());
1565 }
1567 isValid, storm::exceptions::WrongFormatException,
1568 "Error in " << command.getFilename() << ", line " << command.getLineNumber()
1569 << ": likelihood expression refers to unknown identifiers: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
1570 }
1571
1572 // Check all assignments.
1573 std::set<storm::expressions::Variable> alreadyAssignedVariables;
1574 for (auto const& assignment : update.getAssignments()) {
1575 storm::expressions::Variable assignedVariable = manager->getVariable(assignment.getVariableName());
1576
1577 if (legalVariables.find(assignedVariable) == legalVariables.end()) {
1578 if (all.find(assignedVariable) != all.end()) {
1579 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
1580 "Error in " << command.getFilename() << ", line " << command.getLineNumber()
1581 << ": assignment illegally refers to variable '" << assignment.getVariableName() << "'.");
1582 } else {
1583 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
1584 "Error in " << command.getFilename() << ", line " << command.getLineNumber()
1585 << ": assignment refers to unknown variable '" << assignment.getVariableName() << "'.");
1586 }
1587 }
1588 STORM_LOG_THROW(alreadyAssignedVariables.find(assignedVariable) == alreadyAssignedVariables.end(), storm::exceptions::WrongFormatException,
1589 "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": duplicate assignment to variable '"
1590 << assignment.getVariableName() << "'.");
1591 STORM_LOG_THROW(assignedVariable.getType() == assignment.getExpression().getType() ||
1592 (assignedVariable.getType().isRationalType() && assignment.getExpression().getType().isNumericalType()),
1593 storm::exceptions::WrongFormatException,
1594 "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": illegally assigning a value of type '"
1595 << assignment.getExpression().getType() << "' to variable '" << assignment.getVariableName() << "' of type '"
1596 << assignedVariable.getType() << "'.");
1597
1598 if (command.isLabeled() && globalVariables.find(assignedVariable) != globalVariables.end()) {
1599 std::pair<storm::expressions::Variable, uint64_t> variableActionIndexPair(assignedVariable, command.getActionIndex());
1600 std::pair<uint64_t, std::string> lineModuleNamePair(command.getLineNumber(), module.getName());
1601 auto insertionResult = writtenGlobalVariables.emplace(variableActionIndexPair, lineModuleNamePair);
1603 insertionResult.second || insertionResult.first->second.second == module.getName(), storm::exceptions::WrongFormatException,
1604 "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": Syncronizing command with action label '"
1605 << command.getActionName() << "' illegally assigns a value to global variable '" << assignedVariable.getName()
1606 << "'. Previous assignment to the variable at line " << insertionResult.first->second.first << " in module '"
1607 << insertionResult.first->second.second << "'.");
1608 }
1609
1610 containedVariables = assignment.getExpression().getVariables();
1611 illegalVariables.clear();
1612 std::set_difference(containedVariables.begin(), containedVariables.end(), variablesAndConstants.begin(), variablesAndConstants.end(),
1613 std::inserter(illegalVariables, illegalVariables.begin()));
1614 isValid = illegalVariables.empty();
1615 if (!isValid) {
1616 std::vector<std::string> illegalVariableNames;
1617 for (auto const& var : illegalVariables) {
1618 illegalVariableNames.push_back(var.getName());
1619 }
1621 isValid, storm::exceptions::WrongFormatException,
1622 "Error in " << command.getFilename() << ", line " << command.getLineNumber()
1623 << ": assigned expression refers to unknown identifiers: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
1624 }
1625
1626 // Add the current variable to the set of assigned variables (of this update).
1627 alreadyAssignedVariables.insert(assignedVariable);
1628 }
1629 }
1630 }
1631 }
1632
1633 if (hasLabeledMarkovianCommand) {
1634 if (prismCompatibility) {
1636 false, "The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.");
1637 } else {
1638 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
1639 "The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.");
1640 }
1641 }
1642
1643 if (this->getModelType() == Program::ModelType::DTMC || this->getModelType() == Program::ModelType::MDP) {
1644 STORM_LOG_THROW(!hasMarkovianCommand, storm::exceptions::WrongFormatException, "Discrete-time model must not have Markovian commands.");
1645 } else if (this->getModelType() == Program::ModelType::CTMC) {
1646 STORM_LOG_THROW(!hasProbabilisticCommand, storm::exceptions::WrongFormatException,
1647 "The input model is a CTMC, but uses probabilistic commands like they are used in PRISM. Please use Markovian commands instead or turn "
1648 "on the PRISM compatibility mode using the flag '-pc'.");
1649 }
1650
1651 // Now check the reward models.
1652 for (auto const& rewardModel : this->getRewardModels()) {
1653 for (auto const& stateReward : rewardModel.getStateRewards()) {
1654 std::set<storm::expressions::Variable> containedVariables = stateReward.getStatePredicateExpression().getVariables();
1655 bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1656 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1657 "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber()
1658 << ": state reward expression refers to unknown identifiers.");
1660 stateReward.getStatePredicateExpression().hasBooleanType(), storm::exceptions::WrongFormatException,
1661 "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": state predicate must evaluate to type 'bool'.");
1662
1663 containedVariables = stateReward.getRewardValueExpression().getVariables();
1664 isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1665 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1666 "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber()
1667 << ": state reward value expression refers to unknown identifiers.");
1668 STORM_LOG_THROW(stateReward.getRewardValueExpression().hasNumericalType(), storm::exceptions::WrongFormatException,
1669 "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber()
1670 << ": reward value expression must evaluate to numerical type.");
1671 }
1672
1673 for (auto const& stateActionReward : rewardModel.getStateActionRewards()) {
1674 std::set<storm::expressions::Variable> containedVariables = stateActionReward.getStatePredicateExpression().getVariables();
1675 bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1676 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1677 "Error in " << stateActionReward.getFilename() << ", line " << stateActionReward.getLineNumber()
1678 << ": state reward expression refers to unknown identifiers.");
1679 STORM_LOG_THROW(stateActionReward.getStatePredicateExpression().hasBooleanType(), storm::exceptions::WrongFormatException,
1680 "Error in " << stateActionReward.getFilename() << ", line " << stateActionReward.getLineNumber()
1681 << ": state predicate must evaluate to type 'bool'.");
1682
1683 containedVariables = stateActionReward.getRewardValueExpression().getVariables();
1684 isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1685 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1686 "Error in " << stateActionReward.getFilename() << ", line " << stateActionReward.getLineNumber()
1687 << ": state reward value expression refers to unknown identifiers.");
1688 STORM_LOG_THROW(stateActionReward.getRewardValueExpression().hasNumericalType(), storm::exceptions::WrongFormatException,
1689 "Error in " << stateActionReward.getFilename() << ", line " << stateActionReward.getLineNumber()
1690 << ": reward value expression must evaluate to numerical type.");
1691 }
1692
1693 for (auto const& transitionReward : rewardModel.getTransitionRewards()) {
1694 std::set<storm::expressions::Variable> containedVariables = transitionReward.getSourceStatePredicateExpression().getVariables();
1695 bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1696 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1697 "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber()
1698 << ": state reward expression refers to unknown identifiers.");
1699 STORM_LOG_THROW(transitionReward.getSourceStatePredicateExpression().hasBooleanType(), storm::exceptions::WrongFormatException,
1700 "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber()
1701 << ": state predicate must evaluate to type 'bool'.");
1702
1703 containedVariables = transitionReward.getTargetStatePredicateExpression().getVariables();
1704 isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1705 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1706 "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber()
1707 << ": state reward expression refers to unknown identifiers.");
1708 STORM_LOG_THROW(transitionReward.getTargetStatePredicateExpression().hasBooleanType(), storm::exceptions::WrongFormatException,
1709 "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber()
1710 << ": state predicate must evaluate to type 'bool'.");
1711
1712 containedVariables = transitionReward.getRewardValueExpression().getVariables();
1713 isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1714 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1715 "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber()
1716 << ": state reward value expression refers to unknown identifiers.");
1717 STORM_LOG_THROW(transitionReward.getRewardValueExpression().hasNumericalType(), storm::exceptions::WrongFormatException,
1718 "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber()
1719 << ": reward value expression must evaluate to numerical type.");
1720 }
1721 }
1722
1723 // Check the initial states expression.
1724 if (this->hasInitialConstruct()) {
1725 std::set<storm::expressions::Variable> containedIdentifiers = this->getInitialConstruct().getInitialStatesExpression().getVariables();
1726 bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
1727 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1728 "Error in " << this->getInitialConstruct().getFilename() << ", line " << this->getInitialConstruct().getLineNumber()
1729 << ": initial construct refers to unknown identifiers.");
1730 }
1731
1732 // Check the system composition if given.
1733 if (systemCompositionConstruct) {
1734 CompositionValidityChecker checker(*this);
1735 checker.check(systemCompositionConstruct.get().getSystemComposition());
1736 }
1737
1738 // Check the labels.
1739 for (auto const& label : this->getLabels()) {
1740 std::set<storm::expressions::Variable> containedVariables = label.getStatePredicateExpression().getVariables();
1741 bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1742 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1743 "Error in " << label.getFilename() << ", line " << label.getLineNumber() << ": label expression refers to unknown identifiers.");
1744 STORM_LOG_THROW(label.getStatePredicateExpression().hasBooleanType(), storm::exceptions::WrongFormatException,
1745 "Error in " << label.getFilename() << ", line " << label.getLineNumber() << ": label predicate must evaluate to type 'bool'.");
1746 }
1747
1748 // Check the players
1749 for (auto const& player : this->getPlayers()) {
1750 // The stored action/module names shall be available
1751 for (auto const& controlledAction : player.getActions()) {
1752 STORM_LOG_THROW(this->hasAction(controlledAction), storm::exceptions::InternalException,
1753 "Error in " << player.getFilename() << ", line " << player.getLineNumber() << ": The player controlled action " << controlledAction
1754 << " is not available.");
1755 }
1756 for (auto const& controlledModule : player.getModules()) {
1757 STORM_LOG_THROW(this->hasModule(controlledModule), storm::exceptions::InternalException,
1758 "Error in " << player.getFilename() << ", line " << player.getLineNumber() << ": The player controlled module " << controlledModule
1759 << " is not available.");
1760 }
1761 }
1762
1763 if (lvl >= Program::ValidityCheckLevel::READYFORPROCESSING) {
1764 // We check for each global variable and each labeled command, whether there is at most one instance writing to that variable.
1765 std::set<std::pair<std::string, std::string>> globalBVarsWrittenToByCommand;
1766 std::set<std::pair<std::string, std::string>> globalIVarsWrittenToByCommand;
1767 for (auto const& module : this->getModules()) {
1768 std::set<std::pair<std::string, std::string>> globalBVarsWrittenToByCommandInThisModule;
1769 std::set<std::pair<std::string, std::string>> globalIVarsWrittenToByCommandInThisModule;
1770 for (auto const& command : module.getCommands()) {
1771 if (!command.isLabeled())
1772 continue;
1773 for (auto const& update : command.getUpdates()) {
1774 for (auto const& assignment : update.getAssignments()) {
1775 if (this->globalBooleanVariableExists(assignment.getVariable().getName())) {
1776 globalBVarsWrittenToByCommandInThisModule.insert({assignment.getVariable().getName(), command.getActionName()});
1777 } else if (this->globalIntegerVariableExists(assignment.getVariable().getName())) {
1778 globalIVarsWrittenToByCommandInThisModule.insert({assignment.getVariable().getName(), command.getActionName()});
1779 }
1780 }
1781 }
1782 }
1783 for (auto const& entry : globalIVarsWrittenToByCommandInThisModule) {
1784 if (globalIVarsWrittenToByCommand.find(entry) != globalIVarsWrittenToByCommand.end()) {
1785 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
1786 "Error in " << module.getFilename() << ", line " << module.getLineNumber()
1787 << ": assignment of (possibly) synchronizing command with label '" << entry.second
1788 << "' writes to global variable '" << entry.first << "'.");
1789 }
1790 }
1791 for (auto const& entry : globalBVarsWrittenToByCommandInThisModule) {
1792 if (globalBVarsWrittenToByCommand.find(entry) != globalBVarsWrittenToByCommand.end()) {
1793 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
1794 "Error in " << module.getFilename() << ", line " << module.getLineNumber()
1795 << ": assignment of (possibly) synchronizing command with label '" << entry.second
1796 << "' writes to global variable '" << entry.first << "'.");
1797 }
1798 }
1799 }
1800 }
1801}
1802
1803Program Program::simplify() {
1804 // Start by substituting the constants, because this will potentially erase some commands or even actions.
1805 Program substitutedProgram = this->substituteConstantsFormulas();
1806
1807 // As we possibly delete some commands and some actions might be dropped from modules altogether, we need to
1808 // maintain a list of actions that we need to remove in other modules. For example, if module A loses all [a]
1809 // commands, we need to delete all [a] commands from all other modules as well. If we do not do that, we will
1810 // remove the forced synchronization that was there before.
1811 std::set<uint_fast64_t> actionIndicesToDelete;
1812
1813 std::vector<Module> newModules;
1814 std::vector<Constant> newConstants = substitutedProgram.getConstants();
1815 for (auto const& module : substitutedProgram.getModules()) {
1816 // Discard all commands with a guard equivalent to false and remove identity assignments from the updates.
1817 std::vector<Command> newCommands;
1818 for (auto const& command : module.getCommands()) {
1819 if (!command.getGuardExpression().isFalse()) {
1820 newCommands.emplace_back(command.simplify());
1821 }
1822 }
1823
1824 // Substitute variables by global constants if possible.
1825 std::map<storm::expressions::Variable, storm::expressions::Expression> booleanVars;
1826 std::map<storm::expressions::Variable, storm::expressions::Expression> integerVars;
1827 for (auto const& variable : module.getBooleanVariables()) {
1828 booleanVars.emplace(variable.getExpressionVariable(), variable.getInitialValueExpression());
1829 }
1830 for (auto const& variable : module.getIntegerVariables()) {
1831 integerVars.emplace(variable.getExpressionVariable(), variable.getInitialValueExpression());
1832 }
1833
1834 // Collect all variables that are being written. These variables cannot be turned to constants.
1835 for (auto const& command : newCommands) {
1836 // Check all updates.
1837 for (auto const& update : command.getUpdates()) {
1838 // Check all assignments.
1839 for (auto const& assignment : update.getAssignments()) {
1840 if (assignment.getVariable().getType().isBooleanType()) {
1841 auto it = booleanVars.find(assignment.getVariable());
1842 if (it != booleanVars.end()) {
1843 booleanVars.erase(it);
1844 }
1845 } else {
1846 auto it = integerVars.find(assignment.getVariable());
1847 if (it != integerVars.end()) {
1848 integerVars.erase(it);
1849 }
1850 }
1851 }
1852 }
1853 }
1854
1855 std::vector<storm::prism::BooleanVariable> newBooleanVars;
1856 for (auto const& variable : module.getBooleanVariables()) {
1857 if (booleanVars.find(variable.getExpressionVariable()) == booleanVars.end()) {
1858 newBooleanVars.push_back(variable);
1859 }
1860 }
1861 std::vector<storm::prism::IntegerVariable> newIntegerVars;
1862 for (auto const& variable : module.getIntegerVariables()) {
1863 if (integerVars.find(variable.getExpressionVariable()) == integerVars.end()) {
1864 newIntegerVars.push_back(variable);
1865 }
1866 }
1867
1868 for (auto const& variable : module.getBooleanVariables()) {
1869 if (booleanVars.find(variable.getExpressionVariable()) != booleanVars.end()) {
1870 if (variable.hasInitialValue()) {
1871 newConstants.emplace_back(variable.getExpressionVariable(), variable.getInitialValueExpression());
1872 } else {
1873 newBooleanVars.push_back(variable);
1874 }
1875 }
1876 }
1877 for (auto const& variable : module.getIntegerVariables()) {
1878 if (integerVars.find(variable.getExpressionVariable()) != integerVars.end()) {
1879 if (variable.hasInitialValue()) {
1880 newConstants.emplace_back(variable.getExpressionVariable(), variable.getInitialValueExpression());
1881 } else {
1882 newIntegerVars.push_back(variable);
1883 }
1884 }
1885 }
1886
1887 // we currently do not simplify clock variables or invariants
1888 newModules.emplace_back(module.getName(), newBooleanVars, newIntegerVars, module.getClockVariables(), module.getInvariant(), newCommands);
1889
1890 // Determine the set of action indices that have been deleted entirely.
1891 std::set_difference(module.getSynchronizingActionIndices().begin(), module.getSynchronizingActionIndices().end(),
1892 newModules.back().getSynchronizingActionIndices().begin(), newModules.back().getSynchronizingActionIndices().end(),
1893 std::inserter(actionIndicesToDelete, actionIndicesToDelete.begin()));
1894 }
1895
1896 // If we have to delete whole actions, do so now.
1897 std::map<std::string, uint_fast64_t> newActionToIndexMap;
1898 std::vector<RewardModel> newRewardModels;
1899 std::vector<Player> newPlayers;
1900 if (!actionIndicesToDelete.empty()) {
1902 std::set_difference(this->getSynchronizingActionIndices().begin(), this->getSynchronizingActionIndices().end(), actionIndicesToDelete.begin(),
1903 actionIndicesToDelete.end(), std::inserter(actionsToKeep, actionsToKeep.begin()));
1904
1905 // Insert the silent action as this is not contained in the synchronizing action indices.
1906 actionsToKeep.insert(0);
1907
1908 std::vector<Module> cleanedModules;
1909 cleanedModules.reserve(newModules.size());
1910 for (auto const& module : newModules) {
1911 cleanedModules.emplace_back(module.restrictActionIndices(actionsToKeep));
1912 }
1913 newModules = std::move(cleanedModules);
1914
1915 newRewardModels.reserve(substitutedProgram.getNumberOfRewardModels());
1916 for (auto const& rewardModel : substitutedProgram.getRewardModels()) {
1917 newRewardModels.emplace_back(rewardModel.restrictActionRelatedRewards(actionsToKeep));
1918 }
1919
1920 // Restrict action name to index mapping. Old action indices remain valid.
1921 for (auto const& entry : this->getActionNameToIndexMapping()) {
1922 if (actionsToKeep.find(entry.second) != actionsToKeep.end()) {
1923 newActionToIndexMap.emplace(entry.first, entry.second);
1924 }
1925 }
1926
1927 // Restrict player controlled actions
1928 for (auto const& player : this->getPlayers()) {
1929 std::unordered_set<std::string> newControlledActions;
1930 for (auto const& act : player.getActions()) {
1931 if (newActionToIndexMap.count(act) != 0) {
1932 newControlledActions.insert(act);
1933 }
1934 }
1935 newPlayers.emplace_back(player.getName(), player.getModules(), newControlledActions, player.getFilename(), player.getLineNumber());
1936 }
1937 }
1938
1939 std::vector<Label> newLabels;
1940 for (auto const& label : this->getLabels()) {
1941 newLabels.emplace_back(label.getName(), label.getStatePredicateExpression().simplify());
1942 }
1943
1944 return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(),
1945 actionIndicesToDelete.empty() ? this->getPlayers() : newPlayers, newModules,
1946 actionIndicesToDelete.empty() ? getActionNameToIndexMapping() : newActionToIndexMap,
1947 actionIndicesToDelete.empty() ? this->getRewardModels() : newRewardModels, newLabels, getObservationLabels(), getOptionalInitialConstruct(),
1948 this->getOptionalSystemCompositionConstruct(), prismCompatibility);
1949}
1950
1951Program Program::flattenModules(std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) const {
1952 // If the current program has only one module, we can simply return a copy.
1953 if (this->getNumberOfModules() == 1) {
1954 return Program(*this);
1955 }
1956
1957 STORM_LOG_THROW(this->getModelType() == ModelType::DTMC || this->getModelType() == ModelType::MDP, storm::exceptions::InvalidTypeException,
1958 "Unable to flatten modules for model of type '" << this->getModelType() << "'.");
1959
1960 // Otherwise, we need to actually flatten the contained modules.
1961
1962 // Get an SMT solver for computing the possible guard combinations.
1963 std::unique_ptr<storm::solver::SmtSolver> solver = smtSolverFactory->create(*manager);
1964
1965 // Set up the data we need to gather to create the flat module.
1966 std::stringstream newModuleName;
1967 std::vector<storm::prism::BooleanVariable> allBooleanVariables;
1968 std::vector<storm::prism::IntegerVariable> allIntegerVariables;
1969 std::vector<storm::prism::ClockVariable> allClockVariables;
1970 std::vector<storm::prism::Command> newCommands;
1971 uint_fast64_t nextCommandIndex = 0;
1972 uint_fast64_t nextUpdateIndex = 0;
1973
1974 // Assert the values of the constants.
1975 for (auto const& constant : this->getConstants()) {
1976 if (constant.isDefined()) {
1977 if (constant.getType().isBooleanType()) {
1978 solver->add(storm::expressions::iff(constant.getExpressionVariable(), constant.getExpression()));
1979 } else {
1980 solver->add(constant.getExpressionVariable() == constant.getExpression());
1981 }
1982 }
1983 }
1984
1985 // Assert the bounds of the global variables.
1986 for (auto const& variable : this->getGlobalIntegerVariables()) {
1987 solver->add(variable.getRangeExpression());
1988 }
1989
1990 // Make the global variables local, such that the resulting module covers all occurring variables. Note that
1991 // this is just for simplicity and is not needed.
1992 allBooleanVariables.insert(allBooleanVariables.end(), this->getGlobalBooleanVariables().begin(), this->getGlobalBooleanVariables().end());
1993 allIntegerVariables.insert(allIntegerVariables.end(), this->getGlobalIntegerVariables().begin(), this->getGlobalIntegerVariables().end());
1994 storm::expressions::Expression newInvariant;
1995
1996 // Now go through the modules, gather the variables, construct the name of the new module and assert the
1997 // bounds of the discovered variables.
1998 for (auto const& module : this->getModules()) {
1999 newModuleName << module.getName() << "_";
2000 allBooleanVariables.insert(allBooleanVariables.end(), module.getBooleanVariables().begin(), module.getBooleanVariables().end());
2001 allIntegerVariables.insert(allIntegerVariables.end(), module.getIntegerVariables().begin(), module.getIntegerVariables().end());
2002 allClockVariables.insert(allClockVariables.end(), module.getClockVariables().begin(), module.getClockVariables().end());
2003
2004 for (auto const& variable : module.getIntegerVariables()) {
2005 solver->add(variable.getRangeExpression());
2006 }
2007
2008 if (module.hasInvariant()) {
2009 newInvariant = newInvariant.isInitialized() ? (newInvariant && module.getInvariant()) : module.getInvariant();
2010 }
2011
2012 // The commands without a synchronizing action name, can simply be copied (plus adjusting the global
2013 // indices of the command and its updates).
2014 for (auto const& command : module.getCommands()) {
2015 if (!command.isLabeled()) {
2016 std::vector<storm::prism::Update> updates;
2017 updates.reserve(command.getUpdates().size());
2018
2019 for (auto const& update : command.getUpdates()) {
2020 updates.push_back(
2021 storm::prism::Update(nextUpdateIndex, update.getLikelihoodExpression(), update.getAssignments(), update.getFilename(), 0));
2022 ++nextUpdateIndex;
2023 }
2024
2025 newCommands.push_back(storm::prism::Command(nextCommandIndex, command.isMarkovian(), actionToIndexMap.find("")->second, "",
2026 command.getGuardExpression(), updates, command.getFilename(), 0));
2027 ++nextCommandIndex;
2028 }
2029 }
2030 }
2031
2032 // Save state of solver so that we can always restore the point where we have exactly the constant values
2033 // and variables bounds on the assertion stack.
2034 solver->push();
2035
2036 // Now we need to enumerate all possible combinations of synchronizing commands. For this, we iterate over
2037 // all actions and let the solver enumerate the possible combinations of commands that can be enabled together.
2038 for (auto const& actionIndex : this->getSynchronizingActionIndices()) {
2039 bool noCombinationsForAction = false;
2040
2041 // Prepare the list that stores for each module the list of commands with the given action.
2042 std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>> possibleCommands;
2043
2044 for (auto const& module : this->getModules()) {
2045 // If the module has no command with this action, we can skip it.
2046 if (!module.hasActionIndex(actionIndex)) {
2047 continue;
2048 }
2049
2050 std::set<uint_fast64_t> const& commandIndices = module.getCommandIndicesByActionIndex(actionIndex);
2051
2052 // If there is no command even though the module has this action, there is no valid command
2053 // combination with this action.
2054 if (commandIndices.empty()) {
2055 noCombinationsForAction = true;
2056 break;
2057 }
2058
2059 // Prepare empty list of commands for this module.
2060 possibleCommands.push_back(std::vector<std::reference_wrapper<storm::prism::Command const>>());
2061
2062 // Add references to the commands labeled with the current action.
2063 for (auto const& commandIndex : commandIndices) {
2064 possibleCommands.back().push_back(module.getCommand(commandIndex));
2065 }
2066 }
2067
2068 // If there are no valid combinations for the action, we need to skip the generation of synchronizing
2069 // commands.
2070 if (!noCombinationsForAction) {
2071 // Save the solver state to be able to restore it when this action index is done.
2072 solver->push();
2073
2074 // Start by creating a fresh auxiliary variable for each command and link it with the guard.
2075 std::vector<std::vector<storm::expressions::Variable>> commandVariables(possibleCommands.size());
2076 std::vector<storm::expressions::Variable> allCommandVariables;
2077 for (uint_fast64_t outerIndex = 0; outerIndex < possibleCommands.size(); ++outerIndex) {
2078 // Create auxiliary variables and link them with the guards.
2079 for (uint_fast64_t innerIndex = 0; innerIndex < possibleCommands[outerIndex].size(); ++innerIndex) {
2080 commandVariables[outerIndex].push_back(manager->declareFreshBooleanVariable());
2081 allCommandVariables.push_back(commandVariables[outerIndex].back());
2082 solver->add(implies(commandVariables[outerIndex].back(), possibleCommands[outerIndex][innerIndex].get().getGuardExpression()));
2083 }
2084
2085 storm::expressions::Expression atLeastOneCommandFromModule = manager->boolean(false);
2086 for (auto const& commandVariable : commandVariables[outerIndex]) {
2087 atLeastOneCommandFromModule = atLeastOneCommandFromModule || commandVariable;
2088 }
2089 solver->add(atLeastOneCommandFromModule);
2090 }
2091
2092 // Now we are in a position to start the enumeration over all command variables. While doing so, we
2093 // keep track of previously seen command combinations, because the AllSat procedures are not
2094 // always guaranteed to only provide distinct models.
2095 std::unordered_set<std::vector<uint_fast64_t>, storm::utility::vector::VectorHash<uint_fast64_t>> seenCommandCombinations;
2096 solver->allSat(allCommandVariables, [&](storm::solver::SmtSolver::ModelReference& modelReference) -> bool {
2097 // Now we need to reconstruct the chosen commands from the valuation of the command variables.
2098 std::vector<std::vector<std::reference_wrapper<Command const>>> chosenCommands(possibleCommands.size());
2099
2100 for (uint_fast64_t outerIndex = 0; outerIndex < commandVariables.size(); ++outerIndex) {
2101 for (uint_fast64_t innerIndex = 0; innerIndex < commandVariables[outerIndex].size(); ++innerIndex) {
2102 if (modelReference.getBooleanValue(commandVariables[outerIndex][innerIndex])) {
2103 chosenCommands[outerIndex].push_back(possibleCommands[outerIndex][innerIndex]);
2104 }
2105 }
2106 }
2107
2108 // Now that we have retrieved the commands, we need to build their synchronizations and add them
2109 // to the flattened module.
2110 std::vector<std::vector<std::reference_wrapper<Command const>>::const_iterator> iterators;
2111 for (auto const& element : chosenCommands) {
2112 iterators.push_back(element.begin());
2113 }
2114
2115 bool movedAtLeastOneIterator = false;
2116 std::vector<std::reference_wrapper<Command const>> commandCombination(chosenCommands.size(), chosenCommands.front().front());
2117 std::vector<uint_fast64_t> commandCombinationIndices(iterators.size());
2118 do {
2119 for (uint_fast64_t index = 0; index < iterators.size(); ++index) {
2120 commandCombination[index] = *iterators[index];
2121 commandCombinationIndices[index] = commandCombination[index].get().getGlobalIndex();
2122 }
2123
2124 // Only add the command combination if it was not previously seen.
2125 auto seenIt = seenCommandCombinations.find(commandCombinationIndices);
2126 if (seenIt == seenCommandCombinations.end()) {
2127 newCommands.push_back(synchronizeCommands(nextCommandIndex, actionIndex, nextUpdateIndex, indexToActionMap.find(actionIndex)->second,
2128 commandCombination));
2129 seenCommandCombinations.insert(commandCombinationIndices);
2130
2131 // Move the counters appropriately.
2132 ++nextCommandIndex;
2133 nextUpdateIndex += newCommands.back().getNumberOfUpdates();
2134 }
2135
2136 movedAtLeastOneIterator = false;
2137 for (uint_fast64_t index = 0; index < iterators.size(); ++index) {
2138 ++iterators[index];
2139 if (iterators[index] != chosenCommands[index].cend()) {
2140 movedAtLeastOneIterator = true;
2141 break;
2142 } else {
2143 iterators[index] = chosenCommands[index].cbegin();
2144 }
2145 }
2146 } while (movedAtLeastOneIterator);
2147
2148 return true;
2149 });
2150
2151 solver->pop();
2152 }
2153 }
2154
2155 // Finally, we can create the module and the program and return it.
2156 storm::prism::Module singleModule(newModuleName.str(), allBooleanVariables, allIntegerVariables, allClockVariables, newInvariant, newCommands,
2157 this->getFilename(), 0);
2158
2159 return Program(manager, this->getModelType(), this->getConstants(), std::vector<storm::prism::BooleanVariable>(),
2160 std::vector<storm::prism::IntegerVariable>(), this->getFormulas(), this->getPlayers(), {singleModule}, actionToIndexMap,
2161 this->getRewardModels(), this->getLabels(), this->getObservationLabels(), this->getOptionalInitialConstruct(),
2162 this->getOptionalSystemCompositionConstruct(), prismCompatibility, this->getFilename(), 0, true);
2163}
2164
2165std::vector<Constant> Program::usedConstants() const {
2166 std::unordered_set<expressions::Variable> vars;
2167 for (auto const& m : this->modules) {
2168 for (auto const& c : m.getCommands()) {
2169 auto const& found_gex = c.getGuardExpression().getVariables();
2170 vars.insert(found_gex.begin(), found_gex.end());
2171 for (auto const& u : c.getUpdates()) {
2172 auto const& found_lex = u.getLikelihoodExpression().getVariables();
2173 vars.insert(found_lex.begin(), found_lex.end());
2174 for (auto const& a : u.getAssignments()) {
2175 auto const& found_ass = a.getExpression().getVariables();
2176 vars.insert(found_ass.begin(), found_ass.end());
2177 }
2178 }
2179 }
2180 for (auto const& v : m.getBooleanVariables()) {
2181 if (v.hasInitialValue()) {
2182 auto const& found_def = v.getInitialValueExpression().getVariables();
2183 vars.insert(found_def.begin(), found_def.end());
2184 }
2185 }
2186 for (auto const& v : m.getIntegerVariables()) {
2187 if (v.hasInitialValue()) {
2188 auto const& found_def = v.getInitialValueExpression().getVariables();
2189 vars.insert(found_def.begin(), found_def.end());
2190 }
2191 }
2192 }
2193
2194 for (auto const& f : this->formulas) {
2195 auto const& found_def = f.getExpression().getVariables();
2196 vars.insert(found_def.begin(), found_def.end());
2197 }
2198
2199 for (auto const& v : this->constants) {
2200 if (v.isDefined()) {
2201 auto const& found_def = v.getExpression().getVariables();
2202 vars.insert(found_def.begin(), found_def.end());
2203 }
2204 }
2205
2206 for (auto const& v : this->globalBooleanVariables) {
2207 if (v.hasInitialValue()) {
2208 auto const& found_def = v.getExpression().getVariables();
2209 vars.insert(found_def.begin(), found_def.end());
2210 }
2211 }
2212
2213 for (auto const& v : this->globalIntegerVariables) {
2214 if (v.hasInitialValue()) {
2215 auto const& found_def = v.getExpression().getVariables();
2216 vars.insert(found_def.begin(), found_def.end());
2217 }
2218 }
2219
2220 std::unordered_set<uint64_t> varIndices;
2221 for (auto const& v : vars) {
2222 varIndices.insert(v.getIndex());
2223 }
2224
2225 std::vector<Constant> usedConstants;
2226 for (auto const& c : this->constants) {
2227 if (varIndices.count(c.getExpressionVariable().getIndex())) {
2228 usedConstants.push_back(c);
2229 }
2230 }
2231
2232 return usedConstants;
2233}
2234
2235std::unordered_map<uint_fast64_t, std::string> Program::buildCommandIndexToActionNameMap() const {
2236 std::unordered_map<uint_fast64_t, std::string> res;
2237 for (auto const& m : this->modules) {
2238 for (auto const& c : m.getCommands()) {
2239 res.emplace(c.getGlobalIndex(), c.getActionName());
2240 }
2241 }
2242 return res;
2243}
2244
2245std::unordered_map<uint_fast64_t, std::string> Program::buildActionIndexToActionNameMap() const {
2246 std::unordered_map<uint_fast64_t, std::string> res;
2247 for (auto const& nameIndexPair : actionToIndexMap) {
2248 res.emplace(nameIndexPair.second, nameIndexPair.first);
2249 }
2250 return res;
2251}
2252
2253std::unordered_map<uint_fast64_t, uint_fast64_t> Program::buildCommandIndexToActionIndex() const {
2254 std::unordered_map<uint_fast64_t, uint_fast64_t> res;
2255 for (auto const& m : this->modules) {
2256 for (auto const& c : m.getCommands()) {
2257 res.emplace(c.getGlobalIndex(), c.getActionIndex());
2258 }
2259 }
2260 return res;
2261}
2262
2263Command Program::synchronizeCommands(uint_fast64_t newCommandIndex, uint_fast64_t actionIndex, uint_fast64_t firstUpdateIndex, std::string const& actionName,
2264 std::vector<std::reference_wrapper<Command const>> const& commands) const {
2265 // To construct the synchronous product of the commands, we need to store a list of its updates.
2266 std::vector<storm::prism::Update> newUpdates;
2267 uint_fast64_t numberOfUpdates = 1;
2268 for (uint_fast64_t i = 0; i < commands.size(); ++i) {
2269 numberOfUpdates *= commands[i].get().getNumberOfUpdates();
2270 }
2271 newUpdates.reserve(numberOfUpdates);
2272
2273 // Initialize all update iterators.
2274 std::vector<std::vector<storm::prism::Update>::const_iterator> updateIterators;
2275 for (uint_fast64_t i = 0; i < commands.size(); ++i) {
2276 updateIterators.push_back(commands[i].get().getUpdates().cbegin());
2277 }
2278
2279 bool doneUpdates = false;
2280 do {
2281 // We create the new likelihood expression by multiplying the particapting updates' expressions.
2282 storm::expressions::Expression newLikelihoodExpression = updateIterators[0]->getLikelihoodExpression();
2283 for (uint_fast64_t i = 1; i < updateIterators.size(); ++i) {
2284 newLikelihoodExpression = newLikelihoodExpression * updateIterators[i]->getLikelihoodExpression();
2285 }
2286
2287 // Now concatenate all assignments of all participating updates.
2288 std::vector<storm::prism::Assignment> newAssignments;
2289 for (uint_fast64_t i = 0; i < updateIterators.size(); ++i) {
2290 newAssignments.insert(newAssignments.end(), updateIterators[i]->getAssignments().begin(), updateIterators[i]->getAssignments().end());
2291 }
2292
2293 // Then we are ready to create the new update.
2294 newUpdates.push_back(storm::prism::Update(firstUpdateIndex, newLikelihoodExpression, newAssignments, this->getFilename(), 0));
2295 ++firstUpdateIndex;
2296
2297 // Now check whether there is some update combination we have not yet explored.
2298 bool movedIterator = false;
2299 for (int_fast64_t j = updateIterators.size() - 1; j >= 0; --j) {
2300 ++updateIterators[j];
2301 if (updateIterators[j] != commands[j].get().getUpdates().cend()) {
2302 movedIterator = true;
2303 break;
2304 } else {
2305 // Reset the iterator to the beginning of the list.
2306 updateIterators[j] = commands[j].get().getUpdates().cbegin();
2307 }
2308 }
2309
2310 doneUpdates = !movedIterator;
2311 } while (!doneUpdates);
2312
2313 storm::expressions::Expression newGuard = commands[0].get().getGuardExpression();
2314 for (uint_fast64_t i = 1; i < commands.size(); ++i) {
2315 newGuard = newGuard && commands[i].get().getGuardExpression();
2316 }
2317
2318 return Command(newCommandIndex, false, actionIndex, actionName, newGuard, newUpdates, this->getFilename(), 0);
2319}
2320
2321storm::jani::Model Program::toJani(bool allVariablesGlobal, std::string suffix) const {
2322 ToJaniConverter converter;
2323 auto janiModel = converter.convert(*this, allVariablesGlobal, {}, suffix);
2324 STORM_LOG_WARN_COND(!converter.labelsWereRenamed(), "Labels were renamed in PRISM-to-JANI conversion, but the mapping is not stored.");
2325 STORM_LOG_WARN_COND(!converter.rewardModelsWereRenamed(), "Rewardmodels were renamed in PRISM-to-JANI conversion, but the mapping is not stored.");
2326 return janiModel;
2327}
2328
2329std::pair<storm::jani::Model, std::vector<storm::jani::Property>> Program::toJani(std::vector<storm::jani::Property> const& properties, bool allVariablesGlobal,
2330 std::string suffix) const {
2331 ToJaniConverter converter;
2332 std::set<storm::expressions::Variable> variablesToMakeGlobal;
2333 if (!allVariablesGlobal) {
2334 for (auto const& prop : properties) {
2335 auto vars = prop.getUsedVariablesAndConstants();
2336 variablesToMakeGlobal.insert(vars.begin(), vars.end());
2337 }
2338 }
2339 auto janiModel = converter.convert(*this, allVariablesGlobal, variablesToMakeGlobal, suffix);
2340 std::vector<storm::jani::Property> newProperties;
2341 if (converter.labelsWereRenamed() || converter.rewardModelsWereRenamed()) {
2342 newProperties = converter.applyRenaming(properties);
2343 } else {
2344 newProperties = properties; // Nothing to be done here. Notice that the copy operation is suboptimal.
2345 }
2346 return std::make_pair(janiModel, newProperties);
2347}
2348
2349uint64_t Program::getHighestCommandIndex() const {
2350 uint64_t highest = 0;
2351 for (auto const& m : getModules()) {
2352 for (auto const& c : m.getCommands()) {
2353 highest = std::max(highest, c.getGlobalIndex());
2354 }
2355 }
2356 return highest;
2357}
2358
2359storm::expressions::ExpressionManager& Program::getManager() const {
2360 return *this->manager;
2361}
2362
2363void Program::createMissingInitialValues() {
2364 for (auto& variable : globalBooleanVariables) {
2365 variable.createMissingInitialValue();
2366 }
2367 for (auto& variable : globalIntegerVariables) {
2368 variable.createMissingInitialValue();
2369 }
2370}
2371
2372std::ostream& operator<<(std::ostream& out, Program::ModelType const& type) {
2373 switch (type) {
2374 case Program::ModelType::UNDEFINED:
2375 out << "undefined";
2376 break;
2377 case Program::ModelType::DTMC:
2378 out << "dtmc";
2379 break;
2380 case Program::ModelType::CTMC:
2381 out << "ctmc";
2382 break;
2383 case Program::ModelType::MDP:
2384 out << "mdp";
2385 break;
2386 case Program::ModelType::CTMDP:
2387 out << "ctmdp";
2388 break;
2389 case Program::ModelType::MA:
2390 out << "ma";
2391 break;
2392 case Program::ModelType::POMDP:
2393 out << "pomdp";
2394 break;
2395 case Program::ModelType::PTA:
2396 out << "pta";
2397 break;
2398 case Program::ModelType::SMG:
2399 out << "smg";
2400 break;
2401 }
2402 return out;
2403}
2404
2405std::ostream& operator<<(std::ostream& stream, Program const& program) {
2406 stream << program.getModelType() << '\n';
2407 for (auto const& constant : program.getConstants()) {
2408 stream << constant << '\n';
2409 }
2410 stream << '\n';
2411
2412 for (auto const& player : program.getPlayers()) {
2413 stream << player << '\n';
2414 }
2415
2416 for (auto const& variable : program.getGlobalBooleanVariables()) {
2417 stream << "global " << variable << '\n';
2418 }
2419 for (auto const& variable : program.getGlobalIntegerVariables()) {
2420 stream << "global " << variable << '\n';
2421 }
2422 stream << '\n';
2423
2424 for (auto const& formula : program.getFormulas()) {
2425 stream << formula << '\n';
2426 }
2427 stream << '\n';
2428
2429 for (auto const& module : program.getModules()) {
2430 stream << module << '\n';
2431 }
2432
2433 for (auto const& rewardModel : program.getRewardModels()) {
2434 stream << rewardModel << '\n';
2435 }
2436
2437 for (auto const& label : program.getLabels()) {
2438 stream << label << '\n';
2439 }
2440
2441 if (program.hasInitialConstruct()) {
2442 stream << program.getInitialConstruct() << '\n';
2443 }
2444
2445 if (program.specifiesSystemComposition()) {
2446 stream << program.getSystemCompositionConstruct();
2447 }
2448
2449 return stream;
2450}
2451
2452} // namespace prism
2453} // namespace storm
bool isInitialized() const
Checks whether the object encapsulates a base-expression.
This class is responsible for managing a set of typed variables and all expressions using these varia...
bool isBooleanType() const
Checks whether this type is a boolean type.
Definition Type.cpp:178
bool isRationalType() const
Checks whether this type is a rational type.
Definition Type.cpp:214
Type const & getType() const
Retrieves the type of the variable.
Definition Variable.cpp:50
std::string const & getName() const
Retrieves the name of the variable.
Definition Variable.cpp:46
std::size_t getNumberOfUpdates() const
Retrieves the number of updates associated with this command.
Definition Command.cpp:39
virtual boost::any accept(CompositionVisitor &visitor, boost::any const &data) const =0
virtual boost::any visit(InterleavingParallelComposition const &composition, boost::any const &data) override
Definition Program.cpp:111
virtual boost::any visit(SynchronizingParallelComposition const &composition, boost::any const &data) override
Definition Program.cpp:98
void check(Composition const &composition)
Definition Program.cpp:37
virtual boost::any visit(RestrictedParallelComposition const &composition, boost::any const &data) override
Definition Program.cpp:124
virtual boost::any visit(ModuleComposition const &composition, boost::any const &) override
Definition Program.cpp:44
virtual boost::any visit(HidingComposition const &composition, boost::any const &data) override
Definition Program.cpp:80
CompositionValidityChecker(storm::prism::Program const &program)
Definition Program.cpp:33
virtual boost::any visit(RenamingComposition const &composition, boost::any const &data) override
Definition Program.cpp:56
storm::expressions::Variable const & getExpressionVariable() const
Retrieves the expression variable associated with this constant.
Definition Constant.cpp:26
storm::expressions::Type const & getType() const
Retrieves the type of the constant.
Definition Constant.cpp:22
storm::expressions::Expression const & getExpression() const
Retrieves the expression that defines the constant.
Definition Constant.cpp:34
std::set< std::string > const & getActionsToHide() const
Composition const & getSubcomposition() const
std::string const & getModuleName() const
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 Module.cpp:173
bool isRenamedFromModule() const
Retrieves whether this module was created from another module via renaming.
Definition Module.cpp:163
std::set< uint_fast64_t > const & getSynchronizingActionIndices() const
Retrieves the set of synchronizing action indices present in this module.
Definition Module.cpp:145
Composition const & getLeftSubcomposition() const
Composition const & getRightSubcomposition() const
ModelType getModelType() const
Retrieves the model type of the model.
Definition Program.cpp:247
std::vector< RewardModel > const & getRewardModels() const
Retrieves the reward models of the program.
Definition Program.cpp:808
std::vector< Player > const & getPlayers() const
Retrieves the players of the program.
Definition Program.cpp:562
std::vector< BooleanVariable > const & getGlobalBooleanVariables() const
Retrieves the global boolean variables of the program.
Definition Program.cpp:482
ModelType
An enum for the different model types.
Definition Program.h:37
bool hasAction(std::string const &actionName) const
Retrieves whether the program has an action with the given name.
Definition Program.cpp:754
std::vector< Module > const & getModules() const
Retrieves all modules of the program.
Definition Program.cpp:629
Module const & getModule(uint_fast64_t index) const
Retrieves the module with the given index.
Definition Program.cpp:615
uint_fast64_t getActionIndex(std::string const &actionName) const
Retrieves the index of the action with the given name.
Definition Program.cpp:748
std::set< uint_fast64_t > const & getModuleIndicesByActionIndex(uint_fast64_t actionIndex) const
Retrieves the indices of all modules within this program that contain commands that are labelled with...
Definition Program.cpp:768
SystemCompositionConstruct const & getSystemCompositionConstruct() const
If the program specifies a system composition construct, this method retrieves it.
Definition Program.cpp:714
Program substituteConstants() const
Substitutes all constants appearing in the expressions of the program by their defining expressions.
Definition Program.cpp:1026
bool hasModule(std::string const &moduleName) const
Retrieves whether the program has a module with the given name.
Definition Program.cpp:619
std::vector< Constant > const & getConstants() const
Retrieves all constants defined in the program.
Definition Program.cpp:402
std::vector< IntegerVariable > const & getGlobalIntegerVariables() const
Retrieves the global integer variables of the program.
Definition Program.cpp:486
std::size_t getNumberOfModules() const
Retrieves the number of modules in the program.
Definition Program.cpp:611
bool hasInitialConstruct() const
Retrieves whether the program specifies an initial construct.
Definition Program.cpp:645
bool specifiesSystemComposition() const
Retrieves whether the program specifies a system composition in terms of process algebra operations o...
Definition Program.cpp:710
std::vector< Label > const & getLabels() const
Retrieves all labels that are defined by the probabilitic program.
Definition Program.cpp:833
std::vector< Formula > const & getFormulas() const
Retrieves the formulas defined in the program.
Definition Program.cpp:558
Composition const & getSubcomposition() const
std::map< std::string, std::string > const & getActionRenaming() const
std::set< std::string > const & getSynchronizingActions() const
storm::jani::Model convert(storm::prism::Program const &program, bool allVariablesGlobal=true, std::set< storm::expressions::Variable > const &variablesToMakeGlobal={}, std::string suffix="")
storm::jani::Property applyRenaming(storm::jani::Property const &property) const
The base class for all model references.
Definition SmtSolver.h:31
virtual bool getBooleanValue(storm::expressions::Variable const &variable) const =0
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:18
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
#define STORM_LOG_WARN_COND(cond, message)
Definition macros.h:38
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
Expression iff(Expression const &first, Expression const &second)
Expression implies(Expression const &first, Expression const &second)
storm::expressions::Expression substituteJaniExpression(storm::expressions::Expression const &expression, std::map< storm::expressions::Variable, storm::expressions::Expression > const &identifierToExpressionMap, bool const substituteTranscendentalNumbers)
ModelType getModelType(std::string const &type)
Definition ModelType.cpp:9
bool hasModule()
Returns true if the given module is registered.
SettingsManager const & manager()
Retrieves the settings manager.
PlayerIndex const INVALID_PLAYER_INDEX
Definition PlayerIndex.h:8
uint64_t PlayerIndex
Definition PlayerIndex.h:7
boost::container::flat_set< Key, std::less< Key >, boost::container::new_allocator< Key > > FlatSet
Redefinition of flat_set was needed, because from Boost 1.70 on the default allocator is set to void.
Definition BoostTypes.h:13
LabParser.cpp.
Definition cli.cpp:18