mCRL2
Loading...
Searching...
No Matches
mcrl2::lps::deadlock_summand Class Reference

LPS summand containing a deadlock. More...

#include <deadlock_summand.h>

Inheritance diagram for mcrl2::lps::deadlock_summand:
mcrl2::lps::summand_base

Public Member Functions

 deadlock_summand ()
 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_summandoperator= (const deadlock_summand &) noexcept=default
 
deadlock_summandoperator= (deadlock_summand &&) noexcept=default
 
const lps::deadlockdeadlock () const
 Returns the deadlock of this summand.
 
lps::deadlockdeadlock ()
 Returns the deadlock of this summand.
 
bool has_time () const
 Returns true if time is available.
 
void swap (deadlock_summand &other)
 Swaps the contents.
 
- Public Member Functions inherited from mcrl2::lps::summand_base
 summand_base ()
 Constructor.
 
 summand_base (const data::variable_list &summation_variables, const data::data_expression &condition)
 Constructor.
 
data::variable_listsummation_variables ()
 Returns the sequence of summation variables.
 
const data::variable_listsummation_variables () const
 Returns the sequence of summation variables.
 
const data::data_expressioncondition () const
 Returns the condition expression.
 
data::data_expressioncondition ()
 Returns the condition expression.
 
void swap (summand_base &other)
 Swaps the contents.
 

Protected Types

typedef summand_base super
 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 24 of file deadlock_summand.h.

Member Typedef Documentation

◆ super

The super class.

Definition at line 28 of file deadlock_summand.h.

Constructor & Destructor Documentation

◆ deadlock_summand() [1/4]

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

Constructor.

Definition at line 36 of file deadlock_summand.h.

◆ 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 40 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 58 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 52 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 65 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)
inline

Swaps the contents.

Definition at line 71 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 31 of file deadlock_summand.h.


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