Public Member Functions
	JaniScopeChanger ()=default

void	makeVariableGlobal (storm::expressions::Variable const &variable, Model &model) const
	Moves the given variable to the global scope.

void	makeVariableLocal (storm::expressions::Variable const &variable, Model &model, uint64_t automatonIndex) const
	Moves the given variable into the local scope of the automaton with the given index.

bool	canMakeVariableGlobal (storm::expressions::Variable const &variable, Model const &model) const
	Checks whether this variable can be made global without introducing name clashes.

std::pair< bool, uint64_t >	canMakeVariableLocal (storm::expressions::Variable const &variable, Model const &model, storm::OptionalRef< std::vector< Property > const > properties=storm::NullRef, std::optional< uint64_t > automatonIndex=std::nullopt) const
	Checks whether this variable can be made local without introducing out-of-scope accesses.

void	makeVariablesGlobal (Model &model) const
	Moves as many variables to the global scope as possible.

void	makeVariablesLocal (Model &model, storm::OptionalRef< std::vector< Property > const > properties=storm::NullRef) const
	Moves as many variables to a local scope as possible.

Detailed Description

Definition at line 20 of file JaniScopeChanger.h.

Constructor & Destructor Documentation

storm::jani::JaniScopeChanger::JaniScopeChanger ( )

default

bool storm::jani::JaniScopeChanger::canMakeVariableGlobal	(	storm::expressions::Variable const &	variable,
		Model const &	model
	)		const

Checks whether this variable can be made global without introducing name clashes.

Definition at line 89 of file JaniScopeChanger.cpp.

std::pair< bool, uint64_t > storm::jani::JaniScopeChanger::canMakeVariableLocal	(	storm::expressions::Variable const &	variable,
		Model const &	model,
		storm::OptionalRef< std::vector< Property > const >	properties = `storm::NullRef`,
		std::optional< uint64_t >	automatonIndex = `std::nullopt`
	)		const

Checks whether this variable can be made local without introducing out-of-scope accesses.

Returns true if this is a case as well as an automaton index where to pout the variable

Definition at line 108 of file JaniScopeChanger.cpp.

void storm::jani::JaniScopeChanger::makeVariableGlobal	(	storm::expressions::Variable const &	variable,
		Model &	model
	)		const

Moves the given variable to the global scope.

It is not checked whether this introduces name clashes

Definition at line 66 of file JaniScopeChanger.cpp.

void storm::jani::JaniScopeChanger::makeVariableLocal	(	storm::expressions::Variable const &	variable,
		Model &	model,
		uint64_t	automatonIndex
	)		const

Moves the given variable into the local scope of the automaton with the given index.

It is not checked whether this introduces out-of-scope accesses.

Definition at line 81 of file JaniScopeChanger.cpp.

void storm::jani::JaniScopeChanger::makeVariablesGlobal ( Model & model ) const

Moves as many variables to the global scope as possible.

Definition at line 164 of file JaniScopeChanger.cpp.

void storm::jani::JaniScopeChanger::makeVariablesLocal	(	Model &	model,
		storm::OptionalRef< std::vector< Property > const >	properties = `storm::NullRef`
	)		const

Moves as many variables to a local scope as possible.

Definition at line 179 of file JaniScopeChanger.cpp.

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