Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Module.h
Go to the documentation of this file.
1#ifndef STORM_STORAGE_PRISM_MODULE_H_
2#define STORM_STORAGE_PRISM_MODULE_H_
3
4#include <map>
5#include <memory>
6#include <set>
7#include <string>
8#include <vector>
9
16
17namespace storm {
18namespace prism {
19class Module : public LocatedInformation {
20 public:
33 Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables,
34 std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::ClockVariable> const& clockVariables,
35 storm::expressions::Expression const& invariant, std::vector<storm::prism::Command> const& commands, std::string const& filename = "",
36 uint_fast64_t lineNumber = 0);
37
53 Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables,
54 std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::ClockVariable> const& clockVariables,
55 storm::expressions::Expression const& invariant, std::vector<storm::prism::Command> const& commands, std::string const& renamedFromModule,
56 storm::prism::ModuleRenaming const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0);
57
58 // Create default implementations of constructors/assignment.
59 Module() = default;
60 Module(Module const& other) = default;
61 Module& operator=(Module const& other) = default;
62 Module(Module&& other) = default;
63 Module& operator=(Module&& other) = default;
64
68 bool hasUnboundedVariables() const;
69
75 std::size_t getNumberOfBooleanVariables() const;
76
82 std::size_t getNumberOfIntegerVariables() const;
83
90 storm::prism::BooleanVariable const& getBooleanVariable(std::string const& variableName) const;
91
97 std::vector<storm::prism::BooleanVariable> const& getBooleanVariables() const;
98
105 storm::prism::IntegerVariable const& getIntegerVariable(std::string const& variableName) const;
106
112 std::vector<storm::prism::IntegerVariable> const& getIntegerVariables() const;
113
119 std::size_t getNumberOfClockVariables() const;
120
127 storm::prism::ClockVariable const& getClockVariable(std::string const& variableName) const;
128
134 std::vector<storm::prism::ClockVariable> const& getClockVariables() const;
135
141 std::set<storm::expressions::Variable> getAllExpressionVariables() const;
142
149 std::vector<storm::expressions::Expression> getAllRangeExpressions() const;
150
156 std::size_t getNumberOfCommands() const;
157
163 std::size_t getNumberOfUpdates() const;
164
171 storm::prism::Command const& getCommand(uint_fast64_t index) const;
172
178 std::vector<storm::prism::Command> const& getCommands() const;
179
185 std::vector<storm::prism::Command>& getCommands();
186
192 std::string const& getName() const;
193
199 std::set<uint_fast64_t> const& getSynchronizingActionIndices() const;
200
207 bool hasActionIndex(uint_fast64_t actionIndex) const;
208
214 bool isRenamedFromModule() const;
215
222 std::string const& getBaseModule() const;
223
230 std::map<std::string, std::string> const& getRenaming() const;
231
238 std::set<uint_fast64_t> const& getCommandIndicesByActionIndex(uint_fast64_t actionIndex) const;
239
247
255
262 Module substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
263
269
278 Module labelUnlabelledCommands(std::map<uint64_t, std::string> const& suggestions, uint64_t& newId, std::map<std::string, uint64_t>& nameToIdMapping) const;
279
286 bool containsVariablesOnlyInUpdateProbabilities(std::set<storm::expressions::Variable> const& undefinedConstantVariables) const;
287
292
298
299 /*
300 * Gets the number of commands without a label
301 */
302 uint64_t getNumberOfUnlabeledCommands() const;
303
307 bool hasInvariant() const;
308
313
314 friend std::ostream& operator<<(std::ostream& stream, Module const& module);
315
316 private:
320 void createMappings();
321
322 // The name of the module.
323 std::string moduleName;
324
325 // A list of boolean variables.
326 std::vector<storm::prism::BooleanVariable> booleanVariables;
327
328 // A mapping from boolean variables to the corresponding indices in the vector.
329 std::map<std::string, uint_fast64_t> booleanVariableToIndexMap;
330
331 // A list of integer variables.
332 std::vector<storm::prism::IntegerVariable> integerVariables;
333
334 // A mapping from integer variables to the corresponding indices in the vector.
335 std::map<std::string, uint_fast64_t> integerVariableToIndexMap;
336
337 // A list of clock variables.
338 std::vector<storm::prism::ClockVariable> clockVariables;
339
340 // A mapping from clock variables to the corresponding indices in the vector.
341 std::map<std::string, uint_fast64_t> clockVariableToIndexMap;
342
343 // An invariant (only for PTA models)
345
346 // The commands associated with the module.
347 std::vector<storm::prism::Command> commands;
348
349 // The set of action indices present in this module.
350 std::set<uint_fast64_t> synchronizingActionIndices;
351
352 // A map of actions to the set of commands labeled with this action.
353 std::map<uint_fast64_t, std::set<uint_fast64_t>> actionIndicesToCommandIndexMap;
354
355 // This string indicates whether and from what module this module was created via renaming.
356 std::string renamedFromModule;
357
358 // If the module was created by renaming, this mapping contains the provided renaming of identifiers.
360};
361
362} // namespace prism
363} // namespace storm
364
365#endif /* STORM_STORAGE_PRISM_MODULE_H_ */
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
Module(Module &&other)=default
Module(Module const &other)=default
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
Module & operator=(Module const &other)=default
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
friend std::ostream & operator<<(std::ostream &stream, Module const &module)
Definition Module.cpp:392
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
Module & operator=(Module &&other)=default
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
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.