mcrl2/modal_formula/typecheck.h

Include file:

#include "mcrl2/modal_formula/typecheck.h"

add your file description here.

Classes

Functions

action_formula mcrl2::action_formulas::typecheck_action_formula(const action_formula &x, const data::data_specification &dataspec, const VariableContainer &variables, const ActionLabelContainer &actions)
action_formula mcrl2::action_formulas::typecheck_action_formula(const action_formula &x, const lps::specification &lpsspec)

Functions

typecheck_builder mcrl2::action_formulas::detail::make_typecheck_builder(data::data_type_checker &data_typechecker, const data::detail::variable_context &variables, const process::detail::action_context &actions)

Functions

regular_formula mcrl2::regular_formulas::typecheck_regular_formula(const regular_formula &x, const data::data_specification &dataspec, const VariableContainer &variables, const ActionLabelContainer &actions)
regular_formula mcrl2::regular_formulas::typecheck_regular_formula(const regular_formula &x, const lps::specification &lpsspec)

Functions

typecheck_builder mcrl2::regular_formulas::detail::make_typecheck_builder(data::data_type_checker &data_typechecker, const data::detail::variable_context &variables, const process::detail::action_context &actions)

Functions

state_formula mcrl2::state_formulas::typecheck_state_formula(const state_formula &x, const data::data_specification &dataspec = data::data_specification(), const ActionLabelContainer &action_labels = ActionLabelContainer(), const VariableContainer &variables = VariableContainer())

Type check a state formula. Throws an exception if something went wrong.

Parameters:

  • x A state formula that has not been type checked.
  • dataspec The data specification against which the formulas is checked.
  • action_labels A declaration of action labels that can be used in the state formulas.
  • variables A container with global data variables.

Post: formula is type checked.

state_formula mcrl2::state_formulas::typecheck_state_formula(const state_formula &x, const lps::specification &lpsspec)

Type check a state formula. Throws an exception if something went wrong.

Parameters:

  • x A state formula that has not been type checked.
  • lpsspec A linear process specifications containing data, action and global variable declarations to be used when typechecking the formula.

Post: formula is type checked.

void mcrl2::state_formulas::typecheck_state_formula_specification(state_formula_specification &formspec)

Typecheck the state formula specification formspec. It is assumed that the formula is self contained, i.e. all actions and sorts must be declared.

void mcrl2::state_formulas::typecheck_state_formula_specification(state_formula_specification &formspec, const lps::specification &lpsspec)

Typecheck the state formula specification formspec. It is assumed that the formula is not self contained, i.e. some of the actions and sorts may be declared in lpsspec.

Functions

typecheck_builder mcrl2::state_formulas::detail::make_typecheck_builder(data::data_type_checker &data_typechecker, const data::detail::variable_context &variable_context, const process::detail::action_context &action_context, const detail::state_variable_context &state_variable_context)