mcrl2/pbes/pbes_expression.h

Include file:

#include "mcrl2/pbes/pbes_expression.h"

The class pbes_expression.

Typedefs

type pbes_expression_list

typedef for atermpp::term_list< pbes_expression >

list of pbes_expressions

type pbes_expression_vector

typedef for std::vector< pbes_expression >

vector of pbes_expressions

type propositional_variable_instantiation_list

typedef for atermpp::term_list< propositional_variable_instantiation >

list of propositional_variable_instantiations

type propositional_variable_instantiation_vector

typedef for std::vector< propositional_variable_instantiation >

vector of propositional_variable_instantiations

type propositional_variable_key_type

typedef for std::pair< core::identifier_string, data::data_expression_list >

Functions

pbes_expression mcrl2::pbes_system::false_()

Returns: Returns the value false

std::set<data::variable> find_free_variables(const pbes_system::pbes_expression &x)
std::set<core::identifier_string> find_identifiers(const pbes_system::pbes_expression &x)
std::set<pbes_system::propositional_variable_instantiation> find_propositional_variable_instantiations(const pbes_system::pbes_expression &x)
data::variable_list mcrl2::pbes_system::free_variables(const pbes_expression &x)
bool is_and(const atermpp::aterm_appl &x)

Test for a and expression.

Parameters:

  • x A term

Returns: True if 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)

Test for a exists expression.

Parameters:

  • x A term

Returns: True if 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)

Test for a forall expression.

Parameters:

  • x A term

Returns: True if x is a forall expression

bool is_imp(const atermpp::aterm_appl &x)

Test for a imp expression.

Parameters:

  • x A term

Returns: True if x is a imp expression

bool is_not(const atermpp::aterm_appl &x)

Test for a not expression.

Parameters:

  • x A term

Returns: True if x is a not expression

bool is_or(const atermpp::aterm_appl &x)

Test for a or expression.

Parameters:

  • x A term

Returns: True if 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)

Test for a pbes_expression expression.

Parameters:

  • x A term

Returns: True if 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)

Test for a propositional_variable_instantiation expression.

Parameters:

  • x A term

Returns: True if 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

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

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

pbes_system::pbes_expression normalize_sorts(const pbes_system::pbes_expression &x, const data::sort_specification &sortspec)
std::ostream &mcrl2::pbes_system::operator<<(std::ostream &out, const pbes_expression &x)

Outputs the object to a stream.

Parameters:

  • out An output stream
  • x Object x

Returns: The output stream

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

Outputs the object to a stream.

Parameters:

  • out An output stream
  • x Object x

Returns: The output stream

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

Outputs the object to a stream.

Parameters:

  • out An output stream
  • x Object x

Returns: The output stream

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

Outputs the object to a stream.

Parameters:

  • out An output stream
  • x Object x

Returns: The output stream

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

Outputs the object to a stream.

Parameters:

  • out An output stream
  • x Object x

Returns: The output stream

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

Outputs the object to a stream.

Parameters:

  • out An output stream
  • x Object x

Returns: The output stream

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

Outputs the object to a stream.

Parameters:

  • out An output stream
  • x Object x

Returns: The output stream

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

Outputs the object to a stream.

Parameters:

  • out An output stream
  • x Object x

Returns: The output stream

pbes_expression mcrl2::pbes_system::optimized_and(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

pbes_expression mcrl2::pbes_system::optimized_exists(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

pbes_expression mcrl2::pbes_system::optimized_forall(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

pbes_expression mcrl2::pbes_system::optimized_imp(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

pbes_expression mcrl2::pbes_system::optimized_not(const pbes_expression &p)

Make a negation.

Parameters:

  • p A PBES expression

Returns: The value !p

pbes_expression mcrl2::pbes_system::optimized_or(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

std::string pp(const pbes_expression &x)
std::string pp(const propositional_variable_instantiation &x)
std::string pp(const not_ &x)
std::string pp(const and_ &x)
std::string pp(const or_ &x)
std::string pp(const imp &x)
std::string pp(const forall &x)
std::string pp(const exists &x)
std::string pp(const pbes_expression_list &x)
std::string pp(const pbes_expression_vector &x)
std::string pp(const propositional_variable_instantiation_list &x)
std::string pp(const propositional_variable_instantiation_vector &x)
const data::variable_list &mcrl2::pbes_system::quantifier_variables(const pbes_expression &x)
bool search_variable(const pbes_system::pbes_expression &x, const data::variable &v)
void mcrl2::pbes_system::swap(pbes_expression &t1, pbes_expression &t2)

swap overload

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

swap overload

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

swap overload

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

swap overload

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

swap overload

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

swap overload

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

swap overload

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

swap overload

pbes_system::pbes_expression translate_user_notation(const pbes_system::pbes_expression &x)
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