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,
12 uint_fast64_t lineNumber)
13 :
Module(moduleName, booleanVariables, integerVariables, clockVariables, invariant, commands,
"",
storm::prism::
ModuleRenaming(), filename, lineNumber) {
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,
22 moduleName(moduleName),
23 booleanVariables(booleanVariables),
24 booleanVariableToIndexMap(),
25 integerVariables(integerVariables),
26 integerVariableToIndexMap(),
27 clockVariables(clockVariables),
28 clockVariableToIndexMap(),
31 synchronizingActionIndices(),
32 actionIndicesToCommandIndexMap(),
33 renamedFromModule(renamedFromModule),
36 this->createMappings();
40 for (
auto const& integerVariable : this->integerVariables) {
41 if (!integerVariable.hasLowerBoundExpression() || !integerVariable.hasUpperBoundExpression()) {
49 return this->booleanVariables.size();
53 return this->integerVariables.size();
57 auto const& nameIndexPair = this->booleanVariableToIndexMap.find(variableName);
58 STORM_LOG_THROW(nameIndexPair != this->booleanVariableToIndexMap.end(), storm::exceptions::InvalidArgumentException,
59 "Unknown boolean variable '" << variableName <<
"'.");
64 return this->booleanVariables;
68 auto const& nameIndexPair = this->integerVariableToIndexMap.find(variableName);
69 STORM_LOG_THROW(nameIndexPair != this->integerVariableToIndexMap.end(), storm::exceptions::InvalidArgumentException,
70 "Unknown integer variable '" << variableName <<
"'.");
75 return this->integerVariables;
79 return this->clockVariables.size();
83 auto const& nameIndexPair = this->clockVariableToIndexMap.find(variableName);
84 STORM_LOG_THROW(nameIndexPair != this->clockVariableToIndexMap.end(), storm::exceptions::InvalidArgumentException,
85 "Unknown clock variable '" << variableName <<
"'.");
90 return this->clockVariables;
94 std::set<storm::expressions::Variable> result;
96 result.insert(var.getExpressionVariable());
99 result.insert(var.getExpressionVariable());
102 result.insert(var.getExpressionVariable());
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());
118 return this->commands.size();
122 std::size_t result = 0;
124 result += command.getNumberOfUpdates();
130 return this->commands[index];
134 return this->commands;
138 return this->commands;
142 return this->moduleName;
146 return this->synchronizingActionIndices;
150 return this->actionIndicesToCommandIndexMap.find(actionIndex) != this->actionIndicesToCommandIndexMap.end();
155 for (
auto const& cmd : commands) {
156 if (!cmd.isLabeled()) {
164 return this->renamedFromModule !=
"";
169 "Unable to retrieve base module of module that was not created by renaming.");
170 return this->renamedFromModule;
175 "Unable to retrieve renaming of module that was not created by renaming.");
180 auto actionIndicesCommandSetPair = this->actionIndicesToCommandIndexMap.find(actionIndex);
181 if (actionIndicesCommandSetPair != this->actionIndicesToCommandIndexMap.end()) {
182 return actionIndicesCommandSetPair->second;
185 STORM_LOG_THROW(
false, storm::exceptions::OutOfRangeException,
"Action index '" << actionIndex <<
"' does not exist in module.");
188void Module::createMappings() {
190 this->actionIndicesToCommandIndexMap.clear();
191 this->booleanVariableToIndexMap.clear();
192 this->integerVariableToIndexMap.clear();
195 for (uint_fast64_t i = 0; i < this->booleanVariables.size(); ++i) {
198 for (uint_fast64_t i = 0; i < this->integerVariables.size(); ++i) {
201 for (uint_fast64_t i = 0; i < this->clockVariables.size(); ++i) {
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>());
212 this->actionIndicesToCommandIndexMap[actionIndex].insert(i);
215 if (actionIndex != 0) {
216 this->synchronizingActionIndices.insert(actionIndex);
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>();
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);
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);
255 std::vector<BooleanVariable> newBooleanVariables;
258 newBooleanVariables.emplace_back(booleanVariable.substitute(substitution));
261 std::vector<IntegerVariable> newIntegerVariables;
264 newIntegerVariables.emplace_back(integerVariable.substitute(substitution));
267 std::vector<Command> newCommands;
270 newCommands.emplace_back(command.substitute(substitution));
278 std::vector<BooleanVariable> newBooleanVariables;
281 newBooleanVariables.emplace_back(booleanVariable.substituteNonStandardPredicates());
284 std::vector<IntegerVariable> newIntegerVariables;
287 newIntegerVariables.emplace_back(integerVariable.substituteNonStandardPredicates());
290 std::vector<Command> newCommands;
293 newCommands.emplace_back(command.substituteNonStandardPredicates());
301 std::map<std::string, uint64_t>& nameToIdMapping)
const {
302 std::vector<Command> newCommands;
305 if (command.isLabeled()) {
306 newCommands.push_back(command);
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;
316 actionId = it->second;
318 newCommands.emplace_back(command.getGlobalIndex(), command.isMarkovian(), actionId, newActionName, command.getGuardExpression(),
319 command.getUpdates(), command.getFilename(), command.getLineNumber());
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;
335 if (booleanVariable.hasInitialValue() && booleanVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
340 if (integerVariable.hasInitialValue() && integerVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
343 if (integerVariable.hasLowerBoundExpression() && integerVariable.getLowerBoundExpression().containsVariable(undefinedConstantVariables)) {
346 if (integerVariable.hasUpperBoundExpression() && integerVariable.getUpperBoundExpression().containsVariable(undefinedConstantVariables)) {
352 if (!command.containsVariablesOnlyInUpdateProbabilities(undefinedConstantVariables)) {
361 for (
auto& variable : booleanVariables) {
362 variable.createMissingInitialValue();
364 for (
auto& variable : integerVariables) {
365 variable.createMissingInitialValue();
367 for (
auto& variable : clockVariables) {
368 variable.createMissingInitialValue();
373 for (
auto& variable : booleanVariables) {
376 for (
auto& variable : integerVariables) {
379 for (
auto& variable : clockVariables) {
389 return this->invariant;
393 stream <<
"module " <<
module.getName() << '\n';
394 for (
auto const& booleanVariable :
module.getBooleanVariables()) {
395 stream << "\t" << booleanVariable << '\n';
397 for (
auto const& integerVariable : module.getIntegerVariables()) {
398 stream <<
"\t" << integerVariable <<
'\n';
400 for (
auto const& clockVariable : module.getClockVariables()) {
401 stream <<
"\t" << clockVariable <<
'\n';
403 for (
auto const& command : module.getCommands()) {
404 stream <<
"\t" << command <<
'\n';
406 stream <<
"endmodule\n";
bool isInitialized() const
Checks whether the object encapsulates a base-expression.
Module substitute(std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution) const
Substitutes all variables in the module according to the given map.
std::size_t getNumberOfBooleanVariables() const
Retrieves the number of boolean variables in the module.
uint64_t getNumberOfUnlabeledCommands() const
void createMissingInitialValues()
Equips all of the modules' variables without initial values with initial values based on their type.
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 ...
std::vector< storm::prism::Command > const & getCommands() const
Retrieves the commands of the module.
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 ...
storm::prism::Command const & getCommand(uint_fast64_t index) const
Retrieves a reference to the command with the given index.
storm::prism::ClockVariable const & getClockVariable(std::string const &variableName) const
Retrieves a reference to the clock variable with the given name.
std::string const & getBaseModule() const
If the module was created via renaming, this method retrieves the name of the module that was used as...
bool hasActionIndex(uint_fast64_t actionIndex) const
Retrieves whether or not this module contains a command labeled with the given action index.
Module substituteNonStandardPredicates() const
Nonstandard predicates such as ExacltyOneOff etc can be substituted.
void removeVariableInitialization()
Auxiliary function for Program::replaceVariableInitializationByInitExpression Effect: All of the modu...
std::vector< storm::prism::IntegerVariable > const & getIntegerVariables() const
Retrieves the integer variables of the module.
storm::prism::IntegerVariable const & getIntegerVariable(std::string const &variableName) const
Retrieves a reference to the integer variable with the given name.
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.
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.
std::vector< storm::prism::BooleanVariable > const & getBooleanVariables() const
Retrieves the boolean variables of the module.
std::size_t getNumberOfClockVariables() const
Retrieves the number of clock variables in the module.
storm::expressions::Expression const & getInvariant() const
Returns the specified invariant (only relevant for PTA models)
bool isRenamedFromModule() const
Retrieves whether this module was created from another module via renaming.
bool hasInvariant() const
Returns true, if an invariant was specified (only relevant for PTA models)
Module labelUnlabelledCommands(std::map< uint64_t, std::string > const &suggestions, uint64_t &newId, std::map< std::string, uint64_t > &nameToIdMapping) const
Label unlabelled commands.
bool hasUnboundedVariables() const
std::string const & getName() const
Retrieves the name of the module.
std::set< storm::expressions::Variable > getAllExpressionVariables() const
Retrieves all expression variables used by this module.
std::size_t getNumberOfUpdates() const
Retrieves the total number of updates of this module.
std::set< uint_fast64_t > const & getSynchronizingActionIndices() const
Retrieves the set of synchronizing action indices present in this module.
std::vector< storm::prism::ClockVariable > const & getClockVariables() const
Retrieves the clock variables of the module.
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.
std::size_t getNumberOfIntegerVariables() const
Retrieves the number of integer variables in the module.
std::size_t getNumberOfCommands() const
Retrieves the number of commands of this module.
storm::prism::BooleanVariable const & getBooleanVariable(std::string const &variableName) const
Retrieves a reference to the boolean variable with the given name.
std::vector< storm::expressions::Expression > getAllRangeExpressions() const
Retrieves a list of expressions that characterize the legal ranges of all variables declared by this ...
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)
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.