Add your file description here. More...

Classes
struct	mcrl2::state_formulas::state_formula_predicate_variable_rename_builder< IdentifierGenerator >

struct	mcrl2::state_formulas::state_formula_variable_rename_builder
	Visitor that renames variables using the specified identifier generator. Also bound variables are renamed! 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

Functions
template<typename IdentifierGenerator >
state_formula_predicate_variable_rename_builder< IdentifierGenerator >	mcrl2::state_formulas::make_state_formula_predicate_variable_rename_builder (IdentifierGenerator &generator)
	Utility function for creating a state_formula_predicate_variable_rename_builder.

template<typename IdentifierGenerator >
state_formula	mcrl2::state_formulas::rename_predicate_variables (const state_formula &f, IdentifierGenerator &generator)
	Renames predicate variables of the formula f using the specified identifier generator.

state_formula	mcrl2::state_formulas::rename_variables (const state_formula &f, const std::set< core::identifier_string > &forbidden_identifiers)
	Renames all data variables in the formula f such that the forbidden identifiers are not used.

Detailed Description

Add your file description here.

Classes