mcrl2/pbes/pbes_expression.h

Include file:

#include "mcrl2/pbes/pbes_expression.h"

The class pbes_expression.

Classes

• mcrl2::pbes_system::and_
• mcrl2::pbes_system::exists
• mcrl2::pbes_system::forall
• std::hash
• std::hash
• mcrl2::pbes_system::imp
• mcrl2::pbes_system::not_
• mcrl2::pbes_system::or_
• mcrl2::pbes_system::pbes_expression
• mcrl2::pbes_system::propositional_variable_instantiation
• mcrl2::core::term_traits

Typedefs

type mcrl2::pbes_system::pbes_expression_list

typedef for atermpp::term_list< pbes_expression >

brief list of pbes_expressions

type mcrl2::pbes_system::pbes_expression_vector

typedef for std::vector< pbes_expression >

brief vector of pbes_expressions

type mcrl2::pbes_system::propositional_variable_instantiation_list

typedef for atermpp::term_list< propositional_variable_instantiation >

brief list of propositional_variable_instantiations

type mcrl2::pbes_system::propositional_variable_instantiation_vector

typedef for std::vector< propositional_variable_instantiation >

brief vector of propositional_variable_instantiations

Functions

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

Returns: Returns the value false

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

bool is_and(const atermpp::aterm_appl &x)

brief Test for a and expression param x A term return True if a x is a and expression

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

bool mcrl2::pbes_system::is_data(const pbes_expression &t)

Returns true if the term t is a data expression.

Parameters:

• t A PBES expression

Returns: True if the term t is a data expression

bool is_exists(const atermpp::aterm_appl &x)

brief Test for a exists expression param x A term return True if a x is a exists expression

bool mcrl2::pbes_system::is_false(const pbes_expression &t)

Test for the value false.

Parameters:

• t A PBES expression

Returns: True if it is the value false

bool is_forall(const atermpp::aterm_appl &x)

brief Test for a forall expression param x A term return True if a x is a forall expression

bool is_imp(const atermpp::aterm_appl &x)

brief Test for a imp expression param x A term return True if a x is a imp expression

bool is_not(const atermpp::aterm_appl &x)

brief Test for a not expression param x A term return True if a x is a not expression

bool is_or(const atermpp::aterm_appl &x)

brief Test for a or expression param x A term return True if a x is a or expression

bool mcrl2::pbes_system::is_pbes_and(const pbes_expression &t)

Returns true if the term t is an and expression.

Parameters:

• t A PBES expression

Returns: True if the term t is an and expression

bool mcrl2::pbes_system::is_pbes_exists(const pbes_expression &t)

Returns true if the term t is an existential quantification.

Parameters:

• t A PBES expression

Returns: True if the term t is an existential quantification

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

brief Test for a pbes_expression expression param x A term return True if a x is a pbes_expression expression

bool mcrl2::pbes_system::is_pbes_forall(const pbes_expression &t)

Returns true if the term t is a universal quantification.

Parameters:

• t A PBES expression

Returns: True if the term t is a universal quantification

bool mcrl2::pbes_system::is_pbes_imp(const pbes_expression &t)

Returns true if the term t is an imp expression.

Parameters:

• t A PBES expression

Returns: True if the term t is an imp expression

bool mcrl2::pbes_system::is_pbes_not(const pbes_expression &t)

Returns true if the term t is a not expression.

Parameters:

• t A PBES expression

Returns: True if the term t is a not expression

bool mcrl2::pbes_system::is_pbes_or(const pbes_expression &t)

Returns true if the term t is an or expression.

Parameters:

• t A PBES expression

Returns: True if the term t is an or expression

bool is_propositional_variable_instantiation(const atermpp::aterm_appl &x)

brief Test for a propositional_variable_instantiation expression param x A term return True if a x is a propositional_variable_instantiation expression

bool mcrl2::pbes_system::is_true(const pbes_expression &t)

Test for the value true.

Parameters:

• t A PBES expression

Returns: True if it is the value true

bool mcrl2::pbes_system::is_universal_and(const pbes_expression &t)

Test for a conjunction.

Parameters:

• t A PBES expression or a data expression

Returns: True if it is a conjunction

bool mcrl2::pbes_system::is_universal_not(const pbes_expression &t)

Test for a conjunction.

Parameters:

• t A PBES expression or a data expression

Returns: True if it is a conjunction

bool mcrl2::pbes_system::is_universal_or(const pbes_expression &t)

Test for a disjunction.

Parameters:

• t A PBES expression or a data expression

Returns: True if it is a disjunction

void mcrl2::pbes_system::make_and_(atermpp::aterm_appl &t, const ARGUMENTS&... args)

brief Make_and_ constructs a new term into a given address.

Parameters:

• t The reference into which the new and_ is constructed.

void mcrl2::pbes_system::make_exists(atermpp::aterm_appl &t, const ARGUMENTS&... args)

brief Make_exists constructs a new term into a given address.

Parameters:

• t The reference into which the new exists is constructed.

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.

Parameters:

• l A sequence of data variables
• p A PBES expression

Returns: The value exists l.p

void mcrl2::pbes_system::make_forall(atermpp::aterm_appl &t, const ARGUMENTS&... args)

brief Make_forall constructs a new term into a given address.

Parameters:

• t The reference into which the new forall is constructed.

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.

Parameters:

• l A sequence of data variables
• p A PBES expression

Returns: The value forall l.p

void mcrl2::pbes_system::make_imp(atermpp::aterm_appl &t, const ARGUMENTS&... args)

brief Make_imp constructs a new term into a given address.

Parameters:

• t The reference into which the new imp is constructed.

void mcrl2::pbes_system::make_not_(atermpp::aterm_appl &t, const ARGUMENTS&... args)

brief Make_not_ constructs a new term into a given address.

Parameters:

• t The reference into which the new not_ is constructed.

void mcrl2::pbes_system::make_or_(atermpp::aterm_appl &t, const ARGUMENTS&... args)

brief Make_or_ constructs a new term into a given address.

Parameters:

• t The reference into which the new or_ is constructed.

void mcrl2::pbes_system::make_propositional_variable_instantiation(atermpp::aterm_appl &t, const ARGUMENTS&... args)

brief Make_propositional_variable_instantiation constructs a new term into a given address.

Parameters:

• t The reference into which the new propositional_variable_instantiation is constructed.

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

brief Outputs the object to a stream param out An output stream param x Object x return The output stream

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

brief Outputs the object to a stream param out An output stream param x Object x return The output stream

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

brief Outputs the object to a stream param out An output stream param x Object x return The output stream

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

brief Outputs the object to a stream param out An output stream param x Object x return The output stream

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

brief Outputs the object to a stream param out An output stream param x Object x return The output stream

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

brief Outputs the object to a stream param out An output stream param x Object x return The output stream

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

brief Outputs the object to a stream param out An output stream param x Object x return The output stream

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

brief Outputs the object to a stream param out An output stream param x Object x return The output stream

void mcrl2::pbes_system::optimized_and(pbes_expression &result, const pbes_expression &p, const pbes_expression &q)

Make a conjunction.

Parameters:

• p A PBES expression
• q A PBES expression

Returns: The value p && q

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.

Parameters:

• l A sequence of data variables
• p A PBES expression

Returns: The value exists l.p

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.

Parameters:

• l A sequence of data variables
• p A PBES expression

Returns: The value forall l.p

void mcrl2::pbes_system::optimized_imp(pbes_expression &result, const pbes_expression &p, const pbes_expression &q)

Make an implication.

Parameters:

• p A PBES expression
• q A PBES expression

Returns: The value p => q

void mcrl2::pbes_system::optimized_not(pbes_expression &result, const pbes_expression &p)

Make a negation.

Parameters:

• p A PBES expression

Returns: The value !p

void mcrl2::pbes_system::optimized_or(pbes_expression &result, const pbes_expression &p, const pbes_expression &q)

Make a disjunction.

Parameters:

• p A PBES expression
• q A PBES expression

Returns: The value p || q

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

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

brief swap overload

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

brief swap overload

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

brief swap overload

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

brief swap overload

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

brief swap overload

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

brief swap overload

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

brief swap overload

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

brief swap overload

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

Returns: Returns the value true

Functions

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.

Parameters:

• t A PBES expression

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.

Parameters:

• t A PBES expression or a data expression

Returns: The pbes expression argument of expressions of type not, exists and forall.

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.

Parameters:

• x A PBES expression or a data expression

Returns: The left 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.

Parameters:

• x A PBES expression or a data expression

Returns: The left hand side of an expression of type and, or or imp.

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.

Parameters:

• t A PBES expression

Returns: The left hand side of an expression of type and, or or imp.

const core::identifier_string &mcrl2::pbes_system::accessors::name(const pbes_expression &t)

Returns the name of a propositional variable expression.

Parameters:

• t A PBES expression

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.

Parameters:

• t A PBES expression

Returns: The parameters of a propositional variable instantiation.

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.

Parameters:

• t A PBES expression

Returns: The right 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.

Parameters:

• t A PBES expression

Returns: The variables of a quantification expression