mcrl2/pbes/pbes_functions.h

Include file:

#include "mcrl2/pbes/pbes_functions.h"

add your file description here.

Classes

  • mcrl2::pbes_system::print_brief_traverser

Functions

bool mcrl2::pbes_system::is_non_simple_conjunct(const pbes_expression &t)

Test for a conjunction.

Parameters:

  • t A PBES expression

Returns: True if it is a conjunction and not a simple expression

bool mcrl2::pbes_system::is_non_simple_disjunct(const pbes_expression &t)

Test for a disjunction.

Parameters:

  • t A PBES expression

Returns: True if it is a disjunction and not a simple expression

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

Determines if an expression is a simple expression. An expression is simple if it is free of propositional variables.

Parameters:

  • x a PBES object

Returns: true if x is a simple expression.

std::string mcrl2::pbes_system::print_brief(const T &x)

Returns a string representation of the root node of a PBES.

Parameters:

  • x a PBES object
std::vector<pbes_expression> mcrl2::pbes_system::split_conjuncts(const pbes_expression &expr, bool split_simple_expr = false)

Splits a conjunction into a sequence of operands Given a pbes expression of the form p1 && p2 && …. && pn, this will yield a set of the form { p1, p2, …, pn }, assuming that pi does not have a && as main function symbol.

Parameters:

  • expr A PBES expression
  • split_simple_expr If true, pbes conjuncts are split, even if no proposition variables occur. If false, pbes conjuncts are only split if a proposition variable occurs somewhere in expr.

Note

This never splits data conjuncts.

Returns: A sequence of operands

std::vector<pbes_expression> mcrl2::pbes_system::split_disjuncts(const pbes_expression &expr, bool split_simple_expr = false)

Splits a disjunction into a sequence of operands. Given a pbes expression of the form p1 || p2 || …. || pn, this will yield a set of the form { p1, p2, …, pn }, assuming that pi does not have a || as main function symbol.

Parameters:

  • expr A PBES expression.
  • split_simple_expr If true, pbes disjuncts are split, even if no proposition variables occur. If false, pbes disjuncts are only split if a proposition variable occurs somewhere in expr.

Note

This never splits data disjuncts.

Returns: A sequence of operands.