A visitor class for PBES equations in BQNF. There is a visit_<node> function for each type of node. By default these functions do nothing, but check that the PBES equations are indeed in BQNF, so they must be overridden in order to add behaviour. More...

#include <bqnf_visitor.h>

Inheritance diagram for mcrl2::pbes_system::detail::bqnf_visitor:

Public Member Functions
virtual	~bqnf_visitor ()=default
	Destructor.

virtual bool	visit_simple_expression (const fixpoint_symbol &sigma, const propositional_variable &var, 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 fixpoint_symbol &, const propositional_variable &, const pbes_expression &e)
	Visits a propositional variable expression.

virtual bool	visit_inner_and (const fixpoint_symbol &sigma, const propositional_variable &var, const pbes_expression &e)
	Visits a conjunctive expression within an inner existential quantifier expression.

virtual bool	visit_inner_bounded_exists (const fixpoint_symbol &sigma, const propositional_variable &var, const pbes_expression &e)
	Visits a bounded existential quantifier expression within a disjunctive expression.

virtual bool	visit_or (const fixpoint_symbol &sigma, const propositional_variable &var, const pbes_expression &e)
	Visits a disjunctive expression.

virtual bool	visit_inner_bounded_forall (const fixpoint_symbol &sigma, const propositional_variable &var, const pbes_expression &e)
	Visits a bounded universal quantifier expression within a conjunctive expression.

virtual bool	visit_and (const fixpoint_symbol &sigma, const propositional_variable &var, const pbes_expression &e)
	Visits a conjunctive expression.

virtual bool	visit_bounded_forall (const fixpoint_symbol &sigma, const propositional_variable &var, const pbes_expression &e)
	Visits a bounded universal quantifier expression.

virtual bool	visit_bounded_exists (const fixpoint_symbol &sigma, const propositional_variable &var, const pbes_expression &e)
	Visits a bounded existential quantifier expression.

virtual bool	visit_bounded_quantifier (const fixpoint_symbol &sigma, const propositional_variable &var, const pbes_expression &e)
	Visits a bounded quantifier expression.

virtual bool	visit_bqnf_expression (const fixpoint_symbol &sigma, const propositional_variable &var, const pbes_expression &e)
	Visits a BQNF expression.

virtual bool	visit_bqnf_expression (const pbes_expression &e)
	Visits a BQNF expression. In the current BQNF visitor sigma and var parameters are added for use in bqnf2ppg_rewriter. This functions adds dummy values for sigma and var.

virtual bool	visit_bqnf_equation (const pbes_equation &eqn)
	Visits a BQNF equation.

virtual bool	visit_bqnf_equation_debug (const pbes_equation &eqn)
	Visits a BQNF equation in debug mode.

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.

static bool	is_inner_and (const pbes_expression &e)
	Determines if an expression if of the form phi /\ psi where phi is a simple expression and psi is an arbitrary expression.

static bool	is_inner_implies (const pbes_expression &e)
	Determines if an expression if of the form phi => psi or of the form phi \/ psi where phi is a simple expression and psi is an arbitrary expression.

Public Attributes
bool	debug = false
	flag that indicates if debug output should be printed.

Detailed Description

A visitor class for PBES equations in BQNF. There is a visit_<node> function for each type of node. By default these functions do nothing, but check that the PBES equations are indeed in BQNF, so they must be overridden in order to add behaviour.

Definition at line 53 of file bqnf_visitor.h.

Constructor & Destructor Documentation

◆ ~bqnf_visitor()

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

virtualdefault

Destructor.

Member Function Documentation

◆ is_inner_and()

static bool mcrl2::pbes_system::detail::bqnf_visitor::is_inner_and ( const pbes_expression & e )

inlinestatic

Determines if an expression if of the form phi /\ psi where phi is a simple expression and psi is an arbitrary expression.

Parameters

e	an expression

Returns: true if e is of the form phi /\ psi.

Definition at line 87 of file bqnf_visitor.h.

◆ is_inner_implies()

static bool mcrl2::pbes_system::detail::bqnf_visitor::is_inner_implies ( const pbes_expression & e )

inlinestatic

Determines if an expression if of the form phi => psi or of the form phi \/ psi where phi is a simple expression and psi is an arbitrary expression.

Parameters

e	an expression

Returns: true if e is of the form phi => psi or phi \/ psi.

Definition at line 111 of file bqnf_visitor.h.

◆ print_brief()

static std::string mcrl2::pbes_system::detail::bqnf_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 61 of file bqnf_visitor.h.

◆ visit_and()

virtual bool mcrl2::pbes_system::detail::bqnf_visitor::visit_and	(	const fixpoint_symbol &	sigma,
		const propositional_variable &	var,
		const pbes_expression &	e
	)

inlinevirtual

Visits a conjunctive expression.

Parameters

sigma	fixpoint symbol (unused in this class)
var	propositional variable (unused in this class)
e	a PBES expression

Returns: true if the expression e conforms to BQNF.

Reimplemented in mcrl2::pbes_system::detail::bqnf2ppg_rewriter.

Definition at line 308 of file bqnf_visitor.h.

◆ visit_bounded_exists()

virtual bool mcrl2::pbes_system::detail::bqnf_visitor::visit_bounded_exists	(	const fixpoint_symbol &	sigma,
		const propositional_variable &	var,
		const pbes_expression &	e
	)

inlinevirtual

Visits a bounded existential quantifier expression.

Parameters

sigma	fixpoint symbol (unused in this class)
var	propositional variable (unused in this class)
e	a PBES expression

Returns: true if the expression e conforms to BQNF.

Reimplemented in mcrl2::pbes_system::detail::bqnf2ppg_rewriter.

Definition at line 367 of file bqnf_visitor.h.

◆ visit_bounded_forall()

virtual bool mcrl2::pbes_system::detail::bqnf_visitor::visit_bounded_forall	(	const fixpoint_symbol &	sigma,
		const propositional_variable &	var,
		const pbes_expression &	e
	)

inlinevirtual

Visits a bounded universal quantifier expression.

Parameters

sigma	fixpoint symbol (unused in this class)
var	propositional variable (unused in this class)
e	a PBES expression

Returns: true if the expression e conforms to BQNF.

Reimplemented in mcrl2::pbes_system::detail::bqnf2ppg_rewriter.

Definition at line 332 of file bqnf_visitor.h.

◆ visit_bounded_quantifier()

virtual bool mcrl2::pbes_system::detail::bqnf_visitor::visit_bounded_quantifier	(	const fixpoint_symbol &	sigma,
		const propositional_variable &	var,
		const pbes_expression &	e
	)

inlinevirtual

Visits a bounded quantifier expression.

Parameters

sigma	fixpoint symbol (unused in this class)
var	propositional variable (unused in this class)
e	a PBES expression

Returns: true if the expression e conforms to BQNF.

Definition at line 402 of file bqnf_visitor.h.

◆ visit_bqnf_equation()

virtual bool mcrl2::pbes_system::detail::bqnf_visitor::visit_bqnf_equation ( const pbes_equation & eqn )

inlinevirtual

Visits a BQNF equation.

Parameters

eqn	a PBES equation

Returns: true if the right hand side of the equation is in BQNF.

Reimplemented in mcrl2::pbes_system::detail::bqnf2ppg_rewriter.

Definition at line 458 of file bqnf_visitor.h.

◆ visit_bqnf_equation_debug()

virtual bool mcrl2::pbes_system::detail::bqnf_visitor::visit_bqnf_equation_debug ( const pbes_equation & eqn )

inlinevirtual

Visits a BQNF equation in debug mode.

Parameters

eqn	a PBES equation

Returns: true if the right hand side of the equation is in BQNF.

Definition at line 479 of file bqnf_visitor.h.

◆ visit_bqnf_expression() [1/2]

virtual bool mcrl2::pbes_system::detail::bqnf_visitor::visit_bqnf_expression	(	const fixpoint_symbol &	sigma,
		const propositional_variable &	var,
		const pbes_expression &	e
	)

inlinevirtual

Visits a BQNF expression.

Parameters

sigma	fixpoint symbol (unused in this class)
var	propositional variable (unused in this class)
e	a PBES expression

Returns: true if the expression e is in BQNF.

Reimplemented in mcrl2::pbes_system::detail::bqnf2ppg_rewriter.

Definition at line 426 of file bqnf_visitor.h.

◆ visit_bqnf_expression() [2/2]

virtual bool mcrl2::pbes_system::detail::bqnf_visitor::visit_bqnf_expression ( const pbes_expression & e )

inlinevirtual

Visits a BQNF expression. In the current BQNF visitor sigma and var parameters are added for use in bqnf2ppg_rewriter. This functions adds dummy values for sigma and var.

Parameters

e	a PBES expression

Returns: true if the expression e is in BQNF.

Definition at line 449 of file bqnf_visitor.h.

◆ visit_inner_and()

virtual bool mcrl2::pbes_system::detail::bqnf_visitor::visit_inner_and	(	const fixpoint_symbol &	sigma,
		const propositional_variable &	var,
		const pbes_expression &	e
	)

inlinevirtual

Visits a conjunctive expression within an inner existential quantifier expression.

Parameters

sigma	fixpoint symbol (unused in this class)
var	propositional variable (unused in this class)
e	a PBES expression

Returns: true if the expression e conforms to BQNF.

Definition at line 200 of file bqnf_visitor.h.

◆ visit_inner_bounded_exists()

virtual bool mcrl2::pbes_system::detail::bqnf_visitor::visit_inner_bounded_exists	(	const fixpoint_symbol &	sigma,
		const propositional_variable &	var,
		const pbes_expression &	e
	)

inlinevirtual

Visits a bounded existential quantifier expression within a disjunctive expression.

Parameters

sigma	fixpoint symbol (unused in this class)
var	propositional variable (unused in this class)
e	a PBES expression

Returns: true if the expression e conforms to BQNF.

Definition at line 228 of file bqnf_visitor.h.

◆ visit_inner_bounded_forall()

virtual bool mcrl2::pbes_system::detail::bqnf_visitor::visit_inner_bounded_forall	(	const fixpoint_symbol &	sigma,
		const propositional_variable &	var,
		const pbes_expression &	e
	)

inlinevirtual

Visits a bounded universal quantifier expression within a conjunctive expression.

Parameters

sigma	fixpoint symbol (unused in this class)
var	propositional variable (unused in this class)
e	a PBES expression

Returns: true if the expression e conforms to BQNF.

Definition at line 274 of file bqnf_visitor.h.

◆ visit_or()

virtual bool mcrl2::pbes_system::detail::bqnf_visitor::visit_or	(	const fixpoint_symbol &	sigma,
		const propositional_variable &	var,
		const pbes_expression &	e
	)

inlinevirtual

Visits a disjunctive expression.

Parameters

sigma	fixpoint symbol (unused in this class)
var	propositional variable (unused in this class)
e	a PBES expression

Returns: true if the expression e conforms to BQNF.

Reimplemented in mcrl2::pbes_system::detail::bqnf2ppg_rewriter.

Definition at line 250 of file bqnf_visitor.h.

◆ visit_propositional_variable()

virtual bool mcrl2::pbes_system::detail::bqnf_visitor::visit_propositional_variable	(	const fixpoint_symbol &	,
		const propositional_variable &	,
		const pbes_expression &	e
	)

inlinevirtual

Visits a propositional variable expression.

Parameters

sigma	fixpoint symbol (unused in this class)
var	propositional variable (unused in this class)
e	PBES expression

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

Definition at line 175 of file bqnf_visitor.h.

◆ visit_simple_expression()

virtual bool mcrl2::pbes_system::detail::bqnf_visitor::visit_simple_expression	(	const fixpoint_symbol &	sigma,
		const propositional_variable &	var,
		const pbes_expression &	e
	)

inlinevirtual

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

Parameters

sigma	fixpoint symbol (unused in this class)
var	propositional variable (unused in this class)
e	a PBES expression

Returns: true if the expression e is a simple expression.

Definition at line 139 of file bqnf_visitor.h.

Member Data Documentation

◆ debug

bool mcrl2::pbes_system::detail::bqnf_visitor::debug = false

flag that indicates if debug output should be printed.

Definition at line 56 of file bqnf_visitor.h.

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

pbes/include/mcrl2/pbes/detail/bqnf_visitor.h

Public Member Functions

Static Public Member Functions

Public Attributes

Detailed Description

Constructor & Destructor Documentation

◆ ~bqnf_visitor()

Member Function Documentation

◆ is_inner_and()

◆ is_inner_implies()

◆ print_brief()

◆ visit_and()

◆ visit_bounded_exists()

◆ visit_bounded_forall()

◆ visit_bounded_quantifier()

◆ visit_bqnf_equation()

◆ visit_bqnf_equation_debug()

◆ visit_bqnf_expression() [1/2]

◆ visit_bqnf_expression() [2/2]

◆ visit_inner_and()

◆ visit_inner_bounded_exists()

◆ visit_inner_bounded_forall()

◆ visit_or()

◆ visit_propositional_variable()

◆ visit_simple_expression()

Member Data Documentation

◆ debug