pfnf_traverser.h File Reference

add your file description here. More...

Go to the source code of this file.

Classes
struct	mcrl2::pbes_system::detail::variable_variable_substitution
struct	mcrl2::pbes_system::detail::variable_data_expression_substitution
struct	mcrl2::pbes_system::detail::pfnf_traverser_implication
	Represents the implication g => ( X0(e0) \/ ... \/ Xk(ek) ) More...
struct	mcrl2::pbes_system::detail::pfnf_traverser_expression
struct	mcrl2::pbes_system::detail::pfnf_traverser
	Applies the PFNF rewriter to a PBES expression. More...

Namespaces
namespace	mcrl2
	A class that takes a linear process specification and checks all tau-summands of that LPS for confluence.
namespace	mcrl2::pbes_system
	The main namespace for the PBES library.
namespace	mcrl2::pbes_system::detail

Typedefs
typedef std::pair< bool, data::variable_list >	mcrl2::pbes_system::detail::pfnf_traverser_quantifier
	Represents a quantifier Qv:V. If the bool is true it is a forall, otherwise an exists.

Functions
template<typename Container >
Container	mcrl2::pbes_system::detail::concat (const Container &x, const Container &y)
	Concatenates two containers.

Detailed Description

add your file description here.

Definition in file pfnf_traverser.h.