mcrl2::pbes_system::pbes_traits Struct Reference

Traits class for pbes expressions. More...

#include <pbes_gauss_elimination.h>

Public Types
using	expression_type = pbes_expression
using	variable_type = propositional_variable
using	equation_type = pbes_equation
using	symbol_type = fixpoint_symbol

Static Public Member Functions
static expression_type	substitute (const expression_type &t, const variable_type &X, const expression_type &phi)
	Applies the substitution X := phi to the PBES expression t.
static expression_type	true_ ()
	Returns the value true.
static expression_type	false_ ()
	Returns the value false.
static symbol_type	mu ()
	Returns the fixpoint symbol mu.
static symbol_type	nu ()
	Returns the fixpoint symbol nu.
static std::string	print (const equation_type &eq)
	Pretty print an equation without generating a newline after the equal sign.

Detailed Description

Traits class for pbes expressions.

Definition at line 22 of file pbes_gauss_elimination.h.

Member Typedef Documentation

equation_type

using mcrl2::pbes_system::pbes_traits::equation_type = pbes_equation

Definition at line 27 of file pbes_gauss_elimination.h.

expression_type

using mcrl2::pbes_system::pbes_traits::expression_type = pbes_expression

Definition at line 25 of file pbes_gauss_elimination.h.

symbol_type

using mcrl2::pbes_system::pbes_traits::symbol_type = fixpoint_symbol

Definition at line 28 of file pbes_gauss_elimination.h.

variable_type

using mcrl2::pbes_system::pbes_traits::variable_type = propositional_variable

Definition at line 26 of file pbes_gauss_elimination.h.

Member Function Documentation

false_()

static expression_type mcrl2::pbes_system::pbes_traits::false_ ( )

inlinestatic

Returns the value false.

Definition at line 50 of file pbes_gauss_elimination.h.

mu()

static symbol_type mcrl2::pbes_system::pbes_traits::mu ( )

inlinestatic

Returns the fixpoint symbol mu.

Definition at line 57 of file pbes_gauss_elimination.h.

nu()

static symbol_type mcrl2::pbes_system::pbes_traits::nu ( )

inlinestatic

Returns the fixpoint symbol nu.

Definition at line 64 of file pbes_gauss_elimination.h.

print()

static std::string mcrl2::pbes_system::pbes_traits::print ( const equation_type &  eq )

inlinestatic

Pretty print an equation without generating a newline after the equal sign.

Parameters

eq	An equation

Returns

A pretty printed string

Definition at line 73 of file pbes_gauss_elimination.h.

substitute()

static expression_type mcrl2::pbes_system::pbes_traits::substitute ( const expression_type &  t, const variable_type &  X, const expression_type &  phi  )

inlinestatic

Applies the substitution X := phi to the PBES expression t.

Parameters

t	A PBES expression
X	A propositional variable
phi	A PBES expression

Returns

The substition result

Definition at line 36 of file pbes_gauss_elimination.h.

true_()

static expression_type mcrl2::pbes_system::pbes_traits::true_ ( )

inlinestatic

Returns the value true.

Definition at line 43 of file pbes_gauss_elimination.h.

---

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

• pbes/include/mcrl2/pbes/pbes_gauss_elimination.h