mcrl2::pbes_system::pbes_equation

Include file:

#include "mcrl2/pbes/pbes_equation.h

class mcrl2::pbes_system::pbes_equation

pbes equation.

Public types

type mcrl2::pbes_system::pbes_equation::symbol_type

typedef for fixpoint_symbol

The symbol type of the equation.

type mcrl2::pbes_system::pbes_equation::term_type

typedef for pbes_expression

The expression type of the equation.

type mcrl2::pbes_system::pbes_equation::variable_type

typedef for propositional_variable

The variable type of the equation.

Protected attributes

pbes_expression mcrl2::pbes_system::pbes_equation::m_formula

The expression on the right hand side of the equation.

fixpoint_symbol mcrl2::pbes_system::pbes_equation::m_symbol

The fixpoint symbol of the equation.

propositional_variable mcrl2::pbes_system::pbes_equation::m_variable

The variable on the left hand side of the equation.

Public member functions

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.

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.

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 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.

fixpoint_symbol &symbol()

Returns the fixpoint symbol of the equation.

Returns: The fixpoint symbol of the equation.

const fixpoint_symbol &symbol() const

Returns the fixpoint symbol of the equation.

Returns: The fixpoint symbol of the equation.

propositional_variable &variable()

Returns the pbes variable of the equation.

Returns: The pbes variable of the equation.

const propositional_variable &variable() const

Returns the pbes variable of the equation.

Returns: The pbes variable of the equation.