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.