Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Module.cpp
Go to the documentation of this file.
6
7namespace storm {
8namespace prism {
9Module::Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables,
10 std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::ClockVariable> const& clockVariables,
11 storm::expressions::Expression const& invariant, std::vector<storm::prism::Command> const& commands, std::string const& filename,
12 uint_fast64_t lineNumber)
13 : Module(moduleName, booleanVariables, integerVariables, clockVariables, invariant, commands, "", storm::prism::ModuleRenaming(), filename, lineNumber) {
14 // Intentionally left empty.
15}
16
17Module::Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables,
18 std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::ClockVariable> const& clockVariables,
19 storm::expressions::Expression const& invariant, std::vector<storm::prism::Command> const& commands, std::string const& renamedFromModule,
20 storm::prism::ModuleRenaming const& renaming, std::string const& filename, uint_fast64_t lineNumber)
21 : LocatedInformation(filename, lineNumber),
22 moduleName(moduleName),
23 booleanVariables(booleanVariables),
24 booleanVariableToIndexMap(),
25 integerVariables(integerVariables),
26 integerVariableToIndexMap(),
27 clockVariables(clockVariables),
28 clockVariableToIndexMap(),
29 invariant(invariant),
30 commands(commands),
31 synchronizingActionIndices(),
32 actionIndicesToCommandIndexMap(),
33 renamedFromModule(renamedFromModule),
34 renaming(renaming) {
35 // Initialize the internal mappings for fast information retrieval.
36 this->createMappings();
37}
38
40 for (auto const& integerVariable : this->integerVariables) {
41 if (!integerVariable.hasLowerBoundExpression() || !integerVariable.hasUpperBoundExpression()) {
42 return true;
43 }
44 }
45 return false;
46}
47
49 return this->booleanVariables.size();
50}
51
53 return this->integerVariables.size();
54}
55
56storm::prism::BooleanVariable const& Module::getBooleanVariable(std::string const& variableName) const {
57 auto const& nameIndexPair = this->booleanVariableToIndexMap.find(variableName);
58 STORM_LOG_THROW(nameIndexPair != this->booleanVariableToIndexMap.end(), storm::exceptions::InvalidArgumentException,
59 "Unknown boolean variable '" << variableName << "'.");
60 return this->getBooleanVariables()[nameIndexPair->second];
61}
62
63std::vector<storm::prism::BooleanVariable> const& Module::getBooleanVariables() const {
64 return this->booleanVariables;
65}
66
67storm::prism::IntegerVariable const& Module::getIntegerVariable(std::string const& variableName) const {
68 auto const& nameIndexPair = this->integerVariableToIndexMap.find(variableName);
69 STORM_LOG_THROW(nameIndexPair != this->integerVariableToIndexMap.end(), storm::exceptions::InvalidArgumentException,
70 "Unknown integer variable '" << variableName << "'.");
71 return this->getIntegerVariables()[nameIndexPair->second];
72}
73
74std::vector<storm::prism::IntegerVariable> const& Module::getIntegerVariables() const {
75 return this->integerVariables;
76}
77
79 return this->clockVariables.size();
80}
81
82storm::prism::ClockVariable const& Module::getClockVariable(std::string const& variableName) const {
83 auto const& nameIndexPair = this->clockVariableToIndexMap.find(variableName);
84 STORM_LOG_THROW(nameIndexPair != this->clockVariableToIndexMap.end(), storm::exceptions::InvalidArgumentException,
85 "Unknown clock variable '" << variableName << "'.");
86 return this->getClockVariables()[nameIndexPair->second];
87}
88
89std::vector<storm::prism::ClockVariable> const& Module::getClockVariables() const {
90 return this->clockVariables;
91}
92
93std::set<storm::expressions::Variable> Module::getAllExpressionVariables() const {
94 std::set<storm::expressions::Variable> result;
95 for (auto const& var : this->getBooleanVariables()) {
96 result.insert(var.getExpressionVariable());
97 }
98 for (auto const& var : this->getIntegerVariables()) {
99 result.insert(var.getExpressionVariable());
100 }
101 for (auto const& var : this->getClockVariables()) {
102 result.insert(var.getExpressionVariable());
103 }
104 return result;
105}
106
107std::vector<storm::expressions::Expression> Module::getAllRangeExpressions() const {
108 std::vector<storm::expressions::Expression> result;
109 for (auto const& integerVariable : this->integerVariables) {
110 if (integerVariable.hasLowerBoundExpression() || integerVariable.hasUpperBoundExpression()) {
111 result.push_back(integerVariable.getRangeExpression());
112 }
113 }
114 return result;
115}
116
117std::size_t Module::getNumberOfCommands() const {
118 return this->commands.size();
119}
120
121std::size_t Module::getNumberOfUpdates() const {
122 std::size_t result = 0;
123 for (auto const& command : this->getCommands()) {
124 result += command.getNumberOfUpdates();
125 }
126 return result;
127}
128
129storm::prism::Command const& Module::getCommand(uint_fast64_t index) const {
130 return this->commands[index];
131}
132
133std::vector<storm::prism::Command> const& Module::getCommands() const {
134 return this->commands;
135}
136
137std::vector<storm::prism::Command>& Module::getCommands() {
138 return this->commands;
139}
140
141std::string const& Module::getName() const {
142 return this->moduleName;
143}
144
145std::set<uint_fast64_t> const& Module::getSynchronizingActionIndices() const {
146 return this->synchronizingActionIndices;
147}
148
149bool Module::hasActionIndex(uint_fast64_t actionIndex) const {
150 return this->actionIndicesToCommandIndexMap.find(actionIndex) != this->actionIndicesToCommandIndexMap.end();
151}
152
154 uint64_t result = 0;
155 for (auto const& cmd : commands) {
156 if (!cmd.isLabeled()) {
157 result++;
158 }
159 }
160 return result;
161}
162
164 return this->renamedFromModule != "";
165}
166
167std::string const& Module::getBaseModule() const {
168 STORM_LOG_THROW(this->isRenamedFromModule(), storm::exceptions::InvalidAccessException,
169 "Unable to retrieve base module of module that was not created by renaming.");
170 return this->renamedFromModule;
171}
172
173std::map<std::string, std::string> const& Module::getRenaming() const {
174 STORM_LOG_THROW(this->isRenamedFromModule(), storm::exceptions::InvalidAccessException,
175 "Unable to retrieve renaming of module that was not created by renaming.");
176 return this->renaming.getRenaming();
177}
178
179std::set<uint_fast64_t> const& Module::getCommandIndicesByActionIndex(uint_fast64_t actionIndex) const {
180 auto actionIndicesCommandSetPair = this->actionIndicesToCommandIndexMap.find(actionIndex);
181 if (actionIndicesCommandSetPair != this->actionIndicesToCommandIndexMap.end()) {
182 return actionIndicesCommandSetPair->second;
183 }
184
185 STORM_LOG_THROW(false, storm::exceptions::OutOfRangeException, "Action index '" << actionIndex << "' does not exist in module.");
186}
187
188void Module::createMappings() {
189 // Clear the current mappings.
190 this->actionIndicesToCommandIndexMap.clear();
191 this->booleanVariableToIndexMap.clear();
192 this->integerVariableToIndexMap.clear();
193
194 // Create the mappings for the variables.
195 for (uint_fast64_t i = 0; i < this->booleanVariables.size(); ++i) {
196 this->booleanVariableToIndexMap[this->getBooleanVariables()[i].getName()] = i;
197 }
198 for (uint_fast64_t i = 0; i < this->integerVariables.size(); ++i) {
199 this->integerVariableToIndexMap[this->getIntegerVariables()[i].getName()] = i;
200 }
201 for (uint_fast64_t i = 0; i < this->clockVariables.size(); ++i) {
202 this->booleanVariableToIndexMap[this->getClockVariables()[i].getName()] = i;
203 }
204
205 // Add the mapping for all commands.
206 for (uint_fast64_t i = 0; i < this->commands.size(); i++) {
207 if (this->commands[i].isLabeled()) {
208 uint_fast64_t actionIndex = this->commands[i].getActionIndex();
209 if (this->actionIndicesToCommandIndexMap.find(actionIndex) == this->actionIndicesToCommandIndexMap.end()) {
210 this->actionIndicesToCommandIndexMap.emplace(actionIndex, std::set<uint_fast64_t>());
211 }
212 this->actionIndicesToCommandIndexMap[actionIndex].insert(i);
213
214 // Only take the command into the set if it's non-synchronizing.
215 if (actionIndex != 0) {
216 this->synchronizingActionIndices.insert(actionIndex);
217 }
218 }
219 }
220
221 // For all actions that are "in the module", but for which no command exists, we add the mapping to an empty
222 // set of commands.
223 for (auto const& actionIndex : this->synchronizingActionIndices) {
224 if (this->actionIndicesToCommandIndexMap.find(actionIndex) == this->actionIndicesToCommandIndexMap.end()) {
225 this->actionIndicesToCommandIndexMap[actionIndex] = std::set<uint_fast64_t>();
226 }
227 }
228}
229
231 // First construct the new vector of commands.
232 std::vector<storm::prism::Command> newCommands;
233 for (auto const& command : commands) {
234 if (indexSet.find(command.getGlobalIndex()) != indexSet.end()) {
235 newCommands.push_back(command);
236 }
237 }
238
239 return Module(this->getName(), this->getBooleanVariables(), this->getIntegerVariables(), this->getClockVariables(), this->getInvariant(), newCommands);
240}
241
243 // First construct the new vector of commands.
244 std::vector<storm::prism::Command> newCommands;
245 for (auto const& command : commands) {
246 if (actionIndices.find(command.getActionIndex()) != actionIndices.end()) {
247 newCommands.push_back(command);
248 }
249 }
250
251 return Module(this->getName(), this->getBooleanVariables(), this->getIntegerVariables(), this->getClockVariables(), this->getInvariant(), newCommands);
252}
253
254Module Module::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
255 std::vector<BooleanVariable> newBooleanVariables;
256 newBooleanVariables.reserve(this->getNumberOfBooleanVariables());
257 for (auto const& booleanVariable : this->getBooleanVariables()) {
258 newBooleanVariables.emplace_back(booleanVariable.substitute(substitution));
259 }
260
261 std::vector<IntegerVariable> newIntegerVariables;
262 newBooleanVariables.reserve(this->getNumberOfIntegerVariables());
263 for (auto const& integerVariable : this->getIntegerVariables()) {
264 newIntegerVariables.emplace_back(integerVariable.substitute(substitution));
265 }
266
267 std::vector<Command> newCommands;
268 newCommands.reserve(this->getNumberOfCommands());
269 for (auto const& command : this->getCommands()) {
270 newCommands.emplace_back(command.substitute(substitution));
271 }
272
273 return Module(this->getName(), newBooleanVariables, newIntegerVariables, this->getClockVariables(), this->getInvariant(), newCommands, this->getFilename(),
274 this->getLineNumber());
275}
276
278 std::vector<BooleanVariable> newBooleanVariables;
279 newBooleanVariables.reserve(this->getNumberOfBooleanVariables());
280 for (auto const& booleanVariable : this->getBooleanVariables()) {
281 newBooleanVariables.emplace_back(booleanVariable.substituteNonStandardPredicates());
282 }
283
284 std::vector<IntegerVariable> newIntegerVariables;
285 newBooleanVariables.reserve(this->getNumberOfIntegerVariables());
286 for (auto const& integerVariable : this->getIntegerVariables()) {
287 newIntegerVariables.emplace_back(integerVariable.substituteNonStandardPredicates());
288 }
289
290 std::vector<Command> newCommands;
291 newCommands.reserve(this->getNumberOfCommands());
292 for (auto const& command : this->getCommands()) {
293 newCommands.emplace_back(command.substituteNonStandardPredicates());
294 }
295
296 return Module(this->getName(), newBooleanVariables, newIntegerVariables, this->getClockVariables(), this->getInvariant(), newCommands, this->getFilename(),
297 this->getLineNumber());
298}
299
300Module Module::labelUnlabelledCommands(std::map<uint64_t, std::string> const& suggestions, uint64_t& newId,
301 std::map<std::string, uint64_t>& nameToIdMapping) const {
302 std::vector<Command> newCommands;
303 newCommands.reserve(this->getNumberOfCommands());
304 for (auto const& command : this->getCommands()) {
305 if (command.isLabeled()) {
306 newCommands.push_back(command);
307 } else {
308 if (suggestions.count(command.getGlobalIndex())) {
309 std::string newActionName = suggestions.at(command.getGlobalIndex());
310 auto it = nameToIdMapping.find(newActionName);
311 uint64_t actionId = newId;
312 if (it == nameToIdMapping.end()) {
313 nameToIdMapping[newActionName] = newId;
314 newId++;
315 } else {
316 actionId = it->second;
317 }
318 newCommands.emplace_back(command.getGlobalIndex(), command.isMarkovian(), actionId, newActionName, command.getGuardExpression(),
319 command.getUpdates(), command.getFilename(), command.getLineNumber());
320
321 } else {
322 std::string newActionName = getName() + "_cmd_" + std::to_string(command.getGlobalIndex());
323 newCommands.emplace_back(command.getGlobalIndex(), command.isMarkovian(), newId, newActionName, command.getGuardExpression(),
324 command.getUpdates(), command.getFilename(), command.getLineNumber());
325 nameToIdMapping[newActionName] = newId;
326 newId++;
327 }
328 }
329 }
330 return Module(this->getName(), booleanVariables, integerVariables, clockVariables, invariant, newCommands, this->getFilename(), this->getLineNumber());
331}
332
333bool Module::containsVariablesOnlyInUpdateProbabilities(std::set<storm::expressions::Variable> const& undefinedConstantVariables) const {
334 for (auto const& booleanVariable : this->getBooleanVariables()) {
335 if (booleanVariable.hasInitialValue() && booleanVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
336 return false;
337 }
338 }
339 for (auto const& integerVariable : this->getIntegerVariables()) {
340 if (integerVariable.hasInitialValue() && integerVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
341 return false;
342 }
343 if (integerVariable.hasLowerBoundExpression() && integerVariable.getLowerBoundExpression().containsVariable(undefinedConstantVariables)) {
344 return false;
345 }
346 if (integerVariable.hasUpperBoundExpression() && integerVariable.getUpperBoundExpression().containsVariable(undefinedConstantVariables)) {
347 return false;
348 }
349 }
350
351 for (auto const& command : this->getCommands()) {
352 if (!command.containsVariablesOnlyInUpdateProbabilities(undefinedConstantVariables)) {
353 return false;
354 }
355 }
356
357 return true;
358}
359
361 for (auto& variable : booleanVariables) {
362 variable.createMissingInitialValue();
363 }
364 for (auto& variable : integerVariables) {
365 variable.createMissingInitialValue();
366 }
367 for (auto& variable : clockVariables) {
368 variable.createMissingInitialValue();
369 }
370}
371
373 for (auto& variable : booleanVariables) {
374 variable.setInitialValueExpression(expressions::Expression());
375 }
376 for (auto& variable : integerVariables) {
377 variable.setInitialValueExpression(expressions::Expression());
378 }
379 for (auto& variable : clockVariables) {
380 variable.setInitialValueExpression(expressions::Expression());
381 }
382}
383
385 return this->invariant.isInitialized();
386}
387
389 return this->invariant;
390}
391
392std::ostream& operator<<(std::ostream& stream, Module const& module) {
393 stream << "module " << module.getName() << '\n';
394 for (auto const& booleanVariable : module.getBooleanVariables()) {
395 stream << "\t" << booleanVariable << '\n';
396 }
397 for (auto const& integerVariable : module.getIntegerVariables()) {
398 stream << "\t" << integerVariable << '\n';
399 }
400 for (auto const& clockVariable : module.getClockVariables()) {
401 stream << "\t" << clockVariable << '\n';
402 }
403 for (auto const& command : module.getCommands()) {
404 stream << "\t" << command << '\n';
405 }
406 stream << "endmodule\n";
407 return stream;
408}
409
410} // namespace prism
411} // namespace storm
bool isInitialized() const
Checks whether the object encapsulates a base-expression.
uint_fast64_t getLineNumber() const
Retrieves the line number in which the information was found.
std::string const & getFilename() const
Retrieves the name of the file in which the information was found.
Module substitute(std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution) const
Substitutes all variables in the module according to the given map.
Definition Module.cpp:254
std::size_t getNumberOfBooleanVariables() const
Retrieves the number of boolean variables in the module.
Definition Module.cpp:48
uint64_t getNumberOfUnlabeledCommands() const
Definition Module.cpp:153
void createMissingInitialValues()
Equips all of the modules' variables without initial values with initial values based on their type.
Definition Module.cpp:360
bool containsVariablesOnlyInUpdateProbabilities(std::set< storm::expressions::Variable > const &undefinedConstantVariables) const
Checks whether the given variables only appear in the update probabilities of the module and nowhere ...
Definition Module.cpp:333
std::vector< storm::prism::Command > const & getCommands() const
Retrieves the commands of the module.
Definition Module.cpp:133
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
storm::prism::Command const & getCommand(uint_fast64_t index) const
Retrieves a reference to the command with the given index.
Definition Module.cpp:129
storm::prism::ClockVariable const & getClockVariable(std::string const &variableName) const
Retrieves a reference to the clock variable with the given name.
Definition Module.cpp:82
std::string const & getBaseModule() const
If the module was created via renaming, this method retrieves the name of the module that was used as...
Definition Module.cpp:167
bool hasActionIndex(uint_fast64_t actionIndex) const
Retrieves whether or not this module contains a command labeled with the given action index.
Definition Module.cpp:149
Module substituteNonStandardPredicates() const
Nonstandard predicates such as ExacltyOneOff etc can be substituted.
Definition Module.cpp:277
void removeVariableInitialization()
Auxiliary function for Program::replaceVariableInitializationByInitExpression Effect: All of the modu...
Definition Module.cpp:372
std::vector< storm::prism::IntegerVariable > const & getIntegerVariables() const
Retrieves the integer variables of the module.
Definition Module.cpp:74
storm::prism::IntegerVariable const & getIntegerVariable(std::string const &variableName) const
Retrieves a reference to the integer variable with the given name.
Definition Module.cpp:67
std::set< uint_fast64_t > const & getCommandIndicesByActionIndex(uint_fast64_t actionIndex) const
Retrieves the indices of all commands within this module that are labelled by the given action.
Definition Module.cpp:179
Module restrictCommands(storm::storage::FlatSet< uint_fast64_t > const &indexSet) const
Creates a new module that drops all commands whose indices are not in the given set.
Definition Module.cpp:230
std::vector< storm::prism::BooleanVariable > const & getBooleanVariables() const
Retrieves the boolean variables of the module.
Definition Module.cpp:63
std::size_t getNumberOfClockVariables() const
Retrieves the number of clock variables in the module.
Definition Module.cpp:78
storm::expressions::Expression const & getInvariant() const
Returns the specified invariant (only relevant for PTA models)
Definition Module.cpp:388
bool isRenamedFromModule() const
Retrieves whether this module was created from another module via renaming.
Definition Module.cpp:163
bool hasInvariant() const
Returns true, if an invariant was specified (only relevant for PTA models)
Definition Module.cpp:384
Module labelUnlabelledCommands(std::map< uint64_t, std::string > const &suggestions, uint64_t &newId, std::map< std::string, uint64_t > &nameToIdMapping) const
Label unlabelled commands.
Definition Module.cpp:300
bool hasUnboundedVariables() const
Definition Module.cpp:39
std::string const & getName() const
Retrieves the name of the module.
Definition Module.cpp:141
std::set< storm::expressions::Variable > getAllExpressionVariables() const
Retrieves all expression variables used by this module.
Definition Module.cpp:93
std::size_t getNumberOfUpdates() const
Retrieves the total number of updates of this module.
Definition Module.cpp:121
std::set< uint_fast64_t > const & getSynchronizingActionIndices() const
Retrieves the set of synchronizing action indices present in this module.
Definition Module.cpp:145
std::vector< storm::prism::ClockVariable > const & getClockVariables() const
Retrieves the clock variables of the module.
Definition Module.cpp:89
Module restrictActionIndices(storm::storage::FlatSet< uint_fast64_t > const &actionIndices) const
Creates a new module that drops all commands whose action indices are not in the given set.
Definition Module.cpp:242
std::size_t getNumberOfIntegerVariables() const
Retrieves the number of integer variables in the module.
Definition Module.cpp:52
std::size_t getNumberOfCommands() const
Retrieves the number of commands of this module.
Definition Module.cpp:117
storm::prism::BooleanVariable const & getBooleanVariable(std::string const &variableName) const
Retrieves a reference to the boolean variable with the given name.
Definition Module.cpp:56
std::vector< storm::expressions::Expression > getAllRangeExpressions() const
Retrieves a list of expressions that characterize the legal ranges of all variables declared by this ...
Definition Module.cpp:107
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 ...
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
std::ostream & operator<<(std::ostream &stream, Assignment const &assignment)
boost::container::flat_set< Key, std::less< Key >, boost::container::new_allocator< Key > > FlatSet
Redefinition of flat_set was needed, because from Boost 1.70 on the default allocator is set to void.
Definition BoostTypes.h:13
LabParser.cpp.
Definition cli.cpp:18