mCRL2
Loading...
Searching...
No Matches
Public Types | Public Member Functions | List of all members
mcrl2::state_formulas::add_data_variable_traverser_binding< Builder, Derived > Struct Template Reference

#include <add_binding.h>

Inheritance diagram for mcrl2::state_formulas::add_data_variable_traverser_binding< Builder, Derived >:
mcrl2::state_formulas::add_data_variable_binding< Builder, Derived > mcrl2::regular_formulas::add_data_variable_binding< Builder, Derived > mcrl2::action_formulas::add_data_variable_binding< Builder, Derived > mcrl2::lps::add_data_variable_binding< Builder, Derived > mcrl2::data::add_data_variable_binding< Builder, Derived > mcrl2::core::add_binding< Builder, Derived, variable >

Public Types

typedef add_data_variable_binding< Builder, Derived > super
 
- Public Types inherited from mcrl2::state_formulas::add_data_variable_binding< Builder, Derived >
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 apply (const data::where_clause &x)
 
void enter (exists const &x)
 
void enter (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 (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::state_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 (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_traverser_binding< Builder, Derived >

Definition at line 204 of file add_binding.h.

Member Typedef Documentation

◆ super

template<template< class > class Builder, class Derived >
typedef add_data_variable_binding<Builder, Derived> mcrl2::state_formulas::add_data_variable_traverser_binding< Builder, Derived >::super

Definition at line 206 of file add_binding.h.

Member Function Documentation

◆ apply()

template<template< class > class Builder, class Derived >
void mcrl2::state_formulas::add_data_variable_traverser_binding< Builder, Derived >::apply ( const data::where_clause &  x)
inline

Definition at line 214 of file add_binding.h.

◆ decrease_bind_count()

template<template< class > class Builder, class Derived >
void mcrl2::data::add_data_variable_binding< Builder, Derived >::decrease_bind_count ( const assignment_list &  assignments)
inline

Definition at line 178 of file add_binding.h.

◆ enter() [1/20]

template<template< class > class Builder, class Derived >
void mcrl2::lps::add_data_variable_binding< Builder, Derived >::enter ( const action_summand &  x)
inline

Definition at line 173 of file add_binding.h.

◆ enter() [2/20]

template<template< class > class Builder, class Derived >
void mcrl2::data::add_data_variable_binding< Builder, Derived >::enter ( const data::bag_comprehension &  x)
inline

Definition at line 173 of file add_binding.h.

◆ enter() [3/20]

template<template< class > class Builder, class Derived >
void mcrl2::data::add_data_variable_binding< Builder, Derived >::enter ( const data::data_equation &  x)
inline

Definition at line 173 of file add_binding.h.

◆ enter() [4/20]

template<template< class > class Builder, class Derived >
void mcrl2::data::add_data_variable_binding< Builder, Derived >::enter ( const data::exists &  x)
inline

Definition at line 173 of file add_binding.h.

◆ enter() [5/20]

template<template< class > class Builder, class Derived >
void mcrl2::data::add_data_variable_binding< Builder, Derived >::enter ( const data::forall &  x)
inline

Definition at line 173 of file add_binding.h.

◆ enter() [6/20]

template<template< class > class Builder, class Derived >
void mcrl2::data::add_data_variable_binding< Builder, Derived >::enter ( const data::lambda &  x)
inline

Definition at line 173 of file add_binding.h.

◆ enter() [7/20]

template<template< class > class Builder, class Derived >
void mcrl2::data::add_data_variable_binding< Builder, Derived >::enter ( const data::set_comprehension &  x)
inline

Definition at line 173 of file add_binding.h.

◆ enter() [8/20]

template<template< class > class Builder, class Derived >
void mcrl2::data::add_data_variable_binding< Builder, Derived >::enter ( const data::untyped_set_or_bag_comprehension &  x)
inline

Definition at line 173 of file add_binding.h.

◆ enter() [9/20]

template<template< class > class Builder, class Derived >
void mcrl2::data::add_data_variable_binding< Builder, Derived >::enter ( const data::where_clause &  x)
inline

Definition at line 173 of file add_binding.h.

◆ enter() [10/20]

template<template< class > class Builder, class Derived >
void mcrl2::lps::add_data_variable_binding< Builder, Derived >::enter ( const deadlock_summand &  x)
inline

Definition at line 173 of file add_binding.h.

◆ enter() [11/20]

template<template< class > class Builder, class Derived >
void mcrl2::lps::add_data_variable_binding< Builder, Derived >::enter ( const linear_process &  x)
inline

Definition at line 173 of file add_binding.h.

◆ enter() [12/20]

template<template< class > class Builder, class Derived >
void mcrl2::lps::add_data_variable_binding< Builder, Derived >::enter ( const specification &  x)
inline

Definition at line 173 of file add_binding.h.

◆ enter() [13/20]

template<template< class > class Builder, class Derived >
void mcrl2::lps::add_data_variable_binding< Builder, Derived >::enter ( const stochastic_action_summand &  x)
inline

Definition at line 173 of file add_binding.h.

◆ enter() [14/20]

template<template< class > class Builder, class Derived >
void mcrl2::lps::add_data_variable_binding< Builder, Derived >::enter ( const stochastic_linear_process &  x)
inline

Definition at line 173 of file add_binding.h.

◆ enter() [15/20]

template<template< class > class Builder, class Derived >
void mcrl2::lps::add_data_variable_binding< Builder, Derived >::enter ( const stochastic_process_initializer &  x)
inline

Definition at line 173 of file add_binding.h.

◆ enter() [16/20]

template<template< class > class Builder, class Derived >
void mcrl2::lps::add_data_variable_binding< Builder, Derived >::enter ( const stochastic_specification &  x)
inline

Definition at line 173 of file add_binding.h.

◆ enter() [17/20]

template<template< class > class Builder, class Derived >
void mcrl2::state_formulas::add_data_variable_binding< Builder, Derived >::enter ( exists const &  x)
inline

Definition at line 180 of file add_binding.h.

◆ enter() [18/20]

template<template< class > class Builder, class Derived >
void mcrl2::action_formulas::add_data_variable_binding< Builder, Derived >::enter ( exists const &  x)
inline

Definition at line 173 of file add_binding.h.

◆ enter() [19/20]

template<template< class > class Builder, class Derived >
void mcrl2::state_formulas::add_data_variable_binding< Builder, Derived >::enter ( forall const &  x)
inline

Definition at line 190 of file add_binding.h.

◆ enter() [20/20]

template<template< class > class Builder, class Derived >
void mcrl2::action_formulas::add_data_variable_binding< Builder, Derived >::enter ( forall const &  x)
inline

Definition at line 173 of file add_binding.h.

◆ increase_bind_count()

template<template< class > class Builder, class Derived >
void mcrl2::data::add_data_variable_binding< Builder, Derived >::increase_bind_count ( const assignment_list &  assignments)
inline

Definition at line 177 of file add_binding.h.

◆ leave() [1/20]

template<template< class > class Builder, class Derived >
void mcrl2::lps::add_data_variable_binding< Builder, Derived >::leave ( const action_summand &  x)
inline

Definition at line 174 of file add_binding.h.

◆ leave() [2/20]

template<template< class > class Builder, class Derived >
void mcrl2::data::add_data_variable_binding< Builder, Derived >::leave ( const data::bag_comprehension &  x)
inline

Definition at line 174 of file add_binding.h.

◆ leave() [3/20]

template<template< class > class Builder, class Derived >
void mcrl2::data::add_data_variable_binding< Builder, Derived >::leave ( const data::data_equation &  x)
inline

Definition at line 174 of file add_binding.h.

◆ leave() [4/20]

template<template< class > class Builder, class Derived >
void mcrl2::data::add_data_variable_binding< Builder, Derived >::leave ( const data::exists &  x)
inline

Definition at line 174 of file add_binding.h.

◆ leave() [5/20]

template<template< class > class Builder, class Derived >
void mcrl2::data::add_data_variable_binding< Builder, Derived >::leave ( const data::forall &  x)
inline

Definition at line 174 of file add_binding.h.

◆ leave() [6/20]

template<template< class > class Builder, class Derived >
void mcrl2::data::add_data_variable_binding< Builder, Derived >::leave ( const data::lambda &  x)
inline

Definition at line 174 of file add_binding.h.

◆ leave() [7/20]

template<template< class > class Builder, class Derived >
void mcrl2::data::add_data_variable_binding< Builder, Derived >::leave ( const data::set_comprehension &  x)
inline

Definition at line 174 of file add_binding.h.

◆ leave() [8/20]

template<template< class > class Builder, class Derived >
void mcrl2::data::add_data_variable_binding< Builder, Derived >::leave ( const data::untyped_set_or_bag_comprehension &  x)
inline

Definition at line 174 of file add_binding.h.

◆ leave() [9/20]

template<template< class > class Builder, class Derived >
void mcrl2::data::add_data_variable_binding< Builder, Derived >::leave ( const data::where_clause &  x)
inline

Definition at line 174 of file add_binding.h.

◆ leave() [10/20]

template<template< class > class Builder, class Derived >
void mcrl2::lps::add_data_variable_binding< Builder, Derived >::leave ( const deadlock_summand &  x)
inline

Definition at line 174 of file add_binding.h.

◆ leave() [11/20]

template<template< class > class Builder, class Derived >
void mcrl2::lps::add_data_variable_binding< Builder, Derived >::leave ( const linear_process &  x)
inline

Definition at line 174 of file add_binding.h.

◆ leave() [12/20]

template<template< class > class Builder, class Derived >
void mcrl2::lps::add_data_variable_binding< Builder, Derived >::leave ( const specification &  x)
inline

Definition at line 174 of file add_binding.h.

◆ leave() [13/20]

template<template< class > class Builder, class Derived >
void mcrl2::lps::add_data_variable_binding< Builder, Derived >::leave ( const stochastic_action_summand &  x)
inline

Definition at line 174 of file add_binding.h.

◆ leave() [14/20]

template<template< class > class Builder, class Derived >
void mcrl2::lps::add_data_variable_binding< Builder, Derived >::leave ( const stochastic_linear_process &  x)
inline

Definition at line 174 of file add_binding.h.

◆ leave() [15/20]

template<template< class > class Builder, class Derived >
void mcrl2::lps::add_data_variable_binding< Builder, Derived >::leave ( const stochastic_process_initializer &  x)
inline

Definition at line 174 of file add_binding.h.

◆ leave() [16/20]

template<template< class > class Builder, class Derived >
void mcrl2::lps::add_data_variable_binding< Builder, Derived >::leave ( const stochastic_specification &  x)
inline

Definition at line 174 of file add_binding.h.

◆ leave() [17/20]

template<template< class > class Builder, class Derived >
void mcrl2::state_formulas::add_data_variable_binding< Builder, Derived >::leave ( exists const &  x)
inline

Definition at line 185 of file add_binding.h.

◆ leave() [18/20]

template<template< class > class Builder, class Derived >
void mcrl2::action_formulas::add_data_variable_binding< Builder, Derived >::leave ( exists const &  x)
inline

Definition at line 174 of file add_binding.h.

◆ leave() [19/20]

template<template< class > class Builder, class Derived >
void mcrl2::action_formulas::add_data_variable_binding< Builder, Derived >::leave ( forall const &  x)
inline

Definition at line 174 of file add_binding.h.

◆ leave() [20/20]

template<template< class > class Builder, class Derived >
void mcrl2::state_formulas::add_data_variable_binding< Builder, Derived >::leave ( forall const &  x)
inline

Definition at line 195 of file add_binding.h.

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