mcrl2::pbes_system::pbes_equation¶

Include file:

#include "mcrl2/pbes/pbes_equation.h

class mcrl2::pbes_system::pbes_equation

pbes equation.

Public types¶

type symbol_type

typedef for fixpoint_symbol

The symbol type of the equation.

type term_type

typedef for pbes_expression

The expression type of the equation.

type variable_type

typedef for propositional_variable

The variable type of the equation.

Protected attributes¶

pbes_expression m_formula

The expression on the right hand side of the equation.

fixpoint_symbol m_symbol

The fixpoint symbol of the equation.

propositional_variable m_variable

The variable on the left hand side of the equation.

Public member functions¶

const pbes_expression &formula() const

Returns the predicate formula on the right hand side of the equation.

Returns: The predicate formula on the right hand side of the equation.

pbes_expression &formula()

Returns the predicate formula on the right hand side of the equation.

Returns: The predicate formula on the right hand side of the equation.

bool is_solved() const

Returns true if the predicate formula on the right hand side contains no predicate variables.

Returns: True if the predicate formula on the right hand side contains no predicate variables.

pbes_equation() = default

Constructor.

pbes_equation(const atermpp::aterm_appl &t)

Constructor.

Parameters:

• t A term
pbes_equation(const atermpp::aterm &t1)

Constructor.

Parameters:

• t1 A term
pbes_equation(const fixpoint_symbol &symbol, const propositional_variable &variable, const pbes_expression &expr)

Constructor.

Parameters:

• symbol A fixpoint symbol
• variable A propositional variable declaration
• expr A PBES expression
void swap(pbes_equation &other)

Swaps the contents.

const fixpoint_symbol &symbol() const

Returns the fixpoint symbol of the equation.

Returns: The fixpoint symbol of the equation.

fixpoint_symbol &symbol()

Returns the fixpoint symbol of the equation.

Returns: The fixpoint symbol of the equation.

const propositional_variable &variable() const

Returns the pbes variable of the equation.

Returns: The pbes variable of the equation.

propositional_variable &variable()

Returns the pbes variable of the equation.

Returns: The pbes variable of the equation.