Storm 1.10.0.1
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) {
211 if (getModuleIndicesByActionIndex(syncAction).size() > 1) {
212 possiblySynchronizingActionIndices.insert(syncAction);
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::hasIntervalUpdates() const {
711 for (auto const& module : this->modules) {
712 for (auto const& command : module.getCommands()) {
713 for (auto const& update : command.getUpdates()) {
714 if (update.isLikelihoodInterval()) {
715 return true;
716 }
717 }
718 }
719 }
720 return false;
721}
722
723bool Program::specifiesSystemComposition() const {
724 return static_cast<bool>(systemCompositionConstruct);
725}
726
727SystemCompositionConstruct const& Program::getSystemCompositionConstruct() const {
728 return systemCompositionConstruct.get();
729}
730
731boost::optional<SystemCompositionConstruct> Program::getOptionalSystemCompositionConstruct() const {
732 return systemCompositionConstruct;
733}
734
735std::shared_ptr<Composition> Program::getDefaultSystemComposition() const {
736 std::shared_ptr<Composition> current = std::make_shared<ModuleComposition>(this->modules.front().getName());
737
738 for (uint_fast64_t index = 1; index < this->modules.size(); ++index) {
739 std::shared_ptr<Composition> newComposition =
740 std::make_shared<SynchronizingParallelComposition>(current, std::make_shared<ModuleComposition>(this->modules[index].getName()));
741 current = newComposition;
742 }
743
744 return current;
745}
746
747std::set<std::string> const& Program::getActions() const {
748 return this->actions;
749}
750
751std::set<uint_fast64_t> const& Program::getSynchronizingActionIndices() const {
752 return this->synchronizingActionIndices;
753}
754
755std::string const& Program::getActionName(uint_fast64_t actionIndex) const {
756 auto const& indexNamePair = this->indexToActionMap.find(actionIndex);
757 STORM_LOG_THROW(indexNamePair != this->indexToActionMap.end(), storm::exceptions::InvalidArgumentException, "Unknown action index " << actionIndex << ".");
758 return indexNamePair->second;
759}
760
761uint_fast64_t Program::getActionIndex(std::string const& actionName) const {
762 auto const& nameIndexPair = this->actionToIndexMap.find(actionName);
763 STORM_LOG_THROW(nameIndexPair != this->actionToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Unknown action name '" << actionName << "'.");
764 return nameIndexPair->second;
765}
766
767bool Program::hasAction(std::string const& actionName) const {
768 return this->actionToIndexMap.find(actionName) != this->actionToIndexMap.end();
769}
770
771bool Program::hasAction(uint_fast64_t const& actionIndex) const {
772 return this->indexToActionMap.find(actionIndex) != this->indexToActionMap.end();
773}
774
775std::set<uint_fast64_t> const& Program::getModuleIndicesByAction(std::string const& action) const {
776 auto const& nameIndexPair = this->actionToIndexMap.find(action);
777 STORM_LOG_THROW(nameIndexPair != this->actionToIndexMap.end(), storm::exceptions::OutOfRangeException, "Action name '" << action << "' does not exist.");
778 return this->getModuleIndicesByActionIndex(nameIndexPair->second);
779}
780
781std::set<uint_fast64_t> const& Program::getModuleIndicesByActionIndex(uint_fast64_t actionIndex) const {
782 auto const& actionModuleSetPair = this->actionIndicesToModuleIndexMap.find(actionIndex);
783 STORM_LOG_THROW(actionModuleSetPair != this->actionIndicesToModuleIndexMap.end(), storm::exceptions::OutOfRangeException,
784 "Action with index '" << actionIndex << "' does not exist.");
785 return actionModuleSetPair->second;
786}
787
788uint_fast64_t Program::getModuleIndexByVariable(std::string const& variableName) const {
789 auto const& variableNameToModuleIndexPair = this->variableToModuleIndexMap.find(variableName);
790 STORM_LOG_THROW(variableNameToModuleIndexPair != this->variableToModuleIndexMap.end(), storm::exceptions::OutOfRangeException,
791 "Variable '" << variableName << "' does not exist.");
792 return variableNameToModuleIndexPair->second;
793}
794
795std::pair<uint_fast64_t, uint_fast64_t> Program::getModuleCommandIndexByGlobalCommandIndex(uint_fast64_t globalCommandIndex) const {
796 uint_fast64_t moduleIndex = 0;
797 for (auto const& module : modules) {
798 uint_fast64_t commandIndex = 0;
799 for (auto const& command : module.getCommands()) {
800 if (command.getGlobalIndex() == globalCommandIndex) {
801 return std::pair<uint_fast64_t, uint_fast64_t>(moduleIndex, commandIndex);
802 }
803 ++commandIndex;
804 }
805 ++moduleIndex;
806 }
807 // This point should not be reached if the globalCommandIndex is valid
808 STORM_LOG_THROW(false, storm::exceptions::OutOfRangeException, "Global command index '" << globalCommandIndex << "' does not exist.");
809 return std::pair<uint_fast64_t, uint_fast64_t>(0, 0);
810}
811
812bool Program::hasRewardModel() const {
813 return !this->rewardModels.empty();
814}
815
816bool Program::hasRewardModel(std::string const& name) const {
817 auto const& nameIndexPair = this->rewardModelToIndexMap.find(name);
818 return nameIndexPair != this->rewardModelToIndexMap.end();
819}
820
821std::vector<storm::prism::RewardModel> const& Program::getRewardModels() const {
822 return this->rewardModels;
823}
824
825std::size_t Program::getNumberOfRewardModels() const {
826 return this->getRewardModels().size();
827}
828
829storm::prism::RewardModel const& Program::getRewardModel(std::string const& name) const {
830 auto const& nameIndexPair = this->rewardModelToIndexMap.find(name);
831 STORM_LOG_THROW(nameIndexPair != this->rewardModelToIndexMap.end(), storm::exceptions::OutOfRangeException,
832 "Reward model '" << name << "' does not exist.");
833 return this->getRewardModels()[nameIndexPair->second];
834}
835
836RewardModel const& Program::getRewardModel(uint_fast64_t index) const {
837 STORM_LOG_THROW(this->getNumberOfRewardModels() > index, storm::exceptions::OutOfRangeException, "Reward model with index " << index << " does not exist.");
838 return this->rewardModels[index];
839}
840
841bool Program::hasLabel(std::string const& labelName) const {
842 auto it = std::find_if(labels.begin(), labels.end(), [&labelName](storm::prism::Label const& label) { return label.getName() == labelName; });
843 return it != labels.end();
844}
845
846std::vector<Label> const& Program::getLabels() const {
847 return this->labels;
848}
849
850std::vector<storm::expressions::Expression> Program::getAllGuards(bool negated) const {
851 std::vector<storm::expressions::Expression> allGuards;
852 for (auto const& module : modules) {
853 for (auto const& command : module.getCommands()) {
854 allGuards.push_back(negated ? !command.getGuardExpression() : command.getGuardExpression());
855 }
856 }
857 return allGuards;
858}
859
860storm::expressions::Expression const& Program::getLabelExpression(std::string const& label) const {
861 auto const& labelIndexPair = labelToIndexMap.find(label);
862 STORM_LOG_THROW(labelIndexPair != labelToIndexMap.end(), storm::exceptions::InvalidArgumentException,
863 "Cannot retrieve expression for unknown label '" << label << "'.");
864 return this->labels[labelIndexPair->second].getStatePredicateExpression();
865}
866
867std::map<std::string, storm::expressions::Expression> Program::getLabelToExpressionMapping() const {
868 std::map<std::string, storm::expressions::Expression> result;
869 for (auto const& label : labels) {
870 result.emplace(label.getName(), label.getStatePredicateExpression());
871 }
872 return result;
873}
874
875std::size_t Program::getNumberOfLabels() const {
876 return this->getLabels().size();
877}
878
879void Program::addLabel(std::string const& name, storm::expressions::Expression const& statePredicateExpression) {
880 auto it = std::find_if(this->labels.begin(), this->labels.end(), [&name](storm::prism::Label const& label) { return label.getName() == name; });
881 STORM_LOG_THROW(it == this->labels.end(), storm::exceptions::InvalidArgumentException,
882 "Cannot add a label '" << name << "', because a label with that name already exists.");
883 this->labels.emplace_back(name, statePredicateExpression);
884}
885
886void Program::removeLabel(std::string const& name) {
887 auto it = std::find_if(this->labels.begin(), this->labels.end(), [&name](storm::prism::Label const& label) { return label.getName() == name; });
888 STORM_LOG_THROW(it != this->labels.end(), storm::exceptions::InvalidArgumentException, "Canno remove unknown label '" << name << "'.");
889 this->labels.erase(it);
890}
891
892void Program::removeRewardModels() {
893 this->rewardModels.clear();
894 this->rewardModelToIndexMap.clear();
895}
896
897void Program::filterLabels(std::set<std::string> const& labelSet) {
898 std::vector<storm::prism::Label> newLabels;
899 newLabels.reserve(labelSet.size());
900
901 // Now filter the labels by the criterion whether or not their name appears in the given label set.
902 for (auto it = labels.begin(), ite = labels.end(); it != ite; ++it) {
903 auto setIt = labelSet.find(it->getName());
904 if (setIt != labelSet.end()) {
905 newLabels.emplace_back(*it);
906 }
907 }
908
909 // Move the new labels in place.
910 this->labels = std::move(newLabels);
911}
912
913std::vector<ObservationLabel> const& Program::getObservationLabels() const {
914 return this->observationLabels;
915}
916
917std::size_t Program::getNumberOfObservationLabels() const {
918 return this->observationLabels.size();
919}
920
921storm::storage::BitVector const& Program::getPossiblySynchronizingCommands() const {
922 return possiblySynchronizingCommands;
923}
924
925Program Program::restrictCommands(storm::storage::FlatSet<uint_fast64_t> const& indexSet) const {
926 std::vector<storm::prism::Module> newModules;
927 newModules.reserve(this->getNumberOfModules());
928
929 for (auto const& module : this->getModules()) {
930 newModules.push_back(module.restrictCommands(indexSet));
931 }
932
933 return Program(this->manager, this->getModelType(), this->getConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(),
934 this->getFormulas(), this->getPlayers(), newModules, this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(),
935 this->getObservationLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
936}
937
938void Program::createMappings() {
939 // Build the mappings for constants, global variables, formulas, modules, reward models and labels.
940 for (uint_fast64_t constantIndex = 0; constantIndex < this->getNumberOfConstants(); ++constantIndex) {
941 this->constantToIndexMap[this->getConstants()[constantIndex].getName()] = constantIndex;
942 }
943 for (uint_fast64_t globalVariableIndex = 0; globalVariableIndex < this->getNumberOfGlobalBooleanVariables(); ++globalVariableIndex) {
944 this->globalBooleanVariableToIndexMap[this->getGlobalBooleanVariables()[globalVariableIndex].getName()] = globalVariableIndex;
945 }
946 for (uint_fast64_t globalVariableIndex = 0; globalVariableIndex < this->getNumberOfGlobalIntegerVariables(); ++globalVariableIndex) {
947 this->globalIntegerVariableToIndexMap[this->getGlobalIntegerVariables()[globalVariableIndex].getName()] = globalVariableIndex;
948 }
949 for (uint_fast64_t formulaIndex = 0; formulaIndex < this->getNumberOfFormulas(); ++formulaIndex) {
950 this->formulaToIndexMap[this->getFormulas()[formulaIndex].getName()] = formulaIndex;
951 }
952 for (uint_fast64_t labelIndex = 0; labelIndex < this->getNumberOfLabels(); ++labelIndex) {
953 this->labelToIndexMap[this->getLabels()[labelIndex].getName()] = labelIndex;
954 }
955 for (uint_fast64_t moduleIndex = 0; moduleIndex < this->getNumberOfModules(); ++moduleIndex) {
956 this->moduleToIndexMap[this->getModules()[moduleIndex].getName()] = moduleIndex;
957 }
958 for (storm::storage::PlayerIndex playerIndex = 0; playerIndex < this->getNumberOfPlayers(); ++playerIndex) {
959 this->playerToIndexMap[this->getPlayers()[playerIndex].getName()] = playerIndex;
960 }
961 for (uint_fast64_t rewardModelIndex = 0; rewardModelIndex < this->getNumberOfRewardModels(); ++rewardModelIndex) {
962 this->rewardModelToIndexMap[this->getRewardModels()[rewardModelIndex].getName()] = rewardModelIndex;
963 }
964
965 for (auto const& actionIndexPair : this->getActionNameToIndexMapping()) {
966 this->actions.insert(actionIndexPair.first);
967 this->indexToActionMap.emplace(actionIndexPair.second, actionIndexPair.first);
968
969 // Only let all non-zero indices be synchronizing.
970 if (actionIndexPair.second != 0) {
971 this->synchronizingActionIndices.insert(actionIndexPair.second);
972 this->actionIndicesToModuleIndexMap[actionIndexPair.second] = std::set<uint_fast64_t>();
973 }
974 }
975
976 // Build the mapping from action names to module indices so that the lookup can later be performed quickly.
977 for (unsigned int moduleIndex = 0; moduleIndex < this->getNumberOfModules(); moduleIndex++) {
978 Module const& module = this->getModule(moduleIndex);
979
980 for (auto const& actionIndex : module.getSynchronizingActionIndices()) {
981 this->actionIndicesToModuleIndexMap[actionIndex].insert(moduleIndex);
982 }
983
984 // Put in the appropriate entries for the mapping from variable names to module index.
985 for (auto const& booleanVariable : module.getBooleanVariables()) {
986 this->variableToModuleIndexMap[booleanVariable.getName()] = moduleIndex;
987 }
988 for (auto const& integerVariable : module.getIntegerVariables()) {
989 this->variableToModuleIndexMap[integerVariable.getName()] = moduleIndex;
990 }
991 for (auto const& clockVariable : module.getClockVariables()) {
992 this->variableToModuleIndexMap[clockVariable.getName()] = moduleIndex;
993 }
994 }
995}
996
997Program Program::defineUndefinedConstants(std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) const {
998 // For sanity checking, we keep track of all undefined constants that we define in the course of this procedure.
999 std::set<storm::expressions::Variable> definedUndefinedConstants;
1000
1001 std::vector<Constant> newConstants;
1002 newConstants.reserve(this->getNumberOfConstants());
1003 for (auto const& constant : this->getConstants()) {
1004 // If the constant is already defined, we need to replace the appearances of undefined constants in its
1005 // defining expression
1006 if (constant.isDefined()) {
1007 // Make sure we are not trying to define an already defined constant.
1008 STORM_LOG_THROW(constantDefinitions.find(constant.getExpressionVariable()) == constantDefinitions.end(),
1009 storm::exceptions::InvalidArgumentException, "Illegally defining already defined constant '" << constant.getName() << "'.");
1010
1011 // Now replace the occurrences of undefined constants in its defining expression.
1012 newConstants.emplace_back(constant.getExpressionVariable(), constant.getExpression().substitute(constantDefinitions), constant.getFilename(),
1013 constant.getLineNumber());
1014 } else {
1015 auto const& variableExpressionPair = constantDefinitions.find(constant.getExpressionVariable());
1016
1017 // If the constant is not defined by the mapping, we leave it like it is.
1018 if (variableExpressionPair == constantDefinitions.end()) {
1019 newConstants.emplace_back(constant);
1020 } else {
1021 // Otherwise, we add it to the defined constants and assign it the appropriate expression.
1022 definedUndefinedConstants.insert(constant.getExpressionVariable());
1023
1024 // Make sure the type of the constant is correct.
1025 STORM_LOG_THROW(variableExpressionPair->second.getType() == constant.getType(), storm::exceptions::InvalidArgumentException,
1026 "Illegal type of expression defining constant '" << constant.getName() << "'.");
1027
1028 // Now create the defined constant.
1029 newConstants.emplace_back(constant.getExpressionVariable(), variableExpressionPair->second, constant.getFilename(), constant.getLineNumber());
1030 }
1031 }
1032 }
1033
1034 return Program(this->manager, this->getModelType(), newConstants, this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(),
1035 this->getPlayers(), this->getModules(), this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(),
1036 this->getObservationLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
1037}
1038
1039Program Program::substituteConstants() const {
1040 return substituteConstantsFormulas(true, false);
1041}
1042
1043Program Program::substituteFormulas() const {
1044 return substituteConstantsFormulas(false, true);
1045}
1046
1047Program Program::substituteNonStandardPredicates() const {
1048 // TODO support in constants, initial construct, and rewards
1049
1050 std::vector<Formula> newFormulas;
1051 newFormulas.reserve(this->getNumberOfFormulas());
1052 for (auto const& oldFormula : this->getFormulas()) {
1053 newFormulas.emplace_back(oldFormula.substituteNonStandardPredicates());
1054 }
1055
1056 std::vector<BooleanVariable> newBooleanVariables;
1057 newBooleanVariables.reserve(this->getNumberOfGlobalBooleanVariables());
1058 for (auto const& booleanVariable : this->getGlobalBooleanVariables()) {
1059 newBooleanVariables.emplace_back(booleanVariable.substituteNonStandardPredicates());
1060 }
1061
1062 std::vector<IntegerVariable> newIntegerVariables;
1063 newBooleanVariables.reserve(this->getNumberOfGlobalIntegerVariables());
1064 for (auto const& integerVariable : this->getGlobalIntegerVariables()) {
1065 newIntegerVariables.emplace_back(integerVariable.substituteNonStandardPredicates());
1066 }
1067
1068 std::vector<Module> newModules;
1069 newModules.reserve(this->getNumberOfModules());
1070 for (auto const& module : this->getModules()) {
1071 newModules.emplace_back(module.substituteNonStandardPredicates());
1072 }
1073
1074 std::vector<Label> newLabels;
1075 newLabels.reserve(this->getNumberOfLabels());
1076 for (auto const& label : this->getLabels()) {
1077 newLabels.emplace_back(label.substituteNonStandardPredicates());
1078 }
1079
1080 std::vector<ObservationLabel> newObservationLabels;
1081 newObservationLabels.reserve(this->getNumberOfObservationLabels());
1082 for (auto const& label : this->getObservationLabels()) {
1083 newObservationLabels.emplace_back(label.substituteNonStandardPredicates());
1084 }
1085
1086 return Program(this->manager, this->getModelType(), this->getConstants(), newBooleanVariables, newIntegerVariables, newFormulas, this->getPlayers(),
1087 newModules, this->getActionNameToIndexMapping(), this->getRewardModels(), newLabels, newObservationLabels, initialConstruct,
1088 this->getOptionalSystemCompositionConstruct(), prismCompatibility);
1089}
1090
1091Program Program::substituteConstantsFormulas(bool substituteConstants, bool substituteFormulas) const {
1092 // Formulas need to be substituted first. otherwise, constants appearing in formula expressions can not be handled properly
1093 if (substituteConstants && substituteFormulas) {
1094 return this->substituteFormulas().substituteConstants();
1095 }
1096
1097 // We start by creating the appropriate substitution.
1098 std::map<storm::expressions::Variable, storm::expressions::Expression> substitution =
1099 getConstantsFormulasSubstitution(substituteConstants, substituteFormulas);
1100
1101 std::vector<Constant> newConstants;
1102 newConstants.reserve(this->getNumberOfConstants());
1103 for (auto const& oldConstant : this->getConstants()) {
1104 newConstants.push_back(oldConstant.substitute(substitution));
1105 }
1106
1107 std::vector<Formula> newFormulas;
1108 newFormulas.reserve(this->getNumberOfFormulas());
1109 for (auto const& oldFormula : this->getFormulas()) {
1110 newFormulas.emplace_back(oldFormula.substitute(substitution));
1111 }
1112
1113 std::vector<BooleanVariable> newBooleanVariables;
1114 newBooleanVariables.reserve(this->getNumberOfGlobalBooleanVariables());
1115 for (auto const& booleanVariable : this->getGlobalBooleanVariables()) {
1116 newBooleanVariables.emplace_back(booleanVariable.substitute(substitution));
1117 }
1118
1119 std::vector<IntegerVariable> newIntegerVariables;
1120 newBooleanVariables.reserve(this->getNumberOfGlobalIntegerVariables());
1121 for (auto const& integerVariable : this->getGlobalIntegerVariables()) {
1122 newIntegerVariables.emplace_back(integerVariable.substitute(substitution));
1123 }
1124
1125 std::vector<Module> newModules;
1126 newModules.reserve(this->getNumberOfModules());
1127 for (auto const& module : this->getModules()) {
1128 if (module.isRenamedFromModule()) {
1129 // The renaming needs to be applied to the substitution as well.
1130 auto renamedSubstitution = getSubstitutionForRenamedModule(module, substitution);
1131 newModules.emplace_back(module.substitute(renamedSubstitution));
1132 } else {
1133 newModules.emplace_back(module.substitute(substitution));
1134 }
1135 }
1136
1137 std::vector<RewardModel> newRewardModels;
1138 newRewardModels.reserve(this->getNumberOfRewardModels());
1139 for (auto const& rewardModel : this->getRewardModels()) {
1140 newRewardModels.emplace_back(rewardModel.substitute(substitution));
1141 }
1142
1143 boost::optional<storm::prism::InitialConstruct> newInitialConstruct;
1144 if (this->hasInitialConstruct()) {
1145 newInitialConstruct = this->getInitialConstruct().substitute(substitution);
1146 }
1147
1148 std::vector<Label> newLabels;
1149 newLabels.reserve(this->getNumberOfLabels());
1150 for (auto const& label : this->getLabels()) {
1151 newLabels.emplace_back(label.substitute(substitution));
1152 }
1153
1154 std::vector<ObservationLabel> newObservationLabels;
1155 newObservationLabels.reserve(this->getNumberOfObservationLabels());
1156 for (auto const& label : this->getObservationLabels()) {
1157 newObservationLabels.emplace_back(label.substitute(substitution));
1158 }
1159
1160 return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, this->getPlayers(), newModules,
1161 this->getActionNameToIndexMapping(), newRewardModels, newLabels, newObservationLabels, newInitialConstruct,
1162 this->getOptionalSystemCompositionConstruct(), prismCompatibility);
1163}
1164
1165Program Program::labelUnlabelledCommands(std::map<uint64_t, std::string> const& nameSuggestions) const {
1166 for (auto const& entry : nameSuggestions) {
1167 STORM_LOG_THROW(!hasAction(entry.second), storm::exceptions::InvalidArgumentException, "Cannot suggest names already in the program.");
1168 }
1169 std::vector<Module> newModules;
1170 std::vector<RewardModel> newRewardModels;
1171 std::map<std::string, uint64_t> newActionNameToIndexMapping = getActionNameToIndexMapping();
1172
1173 uint64_t oldId = 1;
1174 if (!getSynchronizingActionIndices().empty()) {
1175 oldId = *(getSynchronizingActionIndices().rbegin()) + 1;
1176 }
1177 uint64_t newId = oldId;
1178 for (auto const& module : modules) {
1179 newModules.push_back(module.labelUnlabelledCommands(nameSuggestions, newId, newActionNameToIndexMapping));
1180 }
1181
1182 std::vector<std::pair<uint64_t, std::string>> newActionNames;
1183 for (auto const& entry : newActionNameToIndexMapping) {
1184 if (!hasAction(entry.first)) {
1185 newActionNames.emplace_back(entry.second, entry.first);
1186 }
1187 }
1188 for (auto const& rewardModel : rewardModels) {
1189 newRewardModels.push_back(rewardModel.labelUnlabelledCommands(newActionNames));
1190 }
1191
1192 return Program(this->manager, this->getModelType(), this->getConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(),
1193 this->getFormulas(), this->getPlayers(), newModules, newActionNameToIndexMapping, newRewardModels, this->getLabels(),
1194 this->getObservationLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
1195}
1196
1197Program Program::replaceVariableInitializationByInitExpression() const {
1198 std::vector<BooleanVariable> newBooleanVariables = globalBooleanVariables;
1199 for (auto& newVar : newBooleanVariables) {
1200 newVar.setInitialValueExpression(storm::expressions::Expression());
1201 }
1202
1203 std::vector<IntegerVariable> newIntegerVariables = globalIntegerVariables;
1204 for (auto& newVar : newIntegerVariables) {
1205 newVar.setInitialValueExpression(storm::expressions::Expression());
1206 }
1207
1208 std::vector<Module> newModules = this->getModules();
1209 for (auto& module : newModules) {
1210 module.removeVariableInitialization();
1211 }
1212
1213 return Program(this->manager, this->getModelType(), this->getConstants(), newBooleanVariables, newIntegerVariables, this->getFormulas(), this->getPlayers(),
1214 newModules, this->actionToIndexMap, this->getRewardModels(), this->getLabels(), this->getObservationLabels(),
1215 InitialConstruct(this->getInitialStatesExpression()), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
1216}
1217
1218Program Program::replaceConstantByVariable(Constant const& c, expressions::Expression const& lowerBound, expressions::Expression const& upperBound,
1219 bool observable) const {
1220 STORM_LOG_THROW(this->getModelType() == ModelType::POMDP || observable, storm::exceptions::InvalidArgumentException,
1221 "Variables can only be unobservable in POMDPs");
1222 std::vector<BooleanVariable> newBooleanVariables = globalBooleanVariables;
1223 std::vector<IntegerVariable> newIntegerVariables = globalIntegerVariables;
1224 std::vector<Constant> newConstants = constants;
1225 auto newEnd = std::remove(newConstants.begin(), newConstants.end(), c);
1226 newConstants.erase(newEnd, newConstants.end()); // Erase is necessary based on Erase-remove idiom
1227 // The following throw is moved here as this is cheaper.
1228 STORM_LOG_THROW(newConstants.size() == constants.size() - 1, exceptions::InvalidArgumentException, "Can only replace a constant if it is present.");
1229 if (c.getType().isBooleanType()) {
1230 newBooleanVariables.emplace_back(c.getExpressionVariable(), c.getExpression(), observable);
1231 } else {
1232 newIntegerVariables.emplace_back(c.getExpressionVariable(), lowerBound, upperBound, c.getExpression(), observable);
1233 }
1234 return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, this->getFormulas(), this->getPlayers(),
1235 modules, this->actionToIndexMap, this->getRewardModels(), this->getLabels(), this->getObservationLabels(),
1236 this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
1237}
1238
1239void Program::checkValidity(Program::ValidityCheckLevel lvl) const {
1240 // Start by checking the constant declarations.
1241 std::set<storm::expressions::Variable> all;
1242 std::set<storm::expressions::Variable> allGlobals;
1243 std::set<storm::expressions::Variable> globalVariables;
1244 std::set<storm::expressions::Variable> constants;
1245 for (auto const& constant : this->getConstants()) {
1246 // Check defining expressions of defined constants.
1247 if (constant.isDefined()) {
1248 std::set<storm::expressions::Variable> containedVariables = constant.getExpression().getVariables();
1249 std::set<storm::expressions::Variable> illegalVariables;
1250 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1251 std::inserter(illegalVariables, illegalVariables.begin()));
1252 bool isValid = illegalVariables.empty();
1253
1254 if (!isValid) {
1255 std::vector<std::string> illegalVariableNames;
1256 for (auto const& var : illegalVariables) {
1257 illegalVariableNames.push_back(var.getName());
1258 }
1259 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1260 "Error in " << constant.getFilename() << ", line " << constant.getLineNumber()
1261 << ": defining expression refers to unknown identifiers: " << boost::algorithm::join(illegalVariableNames, ",")
1262 << ".");
1263 }
1264 }
1265
1266 // Record the new identifier for future checks.
1267 constants.insert(constant.getExpressionVariable());
1268 all.insert(constant.getExpressionVariable());
1269 allGlobals.insert(constant.getExpressionVariable());
1270 }
1271
1272 // Now we check the variable declarations. We start with the global variables.
1273 std::set<storm::expressions::Variable> variables;
1274 for (auto const& variable : this->getGlobalBooleanVariables()) {
1275 if (variable.hasInitialValue()) {
1276 STORM_LOG_THROW(!this->hasInitialConstruct(), storm::exceptions::WrongFormatException,
1277 "Error for " << variable.getName() << " (" << variable.getFilename() << ", line " << variable.getLineNumber()
1278 << "): illegal to specify initial value if an initial construct is present.");
1279
1280 // Check the initial value of the variable.
1281 std::set<storm::expressions::Variable> containedVariables = variable.getInitialValueExpression().getVariables();
1282 std::set<storm::expressions::Variable> illegalVariables;
1283 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1284 std::inserter(illegalVariables, illegalVariables.begin()));
1285 bool isValid = illegalVariables.empty();
1286
1287 if (!isValid) {
1288 std::vector<std::string> illegalVariableNames;
1289 for (auto const& var : illegalVariables) {
1290 illegalVariableNames.push_back(var.getName());
1291 }
1292 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1293 "Error in " << variable.getFilename() << ", line " << variable.getLineNumber()
1294 << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",")
1295 << ".");
1296 }
1297 }
1298
1299 // Record the new identifier for future checks.
1300 variables.insert(variable.getExpressionVariable());
1301 all.insert(variable.getExpressionVariable());
1302 allGlobals.insert(variable.getExpressionVariable());
1303 globalVariables.insert(variable.getExpressionVariable());
1304 }
1305 for (auto const& variable : this->getGlobalIntegerVariables()) {
1306 // Check that bound expressions of the range.
1307 if (variable.hasLowerBoundExpression()) {
1308 std::set<storm::expressions::Variable> containedVariables = variable.getLowerBoundExpression().getVariables();
1309 std::set<storm::expressions::Variable> illegalVariables;
1310 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1311 std::inserter(illegalVariables, illegalVariables.begin()));
1312 bool isValid = illegalVariables.empty();
1313
1314 if (!isValid) {
1315 std::vector<std::string> illegalVariableNames;
1316 for (auto const& var : illegalVariables) {
1317 illegalVariableNames.push_back(var.getName());
1318 }
1319 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1320 "Error in " << variable.getFilename() << ", line " << variable.getLineNumber()
1321 << ": lower bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",")
1322 << ".");
1323 }
1324 }
1325
1326 if (variable.hasUpperBoundExpression()) {
1327 std::set<storm::expressions::Variable> containedVariables = variable.getUpperBoundExpression().getVariables();
1328 std::set<storm::expressions::Variable> illegalVariables;
1329 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1330 std::inserter(illegalVariables, illegalVariables.begin()));
1331 bool isValid = illegalVariables.empty();
1332 if (!isValid) {
1333 std::vector<std::string> illegalVariableNames;
1334 for (auto const& var : illegalVariables) {
1335 illegalVariableNames.push_back(var.getName());
1336 }
1337 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1338 "Error in " << variable.getFilename() << ", line " << variable.getLineNumber()
1339 << ": upper bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",")
1340 << ".");
1341 }
1342 }
1343
1344 if (variable.hasInitialValue()) {
1345 STORM_LOG_THROW(!this->hasInitialConstruct(), storm::exceptions::WrongFormatException,
1346 "Error for " << variable.getName() << " (" << variable.getFilename() << ", line " << variable.getLineNumber()
1347 << "): illegal to specify initial value if an initial construct is present.");
1348
1349 // Check the initial value of the variable.
1350 std::set<storm::expressions::Variable> containedVariables = variable.getInitialValueExpression().getVariables();
1351 std::set<storm::expressions::Variable> illegalVariables;
1352 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1353 std::inserter(illegalVariables, illegalVariables.begin()));
1354 bool isValid = illegalVariables.empty();
1355 if (!isValid) {
1356 std::vector<std::string> illegalVariableNames;
1357 for (auto const& var : illegalVariables) {
1358 illegalVariableNames.push_back(var.getName());
1359 }
1360 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1361 "Error in " << variable.getFilename() << ", line " << variable.getLineNumber()
1362 << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",")
1363 << ".");
1364 }
1365 }
1366
1367 // Record the new identifier for future checks.
1368 variables.insert(variable.getExpressionVariable());
1369 all.insert(variable.getExpressionVariable());
1370 allGlobals.insert(variable.getExpressionVariable());
1371 globalVariables.insert(variable.getExpressionVariable());
1372 }
1373
1374 // Now go through the variables of the modules.
1375 for (auto const& module : this->getModules()) {
1376 for (auto const& variable : module.getBooleanVariables()) {
1377 if (variable.hasInitialValue()) {
1378 STORM_LOG_THROW(!this->hasInitialConstruct(), storm::exceptions::WrongFormatException,
1379 "Error for " << module.getName() << "." << variable.getName() << " (" << variable.getFilename() << ", line "
1380 << variable.getLineNumber() << "): illegal to specify initial value if an initial construct is present.");
1381
1382 // Check the initial value of the variable.
1383 std::set<storm::expressions::Variable> containedVariables = variable.getInitialValueExpression().getVariables();
1384 std::set<storm::expressions::Variable> illegalVariables;
1385 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1386 std::inserter(illegalVariables, illegalVariables.begin()));
1387 bool isValid = illegalVariables.empty();
1388 if (!isValid) {
1389 std::vector<std::string> illegalVariableNames;
1390 for (auto const& var : illegalVariables) {
1391 illegalVariableNames.push_back(var.getName());
1392 }
1394 isValid, storm::exceptions::WrongFormatException,
1395 "Error in " << variable.getFilename() << ", line " << variable.getLineNumber()
1396 << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
1397 }
1398 }
1399
1400 // Record the new identifier for future checks.
1401 variables.insert(variable.getExpressionVariable());
1402 all.insert(variable.getExpressionVariable());
1403 }
1404 for (auto const& variable : module.getIntegerVariables()) {
1405 // Check that bound expressions of the range.
1406 if (variable.hasLowerBoundExpression()) {
1407 std::set<storm::expressions::Variable> containedVariables = variable.getLowerBoundExpression().getVariables();
1408 std::set<storm::expressions::Variable> illegalVariables;
1409 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1410 std::inserter(illegalVariables, illegalVariables.begin()));
1411 bool isValid = illegalVariables.empty();
1412 if (!isValid) {
1413 std::vector<std::string> illegalVariableNames;
1414 for (auto const& var : illegalVariables) {
1415 illegalVariableNames.push_back(var.getName());
1416 }
1417 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1418 "Error in " << variable.getFilename() << ", line " << variable.getLineNumber()
1419 << ": lower bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",")
1420 << ".");
1421 }
1422 }
1423
1424 if (variable.hasUpperBoundExpression()) {
1425 std::set<storm::expressions::Variable> containedVariables = variable.getUpperBoundExpression().getVariables();
1426 std::set<storm::expressions::Variable> illegalVariables;
1427
1428 illegalVariables.clear();
1429 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1430 std::inserter(illegalVariables, illegalVariables.begin()));
1431 bool isValid = illegalVariables.empty();
1432 if (!isValid) {
1433 std::vector<std::string> illegalVariableNames;
1434 for (auto const& var : illegalVariables) {
1435 illegalVariableNames.push_back(var.getName());
1436 }
1437 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1438 "Error in " << variable.getFilename() << ", line " << variable.getLineNumber()
1439 << ": upper bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",")
1440 << ".");
1441 }
1442 }
1443
1444 if (variable.hasInitialValue()) {
1445 STORM_LOG_THROW(!this->hasInitialConstruct(), storm::exceptions::WrongFormatException,
1446 "Error for " << module.getName() << "." << variable.getName() << " (" << variable.getFilename() << ", line "
1447 << variable.getLineNumber() << "): illegal to specify initial value if an initial construct is present.");
1448
1449 // Check the initial value of the variable.
1450 std::set<storm::expressions::Variable> containedVariables = variable.getInitialValueExpression().getVariables();
1451 std::set<storm::expressions::Variable> illegalVariables;
1452 illegalVariables.clear();
1453 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1454 std::inserter(illegalVariables, illegalVariables.begin()));
1455 bool isValid = illegalVariables.empty();
1456 if (!isValid) {
1457 std::vector<std::string> illegalVariableNames;
1458 for (auto const& var : illegalVariables) {
1459 illegalVariableNames.push_back(var.getName());
1460 }
1462 isValid, storm::exceptions::WrongFormatException,
1463 "Error in " << variable.getFilename() << ", line " << variable.getLineNumber()
1464 << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
1465 }
1466 }
1467
1468 // Record the new identifier for future checks.
1469 variables.insert(variable.getExpressionVariable());
1470 all.insert(variable.getExpressionVariable());
1471 }
1472
1473 for (auto const& variable : module.getClockVariables()) {
1474 // Record the new identifier for future checks.
1475 variables.insert(variable.getExpressionVariable());
1476 all.insert(variable.getExpressionVariable());
1477 }
1478 }
1479
1480 // Create the set of valid identifiers for future checks.
1481 std::set<storm::expressions::Variable> variablesAndConstants;
1482 std::set_union(variables.begin(), variables.end(), constants.begin(), constants.end(), std::inserter(variablesAndConstants, variablesAndConstants.begin()));
1483
1484 // Collect the formula placeholders and check formulas
1485 for (auto const& formula : this->getFormulas()) {
1486 std::set<storm::expressions::Variable> containedVariables = formula.getExpression().getVariables();
1487 bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1488 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1489 "Error in " << formula.getFilename() << ", line " << formula.getLineNumber() << ": expression '" << formula.getExpression()
1490 << "'of formula '" << formula.getName() << "' refers to unknown identifiers.");
1491 if (formula.hasExpressionVariable()) {
1492 all.insert(formula.getExpressionVariable());
1493 variablesAndConstants.insert(formula.getExpressionVariable());
1494 }
1495 }
1496
1497 // Check the commands and invariants of the modules.
1498 bool hasProbabilisticCommand = false;
1499 bool hasMarkovianCommand = false;
1500 bool hasLabeledMarkovianCommand = false;
1501 std::map<std::pair<storm::expressions::Variable, uint64_t>, std::pair<uint64_t, std::string>> writtenGlobalVariables;
1502 for (auto const& module : this->getModules()) {
1503 std::set<storm::expressions::Variable> legalVariables = globalVariables;
1504 for (auto const& variable : module.getBooleanVariables()) {
1505 legalVariables.insert(variable.getExpressionVariable());
1506 }
1507 for (auto const& variable : module.getIntegerVariables()) {
1508 legalVariables.insert(variable.getExpressionVariable());
1509 }
1510 for (auto const& variable : module.getClockVariables()) {
1511 legalVariables.insert(variable.getExpressionVariable());
1512 }
1513
1514 if (module.hasInvariant()) {
1515 std::set<storm::expressions::Variable> containedVariables = module.getInvariant().getVariables();
1516 std::set<storm::expressions::Variable> illegalVariables;
1517 std::set_difference(containedVariables.begin(), containedVariables.end(), variablesAndConstants.begin(), variablesAndConstants.end(),
1518 std::inserter(illegalVariables, illegalVariables.begin()));
1519 bool isValid = illegalVariables.empty();
1520 if (!isValid) {
1521 std::vector<std::string> illegalVariableNames;
1522 for (auto const& var : illegalVariables) {
1523 illegalVariableNames.push_back(var.getName());
1524 }
1525 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1526 "Error in " << module.getFilename() << ", line " << module.getLineNumber() << ": invariant " << module.getInvariant()
1527 << " refers to unknown identifiers: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
1528 }
1529 STORM_LOG_THROW(module.getInvariant().hasBooleanType(), storm::exceptions::WrongFormatException,
1530 "Error in " << module.getFilename() << ", line " << module.getLineNumber() << ": invariant " << module.getInvariant()
1531 << " must evaluate to type 'bool'.");
1532 }
1533
1534 for (auto& command : module.getCommands()) {
1535 // Check the guard.
1536 std::set<storm::expressions::Variable> containedVariables = command.getGuardExpression().getVariables();
1537 std::set<storm::expressions::Variable> illegalVariables;
1538 std::set_difference(containedVariables.begin(), containedVariables.end(), variablesAndConstants.begin(), variablesAndConstants.end(),
1539 std::inserter(illegalVariables, illegalVariables.begin()));
1540 bool isValid = illegalVariables.empty();
1541 if (!isValid) {
1542 std::vector<std::string> illegalVariableNames;
1543 for (auto const& var : illegalVariables) {
1544 illegalVariableNames.push_back(var.getName());
1545 }
1546 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1547 "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": guard " << command.getGuardExpression()
1548 << " refers to unknown identifiers: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
1549 }
1551 command.getGuardExpression().hasBooleanType(), storm::exceptions::WrongFormatException,
1552 "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": expression for guard must evaluate to type 'bool'.");
1553
1554 // Record which types of commands were seen.
1555 if (command.isMarkovian()) {
1556 hasMarkovianCommand = true;
1557 } else {
1558 hasProbabilisticCommand = true;
1559 }
1560
1561 // If the command is Markovian and labeled, we throw an error or raise a warning, depending on
1562 // whether or not the PRISM compatibility mode was enabled.
1563 if (command.isMarkovian() && command.isLabeled()) {
1564 hasLabeledMarkovianCommand = true;
1565 }
1566
1567 // Check all updates.
1568 for (auto const& update : command.getUpdates()) {
1569 containedVariables.clear();
1570 if (update.isLikelihoodInterval()) {
1571 update.getLikelihoodExpressionInterval().first.gatherVariables(containedVariables);
1572 update.getLikelihoodExpressionInterval().second.gatherVariables(containedVariables);
1573 } else {
1574 update.getLikelihoodExpression().gatherVariables(containedVariables);
1575 }
1576 illegalVariables.clear();
1577 std::set_difference(containedVariables.begin(), containedVariables.end(), variablesAndConstants.begin(), variablesAndConstants.end(),
1578 std::inserter(illegalVariables, illegalVariables.begin()));
1579 isValid = illegalVariables.empty();
1580 if (!isValid) {
1581 std::vector<std::string> illegalVariableNames;
1582 for (auto const& var : illegalVariables) {
1583 illegalVariableNames.push_back(var.getName());
1584 }
1586 isValid, storm::exceptions::WrongFormatException,
1587 "Error in " << command.getFilename() << ", line " << command.getLineNumber()
1588 << ": likelihood expression refers to unknown identifiers: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
1589 }
1590
1591 // Check all assignments.
1592 std::set<storm::expressions::Variable> alreadyAssignedVariables;
1593 for (auto const& assignment : update.getAssignments()) {
1594 storm::expressions::Variable assignedVariable = manager->getVariable(assignment.getVariableName());
1595
1596 if (legalVariables.find(assignedVariable) == legalVariables.end()) {
1597 if (all.find(assignedVariable) != all.end()) {
1598 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
1599 "Error in " << command.getFilename() << ", line " << command.getLineNumber()
1600 << ": assignment illegally refers to variable '" << assignment.getVariableName() << "'.");
1601 } else {
1602 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
1603 "Error in " << command.getFilename() << ", line " << command.getLineNumber()
1604 << ": assignment refers to unknown variable '" << assignment.getVariableName() << "'.");
1605 }
1606 }
1607 STORM_LOG_THROW(alreadyAssignedVariables.find(assignedVariable) == alreadyAssignedVariables.end(), storm::exceptions::WrongFormatException,
1608 "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": duplicate assignment to variable '"
1609 << assignment.getVariableName() << "'.");
1610 STORM_LOG_THROW(assignedVariable.getType() == assignment.getExpression().getType() ||
1611 (assignedVariable.getType().isRationalType() && assignment.getExpression().getType().isNumericalType()),
1612 storm::exceptions::WrongFormatException,
1613 "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": illegally assigning a value of type '"
1614 << assignment.getExpression().getType() << "' to variable '" << assignment.getVariableName() << "' of type '"
1615 << assignedVariable.getType() << "'.");
1616
1617 if (command.isLabeled() && globalVariables.find(assignedVariable) != globalVariables.end()) {
1618 std::pair<storm::expressions::Variable, uint64_t> variableActionIndexPair(assignedVariable, command.getActionIndex());
1619 std::pair<uint64_t, std::string> lineModuleNamePair(command.getLineNumber(), module.getName());
1620 auto insertionResult = writtenGlobalVariables.emplace(variableActionIndexPair, lineModuleNamePair);
1622 insertionResult.second || insertionResult.first->second.second == module.getName(), storm::exceptions::WrongFormatException,
1623 "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": Syncronizing command with action label '"
1624 << command.getActionName() << "' illegally assigns a value to global variable '" << assignedVariable.getName()
1625 << "'. Previous assignment to the variable at line " << insertionResult.first->second.first << " in module '"
1626 << insertionResult.first->second.second << "'.");
1627 }
1628
1629 containedVariables = assignment.getExpression().getVariables();
1630 illegalVariables.clear();
1631 std::set_difference(containedVariables.begin(), containedVariables.end(), variablesAndConstants.begin(), variablesAndConstants.end(),
1632 std::inserter(illegalVariables, illegalVariables.begin()));
1633 isValid = illegalVariables.empty();
1634 if (!isValid) {
1635 std::vector<std::string> illegalVariableNames;
1636 for (auto const& var : illegalVariables) {
1637 illegalVariableNames.push_back(var.getName());
1638 }
1640 isValid, storm::exceptions::WrongFormatException,
1641 "Error in " << command.getFilename() << ", line " << command.getLineNumber()
1642 << ": assigned expression refers to unknown identifiers: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
1643 }
1644
1645 // Add the current variable to the set of assigned variables (of this update).
1646 alreadyAssignedVariables.insert(assignedVariable);
1647 }
1648 }
1649 }
1650 }
1651
1652 if (hasLabeledMarkovianCommand) {
1653 if (prismCompatibility) {
1655 false, "The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.");
1656 } else {
1657 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
1658 "The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.");
1659 }
1660 }
1661
1662 if (this->getModelType() == Program::ModelType::DTMC || this->getModelType() == Program::ModelType::MDP) {
1663 STORM_LOG_THROW(!hasMarkovianCommand, storm::exceptions::WrongFormatException, "Discrete-time model must not have Markovian commands.");
1664 } else if (this->getModelType() == Program::ModelType::CTMC) {
1665 STORM_LOG_THROW(!hasProbabilisticCommand, storm::exceptions::WrongFormatException,
1666 "The input model is a CTMC, but uses probabilistic commands like they are used in PRISM. Please use Markovian commands instead or turn "
1667 "on the PRISM compatibility mode using the flag '-pc'.");
1668 }
1669
1670 // Now check the reward models.
1671 for (auto const& rewardModel : this->getRewardModels()) {
1672 for (auto const& stateReward : rewardModel.getStateRewards()) {
1673 std::set<storm::expressions::Variable> containedVariables = stateReward.getStatePredicateExpression().getVariables();
1674 bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1675 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1676 "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber()
1677 << ": state reward expression refers to unknown identifiers.");
1679 stateReward.getStatePredicateExpression().hasBooleanType(), storm::exceptions::WrongFormatException,
1680 "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": state predicate must evaluate to type 'bool'.");
1681
1682 containedVariables = stateReward.getRewardValueExpression().getVariables();
1683 isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1684 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1685 "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber()
1686 << ": state reward value expression refers to unknown identifiers.");
1687 STORM_LOG_THROW(stateReward.getRewardValueExpression().hasNumericalType(), storm::exceptions::WrongFormatException,
1688 "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber()
1689 << ": reward value expression must evaluate to numerical type.");
1690 }
1691
1692 for (auto const& stateActionReward : rewardModel.getStateActionRewards()) {
1693 std::set<storm::expressions::Variable> containedVariables = stateActionReward.getStatePredicateExpression().getVariables();
1694 bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1695 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1696 "Error in " << stateActionReward.getFilename() << ", line " << stateActionReward.getLineNumber()
1697 << ": state reward expression refers to unknown identifiers.");
1698 STORM_LOG_THROW(stateActionReward.getStatePredicateExpression().hasBooleanType(), storm::exceptions::WrongFormatException,
1699 "Error in " << stateActionReward.getFilename() << ", line " << stateActionReward.getLineNumber()
1700 << ": state predicate must evaluate to type 'bool'.");
1701
1702 containedVariables = stateActionReward.getRewardValueExpression().getVariables();
1703 isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1704 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1705 "Error in " << stateActionReward.getFilename() << ", line " << stateActionReward.getLineNumber()
1706 << ": state reward value expression refers to unknown identifiers.");
1707 STORM_LOG_THROW(stateActionReward.getRewardValueExpression().hasNumericalType(), storm::exceptions::WrongFormatException,
1708 "Error in " << stateActionReward.getFilename() << ", line " << stateActionReward.getLineNumber()
1709 << ": reward value expression must evaluate to numerical type.");
1710 }
1711
1712 for (auto const& transitionReward : rewardModel.getTransitionRewards()) {
1713 std::set<storm::expressions::Variable> containedVariables = transitionReward.getSourceStatePredicateExpression().getVariables();
1714 bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1715 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1716 "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber()
1717 << ": state reward expression refers to unknown identifiers.");
1718 STORM_LOG_THROW(transitionReward.getSourceStatePredicateExpression().hasBooleanType(), storm::exceptions::WrongFormatException,
1719 "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber()
1720 << ": state predicate must evaluate to type 'bool'.");
1721
1722 containedVariables = transitionReward.getTargetStatePredicateExpression().getVariables();
1723 isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1724 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1725 "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber()
1726 << ": state reward expression refers to unknown identifiers.");
1727 STORM_LOG_THROW(transitionReward.getTargetStatePredicateExpression().hasBooleanType(), storm::exceptions::WrongFormatException,
1728 "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber()
1729 << ": state predicate must evaluate to type 'bool'.");
1730
1731 containedVariables = transitionReward.getRewardValueExpression().getVariables();
1732 isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1733 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1734 "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber()
1735 << ": state reward value expression refers to unknown identifiers.");
1736 STORM_LOG_THROW(transitionReward.getRewardValueExpression().hasNumericalType(), storm::exceptions::WrongFormatException,
1737 "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber()
1738 << ": reward value expression must evaluate to numerical type.");
1739 }
1740 }
1741
1742 // Check the initial states expression.
1743 if (this->hasInitialConstruct()) {
1744 std::set<storm::expressions::Variable> containedIdentifiers = this->getInitialConstruct().getInitialStatesExpression().getVariables();
1745 bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
1746 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1747 "Error in " << this->getInitialConstruct().getFilename() << ", line " << this->getInitialConstruct().getLineNumber()
1748 << ": initial construct refers to unknown identifiers.");
1749 }
1750
1751 // Check the system composition if given.
1752 if (systemCompositionConstruct) {
1753 CompositionValidityChecker checker(*this);
1754 checker.check(systemCompositionConstruct.get().getSystemComposition());
1755 }
1756
1757 // Check the labels.
1758 for (auto const& label : this->getLabels()) {
1759 std::set<storm::expressions::Variable> containedVariables = label.getStatePredicateExpression().getVariables();
1760 bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1761 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException,
1762 "Error in " << label.getFilename() << ", line " << label.getLineNumber() << ": label expression refers to unknown identifiers.");
1763 STORM_LOG_THROW(label.getStatePredicateExpression().hasBooleanType(), storm::exceptions::WrongFormatException,
1764 "Error in " << label.getFilename() << ", line " << label.getLineNumber() << ": label predicate must evaluate to type 'bool'.");
1765 }
1766
1767 // Check the players
1768 for (auto const& player : this->getPlayers()) {
1769 // The stored action/module names shall be available
1770 for (auto const& controlledAction : player.getActions()) {
1771 STORM_LOG_THROW(this->hasAction(controlledAction), storm::exceptions::InternalException,
1772 "Error in " << player.getFilename() << ", line " << player.getLineNumber() << ": The player controlled action " << controlledAction
1773 << " is not available.");
1774 }
1775 for (auto const& controlledModule : player.getModules()) {
1776 STORM_LOG_THROW(this->hasModule(controlledModule), storm::exceptions::InternalException,
1777 "Error in " << player.getFilename() << ", line " << player.getLineNumber() << ": The player controlled module " << controlledModule
1778 << " is not available.");
1779 }
1780 }
1781
1782 if (lvl >= Program::ValidityCheckLevel::READYFORPROCESSING) {
1783 // We check for each global variable and each labeled command, whether there is at most one instance writing to that variable.
1784 std::set<std::pair<std::string, std::string>> globalBVarsWrittenToByCommand;
1785 std::set<std::pair<std::string, std::string>> globalIVarsWrittenToByCommand;
1786 for (auto const& module : this->getModules()) {
1787 std::set<std::pair<std::string, std::string>> globalBVarsWrittenToByCommandInThisModule;
1788 std::set<std::pair<std::string, std::string>> globalIVarsWrittenToByCommandInThisModule;
1789 for (auto const& command : module.getCommands()) {
1790 if (!command.isLabeled())
1791 continue;
1792 for (auto const& update : command.getUpdates()) {
1793 for (auto const& assignment : update.getAssignments()) {
1794 if (this->globalBooleanVariableExists(assignment.getVariable().getName())) {
1795 globalBVarsWrittenToByCommandInThisModule.insert({assignment.getVariable().getName(), command.getActionName()});
1796 } else if (this->globalIntegerVariableExists(assignment.getVariable().getName())) {
1797 globalIVarsWrittenToByCommandInThisModule.insert({assignment.getVariable().getName(), command.getActionName()});
1798 }
1799 }
1800 }
1801 }
1802 for (auto const& entry : globalIVarsWrittenToByCommandInThisModule) {
1803 if (globalIVarsWrittenToByCommand.find(entry) != globalIVarsWrittenToByCommand.end()) {
1804 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
1805 "Error in " << module.getFilename() << ", line " << module.getLineNumber()
1806 << ": assignment of (possibly) synchronizing command with label '" << entry.second
1807 << "' writes to global variable '" << entry.first << "'.");
1808 }
1809 }
1810 for (auto const& entry : globalBVarsWrittenToByCommandInThisModule) {
1811 if (globalBVarsWrittenToByCommand.find(entry) != globalBVarsWrittenToByCommand.end()) {
1812 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
1813 "Error in " << module.getFilename() << ", line " << module.getLineNumber()
1814 << ": assignment of (possibly) synchronizing command with label '" << entry.second
1815 << "' writes to global variable '" << entry.first << "'.");
1816 }
1817 }
1818 }
1819 }
1820}
1821
1822Program Program::simplify() {
1823 // Start by substituting the constants, because this will potentially erase some commands or even actions.
1824 Program substitutedProgram = this->substituteConstantsFormulas();
1825
1826 // As we possibly delete some commands and some actions might be dropped from modules altogether, we need to
1827 // maintain a list of actions that we need to remove in other modules. For example, if module A loses all [a]
1828 // commands, we need to delete all [a] commands from all other modules as well. If we do not do that, we will
1829 // remove the forced synchronization that was there before.
1830 std::set<uint_fast64_t> actionIndicesToDelete;
1831
1832 std::vector<Module> newModules;
1833 std::vector<Constant> newConstants = substitutedProgram.getConstants();
1834 for (auto const& module : substitutedProgram.getModules()) {
1835 // Discard all commands with a guard equivalent to false and remove identity assignments from the updates.
1836 std::vector<Command> newCommands;
1837 for (auto const& command : module.getCommands()) {
1838 if (!command.getGuardExpression().isFalse()) {
1839 newCommands.emplace_back(command.simplify());
1840 }
1841 }
1842
1843 // Substitute variables by global constants if possible.
1844 std::map<storm::expressions::Variable, storm::expressions::Expression> booleanVars;
1845 std::map<storm::expressions::Variable, storm::expressions::Expression> integerVars;
1846 for (auto const& variable : module.getBooleanVariables()) {
1847 booleanVars.emplace(variable.getExpressionVariable(), variable.getInitialValueExpression());
1848 }
1849 for (auto const& variable : module.getIntegerVariables()) {
1850 integerVars.emplace(variable.getExpressionVariable(), variable.getInitialValueExpression());
1851 }
1852
1853 // Collect all variables that are being written. These variables cannot be turned to constants.
1854 for (auto const& command : newCommands) {
1855 // Check all updates.
1856 for (auto const& update : command.getUpdates()) {
1857 // Check all assignments.
1858 for (auto const& assignment : update.getAssignments()) {
1859 if (assignment.getVariable().getType().isBooleanType()) {
1860 auto it = booleanVars.find(assignment.getVariable());
1861 if (it != booleanVars.end()) {
1862 booleanVars.erase(it);
1863 }
1864 } else {
1865 auto it = integerVars.find(assignment.getVariable());
1866 if (it != integerVars.end()) {
1867 integerVars.erase(it);
1868 }
1869 }
1870 }
1871 }
1872 }
1873
1874 std::vector<storm::prism::BooleanVariable> newBooleanVars;
1875 for (auto const& variable : module.getBooleanVariables()) {
1876 if (booleanVars.find(variable.getExpressionVariable()) == booleanVars.end()) {
1877 newBooleanVars.push_back(variable);
1878 }
1879 }
1880 std::vector<storm::prism::IntegerVariable> newIntegerVars;
1881 for (auto const& variable : module.getIntegerVariables()) {
1882 if (integerVars.find(variable.getExpressionVariable()) == integerVars.end()) {
1883 newIntegerVars.push_back(variable);
1884 }
1885 }
1886
1887 for (auto const& variable : module.getBooleanVariables()) {
1888 if (booleanVars.find(variable.getExpressionVariable()) != booleanVars.end()) {
1889 if (variable.hasInitialValue()) {
1890 newConstants.emplace_back(variable.getExpressionVariable(), variable.getInitialValueExpression());
1891 } else {
1892 newBooleanVars.push_back(variable);
1893 }
1894 }
1895 }
1896 for (auto const& variable : module.getIntegerVariables()) {
1897 if (integerVars.find(variable.getExpressionVariable()) != integerVars.end()) {
1898 if (variable.hasInitialValue()) {
1899 newConstants.emplace_back(variable.getExpressionVariable(), variable.getInitialValueExpression());
1900 } else {
1901 newIntegerVars.push_back(variable);
1902 }
1903 }
1904 }
1905
1906 // we currently do not simplify clock variables or invariants
1907 newModules.emplace_back(module.getName(), newBooleanVars, newIntegerVars, module.getClockVariables(), module.getInvariant(), newCommands);
1908
1909 // Determine the set of action indices that have been deleted entirely.
1910 std::set_difference(module.getSynchronizingActionIndices().begin(), module.getSynchronizingActionIndices().end(),
1911 newModules.back().getSynchronizingActionIndices().begin(), newModules.back().getSynchronizingActionIndices().end(),
1912 std::inserter(actionIndicesToDelete, actionIndicesToDelete.begin()));
1913 }
1914
1915 // If we have to delete whole actions, do so now.
1916 std::map<std::string, uint_fast64_t> newActionToIndexMap;
1917 std::vector<RewardModel> newRewardModels;
1918 std::vector<Player> newPlayers;
1919 if (!actionIndicesToDelete.empty()) {
1921 std::set_difference(this->getSynchronizingActionIndices().begin(), this->getSynchronizingActionIndices().end(), actionIndicesToDelete.begin(),
1922 actionIndicesToDelete.end(), std::inserter(actionsToKeep, actionsToKeep.begin()));
1923
1924 // Insert the silent action as this is not contained in the synchronizing action indices.
1925 actionsToKeep.insert(0);
1926
1927 std::vector<Module> cleanedModules;
1928 cleanedModules.reserve(newModules.size());
1929 for (auto const& module : newModules) {
1930 cleanedModules.emplace_back(module.restrictActionIndices(actionsToKeep));
1931 }
1932 newModules = std::move(cleanedModules);
1933
1934 newRewardModels.reserve(substitutedProgram.getNumberOfRewardModels());
1935 for (auto const& rewardModel : substitutedProgram.getRewardModels()) {
1936 newRewardModels.emplace_back(rewardModel.restrictActionRelatedRewards(actionsToKeep));
1937 }
1938
1939 // Restrict action name to index mapping. Old action indices remain valid.
1940 for (auto const& entry : this->getActionNameToIndexMapping()) {
1941 if (actionsToKeep.find(entry.second) != actionsToKeep.end()) {
1942 newActionToIndexMap.emplace(entry.first, entry.second);
1943 }
1944 }
1945
1946 // Restrict player controlled actions
1947 for (auto const& player : this->getPlayers()) {
1948 std::unordered_set<std::string> newControlledActions;
1949 for (auto const& act : player.getActions()) {
1950 if (newActionToIndexMap.count(act) != 0) {
1951 newControlledActions.insert(act);
1952 }
1953 }
1954 newPlayers.emplace_back(player.getName(), player.getModules(), newControlledActions, player.getFilename(), player.getLineNumber());
1955 }
1956 }
1957
1958 std::vector<Label> newLabels;
1959 for (auto const& label : this->getLabels()) {
1960 newLabels.emplace_back(label.getName(), label.getStatePredicateExpression().simplify());
1961 }
1962
1963 return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(),
1964 actionIndicesToDelete.empty() ? this->getPlayers() : newPlayers, newModules,
1965 actionIndicesToDelete.empty() ? getActionNameToIndexMapping() : newActionToIndexMap,
1966 actionIndicesToDelete.empty() ? this->getRewardModels() : newRewardModels, newLabels, getObservationLabels(), getOptionalInitialConstruct(),
1967 this->getOptionalSystemCompositionConstruct(), prismCompatibility);
1968}
1969
1970Program Program::flattenModules(std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) const {
1971 // If the current program has only one module, we can simply return a copy.
1972 if (this->getNumberOfModules() == 1) {
1973 return Program(*this);
1974 }
1975
1976 STORM_LOG_THROW(this->getModelType() == ModelType::DTMC || this->getModelType() == ModelType::MDP, storm::exceptions::InvalidTypeException,
1977 "Unable to flatten modules for model of type '" << this->getModelType() << "'.");
1978
1979 // Otherwise, we need to actually flatten the contained modules.
1980
1981 // Get an SMT solver for computing the possible guard combinations.
1982 std::unique_ptr<storm::solver::SmtSolver> solver = smtSolverFactory->create(*manager);
1983
1984 // Set up the data we need to gather to create the flat module.
1985 std::stringstream newModuleName;
1986 std::vector<storm::prism::BooleanVariable> allBooleanVariables;
1987 std::vector<storm::prism::IntegerVariable> allIntegerVariables;
1988 std::vector<storm::prism::ClockVariable> allClockVariables;
1989 std::vector<storm::prism::Command> newCommands;
1990 uint_fast64_t nextCommandIndex = 0;
1991 uint_fast64_t nextUpdateIndex = 0;
1992
1993 // Assert the values of the constants.
1994 for (auto const& constant : this->getConstants()) {
1995 if (constant.isDefined()) {
1996 if (constant.getType().isBooleanType()) {
1997 solver->add(storm::expressions::iff(constant.getExpressionVariable(), constant.getExpression()));
1998 } else {
1999 solver->add(constant.getExpressionVariable() == constant.getExpression());
2000 }
2001 }
2002 }
2003
2004 // Assert the bounds of the global variables.
2005 for (auto const& variable : this->getGlobalIntegerVariables()) {
2006 solver->add(variable.getRangeExpression());
2007 }
2008
2009 // Make the global variables local, such that the resulting module covers all occurring variables. Note that
2010 // this is just for simplicity and is not needed.
2011 allBooleanVariables.insert(allBooleanVariables.end(), this->getGlobalBooleanVariables().begin(), this->getGlobalBooleanVariables().end());
2012 allIntegerVariables.insert(allIntegerVariables.end(), this->getGlobalIntegerVariables().begin(), this->getGlobalIntegerVariables().end());
2013 storm::expressions::Expression newInvariant;
2014
2015 // Now go through the modules, gather the variables, construct the name of the new module and assert the
2016 // bounds of the discovered variables.
2017 for (auto const& module : this->getModules()) {
2018 newModuleName << module.getName() << "_";
2019 allBooleanVariables.insert(allBooleanVariables.end(), module.getBooleanVariables().begin(), module.getBooleanVariables().end());
2020 allIntegerVariables.insert(allIntegerVariables.end(), module.getIntegerVariables().begin(), module.getIntegerVariables().end());
2021 allClockVariables.insert(allClockVariables.end(), module.getClockVariables().begin(), module.getClockVariables().end());
2022
2023 for (auto const& variable : module.getIntegerVariables()) {
2024 solver->add(variable.getRangeExpression());
2025 }
2026
2027 if (module.hasInvariant()) {
2028 newInvariant = newInvariant.isInitialized() ? (newInvariant && module.getInvariant()) : module.getInvariant();
2029 }
2030
2031 // The commands without a synchronizing action name, can simply be copied (plus adjusting the global
2032 // indices of the command and its updates).
2033 for (auto const& command : module.getCommands()) {
2034 if (!command.isLabeled()) {
2035 std::vector<storm::prism::Update> updates;
2036 updates.reserve(command.getUpdates().size());
2037
2038 for (auto const& update : command.getUpdates()) {
2039 updates.push_back(
2040 storm::prism::Update(nextUpdateIndex, update.getLikelihoodExpression(), update.getAssignments(), update.getFilename(), 0));
2041 ++nextUpdateIndex;
2042 }
2043
2044 newCommands.push_back(storm::prism::Command(nextCommandIndex, command.isMarkovian(), actionToIndexMap.find("")->second, "",
2045 command.getGuardExpression(), updates, command.getFilename(), 0));
2046 ++nextCommandIndex;
2047 }
2048 }
2049 }
2050
2051 // Save state of solver so that we can always restore the point where we have exactly the constant values
2052 // and variables bounds on the assertion stack.
2053 solver->push();
2054
2055 // Now we need to enumerate all possible combinations of synchronizing commands. For this, we iterate over
2056 // all actions and let the solver enumerate the possible combinations of commands that can be enabled together.
2057 for (auto const& actionIndex : this->getSynchronizingActionIndices()) {
2058 bool noCombinationsForAction = false;
2059
2060 // Prepare the list that stores for each module the list of commands with the given action.
2061 std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>> possibleCommands;
2062
2063 for (auto const& module : this->getModules()) {
2064 // If the module has no command with this action, we can skip it.
2065 if (!module.hasActionIndex(actionIndex)) {
2066 continue;
2067 }
2068
2069 std::set<uint_fast64_t> const& commandIndices = module.getCommandIndicesByActionIndex(actionIndex);
2070
2071 // If there is no command even though the module has this action, there is no valid command
2072 // combination with this action.
2073 if (commandIndices.empty()) {
2074 noCombinationsForAction = true;
2075 break;
2076 }
2077
2078 // Prepare empty list of commands for this module.
2079 possibleCommands.push_back(std::vector<std::reference_wrapper<storm::prism::Command const>>());
2080
2081 // Add references to the commands labeled with the current action.
2082 for (auto const& commandIndex : commandIndices) {
2083 possibleCommands.back().push_back(module.getCommand(commandIndex));
2084 }
2085 }
2086
2087 // If there are no valid combinations for the action, we need to skip the generation of synchronizing
2088 // commands.
2089 if (!noCombinationsForAction) {
2090 // Save the solver state to be able to restore it when this action index is done.
2091 solver->push();
2092
2093 // Start by creating a fresh auxiliary variable for each command and link it with the guard.
2094 std::vector<std::vector<storm::expressions::Variable>> commandVariables(possibleCommands.size());
2095 std::vector<storm::expressions::Variable> allCommandVariables;
2096 for (uint_fast64_t outerIndex = 0; outerIndex < possibleCommands.size(); ++outerIndex) {
2097 // Create auxiliary variables and link them with the guards.
2098 for (uint_fast64_t innerIndex = 0; innerIndex < possibleCommands[outerIndex].size(); ++innerIndex) {
2099 commandVariables[outerIndex].push_back(manager->declareFreshBooleanVariable());
2100 allCommandVariables.push_back(commandVariables[outerIndex].back());
2101 solver->add(implies(commandVariables[outerIndex].back(), possibleCommands[outerIndex][innerIndex].get().getGuardExpression()));
2102 }
2103
2104 storm::expressions::Expression atLeastOneCommandFromModule = manager->boolean(false);
2105 for (auto const& commandVariable : commandVariables[outerIndex]) {
2106 atLeastOneCommandFromModule = atLeastOneCommandFromModule || commandVariable;
2107 }
2108 solver->add(atLeastOneCommandFromModule);
2109 }
2110
2111 // Now we are in a position to start the enumeration over all command variables. While doing so, we
2112 // keep track of previously seen command combinations, because the AllSat procedures are not
2113 // always guaranteed to only provide distinct models.
2114 std::unordered_set<std::vector<uint_fast64_t>, storm::utility::vector::VectorHash<uint_fast64_t>> seenCommandCombinations;
2115 solver->allSat(allCommandVariables, [&](storm::solver::SmtSolver::ModelReference& modelReference) -> bool {
2116 // Now we need to reconstruct the chosen commands from the valuation of the command variables.
2117 std::vector<std::vector<std::reference_wrapper<Command const>>> chosenCommands(possibleCommands.size());
2118
2119 for (uint_fast64_t outerIndex = 0; outerIndex < commandVariables.size(); ++outerIndex) {
2120 for (uint_fast64_t innerIndex = 0; innerIndex < commandVariables[outerIndex].size(); ++innerIndex) {
2121 if (modelReference.getBooleanValue(commandVariables[outerIndex][innerIndex])) {
2122 chosenCommands[outerIndex].push_back(possibleCommands[outerIndex][innerIndex]);
2123 }
2124 }
2125 }
2126
2127 // Now that we have retrieved the commands, we need to build their synchronizations and add them
2128 // to the flattened module.
2129 std::vector<std::vector<std::reference_wrapper<Command const>>::const_iterator> iterators;
2130 for (auto const& element : chosenCommands) {
2131 iterators.push_back(element.begin());
2132 }
2133
2134 bool movedAtLeastOneIterator = false;
2135 std::vector<std::reference_wrapper<Command const>> commandCombination(chosenCommands.size(), chosenCommands.front().front());
2136 std::vector<uint_fast64_t> commandCombinationIndices(iterators.size());
2137 do {
2138 for (uint_fast64_t index = 0; index < iterators.size(); ++index) {
2139 commandCombination[index] = *iterators[index];
2140 commandCombinationIndices[index] = commandCombination[index].get().getGlobalIndex();
2141 }
2142
2143 // Only add the command combination if it was not previously seen.
2144 auto seenIt = seenCommandCombinations.find(commandCombinationIndices);
2145 if (seenIt == seenCommandCombinations.end()) {
2146 newCommands.push_back(synchronizeCommands(nextCommandIndex, actionIndex, nextUpdateIndex, indexToActionMap.find(actionIndex)->second,
2147 commandCombination));
2148 seenCommandCombinations.insert(commandCombinationIndices);
2149
2150 // Move the counters appropriately.
2151 ++nextCommandIndex;
2152 nextUpdateIndex += newCommands.back().getNumberOfUpdates();
2153 }
2154
2155 movedAtLeastOneIterator = false;
2156 for (uint_fast64_t index = 0; index < iterators.size(); ++index) {
2157 ++iterators[index];
2158 if (iterators[index] != chosenCommands[index].cend()) {
2159 movedAtLeastOneIterator = true;
2160 break;
2161 } else {
2162 iterators[index] = chosenCommands[index].cbegin();
2163 }
2164 }
2165 } while (movedAtLeastOneIterator);
2166
2167 return true;
2168 });
2169
2170 solver->pop();
2171 }
2172 }
2173
2174 // Finally, we can create the module and the program and return it.
2175 storm::prism::Module singleModule(newModuleName.str(), allBooleanVariables, allIntegerVariables, allClockVariables, newInvariant, newCommands,
2176 this->getFilename(), 0);
2177
2178 return Program(manager, this->getModelType(), this->getConstants(), std::vector<storm::prism::BooleanVariable>(),
2179 std::vector<storm::prism::IntegerVariable>(), this->getFormulas(), this->getPlayers(), {singleModule}, actionToIndexMap,
2180 this->getRewardModels(), this->getLabels(), this->getObservationLabels(), this->getOptionalInitialConstruct(),
2181 this->getOptionalSystemCompositionConstruct(), prismCompatibility, this->getFilename(), 0, true);
2182}
2183
2184std::vector<Constant> Program::usedConstants() const {
2185 std::unordered_set<expressions::Variable> vars;
2186 for (auto const& m : this->modules) {
2187 for (auto const& c : m.getCommands()) {
2188 auto const& found_gex = c.getGuardExpression().getVariables();
2189 vars.insert(found_gex.begin(), found_gex.end());
2190 for (auto const& u : c.getUpdates()) {
2191 auto const& found_lex = u.getLikelihoodExpression().getVariables();
2192 vars.insert(found_lex.begin(), found_lex.end());
2193 for (auto const& a : u.getAssignments()) {
2194 auto const& found_ass = a.getExpression().getVariables();
2195 vars.insert(found_ass.begin(), found_ass.end());
2196 }
2197 }
2198 }
2199 for (auto const& v : m.getBooleanVariables()) {
2200 if (v.hasInitialValue()) {
2201 auto const& found_def = v.getInitialValueExpression().getVariables();
2202 vars.insert(found_def.begin(), found_def.end());
2203 }
2204 }
2205 for (auto const& v : m.getIntegerVariables()) {
2206 if (v.hasInitialValue()) {
2207 auto const& found_def = v.getInitialValueExpression().getVariables();
2208 vars.insert(found_def.begin(), found_def.end());
2209 }
2210 }
2211 }
2212
2213 for (auto const& f : this->formulas) {
2214 auto const& found_def = f.getExpression().getVariables();
2215 vars.insert(found_def.begin(), found_def.end());
2216 }
2217
2218 for (auto const& v : this->constants) {
2219 if (v.isDefined()) {
2220 auto const& found_def = v.getExpression().getVariables();
2221 vars.insert(found_def.begin(), found_def.end());
2222 }
2223 }
2224
2225 for (auto const& v : this->globalBooleanVariables) {
2226 if (v.hasInitialValue()) {
2227 auto const& found_def = v.getExpression().getVariables();
2228 vars.insert(found_def.begin(), found_def.end());
2229 }
2230 }
2231
2232 for (auto const& v : this->globalIntegerVariables) {
2233 if (v.hasInitialValue()) {
2234 auto const& found_def = v.getExpression().getVariables();
2235 vars.insert(found_def.begin(), found_def.end());
2236 }
2237 }
2238
2239 std::unordered_set<uint64_t> varIndices;
2240 for (auto const& v : vars) {
2241 varIndices.insert(v.getIndex());
2242 }
2243
2244 std::vector<Constant> usedConstants;
2245 for (auto const& c : this->constants) {
2246 if (varIndices.count(c.getExpressionVariable().getIndex())) {
2247 usedConstants.push_back(c);
2248 }
2249 }
2250
2251 return usedConstants;
2252}
2253
2254std::unordered_map<uint_fast64_t, std::string> Program::buildCommandIndexToActionNameMap() const {
2255 std::unordered_map<uint_fast64_t, std::string> res;
2256 for (auto const& m : this->modules) {
2257 for (auto const& c : m.getCommands()) {
2258 res.emplace(c.getGlobalIndex(), c.getActionName());
2259 }
2260 }
2261 return res;
2262}
2263
2264std::unordered_map<uint_fast64_t, std::string> Program::buildActionIndexToActionNameMap() const {
2265 std::unordered_map<uint_fast64_t, std::string> res;
2266 for (auto const& nameIndexPair : actionToIndexMap) {
2267 res.emplace(nameIndexPair.second, nameIndexPair.first);
2268 }
2269 return res;
2270}
2271
2272std::unordered_map<uint_fast64_t, uint_fast64_t> Program::buildCommandIndexToActionIndex() const {
2273 std::unordered_map<uint_fast64_t, uint_fast64_t> res;
2274 for (auto const& m : this->modules) {
2275 for (auto const& c : m.getCommands()) {
2276 res.emplace(c.getGlobalIndex(), c.getActionIndex());
2277 }
2278 }
2279 return res;
2280}
2281
2282Command Program::synchronizeCommands(uint_fast64_t newCommandIndex, uint_fast64_t actionIndex, uint_fast64_t firstUpdateIndex, std::string const& actionName,
2283 std::vector<std::reference_wrapper<Command const>> const& commands) const {
2284 // To construct the synchronous product of the commands, we need to store a list of its updates.
2285 std::vector<storm::prism::Update> newUpdates;
2286 uint_fast64_t numberOfUpdates = 1;
2287 for (uint_fast64_t i = 0; i < commands.size(); ++i) {
2288 numberOfUpdates *= commands[i].get().getNumberOfUpdates();
2289 }
2290 newUpdates.reserve(numberOfUpdates);
2291
2292 // Initialize all update iterators.
2293 std::vector<std::vector<storm::prism::Update>::const_iterator> updateIterators;
2294 for (uint_fast64_t i = 0; i < commands.size(); ++i) {
2295 updateIterators.push_back(commands[i].get().getUpdates().cbegin());
2296 }
2297
2298 bool doneUpdates = false;
2299 do {
2300 // We create the new likelihood expression by multiplying the particapting updates' expressions.
2301 storm::expressions::Expression newLikelihoodExpression = updateIterators[0]->getLikelihoodExpression();
2302 for (uint_fast64_t i = 1; i < updateIterators.size(); ++i) {
2303 newLikelihoodExpression = newLikelihoodExpression * updateIterators[i]->getLikelihoodExpression();
2304 }
2305
2306 // Now concatenate all assignments of all participating updates.
2307 std::vector<storm::prism::Assignment> newAssignments;
2308 for (uint_fast64_t i = 0; i < updateIterators.size(); ++i) {
2309 newAssignments.insert(newAssignments.end(), updateIterators[i]->getAssignments().begin(), updateIterators[i]->getAssignments().end());
2310 }
2311
2312 // Then we are ready to create the new update.
2313 newUpdates.push_back(storm::prism::Update(firstUpdateIndex, newLikelihoodExpression, newAssignments, this->getFilename(), 0));
2314 ++firstUpdateIndex;
2315
2316 // Now check whether there is some update combination we have not yet explored.
2317 bool movedIterator = false;
2318 for (int_fast64_t j = updateIterators.size() - 1; j >= 0; --j) {
2319 ++updateIterators[j];
2320 if (updateIterators[j] != commands[j].get().getUpdates().cend()) {
2321 movedIterator = true;
2322 break;
2323 } else {
2324 // Reset the iterator to the beginning of the list.
2325 updateIterators[j] = commands[j].get().getUpdates().cbegin();
2326 }
2327 }
2328
2329 doneUpdates = !movedIterator;
2330 } while (!doneUpdates);
2331
2332 storm::expressions::Expression newGuard = commands[0].get().getGuardExpression();
2333 for (uint_fast64_t i = 1; i < commands.size(); ++i) {
2334 newGuard = newGuard && commands[i].get().getGuardExpression();
2335 }
2336
2337 return Command(newCommandIndex, false, actionIndex, actionName, newGuard, newUpdates, this->getFilename(), 0);
2338}
2339
2340storm::jani::Model Program::toJani(bool allVariablesGlobal, std::string suffix) const {
2341 ToJaniConverter converter;
2342 auto janiModel = converter.convert(*this, allVariablesGlobal, {}, suffix);
2343 STORM_LOG_WARN_COND(!converter.labelsWereRenamed(), "Labels were renamed in PRISM-to-JANI conversion, but the mapping is not stored.");
2344 STORM_LOG_WARN_COND(!converter.rewardModelsWereRenamed(), "Rewardmodels were renamed in PRISM-to-JANI conversion, but the mapping is not stored.");
2345 return janiModel;
2346}
2347
2348std::pair<storm::jani::Model, std::vector<storm::jani::Property>> Program::toJani(std::vector<storm::jani::Property> const& properties, bool allVariablesGlobal,
2349 std::string suffix) const {
2350 ToJaniConverter converter;
2351 std::set<storm::expressions::Variable> variablesToMakeGlobal;
2352 if (!allVariablesGlobal) {
2353 for (auto const& prop : properties) {
2354 auto vars = prop.getUsedVariablesAndConstants();
2355 variablesToMakeGlobal.insert(vars.begin(), vars.end());
2356 }
2357 }
2358 auto janiModel = converter.convert(*this, allVariablesGlobal, variablesToMakeGlobal, suffix);
2359 std::vector<storm::jani::Property> newProperties;
2360 if (converter.labelsWereRenamed() || converter.rewardModelsWereRenamed()) {
2361 newProperties = converter.applyRenaming(properties);
2362 } else {
2363 newProperties = properties; // Nothing to be done here. Notice that the copy operation is suboptimal.
2364 }
2365 return std::make_pair(janiModel, newProperties);
2366}
2367
2368uint64_t Program::getHighestCommandIndex() const {
2369 uint64_t highest = 0;
2370 for (auto const& m : getModules()) {
2371 for (auto const& c : m.getCommands()) {
2372 highest = std::max(highest, c.getGlobalIndex());
2373 }
2374 }
2375 return highest;
2376}
2377
2378storm::expressions::ExpressionManager& Program::getManager() const {
2379 return *this->manager;
2380}
2381
2382void Program::createMissingInitialValues() {
2383 for (auto& variable : globalBooleanVariables) {
2384 variable.createMissingInitialValue();
2385 }
2386 for (auto& variable : globalIntegerVariables) {
2387 variable.createMissingInitialValue();
2388 }
2389}
2390
2391std::ostream& operator<<(std::ostream& out, Program::ModelType const& type) {
2392 switch (type) {
2393 case Program::ModelType::UNDEFINED:
2394 out << "undefined";
2395 break;
2396 case Program::ModelType::DTMC:
2397 out << "dtmc";
2398 break;
2399 case Program::ModelType::CTMC:
2400 out << "ctmc";
2401 break;
2402 case Program::ModelType::MDP:
2403 out << "mdp";
2404 break;
2405 case Program::ModelType::CTMDP:
2406 out << "ctmdp";
2407 break;
2408 case Program::ModelType::MA:
2409 out << "ma";
2410 break;
2411 case Program::ModelType::POMDP:
2412 out << "pomdp";
2413 break;
2414 case Program::ModelType::PTA:
2415 out << "pta";
2416 break;
2417 case Program::ModelType::SMG:
2418 out << "smg";
2419 break;
2420 }
2421 return out;
2422}
2423
2424std::ostream& operator<<(std::ostream& stream, Program const& program) {
2425 stream << program.getModelType() << '\n';
2426 for (auto const& constant : program.getConstants()) {
2427 stream << constant << '\n';
2428 }
2429 stream << '\n';
2430
2431 for (auto const& player : program.getPlayers()) {
2432 stream << player << '\n';
2433 }
2434
2435 for (auto const& variable : program.getGlobalBooleanVariables()) {
2436 stream << "global " << variable << '\n';
2437 }
2438 for (auto const& variable : program.getGlobalIntegerVariables()) {
2439 stream << "global " << variable << '\n';
2440 }
2441 stream << '\n';
2442
2443 for (auto const& formula : program.getFormulas()) {
2444 stream << formula << '\n';
2445 }
2446 stream << '\n';
2447
2448 for (auto const& module : program.getModules()) {
2449 stream << module << '\n';
2450 }
2451
2452 for (auto const& rewardModel : program.getRewardModels()) {
2453 stream << rewardModel << '\n';
2454 }
2455
2456 for (auto const& label : program.getLabels()) {
2457 stream << label << '\n';
2458 }
2459
2460 if (program.hasInitialConstruct()) {
2461 stream << program.getInitialConstruct() << '\n';
2462 }
2463
2464 if (program.specifiesSystemComposition()) {
2465 stream << program.getSystemCompositionConstruct();
2466 }
2467
2468 return stream;
2469}
2470
2471} // namespace prism
2472} // 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:821
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:36
bool hasAction(std::string const &actionName) const
Retrieves whether the program has an action with the given name.
Definition Program.cpp:767
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:761
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:781
SystemCompositionConstruct const & getSystemCompositionConstruct() const
If the program specifies a system composition construct, this method retrieves it.
Definition Program.cpp:727
Program substituteConstants() const
Substitutes all constants appearing in the expressions of the program by their defining expressions.
Definition Program.cpp:1039
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:723
std::vector< Label > const & getLabels() const
Retrieves all labels that are defined by the probabilitic program.
Definition Program.cpp:846
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:16
#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.