Maintains a multiset of bound data variables during traversal. More...

#include <add_binding.h>

Inheritance diagram for mcrl2::state_formulas::add_data_variable_binding< Builder, Derived >:

Public Types
typedef regular_formulas::add_data_variable_binding< Builder, Derived >	super

Public Types inherited from mcrl2::regular_formulas::add_data_variable_binding< Builder, Derived >
typedef action_formulas::add_data_variable_binding< Builder, Derived >	super

Public Types inherited from mcrl2::action_formulas::add_data_variable_binding< Builder, Derived >
typedef lps::add_data_variable_binding< Builder, Derived >	super

Public Types inherited from mcrl2::lps::add_data_variable_binding< Builder, Derived >
typedef data::add_data_variable_binding< Builder, Derived >	super

Public Types inherited from mcrl2::data::add_data_variable_binding< Builder, Derived >
typedef core::add_binding< Builder, Derived, variable >	super

Public Types inherited from mcrl2::core::add_binding< Builder, Derived, variable >
typedef Builder< Derived >	super

typedef variable	variable_type

Public Member Functions
void	enter (exists const &x)

void	leave (exists const &x)

void	enter (forall const &x)

void	leave (forall const &x)

void	enter (exists const &x)

void	enter (forall const &x)

void	enter (const action_summand &x)

void	enter (const stochastic_action_summand &x)

void	enter (const deadlock_summand &x)

void	enter (const linear_process &x)

void	enter (const stochastic_linear_process &x)

void	enter (const specification &x)

void	enter (const stochastic_specification &x)

void	enter (const stochastic_process_initializer &x)

void	enter (const data::where_clause &x)

void	enter (const data::forall &x)

void	enter (const data::exists &x)

void	enter (const data::lambda &x)

void	enter (const data::set_comprehension &x)

void	enter (const data::bag_comprehension &x)

void	enter (const data::untyped_set_or_bag_comprehension &x)

void	enter (const data::data_equation &x)

void	leave (exists const &x)

void	leave (forall const &x)

void	leave (const action_summand &x)

void	leave (const stochastic_action_summand &x)

void	leave (const deadlock_summand &x)

void	leave (const linear_process &x)

void	leave (const stochastic_linear_process &x)

void	leave (const specification &x)

void	leave (const stochastic_specification &x)

void	leave (const stochastic_process_initializer &x)

void	leave (const data::where_clause &x)

void	leave (const data::forall &x)

void	leave (const data::exists &x)

void	leave (const data::lambda &x)

void	leave (const data::set_comprehension &x)

void	leave (const data::bag_comprehension &x)

void	leave (const data::untyped_set_or_bag_comprehension &x)

void	leave (const data::data_equation &x)

void	increase_bind_count (const assignment_list &assignments)

void	decrease_bind_count (const assignment_list &assignments)

Public Member Functions inherited from mcrl2::regular_formulas::add_data_variable_binding< Builder, Derived >
void	enter (exists const &x)

void	enter (forall const &x)

void	enter (const action_summand &x)

void	enter (const stochastic_action_summand &x)

void	enter (const deadlock_summand &x)

void	enter (const linear_process &x)

void	enter (const stochastic_linear_process &x)

void	enter (const specification &x)

void	enter (const stochastic_specification &x)

void	enter (const stochastic_process_initializer &x)

void	enter (const data::where_clause &x)

void	enter (const data::forall &x)

void	enter (const data::exists &x)

void	enter (const data::lambda &x)

void	enter (const data::set_comprehension &x)

void	enter (const data::bag_comprehension &x)

void	enter (const data::untyped_set_or_bag_comprehension &x)

void	enter (const data::data_equation &x)

void	leave (exists const &x)

void	leave (forall const &x)

void	leave (const action_summand &x)

void	leave (const stochastic_action_summand &x)

void	leave (const deadlock_summand &x)

void	leave (const linear_process &x)

void	leave (const stochastic_linear_process &x)

void	leave (const specification &x)

void	leave (const stochastic_specification &x)

void	leave (const stochastic_process_initializer &x)

void	leave (const data::where_clause &x)

void	leave (const data::forall &x)

void	leave (const data::exists &x)

void	leave (const data::lambda &x)

void	leave (const data::set_comprehension &x)

void	leave (const data::bag_comprehension &x)

void	leave (const data::untyped_set_or_bag_comprehension &x)

void	leave (const data::data_equation &x)

void	increase_bind_count (const assignment_list &assignments)

void	decrease_bind_count (const assignment_list &assignments)

Public Member Functions inherited from mcrl2::action_formulas::add_data_variable_binding< Builder, Derived >
void	enter (exists const &x)

void	leave (exists const &x)

void	enter (forall const &x)

void	leave (forall const &x)

void	enter (const action_summand &x)

void	enter (const stochastic_action_summand &x)

void	enter (const deadlock_summand &x)

void	enter (const linear_process &x)

void	enter (const stochastic_linear_process &x)

void	enter (const specification &x)

void	enter (const stochastic_specification &x)

void	enter (const stochastic_process_initializer &x)

void	enter (const data::where_clause &x)

void	enter (const data::forall &x)

void	enter (const data::exists &x)

void	enter (const data::lambda &x)

void	enter (const data::set_comprehension &x)

void	enter (const data::bag_comprehension &x)

void	enter (const data::untyped_set_or_bag_comprehension &x)

void	enter (const data::data_equation &x)

void	leave (const action_summand &x)

void	leave (const stochastic_action_summand &x)

void	leave (const deadlock_summand &x)

void	leave (const linear_process &x)

void	leave (const stochastic_linear_process &x)

void	leave (const specification &x)

void	leave (const stochastic_specification &x)

void	leave (const stochastic_process_initializer &x)

void	leave (const data::where_clause &x)

void	leave (const data::forall &x)

void	leave (const data::exists &x)

void	leave (const data::lambda &x)

void	leave (const data::set_comprehension &x)

void	leave (const data::bag_comprehension &x)

void	leave (const data::untyped_set_or_bag_comprehension &x)

void	leave (const data::data_equation &x)

void	increase_bind_count (const assignment_list &assignments)

void	decrease_bind_count (const assignment_list &assignments)

Public Member Functions inherited from mcrl2::lps::add_data_variable_binding< Builder, Derived >
void	enter (const action_summand &x)

void	leave (const action_summand &x)

void	enter (const stochastic_action_summand &x)

void	leave (const stochastic_action_summand &x)

void	enter (const deadlock_summand &x)

void	leave (const deadlock_summand &x)

void	enter (const linear_process &x)

void	leave (const linear_process &x)

void	enter (const stochastic_linear_process &x)

void	leave (const stochastic_linear_process &x)

void	enter (const specification &x)

void	leave (const specification &x)

void	enter (const stochastic_specification &x)

void	leave (const stochastic_specification &x)

void	enter (const stochastic_process_initializer &x)

void	leave (const stochastic_process_initializer &x)

void	enter (const data::where_clause &x)

void	enter (const data::forall &x)

void	enter (const data::exists &x)

void	enter (const data::lambda &x)

void	enter (const data::set_comprehension &x)

void	enter (const data::bag_comprehension &x)

void	enter (const data::untyped_set_or_bag_comprehension &x)

void	enter (const data::data_equation &x)

void	leave (const data::where_clause &x)

void	leave (const data::forall &x)

void	leave (const data::exists &x)

void	leave (const data::lambda &x)

void	leave (const data::set_comprehension &x)

void	leave (const data::bag_comprehension &x)

void	leave (const data::untyped_set_or_bag_comprehension &x)

void	leave (const data::data_equation &x)

void	increase_bind_count (const assignment_list &assignments)

void	decrease_bind_count (const assignment_list &assignments)

Public Member Functions inherited from mcrl2::data::add_data_variable_binding< Builder, Derived >
void	increase_bind_count (const assignment_list &assignments)

void	decrease_bind_count (const assignment_list &assignments)

void	enter (const data::where_clause &x)

void	leave (const data::where_clause &x)

void	enter (const data::forall &x)

void	leave (const data::forall &x)

void	enter (const data::exists &x)

void	leave (const data::exists &x)

void	enter (const data::lambda &x)

void	leave (const data::lambda &x)

void	enter (const data::set_comprehension &x)

void	leave (const data::set_comprehension &x)

void	enter (const data::bag_comprehension &x)

void	leave (const data::bag_comprehension &x)

void	enter (const data::untyped_set_or_bag_comprehension &x)

void	leave (const data::untyped_set_or_bag_comprehension &x)

void	enter (const data::data_equation &x)

void	leave (const data::data_equation &x)

Public Member Functions inherited from mcrl2::core::add_binding< Builder, Derived, variable >
bool	is_bound (variable_type const &v) const
	Returns true if the variable v is bound.

const std::multiset< variable_type > &	bound_variables () const
	Returns the bound variables.

std::multiset< variable_type >::size_type	bind_count (const variable_type &v)
	Returns the bind count of the variable v.

Additional Inherited Members
Protected Member Functions inherited from mcrl2::core::add_binding< Builder, Derived, variable >
void	increase_bind_count (const variable_type &var)
	Add a variable to the multiset of bound variables.

void	increase_bind_count (const Container &variables, typename atermpp::enable_if_container< Container, variable_type >::type *=nullptr)
	Add a sequence of variables to the multiset of bound variables.

void	decrease_bind_count (const variable_type &var)
	Remove a variable from the multiset of bound variables.

void	decrease_bind_count (const Container &variables, typename atermpp::enable_if_container< Container, variable_type >::type *=nullptr)
	Remove a sequence of variables from the multiset of bound variables.

Protected Attributes inherited from mcrl2::core::add_binding< Builder, Derived, variable >
std::multiset< variable_type >	m_bound_variables

Detailed Description

template<template< class > class Builder, class Derived>
struct mcrl2::state_formulas::add_data_variable_binding< Builder, Derived >

Maintains a multiset of bound data variables during traversal.

Definition at line 170 of file add_binding.h.