has_name_clashes.h File Reference

Go to the source code of this file.

Classes
class	mcrl2::state_formulas::detail::state_variable_name_clash_checker
	Traverser that checks for name clashes in nested mu's/nu's. More...
class	mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_checker
	Traverser that checks for name clashes in parameters of nested mu's/nu's and forall/exists. More...

Namespaces
namespace	mcrl2
	A class that takes a linear process specification and checks all tau-summands of that LPS for confluence.
namespace	mcrl2::state_formulas
namespace	mcrl2::state_formulas::detail

Functions
void	mcrl2::state_formulas::check_state_variable_name_clashes (const state_formula &x)
	Throws an exception if the formula contains name clashes.
bool	mcrl2::state_formulas::has_state_variable_name_clashes (const state_formula &x)
	Returns true if the formula contains name clashes.
void	mcrl2::state_formulas::check_data_variable_name_clashes (const state_formula &x)
	Throws an exception if the formula contains name clashes in the parameters of mu/nu/exists/forall.
bool	mcrl2::state_formulas::has_data_variable_name_clashes (const state_formula &x)
	Returns true if the formula contains parameter name clashes.