mcrl2::state_formulas::detail::has_unscoped_modal_formula_traverser Struct Reference

#include <preprocess_state_formula.h>

Inheritance diagram for mcrl2::state_formulas::detail::has_unscoped_modal_formula_traverser:

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

Public Member Functions
void	push (const state_formula &x)
void	pop ()
	has_unscoped_modal_formula_traverser ()
void	enter (const must &)
void	enter (const may &)
void	enter (const mu &x)
void	leave (const mu &)
void	enter (const nu &x)
void	leave (const nu &)
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
bool	result
std::vector< state_formula >	fixpoints

Detailed Description

Definition at line 141 of file preprocess_state_formula.h.

Member Typedef Documentation

super

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

Definition at line 143 of file preprocess_state_formula.h.

Constructor & Destructor Documentation

has_unscoped_modal_formula_traverser()

mcrl2::state_formulas::detail::has_unscoped_modal_formula_traverser::has_unscoped_modal_formula_traverser ( )

inline

Definition at line 161 of file preprocess_state_formula.h.

Member Function Documentation

enter() [1/4]

void mcrl2::state_formulas::detail::has_unscoped_modal_formula_traverser::enter ( const may &  )

inline

Definition at line 173 of file preprocess_state_formula.h.

enter() [2/4]

void mcrl2::state_formulas::detail::has_unscoped_modal_formula_traverser::enter ( const mu &  x )

inline

Definition at line 181 of file preprocess_state_formula.h.

enter() [3/4]

void mcrl2::state_formulas::detail::has_unscoped_modal_formula_traverser::enter ( const must &  )

inline

Definition at line 165 of file preprocess_state_formula.h.

enter() [4/4]

void mcrl2::state_formulas::detail::has_unscoped_modal_formula_traverser::enter ( const nu &  x )

inline

Definition at line 191 of file preprocess_state_formula.h.

leave() [1/2]

void mcrl2::state_formulas::detail::has_unscoped_modal_formula_traverser::leave ( const mu &  )

inline

Definition at line 186 of file preprocess_state_formula.h.

leave() [2/2]

void mcrl2::state_formulas::detail::has_unscoped_modal_formula_traverser::leave ( const nu &  )

inline

Definition at line 196 of file preprocess_state_formula.h.

pop()

void mcrl2::state_formulas::detail::has_unscoped_modal_formula_traverser::pop ( )

inline

Definition at line 156 of file preprocess_state_formula.h.

push()

void mcrl2::state_formulas::detail::has_unscoped_modal_formula_traverser::push ( const state_formula &  x )

inline

Definition at line 151 of file preprocess_state_formula.h.

Member Data Documentation

fixpoints

std::vector<state_formula> mcrl2::state_formulas::detail::has_unscoped_modal_formula_traverser::fixpoints

Definition at line 149 of file preprocess_state_formula.h.

result

bool mcrl2::state_formulas::detail::has_unscoped_modal_formula_traverser::result

Definition at line 148 of file preprocess_state_formula.h.

---

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

• modal_formula/include/mcrl2/modal_formula/preprocess_state_formula.h