mcrl2::pbes_system::one_point_rule_rewriter

Include file:

#include "mcrl2/pbes/rewriters/one_point_rule_rewriter.h
class mcrl2::pbes_system::one_point_rule_rewriter

A rewriter that applies one point rule quantifier elimination to a PBES.

Public types

type term_type

typedef for pbes_expression

The term type.

type 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.