mcrl2/modal_formula/normalize.h

Include file:

#include "mcrl2/modal_formula/normalize.h"

Add your file description here.

Functions

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

Checks if a state formula is normalized.

Parameters:

  • x A PBES expression.

Returns: True if the state formula is normalized.

void mcrl2::state_formulas::normalize(T &x, bool negated, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *)

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

Parameters:

  • x an object containing state formulas.
  • negated Indication whether the formula must be interpreted as being negated.
T mcrl2::state_formulas::normalize(const T &x, bool negated, typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type *)

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

Parameters:

  • x an object containing state formulas
  • negated Indication whether the formula must be interpreted as being negated.