mcrl2/modal_formula/state_formula_rename.h

Include file:

#include "mcrl2/modal_formula/state_formula_rename.h"

Add your file description here.

Classes

• mcrl2::state_formulas::state_formula_predicate_variable_rename_builder
• mcrl2::state_formulas::state_formula_variable_rename_builder

Functions

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.

Parameters:

• generator A generator for fresh identifiers

Returns: a state_formula_predicate_variable_rename_builder

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.

Post: predicate variables within the same scope have different names

Parameters:

• f A modal formula
• generator A generator for fresh identifiers

Returns: The rename result

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.

Parameters:

• f A modal formula.
• forbidden_identifiers Set of identifiers strings, which are renamed.

Returns: The rename result.