mcrl2::state_formulas::state_formula_predicate_variable_rename_builder< IdentifierGenerator > Struct Template Reference

#include <state_formula_rename.h>

Inheritance diagram for mcrl2::state_formulas::state_formula_predicate_variable_rename_builder< IdentifierGenerator >:

Public Types
typedef state_formulas::state_formula_builder< state_formula_predicate_variable_rename_builder< IdentifierGenerator > >	super
Public Types inherited from mcrl2::state_formulas::add_state_formula_expressions< Builder, Derived >
typedef Builder< Derived >	super

Public Member Functions
	state_formula_predicate_variable_rename_builder (IdentifierGenerator &generator)
	Constructor.
core::identifier_string	push (const core::identifier_string &n)
	Generates a new name for n, and adds a replacement to the replacement stack.
void	pop ()
	Removes the last added replacement.
template<class T >
void	apply (T &result, const variable &x)
	Visit var node.
template<class T >
void	apply (T &result, const mu &x)
	Visit mu node.
template<class T >
void	apply (T &result, const nu &x)
	Visit nu node.
Public Member Functions inherited from mcrl2::state_formulas::add_state_formula_expressions< Builder, Derived >
template<class T >
void	apply (T &result, const state_formulas::true_ &x)
template<class T >
void	apply (T &result, const state_formulas::false_ &x)
template<class T >
void	apply (T &result, const state_formulas::not_ &x)
template<class T >
void	apply (T &result, const state_formulas::minus &x)
template<class T >
void	apply (T &result, const state_formulas::and_ &x)
template<class T >
void	apply (T &result, const state_formulas::or_ &x)
template<class T >
void	apply (T &result, const state_formulas::imp &x)
template<class T >
void	apply (T &result, const state_formulas::plus &x)
template<class T >
void	apply (T &result, const state_formulas::const_multiply &x)
template<class T >
void	apply (T &result, const state_formulas::const_multiply_alt &x)
template<class T >
void	apply (T &result, const state_formulas::forall &x)
template<class T >
void	apply (T &result, const state_formulas::exists &x)
template<class T >
void	apply (T &result, const state_formulas::infimum &x)
template<class T >
void	apply (T &result, const state_formulas::supremum &x)
template<class T >
void	apply (T &result, const state_formulas::sum &x)
template<class T >
void	apply (T &result, const state_formulas::must &x)
template<class T >
void	apply (T &result, const state_formulas::may &x)
template<class T >
void	apply (T &result, const state_formulas::yaled &x)
template<class T >
void	apply (T &result, const state_formulas::yaled_timed &x)
template<class T >
void	apply (T &result, const state_formulas::delay &x)
template<class T >
void	apply (T &result, const state_formulas::delay_timed &x)
template<class T >
void	apply (T &result, const state_formulas::variable &x)
template<class T >
void	apply (T &result, const state_formulas::nu &x)
template<class T >
void	apply (T &result, const state_formulas::mu &x)
void	update (state_formulas::state_formula_specification &x)
template<class T >
void	apply (T &result, const state_formulas::state_formula &x)

Public Attributes
IdentifierGenerator &	generator
	An identifier generator.
std::deque< std::pair< core::identifier_string, core::identifier_string > >	replacements
	A stack of replacements. It may contain pairs with identical values.

Detailed Description

template<typename IdentifierGenerator>
struct mcrl2::state_formulas::state_formula_predicate_variable_rename_builder< IdentifierGenerator >

Visitor that renames predicate variables using the specified identifier generator.

Postcondition

In the generated formula, all predicate variables have different names.

Definition at line 26 of file state_formula_rename.h.

Member Typedef Documentation

super

template<typename IdentifierGenerator >

typedef state_formulas::state_formula_builder<state_formula_predicate_variable_rename_builder<IdentifierGenerator> > mcrl2::state_formulas::state_formula_predicate_variable_rename_builder< IdentifierGenerator >::super

Definition at line 28 of file state_formula_rename.h.

Constructor & Destructor Documentation

state_formula_predicate_variable_rename_builder()

template<typename IdentifierGenerator >

mcrl2::state_formulas::state_formula_predicate_variable_rename_builder< IdentifierGenerator >::state_formula_predicate_variable_rename_builder ( IdentifierGenerator &  generator )

inline

Constructor.

Parameters

generator

A generator for fresh identifiers

Definition at line 42 of file state_formula_rename.h.

Member Function Documentation

apply() [1/3]

template<typename IdentifierGenerator >

template<class T >

void mcrl2::state_formulas::state_formula_predicate_variable_rename_builder< IdentifierGenerator >::apply ( T &  result, const mu &  x  )

inline

Visit mu node.

Parameters

x	The mu state variable.

Returns

The result of visiting the node

Definition at line 84 of file state_formula_rename.h.

apply() [2/3]

template<typename IdentifierGenerator >

template<class T >

void mcrl2::state_formulas::state_formula_predicate_variable_rename_builder< IdentifierGenerator >::apply ( T &  result, const nu &  x  )

inline

Visit nu node.

Parameters

x	The visited nu node.

Returns

The result of visiting the node

Definition at line 97 of file state_formula_rename.h.

apply() [3/3]

template<typename IdentifierGenerator >

template<class T >

void mcrl2::state_formulas::state_formula_predicate_variable_rename_builder< IdentifierGenerator >::apply ( T &  result, const variable &  x  )

inline

Visit var node.

Parameters

x	A variable.

Returns

The result of visiting the node

Definition at line 66 of file state_formula_rename.h.

pop()

template<typename IdentifierGenerator >

void mcrl2::state_formulas::state_formula_predicate_variable_rename_builder< IdentifierGenerator >::pop ( )

inline

Removes the last added replacement.

Definition at line 57 of file state_formula_rename.h.

push()

template<typename IdentifierGenerator >

core::identifier_string mcrl2::state_formulas::state_formula_predicate_variable_rename_builder< IdentifierGenerator >::push ( const core::identifier_string &  n )

inline

Generates a new name for n, and adds a replacement to the replacement stack.

Parameters

n

A

Returns

The new name.

Definition at line 49 of file state_formula_rename.h.

Member Data Documentation

generator

template<typename IdentifierGenerator >

IdentifierGenerator& mcrl2::state_formulas::state_formula_predicate_variable_rename_builder< IdentifierGenerator >::generator

An identifier generator.

Definition at line 35 of file state_formula_rename.h.

replacements

template<typename IdentifierGenerator >

std::deque<std::pair<core::identifier_string, core::identifier_string> > mcrl2::state_formulas::state_formula_predicate_variable_rename_builder< IdentifierGenerator >::replacements

A stack of replacements. It may contain pairs with identical values.

Definition at line 38 of file state_formula_rename.h.

---

The documentation for this struct was generated from the following file:

• modal_formula/include/mcrl2/modal_formula/state_formula_rename.h