pbes_functions.h File Reference

add your file description here. More...

Go to the source code of this file.

Classes
struct	mcrl2::pbes_system::print_brief_traverser
	Visitor for printing the root node of a PBES. More...

Namespaces
namespace	mcrl2
namespace	mcrl2::pbes_system
	The main namespace for the PBES library.

Functions
template<typename T >
std::string	mcrl2::pbes_system::print_brief (const T &x)
	Returns a string representation of the root node of a PBES.
template<typename T >
bool	mcrl2::pbes_system::is_simple_expression (const T &x, bool allow_counter_example_propvar)
	Determines if an expression is a simple expression. An expression is simple if it is free of propositional variables.
bool	mcrl2::pbes_system::is_non_simple_disjunct (const pbes_expression &t)
	Test for a disjunction.
bool	mcrl2::pbes_system::is_non_simple_conjunct (const pbes_expression &t)
	Test for a conjunction.
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.
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.

Detailed Description

add your file description here.

Definition in file pbes_functions.h.