#include <VariableSet.h>

Public Member Functions
	VariableSet ()
	Creates an empty variable set.

detail::Variables< Variable >	getBooleanVariables ()
	Retrieves the boolean variables in this set.

detail::ConstVariables< Variable >	getBooleanVariables () const
	Retrieves the boolean variables in this set.

detail::Variables< Variable >	getBoundedIntegerVariables ()
	Retrieves the bounded integer variables in this set.

detail::ConstVariables< Variable >	getBoundedIntegerVariables () const
	Retrieves the bounded integer variables in this set.

detail::Variables< Variable >	getUnboundedIntegerVariables ()
	Retrieves the unbounded integer variables in this set.

detail::ConstVariables< Variable >	getUnboundedIntegerVariables () const
	Retrieves the unbounded integer variables in this set.

detail::Variables< Variable >	getRealVariables ()
	Retrieves the real variables in this set.

detail::ConstVariables< Variable >	getRealVariables () const
	Retrieves the real variables in this set.

detail::Variables< Variable >	getArrayVariables ()
	Retrieves the Array variables in this set.

detail::ConstVariables< Variable >	getArrayVariables () const
	Retrieves the Array variables in this set.

detail::Variables< Variable >	getClockVariables ()
	Retrieves the clock variables in this set.

detail::ConstVariables< Variable >	getClockVariables () const
	Retrieves the clock variables in this set.

detail::Variables< Variable >	getContinuousVariables ()
	Retrieves the continous variables in this set.

detail::ConstVariables< Variable >	getContinuousVariables () const
	Retrieves the continous variables in this set.

Variable const &	addVariable (Variable const &variable)
	Adds the given variable to this set.

std::vector< std::shared_ptr< Variable > >	dropAllArrayVariables ()
	Removes all array variables in this set.

bool	hasVariable (std::string const &name) const
	Retrieves whether this variable set contains a variable with the given name.

Variable const &	getVariable (std::string const &name) const
	Retrieves the variable with the given name.

bool	hasVariable (storm::jani::Variable const &variable) const
	Retrieves whether this variable set contains a given variable.

bool	hasVariable (storm::expressions::Variable const &variable) const
	Retrieves whether this variable set contains a variable with the expression variable.

Variable const &	getVariable (storm::expressions::Variable const &variable) const
	Retrieves the variable object associated with the given expression variable (if any).

std::shared_ptr< Variable >	eraseVariable (storm::expressions::Variable const &variable)
	Erases the given variable from this set.

bool	hasTransientVariable () const
	Retrieves whether this variable set contains a transient variable.

detail::Variables< Variable >::iterator	begin ()
	Retrieves an iterator to the variables in this set.

detail::ConstVariables< Variable >::iterator	begin () const
	Retrieves an iterator to the variables in this set.

detail::Variables< Variable >::iterator	end ()
	Retrieves the end iterator to the variables in this set.

detail::ConstVariables< Variable >::iterator	end () const
	Retrieves the end iterator to the variables in this set.

bool	containsBooleanVariable () const
	Retrieves whether the set of variables contains a boolean variable.

bool	containsBoundedIntegerVariable () const
	Retrieves whether the set of variables contains a bounded integer variable.

bool	containsUnboundedIntegerVariables () const
	Retrieves whether the set of variables contains an unbounded integer variable.

bool	containsRealVariables () const
	Retrieves whether the set of variables contains a real variable.

bool	containsArrayVariables () const
	Retrieves whether the set of variables contains a Array variable.

bool	containsClockVariables () const
	Retrieves whether the set of variables contains a clock variable.

bool	containsContinuousVariables () const
	Retrieves whether the set of variables contains a clock variable.

bool	containsNonTransientRealVariables () const
	Retrieves whether the set of variables contains a non-transient real variable.

bool	containsNonTransientUnboundedIntegerVariables () const
	Retrieves whether the set of variables contains a non-transient unbounded integer variable.

bool	empty () const
	Retrieves whether this variable set is empty.

uint64_t	getNumberOfVariables () const
	Total number of variables, including transient variables.

uint64_t	getNumberOfNontransientVariables () const

uint64_t	getNumberOfTransientVariables () const
	Retrieves the number of transient variables in this variable set.

uint64_t	getNumberOfRealTransientVariables () const
	Retrieves the number of real transient variables in this variable set.

uint64_t	getNumberOfUnboundedIntegerTransientVariables () const
	Retrieves the number of unbounded integer transient variables in this variable set.

uint64_t	getNumberOfNumericalTransientVariables () const
	Retrieves the number of numerical (i.e.

detail::ConstVariables< Variable >	getTransientVariables () const
	Retrieves the transient variables in this variable set.

bool	containsVariablesInBoundExpressionsOrInitialValues (std::set< storm::expressions::Variable > const &variables) const
	Checks whether any of the provided variables appears in bound expressions or initial values of the variables contained in this variable set.

std::map< std::string, std::reference_wrapper< Variable const > >	getNameToVariableMap () const
	Retrieves a mapping from variable names to (references of) the variable objects.

void	substitute (std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution, bool const substituteTranscendentalNumbers)
	Applies the given substitution to all variables in this set.

void	substituteExpressionVariables (std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution)
	Substitutes the actual variables according to the given substitution.

Detailed Description

Definition at line 21 of file VariableSet.h.

Constructor & Destructor Documentation

◆ VariableSet()

storm::jani::VariableSet::VariableSet ( )

Creates an empty variable set.

Definition at line 12 of file VariableSet.cpp.

Member Function Documentation

◆ addVariable()

Variable const & storm::jani::VariableSet::addVariable ( Variable const & variable )

Adds the given variable to this set.

Definition at line 99 of file VariableSet.cpp.

◆ begin() [1/2]

detail::Variables< Variable >::iterator storm::jani::VariableSet::begin ( )

Retrieves an iterator to the variables in this set.

Definition at line 182 of file VariableSet.cpp.

◆ begin() [2/2]

detail::ConstVariables< Variable >::iterator storm::jani::VariableSet::begin ( ) const

Retrieves an iterator to the variables in this set.

Definition at line 186 of file VariableSet.cpp.

◆ containsArrayVariables()

bool storm::jani::VariableSet::containsArrayVariables ( ) const

Retrieves whether the set of variables contains a Array variable.

Definition at line 234 of file VariableSet.cpp.

◆ containsBooleanVariable()

bool storm::jani::VariableSet::containsBooleanVariable ( ) const

Retrieves whether the set of variables contains a boolean variable.

Definition at line 218 of file VariableSet.cpp.

◆ containsBoundedIntegerVariable()

bool storm::jani::VariableSet::containsBoundedIntegerVariable ( ) const

Retrieves whether the set of variables contains a bounded integer variable.

Definition at line 222 of file VariableSet.cpp.

◆ containsClockVariables()

bool storm::jani::VariableSet::containsClockVariables ( ) const

Retrieves whether the set of variables contains a clock variable.

Definition at line 238 of file VariableSet.cpp.

◆ containsContinuousVariables()

bool storm::jani::VariableSet::containsContinuousVariables ( ) const

Retrieves whether the set of variables contains a clock variable.

Definition at line 242 of file VariableSet.cpp.

◆ containsNonTransientRealVariables()

bool storm::jani::VariableSet::containsNonTransientRealVariables ( ) const

Retrieves whether the set of variables contains a non-transient real variable.

Definition at line 246 of file VariableSet.cpp.

◆ containsNonTransientUnboundedIntegerVariables()

bool storm::jani::VariableSet::containsNonTransientUnboundedIntegerVariables ( ) const

Retrieves whether the set of variables contains a non-transient unbounded integer variable.

Definition at line 255 of file VariableSet.cpp.

◆ containsRealVariables()

bool storm::jani::VariableSet::containsRealVariables ( ) const

Retrieves whether the set of variables contains a real variable.

Definition at line 230 of file VariableSet.cpp.

◆ containsUnboundedIntegerVariables()

bool storm::jani::VariableSet::containsUnboundedIntegerVariables ( ) const

Retrieves whether the set of variables contains an unbounded integer variable.

Definition at line 226 of file VariableSet.cpp.

◆ containsVariablesInBoundExpressionsOrInitialValues()

bool storm::jani::VariableSet::containsVariablesInBoundExpressionsOrInitialValues ( std::set< storm::expressions::Variable > const & variables ) const

Checks whether any of the provided variables appears in bound expressions or initial values of the variables contained in this variable set.

Definition at line 324 of file VariableSet.cpp.

◆ dropAllArrayVariables()

std::vector< std::shared_ptr< Variable > > storm::jani::VariableSet::dropAllArrayVariables ( )

Removes all array variables in this set.

Definition at line 115 of file VariableSet.cpp.

◆ empty()

bool storm::jani::VariableSet::empty ( ) const

Retrieves whether this variable set is empty.

Definition at line 264 of file VariableSet.cpp.

◆ end() [1/2]

detail::Variables< Variable >::iterator storm::jani::VariableSet::end ( )

Retrieves the end iterator to the variables in this set.

Definition at line 190 of file VariableSet.cpp.

◆ end() [2/2]

detail::ConstVariables< Variable >::iterator storm::jani::VariableSet::end ( ) const

Retrieves the end iterator to the variables in this set.

Definition at line 194 of file VariableSet.cpp.

◆ eraseVariable()

std::shared_ptr< Variable > storm::jani::VariableSet::eraseVariable ( storm::expressions::Variable const & variable )

Erases the given variable from this set.

Definition at line 166 of file VariableSet.cpp.

◆ getArrayVariables() [1/2]

detail::Variables< Variable > storm::jani::VariableSet::getArrayVariables ( )

Retrieves the Array variables in this set.

Definition at line 48 of file VariableSet.cpp.

◆ getArrayVariables() [2/2]

detail::ConstVariables< Variable > storm::jani::VariableSet::getArrayVariables ( ) const

Retrieves the Array variables in this set.

Definition at line 52 of file VariableSet.cpp.

◆ getBooleanVariables() [1/2]

detail::Variables< Variable > storm::jani::VariableSet::getBooleanVariables ( )

Retrieves the boolean variables in this set.

Definition at line 16 of file VariableSet.cpp.

◆ getBooleanVariables() [2/2]

detail::ConstVariables< Variable > storm::jani::VariableSet::getBooleanVariables ( ) const

Retrieves the boolean variables in this set.

Definition at line 20 of file VariableSet.cpp.

◆ getBoundedIntegerVariables() [1/2]

detail::Variables< Variable > storm::jani::VariableSet::getBoundedIntegerVariables ( )

Retrieves the bounded integer variables in this set.

Definition at line 24 of file VariableSet.cpp.

◆ getBoundedIntegerVariables() [2/2]

detail::ConstVariables< Variable > storm::jani::VariableSet::getBoundedIntegerVariables ( ) const

Retrieves the bounded integer variables in this set.

Definition at line 28 of file VariableSet.cpp.

◆ getClockVariables() [1/2]

detail::Variables< Variable > storm::jani::VariableSet::getClockVariables ( )

Retrieves the clock variables in this set.

Definition at line 56 of file VariableSet.cpp.

◆ getClockVariables() [2/2]

detail::ConstVariables< Variable > storm::jani::VariableSet::getClockVariables ( ) const

Retrieves the clock variables in this set.

Definition at line 60 of file VariableSet.cpp.

◆ getContinuousVariables() [1/2]

detail::Variables< Variable > storm::jani::VariableSet::getContinuousVariables ( )

Retrieves the continous variables in this set.

Definition at line 64 of file VariableSet.cpp.

◆ getContinuousVariables() [2/2]

detail::ConstVariables< Variable > storm::jani::VariableSet::getContinuousVariables ( ) const

Retrieves the continous variables in this set.

Definition at line 68 of file VariableSet.cpp.

◆ getNameToVariableMap()

std::map< std::string, std::reference_wrapper< Variable const > > storm::jani::VariableSet::getNameToVariableMap ( ) const

Retrieves a mapping from variable names to (references of) the variable objects.

Definition at line 344 of file VariableSet.cpp.

◆ getNumberOfNontransientVariables()

uint64_t storm::jani::VariableSet::getNumberOfNontransientVariables ( ) const

Definition at line 273 of file VariableSet.cpp.

◆ getNumberOfNumericalTransientVariables()

uint_fast64_t storm::jani::VariableSet::getNumberOfNumericalTransientVariables ( ) const

Retrieves the number of numerical (i.e.

real, or integer) transient variables in this variable set.

Definition at line 307 of file VariableSet.cpp.

◆ getNumberOfRealTransientVariables()

uint_fast64_t storm::jani::VariableSet::getNumberOfRealTransientVariables ( ) const

Retrieves the number of real transient variables in this variable set.

Definition at line 287 of file VariableSet.cpp.

◆ getNumberOfTransientVariables()

uint_fast64_t storm::jani::VariableSet::getNumberOfTransientVariables ( ) const

Retrieves the number of transient variables in this variable set.

Definition at line 277 of file VariableSet.cpp.

◆ getNumberOfUnboundedIntegerTransientVariables()

uint_fast64_t storm::jani::VariableSet::getNumberOfUnboundedIntegerTransientVariables ( ) const

Retrieves the number of unbounded integer transient variables in this variable set.

Definition at line 297 of file VariableSet.cpp.

◆ getNumberOfVariables()

uint64_t storm::jani::VariableSet::getNumberOfVariables ( ) const

Total number of variables, including transient variables.

Definition at line 269 of file VariableSet.cpp.

◆ getRealVariables() [1/2]

detail::Variables< Variable > storm::jani::VariableSet::getRealVariables ( )

Retrieves the real variables in this set.

Definition at line 40 of file VariableSet.cpp.

◆ getRealVariables() [2/2]

detail::ConstVariables< Variable > storm::jani::VariableSet::getRealVariables ( ) const

Retrieves the real variables in this set.

Definition at line 44 of file VariableSet.cpp.

◆ getTransientVariables()

detail::ConstVariables< Variable > storm::jani::VariableSet::getTransientVariables ( ) const

Retrieves the transient variables in this variable set.

Definition at line 320 of file VariableSet.cpp.

◆ getUnboundedIntegerVariables() [1/2]

detail::Variables< Variable > storm::jani::VariableSet::getUnboundedIntegerVariables ( )

Retrieves the unbounded integer variables in this set.

Definition at line 32 of file VariableSet.cpp.

◆ getUnboundedIntegerVariables() [2/2]

detail::ConstVariables< Variable > storm::jani::VariableSet::getUnboundedIntegerVariables ( ) const

Retrieves the unbounded integer variables in this set.

Definition at line 36 of file VariableSet.cpp.

◆ getVariable() [1/2]

Variable const & storm::jani::VariableSet::getVariable ( std::string const & name ) const

Retrieves the variable with the given name.

Definition at line 150 of file VariableSet.cpp.

◆ getVariable() [2/2]

Variable const & storm::jani::VariableSet::getVariable ( storm::expressions::Variable const & variable ) const

Retrieves the variable object associated with the given expression variable (if any).

Definition at line 198 of file VariableSet.cpp.

◆ hasTransientVariable()

bool storm::jani::VariableSet::hasTransientVariable ( ) const

Retrieves whether this variable set contains a transient variable.

Definition at line 209 of file VariableSet.cpp.

◆ hasVariable() [1/3]

bool storm::jani::VariableSet::hasVariable ( std::string const & name ) const

Retrieves whether this variable set contains a variable with the given name.

Definition at line 142 of file VariableSet.cpp.

◆ hasVariable() [2/3]

bool storm::jani::VariableSet::hasVariable ( storm::expressions::Variable const & variable ) const

Retrieves whether this variable set contains a variable with the expression variable.

Definition at line 205 of file VariableSet.cpp.

◆ hasVariable() [3/3]

bool storm::jani::VariableSet::hasVariable ( storm::jani::Variable const & variable ) const

Retrieves whether this variable set contains a given variable.

Definition at line 146 of file VariableSet.cpp.

◆ substitute()

void storm::jani::VariableSet::substitute	(	std::map< storm::expressions::Variable, storm::expressions::Expression > const &	substitution,
		bool const	substituteTranscendentalNumbers
	)

Applies the given substitution to all variables in this set.

The substitution does not apply to the variables itself, but to initial expressions, variable bounds, ...

Parameters

substitution

Definition at line 354 of file VariableSet.cpp.

◆ substituteExpressionVariables()

void storm::jani::VariableSet::substituteExpressionVariables ( std::map< storm::expressions::Variable, storm::expressions::Expression > const & substitution )

Substitutes the actual variables according to the given substitution.