mcrl2/modal_formula/has_name_clashes.h

Include file:

#include "mcrl2/modal_formula/has_name_clashes.h"

Classes

• mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_checker
• mcrl2::state_formulas::detail::state_variable_name_clash_checker

Functions

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.

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_data_variable_name_clashes(const state_formula &x)

Returns true if the formula contains parameter name clashes.

bool mcrl2::state_formulas::has_state_variable_name_clashes(const state_formula &x)

Returns true if the formula contains name clashes.