ppg_traverser.h File Reference

Traverser class for Parameterised Parity Games (PPG), PBES expressions of the form: PPG :== /_{i: I} f_i && /_{j: J} forall v: D_j . ( g_j => X_j(e_j) ) | \/_{i: I} f_i || \/_{j: J} exists v: D_j . ( g_j && X_j(e_j) ). More...

Go to the source code of this file.

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

Functions
template<typename T >
bool	mcrl2::pbes_system::detail::is_ppg (const T &x)
	Determines if an expression is a PPG expression.

Detailed Description

Traverser class for Parameterised Parity Games (PPG), PBES expressions of the form: PPG :== /_{i: I} f_i && /_{j: J} forall v: D_j . ( g_j => X_j(e_j) ) | \/_{i: I} f_i || \/_{j: J} exists v: D_j . ( g_j && X_j(e_j) ).

Definition in file ppg_traverser.h.