mcrl2::process::process_specification

Include file:

#include "mcrl2/process/process_specification.h
class mcrl2::process::process_specification

Process specification consisting of a data specification, action labels, a sequence of process equations and a process initialization.

Protected attributes

process::action_label_list mcrl2::process::process_specification::m_action_labels

The action specification of the specification.

data::data_specification mcrl2::process::process_specification::m_data

The data specification of the specification.

std::vector<process_equation> mcrl2::process::process_specification::m_equations

The equations of the specification.

std::set<data::variable> mcrl2::process::process_specification::m_global_variables

The set of global variables.

process_expression mcrl2::process::process_specification::m_initial_process

The initial state of the specification.

Protected member functions

void construct_from_aterm(const atermpp::aterm_appl &t)

Initializes the specification with an aterm.

Parameters:

  • t A term

Public member functions

const process::action_label_list &action_labels() const

Returns the action label specification.

Returns: The action label specification

process::action_label_list &action_labels()

Returns the action label specification.

Returns: The action label specification

const data::data_specification &data() const

Returns the data specification.

Returns: The data specification

data::data_specification &data()

Returns the data specification.

Returns: The data specification

const std::vector<process_equation> &equations() const

Returns the equations of the process specification.

Returns: The equations of the process specification

std::vector<process_equation> &equations()

Returns the equations of the process specification.

Returns: The equations of the process specification

const std::set<data::variable> &global_variables() const

Returns the declared free variables of the process specification.

Returns: The declared free variables of the process specification.

std::set<data::variable> &global_variables()

Returns the declared free variables of the process specification.

Returns: The declared free variables of the process specification.

const process_expression &init() const

Returns the initialization of the process specification.

Returns: The initialization of the process specification

process_expression &init()

Returns the initialization of the process specification.

Returns: The initialization of the process specification

process_specification()

Constructor.

process_specification(atermpp::aterm_appl t)

Constructor.

Parameters:

  • t A term containing an aterm representation of a process specification.

process_specification(data::data_specification data, process::action_label_list action_labels, process_equation_list equations, process_expression init)

Constructor that sets the global variables to empty;.

process_specification(data::data_specification data, process::action_label_list action_labels, data::variable_list global_variables, process_equation_list equations, process_expression init)

Constructor of a process specification.