Traverser that implements the standard form normalization. More...

#include <normal_forms.h>

Inheritance diagram for mcrl2::pbes_system::detail::standard_form_traverser:

Public Types
using	super = pbes_system::pbes_expression_traverser< standard_form_traverser >

Public Types inherited from mcrl2::pbes_system::add_traverser_pbes_expressions< Traverser, Derived >
using	super = Traverser< Derived >

Public Member Functions
standard_form_pair	pop ()
	Pops the stack and returns the popped element.

void	push (const pbes_expression &first, standard_form_type second)
	Pushes (first, second) on the stack.

propositional_variable	fresh_variable (const std::string &hint)
	Generates a fresh pbes variable.

propositional_variable_instantiation	create_variable (const pbes_expression &expr, standard_form_type type, const std::string &hint)
	Generates an equation var=expr for the expression expr (if it does not exist).

	standard_form_traverser (bool recursive_form=false)
	Constructor.

pbes_expression	result () const
	Returns the top element of the expression stack, which is the result of the normalization.

const std::vector< pbes_equation > &	equations () const
	Returns the generated equations.

void	enter (const data::data_expression &x)
	Enter a data_expression that must be either true or false.

void	enter (const propositional_variable_instantiation &x)
	Enter propositional_variable node.

void	leave (const not_ &)
	Leave not node.

void	leave (const and_ &)
	Leave and node.

void	leave (const or_ &)
	Leave or node.

void	leave (const imp &)
	Leave imp node.

void	enter (const pbes_equation &eq)
	Enter an equation.

void	leave (const pbes_equation &eq)
	Leave an equation.

void	enter (const pbes &x)
	Enter a pbes equation system.

void	leave (const pbes &)
	Leave a pbes equation system.

Public Member Functions inherited from mcrl2::pbes_system::add_traverser_pbes_expressions< Traverser, Derived >
void	apply (const pbes_system::pbes_equation &x)

void	apply (const pbes_system::pbes &x)

void	apply (const pbes_system::propositional_variable_instantiation &x)

void	apply (const pbes_system::not_ &x)

void	apply (const pbes_system::and_ &x)

void	apply (const pbes_system::or_ &x)

void	apply (const pbes_system::imp &x)

void	apply (const pbes_system::forall &x)

void	apply (const pbes_system::exists &x)

void	apply (const pbes_system::pbes_expression &x)

Public Attributes
bool	m_recursive_form
	If true, the result will be in standard recursive normal form, otherwise in standard form.

fixpoint_symbol	m_symbol
	The fixpoint symbol of the current equation.

std::string	m_name
	The name of the variable of the current equation, with a trailing underscore added.

bool	m_has_true = false
	Is set to true if the value true is encountered in the PBES.

bool	m_has_false = false
	Is set to true if the value false is encountered in the PBES.

utilities::number_postfix_generator	m_generator
	For generating fresh variables.

std::vector< standard_form_pair >	m_expression_stack
	A stack containing sub-terms.

std::vector< pbes_equation >	m_equations
	A vector containing generated equations.

std::vector< pbes_equation >	m_equations2
	A vector containing generated equations with new variables.

std::map< pbes_expression, propositional_variable_instantiation >	m_table
	Maps right hand sides of equations to their corresponding left hand side.

pbes_expression	m_true
	The expression corresponding to true.

pbes_expression	m_false
	The expression corresponding to false.

Detailed Description

Traverser that implements the standard form normalization.

Definition at line 33 of file normal_forms.h.

Member Typedef Documentation

◆ super

using mcrl2::pbes_system::detail::standard_form_traverser::super = pbes_system::pbes_expression_traverser<standard_form_traverser>

Definition at line 36 of file normal_forms.h.

Constructor & Destructor Documentation

◆ standard_form_traverser()

mcrl2::pbes_system::detail::standard_form_traverser::standard_form_traverser ( bool recursive_form = false )

inline

Constructor.

Parameters

recursive_form Determines whether or not the result will be in standard recursive normal form.

Definition at line 124 of file normal_forms.h.

Member Function Documentation

◆ create_variable()

propositional_variable_instantiation mcrl2::pbes_system::detail::standard_form_traverser::create_variable	(	const pbes_expression &	expr,
		standard_form_type	type,
		const std::string &	hint
	)

inline

Generates an equation var=expr for the expression expr (if it does not exist).

Returns: The variable var.

Definition at line 101 of file normal_forms.h.

◆ enter() [1/4]

void mcrl2::pbes_system::detail::standard_form_traverser::enter ( const data::data_expression & x )

inline

Enter a data_expression that must be either true or false.

Parameters

x A term

Definition at line 153 of file normal_forms.h.

◆ enter() [2/4]

void mcrl2::pbes_system::detail::standard_form_traverser::enter ( const pbes & x )

inline

Enter a pbes equation system.

Definition at line 234 of file normal_forms.h.

◆ enter() [3/4]

void mcrl2::pbes_system::detail::standard_form_traverser::enter ( const pbes_equation & eq )

inline

Enter an equation.

Definition at line 220 of file normal_forms.h.

◆ enter() [4/4]

void mcrl2::pbes_system::detail::standard_form_traverser::enter ( const propositional_variable_instantiation & x )

inline

Enter propositional_variable node.

Parameters

x	A pbes variable.

Definition at line 170 of file normal_forms.h.

◆ equations()

const std::vector< pbes_equation > & mcrl2::pbes_system::detail::standard_form_traverser::equations ( ) const

inline

Returns the generated equations.

Definition at line 146 of file normal_forms.h.

◆ fresh_variable()

propositional_variable mcrl2::pbes_system::detail::standard_form_traverser::fresh_variable ( const std::string & hint )

inline

Generates a fresh pbes variable.

Definition at line 93 of file normal_forms.h.

◆ leave() [1/6]

void mcrl2::pbes_system::detail::standard_form_traverser::leave ( const and_ & )

inline

Leave and node.

Definition at line 182 of file normal_forms.h.

◆ leave() [2/6]

void mcrl2::pbes_system::detail::standard_form_traverser::leave ( const imp & )

inline

Leave imp node.

Definition at line 214 of file normal_forms.h.

◆ leave() [3/6]

void mcrl2::pbes_system::detail::standard_form_traverser::leave ( const not_ & )

inline

Leave not node.

Definition at line 176 of file normal_forms.h.

◆ leave() [4/6]

void mcrl2::pbes_system::detail::standard_form_traverser::leave ( const or_ & )

inline

Leave or node.

Definition at line 198 of file normal_forms.h.

◆ leave() [5/6]

void mcrl2::pbes_system::detail::standard_form_traverser::leave ( const pbes & )

inline

Leave a pbes equation system.

Definition at line 244 of file normal_forms.h.

◆ leave() [6/6]

void mcrl2::pbes_system::detail::standard_form_traverser::leave ( const pbes_equation & eq )

inline

Leave an equation.

Definition at line 227 of file normal_forms.h.

◆ pop()

standard_form_pair mcrl2::pbes_system::detail::standard_form_traverser::pop ( )

inline

Pops the stack and returns the popped element.

Definition at line 79 of file normal_forms.h.

◆ push()

void mcrl2::pbes_system::detail::standard_form_traverser::push	(	const pbes_expression &	first,
		standard_form_type	second
	)

inline

Pushes (first, second) on the stack.

Definition at line 87 of file normal_forms.h.

◆ result()

pbes_expression mcrl2::pbes_system::detail::standard_form_traverser::result ( ) const

inline

Returns the top element of the expression stack, which is the result of the normalization.

Definition at line 140 of file normal_forms.h.

Member Data Documentation

◆ m_equations

std::vector<pbes_equation> mcrl2::pbes_system::detail::standard_form_traverser::m_equations

A vector containing generated equations.

Definition at line 64 of file normal_forms.h.

◆ m_equations2

std::vector<pbes_equation> mcrl2::pbes_system::detail::standard_form_traverser::m_equations2

A vector containing generated equations with new variables.

Definition at line 67 of file normal_forms.h.

◆ m_expression_stack

std::vector<standard_form_pair> mcrl2::pbes_system::detail::standard_form_traverser::m_expression_stack

A stack containing sub-terms.

Definition at line 61 of file normal_forms.h.

◆ m_false

pbes_expression mcrl2::pbes_system::detail::standard_form_traverser::m_false

The expression corresponding to false.

Definition at line 76 of file normal_forms.h.

◆ m_generator

utilities::number_postfix_generator mcrl2::pbes_system::detail::standard_form_traverser::m_generator

For generating fresh variables.

Definition at line 58 of file normal_forms.h.

◆ m_has_false

bool mcrl2::pbes_system::detail::standard_form_traverser::m_has_false = false

Is set to true if the value false is encountered in the PBES.

Definition at line 55 of file normal_forms.h.

◆ m_has_true

bool mcrl2::pbes_system::detail::standard_form_traverser::m_has_true = false

Is set to true if the value true is encountered in the PBES.

Definition at line 52 of file normal_forms.h.

◆ m_name

std::string mcrl2::pbes_system::detail::standard_form_traverser::m_name

The name of the variable of the current equation, with a trailing underscore added.

Definition at line 49 of file normal_forms.h.

◆ m_recursive_form

bool mcrl2::pbes_system::detail::standard_form_traverser::m_recursive_form

If true, the result will be in standard recursive normal form, otherwise in standard form.

Definition at line 43 of file normal_forms.h.

◆ m_symbol

fixpoint_symbol mcrl2::pbes_system::detail::standard_form_traverser::m_symbol

The fixpoint symbol of the current equation.

Definition at line 46 of file normal_forms.h.

◆ m_table

std::map<pbes_expression, propositional_variable_instantiation> mcrl2::pbes_system::detail::standard_form_traverser::m_table

Maps right hand sides of equations to their corresponding left hand side.

Definition at line 70 of file normal_forms.h.

◆ m_true

pbes_expression mcrl2::pbes_system::detail::standard_form_traverser::m_true

The expression corresponding to true.

Definition at line 73 of file normal_forms.h.

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

pbes/include/mcrl2/pbes/normal_forms.h

Public Types

Public Member Functions

Public Attributes

Detailed Description

Member Typedef Documentation

◆ super

Constructor & Destructor Documentation

◆ standard_form_traverser()

Member Function Documentation

◆ create_variable()

◆ enter() [1/4]

◆ enter() [2/4]

◆ enter() [3/4]

◆ enter() [4/4]

◆ equations()

◆ fresh_variable()

◆ leave() [1/6]

◆ leave() [2/6]

◆ leave() [3/6]

◆ leave() [4/6]

◆ leave() [5/6]

◆ leave() [6/6]

◆ pop()

◆ push()

◆ result()

Member Data Documentation

◆ m_equations

◆ m_equations2

◆ m_expression_stack

◆ m_false

◆ m_generator

◆ m_has_false

◆ m_has_true

◆ m_name

◆ m_recursive_form

◆ m_symbol

◆ m_table

◆ m_true