mcrl2/pbes/join.h

Include file:

#include "mcrl2/pbes/join.h"

add your file description here.

Functions

pbes_expression mcrl2::pbes_system::join_and(FwdIt first, FwdIt last)

Returns and applied to the sequence of pbes expressions [first, last)

Parameters:

  • first Start of a sequence of pbes expressions
  • last End of a sequence of of pbes expressions

Returns: And applied to the sequence of pbes expressions [first, last)

pbes_expression mcrl2::pbes_system::join_or(FwdIt first, FwdIt last)

Returns or applied to the sequence of pbes expressions [first, last)

Parameters:

  • first Start of a sequence of pbes expressions
  • last End of a sequence of of pbes expressions

Returns: Or applied to the sequence of pbes expressions [first, last)

pbes_expression mcrl2::pbes_system::optimized_join_and(FwdIt first, FwdIt last)

Returns and applied to the sequence of pbes expressions [first, last)

Parameters:

  • first Start of a sequence of pbes expressions
  • last End of a sequence of pbes expressions

Returns: And applied to the sequence of pbes expressions [first, last)

pbes_expression mcrl2::pbes_system::optimized_join_or(FwdIt first, FwdIt last)

Returns or applied to the sequence of pbes expressions [first, last)

Parameters:

  • first Start of a sequence of pbes expressions
  • last End of a sequence of pbes expressions

Returns: Or applied to the sequence of pbes expressions [first, last)

std::set<pbes_expression> mcrl2::pbes_system::split_and(const pbes_expression &expr, bool split_data_expressions = 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_data_expressions if true, both data and pbes conjunctions are split, otherwise only pbes conjunctions are split.

Returns: A sequence of operands

std::set<pbes_expression> mcrl2::pbes_system::split_or(const pbes_expression &expr, bool split_data_expressions = 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_data_expressions if true, both data and pbes disjunctions are split, otherwise only pbes disjunctions are split.

Returns: A sequence of operands