mcrl2::state_formulas::state_formula_type_checker Class Reference

#include <typecheck.h>

Public Member Functions
template<typename ActionLabelContainer = std::vector<state_formulas::variable>, typename VariableContainer = std::vector<data::variable>>
	state_formula_type_checker (const data::data_specification &dataspec, const bool formula_is_quantitative, const ActionLabelContainer &action_labels=ActionLabelContainer(), const VariableContainer &variables=VariableContainer())
	Constructor for a state_formula type checker.
state_formula	typecheck_state_formula (const state_formula &x)

Protected Attributes
data::data_type_checker	m_data_type_checker
data::detail::variable_context	m_variable_context
process::detail::action_context	m_action_context
detail::state_variable_context	m_state_variable_context
const bool	m_formula_is_quantitative

Detailed Description

Definition at line 729 of file typecheck.h.

Constructor & Destructor Documentation

state_formula_type_checker()

template<typename ActionLabelContainer = std::vector<state_formulas::variable>, typename VariableContainer = std::vector<data::variable>>

mcrl2::state_formulas::state_formula_type_checker::state_formula_type_checker ( const data::data_specification &  dataspec, const bool  formula_is_quantitative, const ActionLabelContainer &  action_labels = ActionLabelContainer(), const VariableContainer &  variables = VariableContainer()  )

inline

Constructor for a state_formula type checker.

Parameters

[in]	dataspec	The data specification against which state formulas are checked.
[in]	action_labels	The data labels that can occur in a state formula.
[in]	variables	A container containing variables that can occur in state formulas.

Definition at line 745 of file typecheck.h.

Member Function Documentation

typecheck_state_formula()

state_formula mcrl2::state_formulas::state_formula_type_checker::typecheck_state_formula ( const state_formula &  x )

inline

Definition at line 765 of file typecheck.h.

Member Data Documentation

m_action_context

process::detail::action_context mcrl2::state_formulas::state_formula_type_checker::m_action_context

protected

Definition at line 734 of file typecheck.h.

m_data_type_checker

data::data_type_checker mcrl2::state_formulas::state_formula_type_checker::m_data_type_checker

protected

Definition at line 732 of file typecheck.h.

m_formula_is_quantitative

const bool mcrl2::state_formulas::state_formula_type_checker::m_formula_is_quantitative

protected

Definition at line 736 of file typecheck.h.

m_state_variable_context

detail::state_variable_context mcrl2::state_formulas::state_formula_type_checker::m_state_variable_context

protected

Definition at line 735 of file typecheck.h.

m_variable_context

data::detail::variable_context mcrl2::state_formulas::state_formula_type_checker::m_variable_context

protected

Definition at line 733 of file typecheck.h.

---

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

• modal_formula/include/mcrl2/modal_formula/typecheck.h