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

#include <process_specification.h>

Public Member Functions
	process_specification ()=default
	Constructor.

	process_specification (atermpp::aterm t)
	Constructor.

	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.

const data::data_specification &	data () const
	Returns the data specification.

data::data_specification &	data ()
	Returns the data specification.

const process::action_label_list &	action_labels () const
	Returns the action label specification.

process::action_label_list &	action_labels ()
	Returns the action label specification.

const std::set< data::variable > &	global_variables () const
	Returns the declared free variables of the process specification.

std::set< data::variable > &	global_variables ()
	Returns the declared free variables of the process specification.

const std::vector< process_equation > &	equations () const
	Returns the equations of the process specification.

std::vector< process_equation > &	equations ()
	Returns the equations of the process specification.

const process_expression &	init () const
	Returns the initialization of the process specification.

process_expression &	init ()
	Returns the initialization of the process specification.

Protected Member Functions
void	construct_from_aterm (const atermpp::aterm &t)
	Initializes the specification with an aterm.

Protected Attributes
data::data_specification	m_data
	The data specification of the specification.

process::action_label_list	m_action_labels
	The action specification of the specification.

std::set< data::variable >	m_global_variables
	The set of global variables.

std::vector< process_equation >	m_equations
	The equations of the specification.

process_expression	m_initial_process
	The initial state of the specification.

Detailed Description

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

Definition at line 48 of file process_specification.h.

Constructor & Destructor Documentation

◆ process_specification() [1/4]

mcrl2::process::process_specification::process_specification ( )

default

Constructor.

◆ process_specification() [2/4]

mcrl2::process::process_specification::process_specification ( atermpp::aterm t )

inlineexplicit

Constructor.

Parameters

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

Definition at line 87 of file process_specification.h.

◆ process_specification() [3/4]

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

inline

Constructor that sets the global variables to empty;.

Definition at line 95 of file process_specification.h.

◆ process_specification() [4/4]

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

inline

Constructor of a process specification.

Definition at line 103 of file process_specification.h.

Member Function Documentation

◆ action_labels() [1/2]

process::action_label_list & mcrl2::process::process_specification::action_labels ( )

inline

Returns the action label specification.

Returns: The action label specification

Definition at line 139 of file process_specification.h.

◆ action_labels() [2/2]

const process::action_label_list & mcrl2::process::process_specification::action_labels ( ) const

inline

Returns the action label specification.

Returns: The action label specification

Definition at line 132 of file process_specification.h.

◆ construct_from_aterm()

void mcrl2::process::process_specification::construct_from_aterm ( const atermpp::aterm & t )

inlineprotected

Initializes the specification with an aterm.

Parameters

t A term

Definition at line 68 of file process_specification.h.

◆ data() [1/2]

data::data_specification & mcrl2::process::process_specification::data ( )

inline

Returns the data specification.

Returns: The data specification

Definition at line 125 of file process_specification.h.

◆ data() [2/2]

const data::data_specification & mcrl2::process::process_specification::data ( ) const

inline

Returns the data specification.

Returns: The data specification

Definition at line 118 of file process_specification.h.

◆ equations() [1/2]

std::vector< process_equation > & mcrl2::process::process_specification::equations ( )

inline

Returns the equations of the process specification.

Returns: The equations of the process specification

Definition at line 167 of file process_specification.h.

◆ equations() [2/2]

const std::vector< process_equation > & mcrl2::process::process_specification::equations ( ) const

inline

Returns the equations of the process specification.

Returns: The equations of the process specification

Definition at line 160 of file process_specification.h.

◆ global_variables() [1/2]

std::set< data::variable > & mcrl2::process::process_specification::global_variables ( )

inline

Returns the declared free variables of the process specification.

Returns: The declared free variables of the process specification.

Definition at line 153 of file process_specification.h.

◆ global_variables() [2/2]

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

inline

Returns the declared free variables of the process specification.

Returns: The declared free variables of the process specification.

Definition at line 146 of file process_specification.h.

◆ init() [1/2]

process_expression & mcrl2::process::process_specification::init ( )

inline

Returns the initialization of the process specification.

Returns: The initialization of the process specification

Definition at line 181 of file process_specification.h.

◆ init() [2/2]

const process_expression & mcrl2::process::process_specification::init ( ) const

inline

Returns the initialization of the process specification.

Returns: The initialization of the process specification

Definition at line 174 of file process_specification.h.

Member Data Documentation

◆ m_action_labels

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

protected

The action specification of the specification.

Definition at line 55 of file process_specification.h.

◆ m_data

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

protected

The data specification of the specification.

Definition at line 52 of file process_specification.h.

◆ m_equations

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

protected

The equations of the specification.

Definition at line 61 of file process_specification.h.

◆ m_global_variables

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

protected

The set of global variables.

Definition at line 58 of file process_specification.h.

◆ m_initial_process

process_expression mcrl2::process::process_specification::m_initial_process

protected

The initial state of the specification.

Definition at line 64 of file process_specification.h.

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

process/include/mcrl2/process/process_specification.h

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ process_specification() [1/4]

◆ process_specification() [2/4]

◆ process_specification() [3/4]

◆ process_specification() [4/4]

Member Function Documentation

◆ action_labels() [1/2]

◆ action_labels() [2/2]

◆ construct_from_aterm()

◆ data() [1/2]

◆ data() [2/2]

◆ equations() [1/2]

◆ equations() [2/2]

◆ global_variables() [1/2]

◆ global_variables() [2/2]

◆ init() [1/2]

◆ init() [2/2]

Member Data Documentation

◆ m_action_labels

◆ m_data

◆ m_equations

◆ m_global_variables

◆ m_initial_process