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

LPS summand containing a multi-action. More...

#include <stochastic_action_summand.h>

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

Public Member Functions

 stochastic_action_summand ()=default
 Constructor.
 
 stochastic_action_summand (const data::variable_list &summation_variables, const data::data_expression &condition, const lps::multi_action &action, const data::assignment_list &assignments, const stochastic_distribution &distribution)
 Constructor.
 
 stochastic_action_summand (const action_summand &s)
 Constructor.
 
 stochastic_action_summand (const stochastic_action_summand &) noexcept=default
 Move semantics.
 
 stochastic_action_summand (stochastic_action_summand &&) noexcept=default
 
stochastic_action_summand & operator= (const stochastic_action_summand &) noexcept=default
 
stochastic_action_summand & operator= (stochastic_action_summand &&) noexcept=default
 
const stochastic_distribution & distribution () const
 Returns the distribution of this summand.
 
stochastic_distribution & distribution ()
 Returns the distribution of this summand.
 
void swap (stochastic_action_summand &other) noexcept
 Swaps the contents.
 
- Public Member Functions inherited from mcrl2::lps::action_summand
 action_summand ()=default
 Constructor.
 
 action_summand (const data::variable_list &summation_variables, const data::data_expression &condition, const lps::multi_action &action, const data::assignment_list &assignments)
 Constructor.
 
 action_summand (const action_summand &) noexcept=default
 Move semantics.
 
 action_summand (action_summand &&) noexcept=default
 
action_summand & operator= (const action_summand &) noexcept=default
 
action_summand & operator= (action_summand &&) noexcept=default
 
const lps::multi_action & multi_action () const
 Returns the multi-action of this summand.
 
lps::multi_action & multi_action ()
 Returns the multi-action of this summand.
 
const data::assignment_list & assignments () const
 Returns the sequence of assignments.
 
data::assignment_list & assignments ()
 Returns the sequence of assignments.
 
bool is_tau () const
 Returns true if the multi-action corresponding to this summand is equal to tau.
 
bool has_time () const
 Returns true if time is available.
 
data::data_expression_list next_state (const data::variable_list &process_parameters) const
 Returns the next state corresponding to this summand.
 
void swap (action_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 Attributes

stochastic_distribution m_distribution
 The distribution of the summand.
 
- Protected Attributes inherited from mcrl2::lps::action_summand
lps::multi_action m_multi_action
 The summation variables of the summand.
 
data::assignment_list m_assignments
 The assignments of the next state.
 
- 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.
 

Additional Inherited Members

- Protected Types inherited from mcrl2::lps::action_summand
using super = summand_base
 The super class.
 

Detailed Description

LPS summand containing a multi-action.

Definition at line 20 of file stochastic_action_summand.h.

Constructor & Destructor Documentation

◆ stochastic_action_summand() [1/5]

mcrl2::lps::stochastic_action_summand::stochastic_action_summand ( )
default

Constructor.

◆ stochastic_action_summand() [2/5]

mcrl2::lps::stochastic_action_summand::stochastic_action_summand ( const data::variable_list &  summation_variables,
const data::data_expression &  condition,
const lps::multi_action &  action,
const data::assignment_list &  assignments,
const stochastic_distribution &  distribution 
)
inline

Constructor.

Definition at line 31 of file stochastic_action_summand.h.

◆ stochastic_action_summand() [3/5]

mcrl2::lps::stochastic_action_summand::stochastic_action_summand ( const action_summand &  s)
inline

Constructor.

Definition at line 37 of file stochastic_action_summand.h.

◆ stochastic_action_summand() [4/5]

mcrl2::lps::stochastic_action_summand::stochastic_action_summand ( const stochastic_action_summand &  )
defaultnoexcept

Move semantics.

◆ stochastic_action_summand() [5/5]

mcrl2::lps::stochastic_action_summand::stochastic_action_summand ( stochastic_action_summand &&  )
defaultnoexcept

Member Function Documentation

◆ distribution() [1/2]

stochastic_distribution & mcrl2::lps::stochastic_action_summand::distribution ( )
inline

Returns the distribution of this summand.

Definition at line 54 of file stochastic_action_summand.h.

◆ distribution() [2/2]

const stochastic_distribution & mcrl2::lps::stochastic_action_summand::distribution ( ) const
inline

Returns the distribution of this summand.

Definition at line 48 of file stochastic_action_summand.h.

◆ operator=() [1/2]

stochastic_action_summand & mcrl2::lps::stochastic_action_summand::operator= ( const stochastic_action_summand &  )
defaultnoexcept

◆ operator=() [2/2]

stochastic_action_summand & mcrl2::lps::stochastic_action_summand::operator= ( stochastic_action_summand &&  )
defaultnoexcept

◆ swap()

void mcrl2::lps::stochastic_action_summand::swap ( stochastic_action_summand &  other)
inlinenoexcept

Swaps the contents.

Definition at line 60 of file stochastic_action_summand.h.

Member Data Documentation

◆ m_distribution

stochastic_distribution mcrl2::lps::stochastic_action_summand::m_distribution
protected

The distribution of the summand.

Definition at line 24 of file stochastic_action_summand.h.


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