mCRL2
Loading...
Searching...
No Matches
Public Types | Public Member Functions | Public Attributes | List of all members
mcrl2::state_formulas::detail::count_modal_operator_nesting_traverser Struct Reference

#include <preprocess_state_formula.h>

Inheritance diagram for mcrl2::state_formulas::detail::count_modal_operator_nesting_traverser:
mcrl2::state_formulas::state_formula_traverser< count_modal_operator_nesting_traverser > mcrl2::state_formulas::add_traverser_state_formula_expressions< Traverser, Derived >

Public Types

typedef state_formula_traverser< count_modal_operator_nesting_traverser > super
 
- Public Types inherited from mcrl2::state_formulas::add_traverser_state_formula_expressions< Traverser, Derived >
typedef Traverser< Derived > super
 

Public Member Functions

 count_modal_operator_nesting_traverser ()
 
void enter_scope ()
 
void leave_scope ()
 
void increase_nesting_depth ()
 
void decrease_nesting_depth ()
 
void enter (const must &)
 
void leave (const must &)
 
void enter (const may &)
 
void leave (const may &)
 
void enter (const mu &)
 
void leave (const mu &)
 
void enter (const nu &)
 
void leave (const nu &)
 
void enter (const forall &)
 
void leave (const forall &)
 
void enter (const exists &)
 
void leave (const exists &)
 
- Public Member Functions inherited from mcrl2::state_formulas::add_traverser_state_formula_expressions< Traverser, Derived >
void apply (const state_formulas::true_ &x)
 
void apply (const state_formulas::false_ &x)
 
void apply (const state_formulas::not_ &x)
 
void apply (const state_formulas::minus &x)
 
void apply (const state_formulas::and_ &x)
 
void apply (const state_formulas::or_ &x)
 
void apply (const state_formulas::imp &x)
 
void apply (const state_formulas::plus &x)
 
void apply (const state_formulas::const_multiply &x)
 
void apply (const state_formulas::const_multiply_alt &x)
 
void apply (const state_formulas::forall &x)
 
void apply (const state_formulas::exists &x)
 
void apply (const state_formulas::infimum &x)
 
void apply (const state_formulas::supremum &x)
 
void apply (const state_formulas::sum &x)
 
void apply (const state_formulas::must &x)
 
void apply (const state_formulas::may &x)
 
void apply (const state_formulas::yaled &x)
 
void apply (const state_formulas::yaled_timed &x)
 
void apply (const state_formulas::delay &x)
 
void apply (const state_formulas::delay_timed &x)
 
void apply (const state_formulas::variable &x)
 
void apply (const state_formulas::nu &x)
 
void apply (const state_formulas::mu &x)
 
void apply (const state_formulas::state_formula_specification &x)
 
void apply (const state_formulas::state_formula &x)
 

Public Attributes

std::size_t result
 
std::vector< std::size_t > nesting_depth
 

Detailed Description

Definition at line 32 of file preprocess_state_formula.h.

Member Typedef Documentation

◆ super

typedef state_formula_traverser<count_modal_operator_nesting_traverser> mcrl2::state_formulas::detail::count_modal_operator_nesting_traverser::super

Definition at line 34 of file preprocess_state_formula.h.

Constructor & Destructor Documentation

◆ count_modal_operator_nesting_traverser()

mcrl2::state_formulas::detail::count_modal_operator_nesting_traverser::count_modal_operator_nesting_traverser ( )
inline

Definition at line 42 of file preprocess_state_formula.h.

Member Function Documentation

◆ decrease_nesting_depth()

void mcrl2::state_formulas::detail::count_modal_operator_nesting_traverser::decrease_nesting_depth ( )
inline

Definition at line 67 of file preprocess_state_formula.h.

◆ enter() [1/6]

void mcrl2::state_formulas::detail::count_modal_operator_nesting_traverser::enter ( const exists &  )
inline

Definition at line 122 of file preprocess_state_formula.h.

◆ enter() [2/6]

void mcrl2::state_formulas::detail::count_modal_operator_nesting_traverser::enter ( const forall &  )
inline

Definition at line 112 of file preprocess_state_formula.h.

◆ enter() [3/6]

void mcrl2::state_formulas::detail::count_modal_operator_nesting_traverser::enter ( const may &  )
inline

Definition at line 82 of file preprocess_state_formula.h.

◆ enter() [4/6]

void mcrl2::state_formulas::detail::count_modal_operator_nesting_traverser::enter ( const mu &  )
inline

Definition at line 92 of file preprocess_state_formula.h.

◆ enter() [5/6]

void mcrl2::state_formulas::detail::count_modal_operator_nesting_traverser::enter ( const must &  )
inline

Definition at line 72 of file preprocess_state_formula.h.

◆ enter() [6/6]

void mcrl2::state_formulas::detail::count_modal_operator_nesting_traverser::enter ( const nu &  )
inline

Definition at line 102 of file preprocess_state_formula.h.

◆ enter_scope()

void mcrl2::state_formulas::detail::count_modal_operator_nesting_traverser::enter_scope ( )
inline

Definition at line 48 of file preprocess_state_formula.h.

◆ increase_nesting_depth()

void mcrl2::state_formulas::detail::count_modal_operator_nesting_traverser::increase_nesting_depth ( )
inline

Definition at line 58 of file preprocess_state_formula.h.

◆ leave() [1/6]

void mcrl2::state_formulas::detail::count_modal_operator_nesting_traverser::leave ( const exists &  )
inline

Definition at line 127 of file preprocess_state_formula.h.

◆ leave() [2/6]

void mcrl2::state_formulas::detail::count_modal_operator_nesting_traverser::leave ( const forall &  )
inline

Definition at line 117 of file preprocess_state_formula.h.

◆ leave() [3/6]

void mcrl2::state_formulas::detail::count_modal_operator_nesting_traverser::leave ( const may &  )
inline

Definition at line 87 of file preprocess_state_formula.h.

◆ leave() [4/6]

void mcrl2::state_formulas::detail::count_modal_operator_nesting_traverser::leave ( const mu &  )
inline

Definition at line 97 of file preprocess_state_formula.h.

◆ leave() [5/6]

void mcrl2::state_formulas::detail::count_modal_operator_nesting_traverser::leave ( const must &  )
inline

Definition at line 77 of file preprocess_state_formula.h.

◆ leave() [6/6]

void mcrl2::state_formulas::detail::count_modal_operator_nesting_traverser::leave ( const nu &  )
inline

Definition at line 107 of file preprocess_state_formula.h.

◆ leave_scope()

void mcrl2::state_formulas::detail::count_modal_operator_nesting_traverser::leave_scope ( )
inline

Definition at line 53 of file preprocess_state_formula.h.

Member Data Documentation

◆ nesting_depth

std::vector<std::size_t> mcrl2::state_formulas::detail::count_modal_operator_nesting_traverser::nesting_depth

Definition at line 40 of file preprocess_state_formula.h.

◆ result

std::size_t mcrl2::state_formulas::detail::count_modal_operator_nesting_traverser::result

Definition at line 39 of file preprocess_state_formula.h.

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