mcrl2::pbes_system::pfnf_rewriter

Include file:

#include "mcrl2/pbes/rewriters/pfnf_rewriter.h

class mcrl2::pbes_system::pfnf_rewriter

A rewriter that brings PBES expressions into PFNF normal form.

Public types

type mcrl2::pbes_system::pfnf_rewriter::term_type

typedef for pbes_expression

The term type.

type mcrl2::pbes_system::pfnf_rewriter::variable_type

typedef for data::variable

The variable type.

Public member functions

pbes_expression operator()(const pbes_expression &x) const

Rewrites a pbes expression.

Parameters:

• x A term

Returns: The rewrite result.

pbes_expression operator()(const pbes_expression &x, SubstitutionFunction sigma) const

Rewrites a pbes expression.

Parameters:

• x A term
• sigma A substitution function

Returns: The rewrite result.