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

Base class for LPS summands. More...

#include <summand.h>

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

Public Member Functions

 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 Attributes

data::variable_list m_summation_variables
 The summation variables of the summand.
 
data::data_expression m_condition
 The condition of the summand.
 

Detailed Description

Base class for LPS summands.

Definition at line 24 of file summand.h.

Constructor & Destructor Documentation

◆ summand_base() [1/2]

mcrl2::lps::summand_base::summand_base ( )
inline

Constructor.

Definition at line 35 of file summand.h.

◆ summand_base() [2/2]

mcrl2::lps::summand_base::summand_base ( const data::variable_list summation_variables,
const data::data_expression condition 
)
inline

Constructor.

Definition at line 39 of file summand.h.

Member Function Documentation

◆ condition() [1/2]

data::data_expression & mcrl2::lps::summand_base::condition ( )
inline

Returns the condition expression.

Returns
The condition expression.

Definition at line 67 of file summand.h.

◆ condition() [2/2]

const data::data_expression & mcrl2::lps::summand_base::condition ( ) const
inline

Returns the condition expression.

Returns
The condition expression.

Definition at line 60 of file summand.h.

◆ summation_variables() [1/2]

data::variable_list & mcrl2::lps::summand_base::summation_variables ( )
inline

Returns the sequence of summation variables.

Returns
The sequence of summation variables.

Definition at line 46 of file summand.h.

◆ summation_variables() [2/2]

const data::variable_list & mcrl2::lps::summand_base::summation_variables ( ) const
inline

Returns the sequence of summation variables.

Returns
The sequence of summation variables.

Definition at line 53 of file summand.h.

◆ swap()

void mcrl2::lps::summand_base::swap ( summand_base other)
inline

Swaps the contents.

Definition at line 73 of file summand.h.

Member Data Documentation

◆ m_condition

data::data_expression mcrl2::lps::summand_base::m_condition
protected

The condition of the summand.

Definition at line 31 of file summand.h.

◆ m_summation_variables

data::variable_list mcrl2::lps::summand_base::m_summation_variables
protected

The summation variables of the summand.

Definition at line 28 of file summand.h.


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