Storm
A Modern Probabilistic Model Checker
|
#include <Module.h>
Public Member Functions | |
Module (std::string const &moduleName, std::vector< storm::prism::BooleanVariable > const &booleanVariables, std::vector< storm::prism::IntegerVariable > const &integerVariables, std::vector< storm::prism::ClockVariable > const &clockVariables, storm::expressions::Expression const &invariant, std::vector< storm::prism::Command > const &commands, std::string const &filename="", uint_fast64_t lineNumber=0) | |
Creates a module with the given name, variables and commands. | |
Module (std::string const &moduleName, std::vector< storm::prism::BooleanVariable > const &booleanVariables, std::vector< storm::prism::IntegerVariable > const &integerVariables, std::vector< storm::prism::ClockVariable > const &clockVariables, storm::expressions::Expression const &invariant, std::vector< storm::prism::Command > const &commands, std::string const &renamedFromModule, storm::prism::ModuleRenaming const &renaming, std::string const &filename="", uint_fast64_t lineNumber=0) | |
Creates a module with the given name, variables and commands that is marked as being renamed from the given module with the given renaming. | |
Module ()=default | |
Module (Module const &other)=default | |
Module & | operator= (Module const &other)=default |
Module (Module &&other)=default | |
Module & | operator= (Module &&other)=default |
bool | hasUnboundedVariables () const |
std::size_t | getNumberOfBooleanVariables () const |
Retrieves the number of boolean variables in the module. | |
std::size_t | getNumberOfIntegerVariables () const |
Retrieves the number of integer variables in the 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::prism::BooleanVariable > const & | getBooleanVariables () const |
Retrieves the boolean 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::vector< storm::prism::IntegerVariable > const & | getIntegerVariables () const |
Retrieves the integer variables of the module. | |
std::size_t | getNumberOfClockVariables () const |
Retrieves the number of clock variables in the module. | |
storm::prism::ClockVariable const & | getClockVariable (std::string const &variableName) const |
Retrieves a reference to the clock variable with the given name. | |
std::vector< storm::prism::ClockVariable > const & | getClockVariables () const |
Retrieves the clock variables of the module. | |
std::set< storm::expressions::Variable > | getAllExpressionVariables () const |
Retrieves all expression variables used by this module. | |
std::vector< storm::expressions::Expression > | getAllRangeExpressions () const |
Retrieves a list of expressions that characterize the legal ranges of all variables declared by this module. | |
std::size_t | getNumberOfCommands () const |
Retrieves the number of commands of this module. | |
std::size_t | getNumberOfUpdates () const |
Retrieves the total number of updates of this module. | |
storm::prism::Command const & | getCommand (uint_fast64_t index) const |
Retrieves a reference to the command with the given index. | |
std::vector< storm::prism::Command > const & | getCommands () const |
Retrieves the commands of the module. | |
std::vector< storm::prism::Command > & | getCommands () |
Retrieves the commands of the module. | |
std::string const & | getName () const |
Retrieves the name of the module. | |
std::set< uint_fast64_t > const & | getSynchronizingActionIndices () const |
Retrieves the set of synchronizing action indices present in this module. | |
bool | hasActionIndex (uint_fast64_t actionIndex) const |
Retrieves whether or not this module contains a command labeled with the given action index. | |
bool | isRenamedFromModule () const |
Retrieves whether this module was created from another module via renaming. | |
std::string const & | getBaseModule () const |
If the module was created via renaming, this method retrieves the name of the module that was used as the in the base in the renaming process. | |
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 for the renaming process. | |
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. | |
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. | |
Module | substitute (std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution) const |
Substitutes all variables in the module according to the given map. | |
Module | substituteNonStandardPredicates () const |
Nonstandard predicates such as ExacltyOneOff etc can be substituted. | |
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 | 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 else. | |
void | createMissingInitialValues () |
Equips all of the modules' variables without initial values with initial values based on their type. | |
void | removeVariableInitialization () |
Auxiliary function for Program::replaceVariableInitializationByInitExpression Effect: All of the modules' variables are no longer initialized. | |
uint64_t | getNumberOfUnlabeledCommands () const |
bool | hasInvariant () const |
Returns true, if an invariant was specified (only relevant for PTA models) | |
storm::expressions::Expression const & | getInvariant () const |
Returns the specified invariant (only relevant for PTA models) | |
![]() | |
LocatedInformation (std::string const &filename, uint_fast64_t lineNumber) | |
Constructs a located information with the given filename and line number. | |
LocatedInformation ()=default | |
LocatedInformation (LocatedInformation const &other)=default | |
LocatedInformation & | operator= (LocatedInformation const &other)=default |
LocatedInformation (LocatedInformation &&other)=default | |
LocatedInformation & | operator= (LocatedInformation &&other)=default |
std::string const & | getFilename () const |
Retrieves the name of the file in which the information was found. | |
void | setFilename (std::string const &filename) |
Sets the filename of this information. | |
uint_fast64_t | getLineNumber () const |
Retrieves the line number in which the information was found. | |
void | setLineNumber (uint_fast64_t lineNumber) |
Sets the line number of this information. | |
Friends | |
std::ostream & | operator<< (std::ostream &stream, Module const &module) |
storm::prism::Module::Module | ( | std::string const & | moduleName, |
std::vector< storm::prism::BooleanVariable > const & | booleanVariables, | ||
std::vector< storm::prism::IntegerVariable > const & | integerVariables, | ||
std::vector< storm::prism::ClockVariable > const & | clockVariables, | ||
storm::expressions::Expression const & | invariant, | ||
std::vector< storm::prism::Command > const & | commands, | ||
std::string const & | filename = "" , |
||
uint_fast64_t | lineNumber = 0 |
||
) |
Creates a module with the given name, variables and commands.
moduleName | The name of the module. |
booleanVariables | The boolean variables defined by the module. |
integerVariables | The integer variables defined by the module. |
clockVariables | The clock variables defined by the module (only for PTA models). |
invariant | An invariant that is used to restrict the values of the clock variables (only for PTA models). |
commands | The commands of the module. |
filename | The filename in which the module is defined. |
lineNumber | The line number in which the module is defined. |
Definition at line 9 of file Module.cpp.
storm::prism::Module::Module | ( | std::string const & | moduleName, |
std::vector< storm::prism::BooleanVariable > const & | booleanVariables, | ||
std::vector< storm::prism::IntegerVariable > const & | integerVariables, | ||
std::vector< storm::prism::ClockVariable > const & | clockVariables, | ||
storm::expressions::Expression const & | invariant, | ||
std::vector< storm::prism::Command > const & | commands, | ||
std::string const & | renamedFromModule, | ||
storm::prism::ModuleRenaming const & | renaming, | ||
std::string const & | filename = "" , |
||
uint_fast64_t | lineNumber = 0 |
||
) |
Creates a module with the given name, variables and commands that is marked as being renamed from the given module with the given renaming.
moduleName | The name of the module. |
booleanVariables | The boolean variables defined by the module. |
integerVariables | The integer variables defined by the module. |
clockVariables | The clock variables defined by the module (only for PTA models). |
invariant | An invariant that is used to restrict the values of the clock variables (only for PTA models). |
commands | The commands of the module. |
renamedFromModule | The name of the module from which this module was renamed. |
renaming | The renaming of identifiers used to create this module. |
filename | The filename in which the module is defined. |
lineNumber | The line number in which the module is defined. |
Definition at line 17 of file Module.cpp.
|
default |
|
default |
|
default |
bool storm::prism::Module::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 else.
undefinedConstantVariables | A set of variables that may only appear in the update probabilities. |
Definition at line 333 of file Module.cpp.
void storm::prism::Module::createMissingInitialValues | ( | ) |
Equips all of the modules' variables without initial values with initial values based on their type.
Definition at line 360 of file Module.cpp.
std::set< storm::expressions::Variable > storm::prism::Module::getAllExpressionVariables | ( | ) | const |
Retrieves all expression variables used by this module.
Definition at line 93 of file Module.cpp.
std::vector< storm::expressions::Expression > storm::prism::Module::getAllRangeExpressions | ( | ) | const |
Retrieves a list of expressions that characterize the legal ranges of all variables declared by this module.
Definition at line 107 of file Module.cpp.
std::string const & storm::prism::Module::getBaseModule | ( | ) | const |
If the module was created via renaming, this method retrieves the name of the module that was used as the in the base in the renaming process.
Definition at line 167 of file Module.cpp.
storm::prism::BooleanVariable const & storm::prism::Module::getBooleanVariable | ( | std::string const & | variableName | ) | const |
Retrieves a reference to the boolean variable with the given name.
variableName | The name of the boolean variable to retrieve. |
Definition at line 56 of file Module.cpp.
std::vector< storm::prism::BooleanVariable > const & storm::prism::Module::getBooleanVariables | ( | ) | const |
Retrieves the boolean variables of the module.
Definition at line 63 of file Module.cpp.
storm::prism::ClockVariable const & storm::prism::Module::getClockVariable | ( | std::string const & | variableName | ) | const |
Retrieves a reference to the clock variable with the given name.
variableName | The name of the clock variable to retrieve. |
Definition at line 82 of file Module.cpp.
std::vector< storm::prism::ClockVariable > const & storm::prism::Module::getClockVariables | ( | ) | const |
Retrieves the clock variables of the module.
Definition at line 89 of file Module.cpp.
storm::prism::Command const & storm::prism::Module::getCommand | ( | uint_fast64_t | index | ) | const |
Retrieves a reference to the command with the given index.
index | The index of the command to retrieve. |
Definition at line 129 of file Module.cpp.
std::set< uint_fast64_t > const & storm::prism::Module::getCommandIndicesByActionIndex | ( | uint_fast64_t | actionIndex | ) | const |
Retrieves the indices of all commands within this module that are labelled by the given action.
actionIndex | The index of the action with which the commands have to be labelled. |
Definition at line 179 of file Module.cpp.
std::vector< storm::prism::Command > & storm::prism::Module::getCommands | ( | ) |
Retrieves the commands of the module.
Definition at line 137 of file Module.cpp.
std::vector< storm::prism::Command > const & storm::prism::Module::getCommands | ( | ) | const |
Retrieves the commands of the module.
Definition at line 133 of file Module.cpp.
storm::prism::IntegerVariable const & storm::prism::Module::getIntegerVariable | ( | std::string const & | variableName | ) | const |
Retrieves a reference to the integer variable with the given name.
variableName | The name of the integer variable to retrieve. |
Definition at line 67 of file Module.cpp.
std::vector< storm::prism::IntegerVariable > const & storm::prism::Module::getIntegerVariables | ( | ) | const |
Retrieves the integer variables of the module.
Definition at line 74 of file Module.cpp.
storm::expressions::Expression const & storm::prism::Module::getInvariant | ( | ) | const |
Returns the specified invariant (only relevant for PTA models)
Definition at line 388 of file Module.cpp.
std::string const & storm::prism::Module::getName | ( | ) | const |
Retrieves the name of the module.
Definition at line 141 of file Module.cpp.
std::size_t storm::prism::Module::getNumberOfBooleanVariables | ( | ) | const |
Retrieves the number of boolean variables in the module.
Definition at line 48 of file Module.cpp.
std::size_t storm::prism::Module::getNumberOfClockVariables | ( | ) | const |
Retrieves the number of clock variables in the module.
Definition at line 78 of file Module.cpp.
std::size_t storm::prism::Module::getNumberOfCommands | ( | ) | const |
Retrieves the number of commands of this module.
Definition at line 117 of file Module.cpp.
std::size_t storm::prism::Module::getNumberOfIntegerVariables | ( | ) | const |
Retrieves the number of integer variables in the module.
Definition at line 52 of file Module.cpp.
uint64_t storm::prism::Module::getNumberOfUnlabeledCommands | ( | ) | const |
Definition at line 153 of file Module.cpp.
std::size_t storm::prism::Module::getNumberOfUpdates | ( | ) | const |
Retrieves the total number of updates of this module.
Definition at line 121 of file Module.cpp.
std::map< std::string, std::string > const & storm::prism::Module::getRenaming | ( | ) | const |
If the module was created via renaming, this method returns the applied renaming of identifiers used for the renaming process.
Definition at line 173 of file Module.cpp.
std::set< uint_fast64_t > const & storm::prism::Module::getSynchronizingActionIndices | ( | ) | const |
Retrieves the set of synchronizing action indices present in this module.
Definition at line 145 of file Module.cpp.
bool storm::prism::Module::hasActionIndex | ( | uint_fast64_t | actionIndex | ) | const |
Retrieves whether or not this module contains a command labeled with the given action index.
actionIndex | The index of the action to look for in this module. |
Definition at line 149 of file Module.cpp.
bool storm::prism::Module::hasInvariant | ( | ) | const |
Returns true, if an invariant was specified (only relevant for PTA models)
Definition at line 384 of file Module.cpp.
bool storm::prism::Module::hasUnboundedVariables | ( | ) | const |
Definition at line 39 of file Module.cpp.
bool storm::prism::Module::isRenamedFromModule | ( | ) | const |
Retrieves whether this module was created from another module via renaming.
Definition at line 163 of file Module.cpp.
Module storm::prism::Module::labelUnlabelledCommands | ( | std::map< uint64_t, std::string > const & | suggestions, |
uint64_t & | newId, | ||
std::map< std::string, uint64_t > & | nameToIdMapping | ||
) | const |
Label unlabelled commands.
suggestions | Map from global index to names that is used to label unlabelled commands |
newId | The new action ids to use are given sequentially from this number onwards (and the argument is updated) |
nameToIdMapping | A mapping that is updated giving action indices to used names |
Definition at line 300 of file Module.cpp.
void storm::prism::Module::removeVariableInitialization | ( | ) |
Auxiliary function for Program::replaceVariableInitializationByInitExpression Effect: All of the modules' variables are no longer initialized.
Definition at line 372 of file Module.cpp.
Module storm::prism::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.
indexSet | The set of action indices for which to keep the commands. |
Definition at line 242 of file Module.cpp.
Module storm::prism::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.
indexSet | The set of indices for which to keep the commands. |
Definition at line 230 of file Module.cpp.
Module storm::prism::Module::substitute | ( | std::map< storm::expressions::Variable, storm::expressions::Expression > const & | substitution | ) | const |
Substitutes all variables in the module according to the given map.
substitution | The substitution to perform. |
Definition at line 254 of file Module.cpp.
Module storm::prism::Module::substituteNonStandardPredicates | ( | ) | const |
Nonstandard predicates such as ExacltyOneOff etc can be substituted.
Definition at line 277 of file Module.cpp.
|
friend |
Definition at line 392 of file Module.cpp.