mcrl2::lps::action_summand

Include file:

#include "mcrl2/lps/action_summand.h

class mcrl2::lps::action_summand

LPS summand containing a multi-action.

Protected types

type mcrl2::lps::action_summand::super

typedef for summand_base

The super class.

Protected attributes

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

The assignments of the next state.

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

The summation variables of the summand.

Public member functions

action_summand()

Constructor.

action_summand(action_summand&&) noexcept = default

action_summand(const action_summand&) noexcept = default

Move semantics.

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

Constructor.

data::assignment_list &assignments()

Returns the sequence of assignments.

Returns: The sequence of assignments.

const data::assignment_list &assignments() const

Returns the sequence of assignments.

Returns: The sequence of assignments.

bool has_time() const

Returns true if time is available.

Returns: True if time is available.

bool is_tau() const

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.

lps::multi_action &multi_action()

Returns the multi-action of this summand.

const lps::multi_action &multi_action() const

Returns the multi-action of this summand.

data::data_expression_list 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_parameters A sequence of data variables

Returns: A symbolic representation of the next states

action_summand &operator=(action_summand&&) noexcept = default

action_summand &operator=(const action_summand&) noexcept = default

void swap(action_summand &other)

Swaps the contents.