Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
storm::prism::Module Class Reference

#include <Module.h>

Inheritance diagram for storm::prism::Module:
Collaboration diagram for storm::prism::Module:

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
 
Moduleoperator= (Module const &other)=default
 
 Module (Module &&other)=default
 
Moduleoperator= (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::VariablegetAllExpressionVariables () const
 Retrieves all expression variables used by this module.
 
std::vector< storm::expressions::ExpressiongetAllRangeExpressions () 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)
 
- Public Member Functions inherited from storm::prism::LocatedInformation
 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
 
LocatedInformationoperator= (LocatedInformation const &other)=default
 
 LocatedInformation (LocatedInformation &&other)=default
 
LocatedInformationoperator= (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)
 

Detailed Description

Definition at line 20 of file Module.h.

Constructor & Destructor Documentation

◆ Module() [1/5]

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.

Parameters
moduleNameThe name of the module.
booleanVariablesThe boolean variables defined by the module.
integerVariablesThe integer variables defined by the module.
clockVariablesThe clock variables defined by the module (only for PTA models).
invariantAn invariant that is used to restrict the values of the clock variables (only for PTA models).
commandsThe commands of the module.
filenameThe filename in which the module is defined.
lineNumberThe line number in which the module is defined.

Definition at line 9 of file Module.cpp.

◆ Module() [2/5]

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.

Parameters
moduleNameThe name of the module.
booleanVariablesThe boolean variables defined by the module.
integerVariablesThe integer variables defined by the module.
clockVariablesThe clock variables defined by the module (only for PTA models).
invariantAn invariant that is used to restrict the values of the clock variables (only for PTA models).
commandsThe commands of the module.
renamedFromModuleThe name of the module from which this module was renamed.
renamingThe renaming of identifiers used to create this module.
filenameThe filename in which the module is defined.
lineNumberThe line number in which the module is defined.

Definition at line 17 of file Module.cpp.

◆ Module() [3/5]

storm::prism::Module::Module ( )
default

◆ Module() [4/5]

storm::prism::Module::Module ( Module const &  other)
default

◆ Module() [5/5]

storm::prism::Module::Module ( Module &&  other)
default

Member Function Documentation

◆ containsVariablesOnlyInUpdateProbabilities()

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.

Parameters
undefinedConstantVariablesA set of variables that may only appear in the update probabilities.
Returns
True iff the given variables only appear in the update probabilities of the module and nowhere else.

Definition at line 333 of file Module.cpp.

◆ createMissingInitialValues()

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.

◆ getAllExpressionVariables()

std::set< storm::expressions::Variable > storm::prism::Module::getAllExpressionVariables ( ) const

Retrieves all expression variables used by this module.

Returns
The set of expression variables used by this module.

Definition at line 93 of file Module.cpp.

◆ getAllRangeExpressions()

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.

Returns
The list of expressions that characterize the legal ranges.

Definition at line 107 of file Module.cpp.

◆ getBaseModule()

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.

Returns
The name of the module from which this module was created via renaming.

Definition at line 167 of file Module.cpp.

◆ getBooleanVariable()

storm::prism::BooleanVariable const & storm::prism::Module::getBooleanVariable ( std::string const &  variableName) const

Retrieves a reference to the boolean variable with the given name.

Parameters
variableNameThe name of the boolean variable to retrieve.
Returns
A reference to the boolean variable with the given name.

Definition at line 56 of file Module.cpp.

◆ getBooleanVariables()

std::vector< storm::prism::BooleanVariable > const & storm::prism::Module::getBooleanVariables ( ) const

Retrieves the boolean variables of the module.

Returns
The boolean variables of the module.

Definition at line 63 of file Module.cpp.

◆ getClockVariable()

storm::prism::ClockVariable const & storm::prism::Module::getClockVariable ( std::string const &  variableName) const

Retrieves a reference to the clock variable with the given name.

Parameters
variableNameThe name of the clock variable to retrieve.
Returns
A reference to the clock variable with the given name.

Definition at line 82 of file Module.cpp.

◆ getClockVariables()

std::vector< storm::prism::ClockVariable > const & storm::prism::Module::getClockVariables ( ) const

Retrieves the clock variables of the module.

Returns
The clock variables of the module.

Definition at line 89 of file Module.cpp.

◆ getCommand()

storm::prism::Command const & storm::prism::Module::getCommand ( uint_fast64_t  index) const

Retrieves a reference to the command with the given index.

Parameters
indexThe index of the command to retrieve.
Returns
A reference to the command with the given index.

Definition at line 129 of file Module.cpp.

◆ getCommandIndicesByActionIndex()

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.

Parameters
actionIndexThe index of the action with which the commands have to be labelled.
Returns
A set of indices of commands that are labelled with the given action index.

Definition at line 179 of file Module.cpp.

◆ getCommands() [1/2]

std::vector< storm::prism::Command > & storm::prism::Module::getCommands ( )

Retrieves the commands of the module.

Returns
The commands of the module.

Definition at line 137 of file Module.cpp.

◆ getCommands() [2/2]

std::vector< storm::prism::Command > const & storm::prism::Module::getCommands ( ) const

Retrieves the commands of the module.

Returns
The commands of the module.

Definition at line 133 of file Module.cpp.

◆ getIntegerVariable()

storm::prism::IntegerVariable const & storm::prism::Module::getIntegerVariable ( std::string const &  variableName) const

Retrieves a reference to the integer variable with the given name.

Parameters
variableNameThe name of the integer variable to retrieve.
Returns
A reference to the integer variable with the given name.

Definition at line 67 of file Module.cpp.

◆ getIntegerVariables()

std::vector< storm::prism::IntegerVariable > const & storm::prism::Module::getIntegerVariables ( ) const

Retrieves the integer variables of the module.

Returns
The integer variables of the module.

Definition at line 74 of file Module.cpp.

◆ getInvariant()

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.

◆ getName()

std::string const & storm::prism::Module::getName ( ) const

Retrieves the name of the module.

Returns
The name of the module.

Definition at line 141 of file Module.cpp.

◆ getNumberOfBooleanVariables()

std::size_t storm::prism::Module::getNumberOfBooleanVariables ( ) const

Retrieves the number of boolean variables in the module.

Returns
the number of boolean variables in the module.

Definition at line 48 of file Module.cpp.

◆ getNumberOfClockVariables()

std::size_t storm::prism::Module::getNumberOfClockVariables ( ) const

Retrieves the number of clock variables in the module.

Returns
the number of clock variables in the module.

Definition at line 78 of file Module.cpp.

◆ getNumberOfCommands()

std::size_t storm::prism::Module::getNumberOfCommands ( ) const

Retrieves the number of commands of this module.

Returns
The number of commands of this module.

Definition at line 117 of file Module.cpp.

◆ getNumberOfIntegerVariables()

std::size_t storm::prism::Module::getNumberOfIntegerVariables ( ) const

Retrieves the number of integer variables in the module.

Returns
The number of integer variables in the module.

Definition at line 52 of file Module.cpp.

◆ getNumberOfUnlabeledCommands()

uint64_t storm::prism::Module::getNumberOfUnlabeledCommands ( ) const

Definition at line 153 of file Module.cpp.

◆ getNumberOfUpdates()

std::size_t storm::prism::Module::getNumberOfUpdates ( ) const

Retrieves the total number of updates of this module.

Returns
The total number of updates of this module.

Definition at line 121 of file Module.cpp.

◆ getRenaming()

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.

Returns
A mapping of identifiers to new identifiers that was used in the renaming process.

Definition at line 173 of file Module.cpp.

◆ getSynchronizingActionIndices()

std::set< uint_fast64_t > const & storm::prism::Module::getSynchronizingActionIndices ( ) const

Retrieves the set of synchronizing action indices present in this module.

Returns
the set of synchronizing action indices present in this module.

Definition at line 145 of file Module.cpp.

◆ hasActionIndex()

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.

Parameters
actionIndexThe index of the action to look for in this module.
Returns
True iff the module has at least one command labeled with the given action index.

Definition at line 149 of file Module.cpp.

◆ hasInvariant()

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.

◆ hasUnboundedVariables()

bool storm::prism::Module::hasUnboundedVariables ( ) const
Returns
True iff the module contains at least one variable with infinite domain

Definition at line 39 of file Module.cpp.

◆ isRenamedFromModule()

bool storm::prism::Module::isRenamedFromModule ( ) const

Retrieves whether this module was created from another module via renaming.

Returns
True iff the module was created via renaming.

Definition at line 163 of file Module.cpp.

◆ labelUnlabelledCommands()

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.

Parameters
suggestionsMap from global index to names that is used to label unlabelled commands
newIdThe new action ids to use are given sequentially from this number onwards (and the argument is updated)
nameToIdMappingA mapping that is updated giving action indices to used names
Returns

Definition at line 300 of file Module.cpp.

◆ operator=() [1/2]

Module & storm::prism::Module::operator= ( Module &&  other)
default

◆ operator=() [2/2]

Module & storm::prism::Module::operator= ( Module const &  other)
default

◆ removeVariableInitialization()

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.

◆ restrictActionIndices()

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.

Parameters
indexSetThe set of action indices for which to keep the commands.
Returns
The module resulting from erasing all commands whose action indices are not in the given set.

Definition at line 242 of file Module.cpp.

◆ restrictCommands()

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.

Parameters
indexSetThe set of indices for which to keep the commands.
Returns
The module resulting from erasing all commands whose indices are not in the given set.

Definition at line 230 of file Module.cpp.

◆ substitute()

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.

Parameters
substitutionThe substitution to perform.
Returns
The resulting module.

Definition at line 254 of file Module.cpp.

◆ substituteNonStandardPredicates()

Module storm::prism::Module::substituteNonStandardPredicates ( ) const

Nonstandard predicates such as ExacltyOneOff etc can be substituted.

Returns

Definition at line 277 of file Module.cpp.

Friends And Related Symbol Documentation

◆ operator<<

std::ostream & operator<< ( std::ostream &  stream,
Module const &  module 
)
friend

Definition at line 392 of file Module.cpp.


The documentation for this class was generated from the following files: