#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

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)

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

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)

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

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.

◆ 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

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.

◆ 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

undefinedConstantVariables A 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

variableName The 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

variableName The 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

index The 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

actionIndex The 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

variableName The 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

actionIndex The 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

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

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

indexSet The 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

indexSet The 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

substitution The 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:

src/storm/storage/prism/Module.h
src/storm/storage/prism/Module.cpp

Public Member Functions

Friends

Detailed Description

Constructor & Destructor Documentation

◆ Module() [1/5]

◆ Module() [2/5]

◆ Module() [3/5]

◆ Module() [4/5]

◆ Module() [5/5]

Member Function Documentation

◆ containsVariablesOnlyInUpdateProbabilities()

◆ createMissingInitialValues()

◆ getAllExpressionVariables()

◆ getAllRangeExpressions()

◆ getBaseModule()

◆ getBooleanVariable()

◆ getBooleanVariables()

◆ getClockVariable()

◆ getClockVariables()

◆ getCommand()

◆ getCommandIndicesByActionIndex()

◆ getCommands() [1/2]

◆ getCommands() [2/2]

◆ getIntegerVariable()

◆ getIntegerVariables()

◆ getInvariant()

◆ getName()

◆ getNumberOfBooleanVariables()

◆ getNumberOfClockVariables()

◆ getNumberOfCommands()

◆ getNumberOfIntegerVariables()

◆ getNumberOfUnlabeledCommands()

◆ getNumberOfUpdates()

◆ getRenaming()

◆ getSynchronizingActionIndices()

◆ hasActionIndex()

◆ hasInvariant()

◆ hasUnboundedVariables()

◆ isRenamedFromModule()

◆ labelUnlabelledCommands()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ removeVariableInitialization()

◆ restrictActionIndices()

◆ restrictCommands()

◆ substitute()

◆ substituteNonStandardPredicates()

Friends And Related Symbol Documentation

◆ operator<<