typecheck.h File Reference

add your file description here. More...

Go to the source code of this file.

Classes
struct	mcrl2::action_formulas::detail::typecheck_builder
struct	mcrl2::regular_formulas::detail::typecheck_builder
struct	mcrl2::state_formulas::detail::typecheck_builder
class	mcrl2::state_formulas::state_formula_type_checker

Namespaces
namespace	mcrl2
	A class that takes a linear process specification and checks all tau-summands of that LPS for confluence.
namespace	mcrl2::action_formulas
namespace	mcrl2::action_formulas::detail
namespace	mcrl2::regular_formulas
namespace	mcrl2::regular_formulas::detail
namespace	mcrl2::state_formulas
namespace	mcrl2::state_formulas::detail

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)
template<typename ActionLabelContainer = std::vector<state_formulas::variable>, typename VariableContainer = std::vector<data::variable>>
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::stochastic_specification &lpsspec)
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)
template<typename ActionLabelContainer = std::vector<state_formulas::variable>, typename VariableContainer = std::vector<data::variable>>
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::stochastic_specification &lpsspec)
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, const bool formula_is_quantitative)
template<typename VariableContainer , typename ActionLabelContainer >
state_formula	mcrl2::state_formulas::typecheck_state_formula (const state_formula &x, const bool formula_is_quantitative, 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.
state_formula	mcrl2::state_formulas::typecheck_state_formula (const state_formula &x, const lps::stochastic_specification &lpsspec, const bool formula_is_quantitative)
	Type check a state formula. Throws an exception if something went wrong.
void	mcrl2::state_formulas::typecheck_state_formula_specification (state_formula_specification &formspec, const bool formula_is_quantitative)
	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::stochastic_specification &lpsspec, const bool formula_is_quantitative)
	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.

Detailed Description

add your file description here.

Definition in file typecheck.h.