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 super

typedef for summand_base

The super class.

Protected attributes

data::assignment_list m_assignments

The assignments of the next state.

lps::multi_action m_multi_action

The summation variables of the 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
const data::assignment_list &assignments() const

Returns the sequence of assignments.

Returns: The sequence of assignments.

data::assignment_list &assignments()

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.

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.

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=(const action_summand&) noexcept = default
action_summand &operator=(action_summand&&) noexcept = default
void swap(action_summand &other)

Swaps the contents.