mcrl2/pbes/normalize.h

Include file:

#include "mcrl2/pbes/normalize.h"

Normalization of pbes expressions.

Functions

bool mcrl2::pbes_system::is_normalized(const T &x)

Checks if a pbes expression is normalized.

Parameters:

• x A PBES expression

Returns: True if the pbes expression is normalized

T mcrl2::pbes_system::normalize(const T &x, typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type * = nullptr)

The function normalize brings (embedded) pbes expressions into positive normal form, i.e. a formula without any occurrences of ! or =>.

Parameters:

• x an object containing pbes expressions

void mcrl2::pbes_system::normalize(T &x, typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type * = nullptr)

The function normalize brings (embedded) pbes expressions into positive normal form, i.e. a formula without any occurrences of ! or =>.

Parameters:

• x an object containing pbes expressions