The class pbes_expression. More...

Classes
class	mcrl2::pbes_system::pbes_expression
	\brief A pbes expression More...

class	mcrl2::pbes_system::propositional_variable_instantiation
	\brief A propositional variable instantiation More...

class	mcrl2::pbes_system::not_
	\brief The not operator for pbes expressions More...

class	mcrl2::pbes_system::and_
	\brief The and operator for pbes expressions More...

class	mcrl2::pbes_system::or_
	\brief The or operator for pbes expressions More...

class	mcrl2::pbes_system::imp
	\brief The implication operator for pbes expressions More...

class	mcrl2::pbes_system::forall
	\brief The universal quantification operator for pbes expressions More...

class	mcrl2::pbes_system::exists
	\brief The existential quantification operator for pbes expressions More...

struct	mcrl2::core::term_traits< pbes_system::pbes_expression >
	Contains type information for pbes expressions. More...

struct	std::hash< mcrl2::pbes_system::pbes_expression >

struct	std::hash< mcrl2::pbes_system::propositional_variable_instantiation >

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::accessors
	The namespace for accessor functions on pbes expressions.

namespace	mcrl2::core

namespace	std
	STL namespace.

Typedefs
typedef atermpp::term_list< pbes_expression >	mcrl2::pbes_system::pbes_expression_list
	\brief list of pbes_expressions

typedef std::vector< pbes_expression >	mcrl2::pbes_system::pbes_expression_vector
	\brief vector of pbes_expressions

typedef atermpp::term_list< propositional_variable_instantiation >	mcrl2::pbes_system::propositional_variable_instantiation_list
	\brief list of propositional_variable_instantiations

typedef std::vector< propositional_variable_instantiation >	mcrl2::pbes_system::propositional_variable_instantiation_vector
	\brief vector of propositional_variable_instantiations

Functions
bool	mcrl2::pbes_system::is_propositional_variable_instantiation (const atermpp::aterm &x)

bool	mcrl2::pbes_system::is_not (const atermpp::aterm &x)

bool	mcrl2::pbes_system::is_and (const atermpp::aterm &x)

bool	mcrl2::pbes_system::is_or (const atermpp::aterm &x)

bool	mcrl2::pbes_system::is_imp (const atermpp::aterm &x)

bool	mcrl2::pbes_system::is_forall (const atermpp::aterm &x)

bool	mcrl2::pbes_system::is_exists (const atermpp::aterm &x)

bool	mcrl2::pbes_system::is_pbes_expression (const atermpp::aterm &x)

std::string	mcrl2::pbes_system::pp (const pbes_expression &x)

std::ostream &	mcrl2::pbes_system::operator<< (std::ostream &out, const pbes_expression &x)

void	mcrl2::pbes_system::swap (pbes_expression &t1, pbes_expression &t2)
	\brief swap overload

template<class... ARGUMENTS>
void	mcrl2::pbes_system::make_propositional_variable_instantiation (atermpp::aterm &t, const ARGUMENTS &... args)

std::string	mcrl2::pbes_system::pp (const propositional_variable_instantiation &x)

std::ostream &	mcrl2::pbes_system::operator<< (std::ostream &out, const propositional_variable_instantiation &x)

void	mcrl2::pbes_system::swap (propositional_variable_instantiation &t1, propositional_variable_instantiation &t2)
	\brief swap overload

template<class... ARGUMENTS>
void	mcrl2::pbes_system::make_not_ (atermpp::aterm &t, const ARGUMENTS &... args)

std::string	mcrl2::pbes_system::pp (const not_ &x)

std::ostream &	mcrl2::pbes_system::operator<< (std::ostream &out, const not_ &x)

void	mcrl2::pbes_system::swap (not_ &t1, not_ &t2)
	\brief swap overload

template<class... ARGUMENTS>
void	mcrl2::pbes_system::make_and_ (atermpp::aterm &t, const ARGUMENTS &... args)

std::string	mcrl2::pbes_system::pp (const and_ &x)

std::ostream &	mcrl2::pbes_system::operator<< (std::ostream &out, const and_ &x)

void	mcrl2::pbes_system::swap (and_ &t1, and_ &t2)
	\brief swap overload

template<class... ARGUMENTS>
void	mcrl2::pbes_system::make_or_ (atermpp::aterm &t, const ARGUMENTS &... args)

std::string	mcrl2::pbes_system::pp (const or_ &x)

std::ostream &	mcrl2::pbes_system::operator<< (std::ostream &out, const or_ &x)

void	mcrl2::pbes_system::swap (or_ &t1, or_ &t2)
	\brief swap overload

template<class... ARGUMENTS>
void	mcrl2::pbes_system::make_imp (atermpp::aterm &t, const ARGUMENTS &... args)

std::string	mcrl2::pbes_system::pp (const imp &x)

std::ostream &	mcrl2::pbes_system::operator<< (std::ostream &out, const imp &x)

void	mcrl2::pbes_system::swap (imp &t1, imp &t2)
	\brief swap overload

template<class... ARGUMENTS>
void	mcrl2::pbes_system::make_forall (atermpp::aterm &t, const ARGUMENTS &... args)

std::string	mcrl2::pbes_system::pp (const forall &x)

std::ostream &	mcrl2::pbes_system::operator<< (std::ostream &out, const forall &x)

void	mcrl2::pbes_system::swap (forall &t1, forall &t2)
	\brief swap overload

template<class... ARGUMENTS>
void	mcrl2::pbes_system::make_exists (atermpp::aterm &t, const ARGUMENTS &... args)

std::string	mcrl2::pbes_system::pp (const exists &x)

std::ostream &	mcrl2::pbes_system::operator<< (std::ostream &out, const exists &x)

void	mcrl2::pbes_system::swap (exists &t1, exists &t2)
	\brief swap overload

std::string	mcrl2::pbes_system::pp (const pbes_expression_list &x)

std::string	mcrl2::pbes_system::pp (const pbes_expression_vector &x)

std::string	mcrl2::pbes_system::pp (const propositional_variable_instantiation_list &x)

std::string	mcrl2::pbes_system::pp (const propositional_variable_instantiation_vector &x)

std::set< pbes_system::propositional_variable_instantiation >	mcrl2::pbes_system::find_propositional_variable_instantiations (const pbes_system::pbes_expression &x)

std::set< core::identifier_string >	mcrl2::pbes_system::find_identifiers (const pbes_system::pbes_expression &x)

std::set< data::variable >	mcrl2::pbes_system::find_free_variables (const pbes_system::pbes_expression &x)

bool	mcrl2::pbes_system::search_variable (const pbes_system::pbes_expression &x, const data::variable &v)

pbes_system::pbes_expression	mcrl2::pbes_system::normalize_sorts (const pbes_system::pbes_expression &x, const data::sort_specification &sortspec)

pbes_system::pbes_expression	mcrl2::pbes_system::translate_user_notation (const pbes_system::pbes_expression &x)

const pbes_expression &	mcrl2::pbes_system::true_ ()

const pbes_expression &	mcrl2::pbes_system::false_ ()

bool	mcrl2::pbes_system::is_true (const pbes_expression &t)
	Test for the value true.

bool	mcrl2::pbes_system::is_false (const pbes_expression &t)
	Test for the value false.

bool	mcrl2::pbes_system::is_pbes_not (const pbes_expression &t)
	Returns true if the term t is a not expression.

bool	mcrl2::pbes_system::is_pbes_and (const pbes_expression &t)
	Returns true if the term t is an and expression.

bool	mcrl2::pbes_system::is_pbes_or (const pbes_expression &t)
	Returns true if the term t is an or expression.

bool	mcrl2::pbes_system::is_pbes_imp (const pbes_expression &t)
	Returns true if the term t is an imp expression.

bool	mcrl2::pbes_system::is_pbes_forall (const pbes_expression &t)
	Returns true if the term t is a universal quantification.

bool	mcrl2::pbes_system::is_pbes_exists (const pbes_expression &t)
	Returns true if the term t is an existential quantification.

bool	mcrl2::pbes_system::is_universal_not (const pbes_expression &t)
	Test for a conjunction.

bool	mcrl2::pbes_system::is_universal_and (const pbes_expression &t)
	Test for a conjunction.

bool	mcrl2::pbes_system::is_universal_or (const pbes_expression &t)
	Test for a disjunction.

bool	mcrl2::pbes_system::is_data (const pbes_expression &t)
	Returns true if the term t is a data expression.

const pbes_expression &	mcrl2::pbes_system::accessors::arg (const pbes_expression &t)
	Returns the pbes expression argument of expressions of type not, exists and forall.

pbes_expression	mcrl2::pbes_system::accessors::data_arg (const pbes_expression &t)
	Returns the pbes expression argument of expressions of type not, exists and forall.

const pbes_expression &	mcrl2::pbes_system::accessors::left (const pbes_expression &t)
	Returns the left hand side of an expression of type and, or or imp.

pbes_expression	mcrl2::pbes_system::accessors::data_left (const pbes_expression &x)
	Returns the left hand side of an expression of type and, or or imp.

const pbes_expression &	mcrl2::pbes_system::accessors::right (const pbes_expression &t)
	Returns the right hand side of an expression of type and, or or imp.

pbes_expression	mcrl2::pbes_system::accessors::data_right (const pbes_expression &x)
	Returns the left hand side of an expression of type and, or or imp.

const data::variable_list &	mcrl2::pbes_system::accessors::var (const pbes_expression &t)
	Returns the variables of a quantification expression.

const core::identifier_string &	mcrl2::pbes_system::accessors::name (const pbes_expression &t)
	Returns the name of a propositional variable expression.

const data::data_expression_list &	mcrl2::pbes_system::accessors::param (const pbes_expression &t)
	Returns the parameters of a propositional variable instantiation.

pbes_expression	mcrl2::pbes_system::make_forall_ (const data::variable_list &l, const pbes_expression &p)
	Make a universal quantification. It checks for an empty variable list, which is not allowed.

pbes_expression	mcrl2::pbes_system::make_exists_ (const data::variable_list &l, const pbes_expression &p)
	Make an existential quantification. It checks for an empty variable list, which is not allowed.

void	mcrl2::pbes_system::optimized_not (pbes_expression &result, const pbes_expression &p)
	Make a negation.

void	mcrl2::pbes_system::optimized_and (pbes_expression &result, const pbes_expression &p, const pbes_expression &q)
	Make a conjunction.

void	mcrl2::pbes_system::optimized_or (pbes_expression &result, const pbes_expression &p, const pbes_expression &q)
	Make a disjunction.

void	mcrl2::pbes_system::optimized_imp (pbes_expression &result, const pbes_expression &p, const pbes_expression &q)
	Make an implication.

void	mcrl2::pbes_system::optimized_forall (pbes_expression &result, const data::variable_list &l, const pbes_expression &p)
	Make a universal quantification If l is empty, p is returned.

void	mcrl2::pbes_system::optimized_exists (pbes_expression &result, const data::variable_list &l, const pbes_expression &p)
	Make an existential quantification If l is empty, p is returned.

bool	mcrl2::pbes_system::is_constant (const pbes_expression &x)

const data::variable_list &	mcrl2::pbes_system::quantifier_variables (const pbes_expression &x)

data::variable_list	mcrl2::pbes_system::free_variables (const pbes_expression &x)

Detailed Description

The class pbes_expression.

Definition in file pbes_expression.h.

Classes

Namespaces

Typedefs

Functions

Detailed Description