mcrl2::state_formulas::detail::state_variable_name_clash_checker Class Reference

Traverser that checks for name clashes in nested mu's/nu's. More...

#include <has_name_clashes.h>

Inheritance diagram for mcrl2::state_formulas::detail::state_variable_name_clash_checker:

Public Types
using	super = state_formulas::state_formula_traverser< state_variable_name_clash_checker >
Public Types inherited from mcrl2::state_formulas::add_traverser_state_formula_expressions< Traverser, Derived >
using	super = Traverser< Derived >

Public Member Functions
void	pop ()
	Pops the stack.
void	push (const core::identifier_string &name)
	Pushes name on the stack.
void	enter (const mu &x)
void	leave (const mu &)
void	enter (const nu &x)
void	leave (const nu &)
Public Member Functions inherited from mcrl2::state_formulas::add_traverser_state_formula_expressions< Traverser, Derived >
void	apply (const state_formulas::true_ &x)
void	apply (const state_formulas::false_ &x)
void	apply (const state_formulas::not_ &x)
void	apply (const state_formulas::minus &x)
void	apply (const state_formulas::and_ &x)
void	apply (const state_formulas::or_ &x)
void	apply (const state_formulas::imp &x)
void	apply (const state_formulas::plus &x)
void	apply (const state_formulas::const_multiply &x)
void	apply (const state_formulas::const_multiply_alt &x)
void	apply (const state_formulas::forall &x)
void	apply (const state_formulas::exists &x)
void	apply (const state_formulas::infimum &x)
void	apply (const state_formulas::supremum &x)
void	apply (const state_formulas::sum &x)
void	apply (const state_formulas::must &x)
void	apply (const state_formulas::may &x)
void	apply (const state_formulas::yaled &x)
void	apply (const state_formulas::yaled_timed &x)
void	apply (const state_formulas::delay &x)
void	apply (const state_formulas::delay_timed &x)
void	apply (const state_formulas::variable &x)
void	apply (const state_formulas::nu &x)
void	apply (const state_formulas::mu &x)
void	apply (const state_formulas::state_formula_specification &x)
void	apply (const state_formulas::state_formula &x)

Public Attributes
std::vector< core::identifier_string >	m_name_stack
	The stack of names.

Detailed Description

Traverser that checks for name clashes in nested mu's/nu's.

Definition at line 23 of file has_name_clashes.h.

Member Typedef Documentation

super

using mcrl2::state_formulas::detail::state_variable_name_clash_checker::super = state_formulas::state_formula_traverser<state_variable_name_clash_checker>

Definition at line 26 of file has_name_clashes.h.

Member Function Documentation

enter() [1/2]

void mcrl2::state_formulas::detail::state_variable_name_clash_checker::enter ( const mu &  x )

inline

Definition at line 52 of file has_name_clashes.h.

enter() [2/2]

void mcrl2::state_formulas::detail::state_variable_name_clash_checker::enter ( const nu &  x )

inline

Definition at line 62 of file has_name_clashes.h.

leave() [1/2]

void mcrl2::state_formulas::detail::state_variable_name_clash_checker::leave ( const mu &  )

inline

Definition at line 57 of file has_name_clashes.h.

leave() [2/2]

void mcrl2::state_formulas::detail::state_variable_name_clash_checker::leave ( const nu &  )

inline

Definition at line 67 of file has_name_clashes.h.

pop()

void mcrl2::state_formulas::detail::state_variable_name_clash_checker::pop ( )

inline

Pops the stack.

Definition at line 36 of file has_name_clashes.h.

push()

void mcrl2::state_formulas::detail::state_variable_name_clash_checker::push ( const core::identifier_string &  name )

inline

Pushes name on the stack.

Definition at line 42 of file has_name_clashes.h.

Member Data Documentation

m_name_stack

std::vector<core::identifier_string> mcrl2::state_formulas::detail::state_variable_name_clash_checker::m_name_stack

The stack of names.

Definition at line 33 of file has_name_clashes.h.

---

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

• modal_formula/include/mcrl2/modal_formula/has_name_clashes.h