mcrl2::process::process_type_checker

Include file:

#include "mcrl2/process/typecheck.h

class mcrl2::process::process_type_checker

Protected attributes

detail::action_context mcrl2::process::process_type_checker::m_action_context

data::data_type_checker mcrl2::process::process_type_checker::m_data_type_checker

detail::process_context mcrl2::process::process_type_checker::m_process_context

data::detail::variable_context mcrl2::process::process_type_checker::m_variable_context

Protected static member functions

static std::vector<process_identifier> equation_identifiers(const std::vector<process_equation> &equations)

Public member functions

process_expression operator()(const process_expression &x, const process_identifier *current_equation = nullptr)

Type check a process expression. Throws a mcrl2::runtime_error exception if the expression is not well typed.

Parameters:

• x A process expression that has not been type checked.

Returns: a process expression where all untyped identifiers have been replace by typed ones.

Typecheck the pbes pbesspec

void operator()(process_specification &procspec)

Typecheck the process specification procspec.

process_type_checker(const data::data_specification &dataspec, const VariableContainer &variables, const ActionLabelContainer &action_labels, const ProcessIdentifierContainer &process_identifiers)

process_type_checker(const data::data_specification &dataspec = data::data_specification())

Default constructor.

Protected member functions

process_expression typecheck_process_expression(const data::detail::variable_context &variables, const process_expression &x, const process_identifier *current_equation = nullptr)