mCRL2
Loading...
Searching...
No Matches
Public Types | Public Member Functions | Public Attributes | List of all members
mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_checker Class Reference

Traverser that checks for name clashes in parameters of nested mu's/nu's and forall/exists. More...

#include <has_name_clashes.h>

Inheritance diagram for mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_checker:
mcrl2::state_formulas::state_formula_traverser< state_formula_data_variable_name_clash_checker > mcrl2::state_formulas::add_traverser_state_formula_expressions< Traverser, Derived >

Public Types

typedef state_formulas::state_formula_traverser< state_formula_data_variable_name_clash_checker > super
 
- Public Types inherited from mcrl2::state_formulas::add_traverser_state_formula_expressions< Traverser, Derived >
typedef Traverser< Derived > super
 

Public Member Functions

void insert (const core::identifier_string &name, const state_formula &x)
 
void erase (const core::identifier_string &name)
 
void enter (const mu &x)
 
void leave (const mu &x)
 
void enter (const nu &x)
 
void leave (const nu &x)
 
void enter (const forall &x)
 
void leave (const forall &x)
 
void enter (const exists &x)
 
void leave (const exists &x)
 
- 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::set< core::identifier_string > m_names
 

Detailed Description

Traverser that checks for name clashes in parameters of nested mu's/nu's and forall/exists.

Definition at line 74 of file has_name_clashes.h.

Member Typedef Documentation

◆ super

typedef state_formulas::state_formula_traverser<state_formula_data_variable_name_clash_checker> mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_checker::super

Definition at line 77 of file has_name_clashes.h.

Member Function Documentation

◆ enter() [1/4]

void mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_checker::enter ( const exists &  x)
inline

Definition at line 148 of file has_name_clashes.h.

◆ enter() [2/4]

void mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_checker::enter ( const forall &  x)
inline

Definition at line 132 of file has_name_clashes.h.

◆ enter() [3/4]

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

Definition at line 100 of file has_name_clashes.h.

◆ enter() [4/4]

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

Definition at line 116 of file has_name_clashes.h.

◆ erase()

void mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_checker::erase ( const core::identifier_string &  name)
inline

Definition at line 95 of file has_name_clashes.h.

◆ insert()

void mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_checker::insert ( const core::identifier_string &  name,
const state_formula &  x 
)
inline

Definition at line 86 of file has_name_clashes.h.

◆ leave() [1/4]

void mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_checker::leave ( const exists &  x)
inline

Definition at line 156 of file has_name_clashes.h.

◆ leave() [2/4]

void mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_checker::leave ( const forall &  x)
inline

Definition at line 140 of file has_name_clashes.h.

◆ leave() [3/4]

void mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_checker::leave ( const mu &  x)
inline

Definition at line 108 of file has_name_clashes.h.

◆ leave() [4/4]

void mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_checker::leave ( const nu &  x)
inline

Definition at line 124 of file has_name_clashes.h.

Member Data Documentation

◆ m_names

std::set<core::identifier_string> mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_checker::m_names

Definition at line 83 of file has_name_clashes.h.

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