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 m_action_context
data::data_type_checker m_data_type_checker
detail::state_variable_context m_state_variable_context
data::detail::variable_context 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)