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

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

#include <action_summand.h>

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

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_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 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.
 

Detailed Description

LPS summand containing a multi-action.

Definition at line 24 of file action_summand.h.

Member Typedef Documentation

◆ super

The super class.

Definition at line 28 of file action_summand.h.

Constructor & Destructor Documentation

◆ action_summand() [1/4]

mcrl2::lps::action_summand::action_summand ( )
inline

Constructor.

Definition at line 38 of file action_summand.h.

◆ action_summand() [2/4]

mcrl2::lps::action_summand::action_summand ( const data::variable_list summation_variables,
const data::data_expression condition,
const lps::multi_action action,
const data::assignment_list assignments 
)
inline

Constructor.

Definition at line 42 of file action_summand.h.

◆ action_summand() [3/4]

mcrl2::lps::action_summand::action_summand ( const action_summand )
defaultnoexcept

Move semantics.

◆ action_summand() [4/4]

mcrl2::lps::action_summand::action_summand ( action_summand &&  )
defaultnoexcept

Member Function Documentation

◆ assignments() [1/2]

data::assignment_list & mcrl2::lps::action_summand::assignments ( )
inline

Returns the sequence of assignments.

Returns
The sequence of assignments.

Definition at line 75 of file action_summand.h.

◆ assignments() [2/2]

const data::assignment_list & mcrl2::lps::action_summand::assignments ( ) const
inline

Returns the sequence of assignments.

Returns
The sequence of assignments.

Definition at line 68 of file action_summand.h.

◆ has_time()

bool mcrl2::lps::action_summand::has_time ( ) const
inline

Returns true if time is available.

Returns
True if time is available.

Definition at line 90 of file action_summand.h.

◆ is_tau()

bool mcrl2::lps::action_summand::is_tau ( ) const
inline

Returns true if the multi-action corresponding to this summand is equal to tau.

Returns
True if the multi-action corresponding to this summand is equal to tau.

Definition at line 83 of file action_summand.h.

◆ multi_action() [1/2]

lps::multi_action & mcrl2::lps::action_summand::multi_action ( )
inline

Returns the multi-action of this summand.

Definition at line 61 of file action_summand.h.

◆ multi_action() [2/2]

const lps::multi_action & mcrl2::lps::action_summand::multi_action ( ) const
inline

Returns the multi-action of this summand.

Definition at line 55 of file action_summand.h.

◆ next_state()

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.

Parameters
process_parametersA sequence of data variables
Returns
A symbolic representation of the next states

Definition at line 68 of file lps.cpp.

◆ operator=() [1/2]

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

◆ operator=() [2/2]

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

◆ swap()

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

Swaps the contents.

Definition at line 105 of file action_summand.h.

Member Data Documentation

◆ m_assignments

data::assignment_list mcrl2::lps::action_summand::m_assignments
protected

The assignments of the next state.

Definition at line 34 of file action_summand.h.

◆ m_multi_action

lps::multi_action mcrl2::lps::action_summand::m_multi_action
protected

The summation variables of the summand.

Definition at line 31 of file action_summand.h.


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