mcrl2/pbes/pbes_functions.h¶

Include file:

#include "mcrl2/pbes/pbes_functions.h"


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.