mCRL2
Loading...
Searching...
No Matches
mcrl2::process::process_type_checker Class Reference

#include <typecheck.h>

Public Member Functions

template<typename VariableContainer , typename ActionLabelContainer , typename ProcessIdentifierContainer >
 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.
 
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.
 
void operator() (process_specification &procspec)
 Typecheck the process specification procspec.
 

Protected Member Functions

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

Static Protected Member Functions

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

Protected Attributes

data::data_type_checker m_data_type_checker
 
detail::action_context m_action_context
 
detail::process_context m_process_context
 
data::detail::variable_context m_variable_context
 

Detailed Description

Definition at line 588 of file typecheck.h.

Constructor & Destructor Documentation

◆ process_type_checker() [1/2]

template<typename VariableContainer , typename ActionLabelContainer , typename ProcessIdentifierContainer >
mcrl2::process::process_type_checker::process_type_checker ( const data::data_specification dataspec,
const VariableContainer &  variables,
const ActionLabelContainer &  action_labels,
const ProcessIdentifierContainer &  process_identifiers 
)
inline

Definition at line 608 of file typecheck.h.

◆ process_type_checker() [2/2]

mcrl2::process::process_type_checker::process_type_checker ( const data::data_specification dataspec = data::data_specification())
inlineexplicit

Default constructor.

Definition at line 621 of file typecheck.h.

Member Function Documentation

◆ equation_identifiers()

static std::vector< process_identifier > mcrl2::process::process_type_checker::equation_identifiers ( const std::vector< process_equation > &  equations)
inlinestaticprotected

Definition at line 596 of file typecheck.h.

◆ operator()() [1/2]

process_expression mcrl2::process::process_type_checker::operator() ( const process_expression x,
const process_identifier current_equation = nullptr 
)
inline

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

Parameters
[in]xA 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

Definition at line 630 of file typecheck.h.

◆ operator()() [2/2]

void mcrl2::process::process_type_checker::operator() ( process_specification procspec)
inline

Typecheck the process specification procspec.

Definition at line 636 of file typecheck.h.

◆ typecheck_process_expression()

process_expression mcrl2::process::process_type_checker::typecheck_process_expression ( const data::detail::variable_context variables,
const process_expression x,
const process_identifier current_equation = nullptr 
)
inlineprotected

Definition at line 672 of file typecheck.h.

Member Data Documentation

◆ m_action_context

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

Definition at line 592 of file typecheck.h.

◆ m_data_type_checker

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

Definition at line 591 of file typecheck.h.

◆ m_process_context

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

Definition at line 593 of file typecheck.h.

◆ m_variable_context

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

Definition at line 594 of file typecheck.h.


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