mcrl2::pbes_system::detail::ppg_visitor Class Reference

#include <ppg_visitor.h>

Public Types
using	bqnf = bqnf_visitor
	The BQNF visitor type.

Public Member Functions
virtual	~ppg_visitor ()=default
	Destructor.
	ppg_visitor ()=default
	Constructor.
virtual bool	visit_simple_expression (const pbes_expression &e)
	Visits a simple expression. An expression is simple if it does not contain propositional variables.
virtual bool	visit_propositional_variable (const pbes_expression &e)
	Visits a propositional variable expression.
virtual bool	visit_inner_and (const pbes_expression &e)
	Visits a conjunctive expression within an inner existential quantifier expression.
virtual bool	visit_inner_bounded_exists (const pbes_expression &e)
	Visits a bounded existential quantifier expression within a disjunctive expression.
virtual bool	visit_or (const pbes_expression &e)
	Visits a disjunctive expression.
virtual bool	visit_inner_implies (const pbes_expression &e)
	Visits a disjunctive expression within an inner universal quantifier expression.
virtual bool	visit_inner_bounded_forall (const pbes_expression &e)
	Visits a bounded universal quantifier expression within a conjunctive expression.
virtual bool	visit_and (const pbes_expression &e)
	Visits a conjunctive expression.
virtual bool	visit_ppg_expression (const pbes_expression &e)
	Visits a PPG expression.

Static Public Member Functions
static std::string	print_brief (const pbes_expression &e)
	Returns a string representation of the type of the root node of the expression.

Detailed Description

Definition at line 23 of file ppg_visitor.h.

Member Typedef Documentation

bqnf

using mcrl2::pbes_system::detail::ppg_visitor::bqnf = bqnf_visitor

The BQNF visitor type.

Definition at line 27 of file ppg_visitor.h.

Constructor & Destructor Documentation

~ppg_visitor()

virtual mcrl2::pbes_system::detail::ppg_visitor::~ppg_visitor ( )

virtualdefault

Destructor.

ppg_visitor()

mcrl2::pbes_system::detail::ppg_visitor::ppg_visitor ( )

default

Constructor.

Member Function Documentation

print_brief()

static std::string mcrl2::pbes_system::detail::ppg_visitor::print_brief ( const pbes_expression &  e )

inlinestatic

Returns a string representation of the type of the root node of the expression.

Parameters

e	a PBES expression

Returns

a string representation of the type of the root node of the expression.

Definition at line 38 of file ppg_visitor.h.

visit_and()

virtual bool mcrl2::pbes_system::detail::ppg_visitor::visit_and ( const pbes_expression &  e )

inlinevirtual

Visits a conjunctive expression.

Parameters

e	a PBES expression

Returns

true if the expression e conforms to PPG.

Definition at line 153 of file ppg_visitor.h.

visit_inner_and()

virtual bool mcrl2::pbes_system::detail::ppg_visitor::visit_inner_and ( const pbes_expression &  e )

inlinevirtual

Visits a conjunctive expression within an inner existential quantifier expression.

Parameters

e	a PBES expression

Returns

true if the expression e conforms to PPG.

Definition at line 68 of file ppg_visitor.h.

visit_inner_bounded_exists()

virtual bool mcrl2::pbes_system::detail::ppg_visitor::visit_inner_bounded_exists ( const pbes_expression &  e )

inlinevirtual

Visits a bounded existential quantifier expression within a disjunctive expression.

Parameters

e	a PBES expression

Returns

true if the expression e conforms to PPG.

Definition at line 88 of file ppg_visitor.h.

visit_inner_bounded_forall()

virtual bool mcrl2::pbes_system::detail::ppg_visitor::visit_inner_bounded_forall ( const pbes_expression &  e )

inlinevirtual

Visits a bounded universal quantifier expression within a conjunctive expression.

Parameters

e	a PBES expression

Returns

true if the expression e conforms to PPG.

Definition at line 139 of file ppg_visitor.h.

visit_inner_implies()

virtual bool mcrl2::pbes_system::detail::ppg_visitor::visit_inner_implies ( const pbes_expression &  e )

inlinevirtual

Visits a disjunctive expression within an inner universal quantifier expression.

Parameters

e	a PBES expression

Returns

true if the expression e conforms to PPG.

Definition at line 119 of file ppg_visitor.h.

visit_or()

virtual bool mcrl2::pbes_system::detail::ppg_visitor::visit_or ( const pbes_expression &  e )

inlinevirtual

Visits a disjunctive expression.

Parameters

e	a PBES expression

Returns

true if the expression e conforms to PPG.

Definition at line 102 of file ppg_visitor.h.

visit_ppg_expression()

virtual bool mcrl2::pbes_system::detail::ppg_visitor::visit_ppg_expression ( const pbes_expression &  e )

inlinevirtual

Visits a PPG expression.

Parameters

e	a PBES expression

Returns

true if the expression e is in PPG form.

Definition at line 170 of file ppg_visitor.h.

visit_propositional_variable()

virtual bool mcrl2::pbes_system::detail::ppg_visitor::visit_propositional_variable ( const pbes_expression &  e )

inlinevirtual

Visits a propositional variable expression.

Parameters

e	PBES expression

Returns

true if the expression is a propositional variable or a simple expression.

Definition at line 56 of file ppg_visitor.h.

visit_simple_expression()

virtual bool mcrl2::pbes_system::detail::ppg_visitor::visit_simple_expression ( const pbes_expression &  e )

inlinevirtual

Visits a simple expression. An expression is simple if it does not contain propositional variables.

Parameters

e	a PBES expression

Returns

true if the expression e is a simple expression.

Definition at line 47 of file ppg_visitor.h.

---

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

• pbes/include/mcrl2/pbes/detail/ppg_visitor.h