mcrl2/pbes/typecheck.h

Include file:

#include "mcrl2/pbes/typecheck.h"

add your file description here.

Classes

Functions

void mcrl2::pbes_system::typecheck_pbes(pbes &pbesspec)

Type check a parsed mCRL2 pbes specification. Throws an exception if something went wrong.

Parameters:

  • pbesspec A process specification that has not been type checked.

Post: pbesspec is type checked.

pbes_expression mcrl2::pbes_system::typecheck_pbes_expression(pbes_expression &x, const VariableContainer &variables, const PropositionalVariableContainer &propositional_variables, const data::data_specification &dataspec = data::data_specification())

Type check a parsed mCRL2 pbes expression. Throws an exception if something went wrong.

Parameters:

  • x A pbes expression.
  • variables A sequence of data variables that may appear in x.
  • propositional_variables A sequence of propositional variables that may appear in x.
  • dataspec A data specification.

Returns: the type checked expression

propositional_variable mcrl2::pbes_system::typecheck_propositional_variable(const propositional_variable &x, const VariableContainer &variables, const data::data_specification &dataspec = data::data_specification())

Type check a parsed mCRL2 propositional variable. Throws an exception if something went wrong.

Parameters:

  • x A propositional variable.
  • variables A sequence of data variables that may appear in x.
  • dataspec A data specification.

Returns: the type checked expression

Functions

typecheck_builder mcrl2::pbes_system::detail::make_typecheck_builder(data::data_type_checker &data_typechecker, const data::detail::variable_context &variables, const detail::pbes_context &propositional_variables)