mcrl2::pbes_system::pbes_type_checker¶

Include file:

#include "mcrl2/pbes/typecheck.h

class mcrl2::pbes_system::pbes_type_checker¶

Protected attributes¶

data::data_type_checker mcrl2::pbes_system::pbes_type_checker::m_data_type_checker¶

detail::pbes_context mcrl2::pbes_system::pbes_type_checker::m_pbes_context¶

data::detail::variable_context mcrl2::pbes_system::pbes_type_checker::m_variable_context¶

Protected member functions¶

std::vector<propositional_variable> equation_variables(const std::vector<pbes_equation> &equations)¶

pbes_expression typecheck(const pbes_expression &x, const data::variable_list &parameters)¶

Public member functions¶

pbes_expression operator()(const pbes_expression &x)¶

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.

void operator()(pbes &pbesspec)¶: Typecheck the pbes pbesspec.

pbes_type_checker(const data::data_specification &dataspec, const VariableContainer &global_variables, const PropositionalVariableContainer &propositional_variables)¶: Constructor.

pbes_type_checker(const data::data_specification &dataspec = data::data_specification())¶: Default constructor.