mcrl2::pbes_system::pbes_equation Class Reference

pbes equation. More...

#include <pbes_equation.h>

Inheritance diagram for mcrl2::pbes_system::pbes_equation:

Public Types
typedef pbes_expression	term_type
	The expression type of the equation.
typedef propositional_variable	variable_type
	The variable type of the equation.
typedef fixpoint_symbol	symbol_type
	The symbol type of the equation.

Public Member Functions
	pbes_equation ()=default
	Constructor.
	pbes_equation (const fixpoint_symbol &symbol, const propositional_variable &variable, const pbes_expression &expr)
	Constructor.
const fixpoint_symbol &	symbol () const
	Returns the fixpoint symbol of the equation.
fixpoint_symbol &	symbol ()
	Returns the fixpoint symbol of the equation.
const propositional_variable &	variable () const
	Returns the pbes variable of the equation.
propositional_variable &	variable ()
	Returns the pbes variable of the equation.
const pbes_expression &	formula () const
	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.
bool	is_solved () const
	Returns true if the predicate formula on the right hand side contains no predicate variables.
void	swap (pbes_equation &other)
	Swaps the contents.
bool	operator< (const pbes_equation &other) const
	A comparison operator on pbes equations. \detail The comparison is on the addresses of aterm objects and can therefore differ in every run. \parameter other The variable to compare with.

Protected Attributes
fixpoint_symbol	m_symbol
	The fixpoint symbol of the equation.
propositional_variable	m_variable
	The variable on the left hand side of the equation.
pbes_expression	m_formula
	The expression on the right hand side of the equation.

Detailed Description

pbes equation.

Definition at line 31 of file pbes_equation.h.

Member Typedef Documentation

symbol_type

typedef fixpoint_symbol mcrl2::pbes_system::pbes_equation::symbol_type

The symbol type of the equation.

Definition at line 51 of file pbes_equation.h.

term_type

typedef pbes_expression mcrl2::pbes_system::pbes_equation::term_type

The expression type of the equation.

Definition at line 45 of file pbes_equation.h.

variable_type

typedef propositional_variable mcrl2::pbes_system::pbes_equation::variable_type

The variable type of the equation.

Definition at line 48 of file pbes_equation.h.

Constructor & Destructor Documentation

pbes_equation() [1/2]

mcrl2::pbes_system::pbes_equation::pbes_equation ( )

default

Constructor.

pbes_equation() [2/2]

mcrl2::pbes_system::pbes_equation::pbes_equation ( const fixpoint_symbol &  symbol, const propositional_variable &  variable, const pbes_expression &  expr  )

inline

Constructor.

Parameters

symbol	A fixpoint symbol
variable	A propositional variable declaration
expr	A PBES expression

Definition at line 60 of file pbes_equation.h.

Member Function Documentation

formula() [1/2]

pbes_expression & mcrl2::pbes_system::pbes_equation::formula ( )

inline

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

Returns

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

Definition at line 105 of file pbes_equation.h.

formula() [2/2]

const pbes_expression & mcrl2::pbes_system::pbes_equation::formula ( ) const

inline

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

Returns

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

Definition at line 98 of file pbes_equation.h.

is_solved()

bool mcrl2::pbes_system::pbes_equation::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.

Definition at line 103 of file pbes.cpp.

operator<()

bool mcrl2::pbes_system::pbes_equation::operator< ( const pbes_equation &  other ) const

inline

A comparison operator on pbes equations. \detail The comparison is on the addresses of aterm objects and can therefore differ in every run. \parameter other The variable to compare with.

Returns

True if the this argument is smaller than other.

Definition at line 128 of file pbes_equation.h.

swap()

void mcrl2::pbes_system::pbes_equation::swap ( pbes_equation &  other )

inline

Swaps the contents.

Definition at line 116 of file pbes_equation.h.

symbol() [1/2]

fixpoint_symbol & mcrl2::pbes_system::pbes_equation::symbol ( )

inline

Returns the fixpoint symbol of the equation.

Returns

The fixpoint symbol of the equation.

Definition at line 77 of file pbes_equation.h.

symbol() [2/2]

const fixpoint_symbol & mcrl2::pbes_system::pbes_equation::symbol ( ) const

inline

Returns the fixpoint symbol of the equation.

Returns

The fixpoint symbol of the equation.

Definition at line 70 of file pbes_equation.h.

variable() [1/2]

propositional_variable & mcrl2::pbes_system::pbes_equation::variable ( )

inline

Returns the pbes variable of the equation.

Returns

The pbes variable of the equation.

Definition at line 91 of file pbes_equation.h.

variable() [2/2]

const propositional_variable & mcrl2::pbes_system::pbes_equation::variable ( ) const

inline

Returns the pbes variable of the equation.

Returns

The pbes variable of the equation.

Definition at line 84 of file pbes_equation.h.

Member Data Documentation

m_formula

pbes_expression mcrl2::pbes_system::pbes_equation::m_formula

protected

The expression on the right hand side of the equation.

Definition at line 41 of file pbes_equation.h.

m_symbol

fixpoint_symbol mcrl2::pbes_system::pbes_equation::m_symbol

protected

The fixpoint symbol of the equation.

Definition at line 35 of file pbes_equation.h.

m_variable

propositional_variable mcrl2::pbes_system::pbes_equation::m_variable

protected

The variable on the left hand side of the equation.

Definition at line 38 of file pbes_equation.h.

---

The documentation for this class was generated from the following files:

• pbes/include/mcrl2/pbes/pbes_equation.h
• pbes/source/pbes.cpp