|
mCRL2
|
LPS summand containing a multi-action. More...
#include <stochastic_action_summand.h>
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. | |
LPS summand containing a multi-action.
Definition at line 20 of file stochastic_action_summand.h.
|
default |
Constructor.
|
inline |
Constructor.
Definition at line 31 of file stochastic_action_summand.h.
|
inline |
Constructor.
Definition at line 37 of file stochastic_action_summand.h.
|
defaultnoexcept |
Move semantics.
|
defaultnoexcept |
|
inline |
Returns the distribution of this summand.
Definition at line 54 of file stochastic_action_summand.h.
|
inline |
Returns the distribution of this summand.
Definition at line 48 of file stochastic_action_summand.h.
|
defaultnoexcept |
|
defaultnoexcept |
|
inlinenoexcept |
Swaps the contents.
Definition at line 60 of file stochastic_action_summand.h.
|
protected |
The distribution of the summand.
Definition at line 24 of file stochastic_action_summand.h.