mcrl2::state_formulas::state_formula_type_checker

Include file:

#include "mcrl2/modal_formula/typecheck.h

class mcrl2::state_formulas::state_formula_type_checker

Protected attributes

process::detail::action_context mcrl2::state_formulas::state_formula_type_checker::m_action_context

data::data_type_checker mcrl2::state_formulas::state_formula_type_checker::m_data_type_checker

detail::state_variable_context mcrl2::state_formulas::state_formula_type_checker::m_state_variable_context

data::detail::variable_context mcrl2::state_formulas::state_formula_type_checker::m_variable_context

Public member functions

state_formula_type_checker(const data::data_specification &dataspec, const ActionLabelContainer &action_labels = ActionLabelContainer(), const VariableContainer &variables = VariableContainer())

Constructor for a state_formula type checker.

Parameters:

• dataspec The data specification against which state formulas are checked.
• action_labels The data labels that can occur in a state formula.
• variables A container containing variables that can occur in state formulas.

state_formula typecheck_state_formula(const state_formula &x)