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 ()
 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_summandoperator= (const stochastic_action_summand &) noexcept=default
 
stochastic_action_summandoperator= (stochastic_action_summand &&) noexcept=default
 
const stochastic_distributiondistribution () const
 Returns the distribution of this summand.
 
stochastic_distributiondistribution ()
 Returns the distribution of this summand.
 
void swap (stochastic_action_summand &other)
 Swaps the contents.
 
- Public Member Functions inherited from mcrl2::lps::action_summand
 action_summand ()
 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_summandoperator= (const action_summand &) noexcept=default
 
action_summandoperator= (action_summand &&) noexcept=default
 
const lps::multi_actionmulti_action () const
 Returns the multi-action of this summand.
 
lps::multi_actionmulti_action ()
 Returns the multi-action of this summand.
 
const data::assignment_listassignments () const
 Returns the sequence of assignments.
 
data::assignment_listassignments ()
 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)
 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 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
typedef summand_base super
 The super class.
 

Detailed Description

LPS summand containing a multi-action.

Definition at line 22 of file stochastic_action_summand.h.

Constructor & Destructor Documentation

◆ stochastic_action_summand() [1/5]

mcrl2::lps::stochastic_action_summand::stochastic_action_summand ( )
inline

Constructor.

Definition at line 30 of file stochastic_action_summand.h.

◆ 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 34 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 40 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 57 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 51 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)
inline

Swaps the contents.

Definition at line 63 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 26 of file stochastic_action_summand.h.


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