mcrl2::pbes_system::pbes_type_checker Class Reference

#include <typecheck.h>

Public Member Functions
	pbes_type_checker (const data::data_specification &dataspec=data::data_specification())
	Default constructor.
template<typename VariableContainer , typename PropositionalVariableContainer >
	pbes_type_checker (const data::data_specification &dataspec, const VariableContainer &global_variables, const PropositionalVariableContainer &propositional_variables)
	Constructor.
void	operator() (pbes &pbesspec)
	Typecheck the pbes pbesspec.
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.

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)

Protected Attributes
data::data_type_checker	m_data_type_checker
data::detail::variable_context	m_variable_context
detail::pbes_context	m_pbes_context

Detailed Description

Definition at line 167 of file typecheck.h.

Constructor & Destructor Documentation

pbes_type_checker() [1/2]

mcrl2::pbes_system::pbes_type_checker::pbes_type_checker ( const data::data_specification &  dataspec = data::data_specification() )

inline

Default constructor.

Definition at line 186 of file typecheck.h.

pbes_type_checker() [2/2]

template<typename VariableContainer , typename PropositionalVariableContainer >

mcrl2::pbes_system::pbes_type_checker::pbes_type_checker ( const data::data_specification &  dataspec, const VariableContainer &  global_variables, const PropositionalVariableContainer &  propositional_variables  )

inline

Constructor.

Definition at line 192 of file typecheck.h.

Member Function Documentation

equation_variables()

std::vector< propositional_variable > mcrl2::pbes_system::pbes_type_checker::equation_variables ( const std::vector< pbes_equation > &  equations )

inlineprotected

Definition at line 174 of file typecheck.h.

operator()() [1/2]

pbes_expression mcrl2::pbes_system::pbes_type_checker::operator() ( const pbes_expression &  x )

inline

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

Parameters

[in]

x

A process expression that has not been type checked.

Returns

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

Definition at line 246 of file typecheck.h.

operator()() [2/2]

void mcrl2::pbes_system::pbes_type_checker::operator() ( pbes &  pbesspec )

inline

Typecheck the pbes pbesspec.

Definition at line 200 of file typecheck.h.

typecheck()

pbes_expression mcrl2::pbes_system::pbes_type_checker::typecheck ( const pbes_expression &  x, const data::variable_list &  parameters  )

inlineprotected

Definition at line 255 of file typecheck.h.

Member Data Documentation

m_data_type_checker

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

protected

Definition at line 170 of file typecheck.h.

m_pbes_context

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

protected

Definition at line 172 of file typecheck.h.

m_variable_context

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

protected

Definition at line 171 of file typecheck.h.

---

The documentation for this class was generated from the following file:

• pbes/include/mcrl2/pbes/typecheck.h