mCRL2
|
LPS summand containing a multi-action. More...
#include <action_summand.h>
Public Member Functions | |
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_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) |
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_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) |
Swaps the contents. | |
Protected Types | |
typedef summand_base | super |
The super class. | |
Protected Attributes | |
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. | |
LPS summand containing a multi-action.
Definition at line 24 of file action_summand.h.
|
protected |
The super class.
Definition at line 28 of file action_summand.h.
|
inline |
Constructor.
Definition at line 38 of file action_summand.h.
|
inline |
Constructor.
Definition at line 42 of file action_summand.h.
|
defaultnoexcept |
Move semantics.
|
defaultnoexcept |
|
inline |
Returns the sequence of assignments.
Definition at line 75 of file action_summand.h.
|
inline |
Returns the sequence of assignments.
Definition at line 68 of file action_summand.h.
|
inline |
Returns true if time is available.
Definition at line 90 of file action_summand.h.
|
inline |
Returns true if the multi-action corresponding to this summand is equal to tau.
Definition at line 83 of file action_summand.h.
|
inline |
Returns the multi-action of this summand.
Definition at line 61 of file action_summand.h.
|
inline |
Returns the multi-action of this summand.
Definition at line 55 of file action_summand.h.
data::data_expression_list mcrl2::lps::action_summand::next_state | ( | const data::variable_list & | process_parameters | ) | const |
Returns the next state corresponding to this summand.
The next state is constructed out of the assignments in this summand, by substituting the assignments to the list of variables that are an argument of this function. In general this argument is the list with the process parameters of this process.
process_parameters | A sequence of data variables |
|
defaultnoexcept |
|
defaultnoexcept |
|
inline |
Swaps the contents.
Definition at line 105 of file action_summand.h.
|
protected |
The assignments of the next state.
Definition at line 34 of file action_summand.h.
|
protected |
The summation variables of the summand.
Definition at line 31 of file action_summand.h.