mcrl2::lps::deadlock_summand Class Reference

LPS summand containing a deadlock. More...

#include <deadlock_summand.h>

Inheritance diagram for mcrl2::lps::deadlock_summand:

Public Member Functions
	deadlock_summand ()=default
	Constructor.
	deadlock_summand (const data::variable_list &summation_variables, const data::data_expression &condition, const lps::deadlock &delta)
	Constructor.
	deadlock_summand (const deadlock_summand &) noexcept=default
	Move semantics.
	deadlock_summand (deadlock_summand &&) noexcept=default
deadlock_summand &	operator= (const deadlock_summand &) noexcept=default
deadlock_summand &	operator= (deadlock_summand &&) noexcept=default
const lps::deadlock &	deadlock () const
	Returns the deadlock of this summand.
lps::deadlock &	deadlock ()
	Returns the deadlock of this summand.
bool	has_time () const
	Returns true if time is available.
void	swap (deadlock_summand &other) noexcept
	Swaps the contents.
Public Member Functions inherited from mcrl2::lps::summand_base
	summand_base ()=default
	Constructor.
	summand_base (const data::variable_list &summation_variables, const data::data_expression &condition)
	Constructor.
data::variable_list &	summation_variables ()
	Returns the sequence of summation variables.
const data::variable_list &	summation_variables () const
	Returns the sequence of summation variables.
const data::data_expression &	condition () const
	Returns the condition expression.
data::data_expression &	condition ()
	Returns the condition expression.
void	swap (summand_base &other) noexcept
	Swaps the contents.

Protected Types
using	super = summand_base
	The super class.

Protected Attributes
lps::deadlock	m_deadlock
	The deadlock of the summand.
Protected Attributes inherited from mcrl2::lps::summand_base
data::variable_list	m_summation_variables
	The summation variables of the summand.
data::data_expression	m_condition
	The condition of the summand.

Detailed Description

LPS summand containing a deadlock.

Definition at line 22 of file deadlock_summand.h.

Member Typedef Documentation

super

using mcrl2::lps::deadlock_summand::super = summand_base

protected

The super class.

Definition at line 26 of file deadlock_summand.h.

Constructor & Destructor Documentation

deadlock_summand() [1/4]

mcrl2::lps::deadlock_summand::deadlock_summand ( )

default

Constructor.

deadlock_summand() [2/4]

mcrl2::lps::deadlock_summand::deadlock_summand ( const data::variable_list &  summation_variables, const data::data_expression &  condition, const lps::deadlock &  delta  )

inline

Constructor.

Definition at line 37 of file deadlock_summand.h.

deadlock_summand() [3/4]

mcrl2::lps::deadlock_summand::deadlock_summand ( const deadlock_summand &  )

defaultnoexcept

Move semantics.

deadlock_summand() [4/4]

mcrl2::lps::deadlock_summand::deadlock_summand ( deadlock_summand &&  )

defaultnoexcept

Member Function Documentation

deadlock() [1/2]

lps::deadlock & mcrl2::lps::deadlock_summand::deadlock ( )

inline

Returns the deadlock of this summand.

Definition at line 55 of file deadlock_summand.h.

deadlock() [2/2]

const lps::deadlock & mcrl2::lps::deadlock_summand::deadlock ( ) const

inline

Returns the deadlock of this summand.

Definition at line 49 of file deadlock_summand.h.

has_time()

bool mcrl2::lps::deadlock_summand::has_time ( ) const

inline

Returns true if time is available.

Returns

True if time is available.

Definition at line 62 of file deadlock_summand.h.

operator=() [1/2]

deadlock_summand & mcrl2::lps::deadlock_summand::operator= ( const deadlock_summand &  )

defaultnoexcept

operator=() [2/2]

deadlock_summand & mcrl2::lps::deadlock_summand::operator= ( deadlock_summand &&  )

defaultnoexcept

swap()

void mcrl2::lps::deadlock_summand::swap ( deadlock_summand &  other )

inlinenoexcept

Swaps the contents.

Definition at line 68 of file deadlock_summand.h.

Member Data Documentation

m_deadlock

lps::deadlock mcrl2::lps::deadlock_summand::m_deadlock

protected

The deadlock of the summand.

Definition at line 29 of file deadlock_summand.h.

---

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

• lps/include/mcrl2/lps/deadlock_summand.h