Linear process specification. More...

#include <specification.h>

Inheritance diagram for mcrl2::lps::specification:

Public Member Functions
	specification ()=default
	Constructor.

	specification (const data::data_specification &data, const process::action_label_list &action_labels, const std::set< data::variable > &global_variables, const linear_process &lps, const process_initializer &initial_process)
	Constructor.

Public Member Functions inherited from mcrl2::lps::specification_base< linear_process, process_initializer >
	specification_base ()=default
	Constructor.

	specification_base (const data::data_specification &data, const process::action_label_list &action_labels, const std::set< data::variable > &global_variables, const linear_process &lps, const process_initializer &initial_process)
	Constructor.

const linear_process &	process () const
	Returns the linear process of the specification.

linear_process &	process ()
	Returns a reference to the linear process of the specification.

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

data::data_specification &	data ()
	Returns a reference to the data specification.

const process::action_label_list &	action_labels () const
	Returns a sequence of action labels. This sequence contains all action labels occurring in the specification (but it can have more).

process::action_label_list &	action_labels ()
	Returns a sequence of action labels. This sequence contains all action labels occurring in the specification (but it can have more).

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

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

const process_initializer &	initial_process () const
	Returns the initial process.

process_initializer &	initial_process ()
	Returns a reference to the initial process.

Protected Types
using	super = specification_base< linear_process, process_initializer >

Additional Inherited Members
Public Types inherited from mcrl2::lps::specification_base< linear_process, process_initializer >
using	process_type = linear_process
	The process type.

using	initial_process_type = process_initializer
	The initial process type.

Protected Attributes inherited from mcrl2::lps::specification_base< linear_process, process_initializer >
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.

linear_process	m_process
	The linear process of the specification.

process_initializer	m_initial_process
	The initial state of the specification.

Detailed Description

Linear process specification.

Definition at line 170 of file specification.h.

Member Typedef Documentation

◆ super

using mcrl2::lps::specification::super = specification_base<linear_process, process_initializer>

protected

Definition at line 173 of file specification.h.

Constructor & Destructor Documentation

◆ specification() [1/2]

mcrl2::lps::specification::specification ( )

default

Constructor.

◆ specification() [2/2]

mcrl2::lps::specification::specification	(	const data::data_specification &	data,
		const process::action_label_list &	action_labels,
		const std::set< data::variable > &	global_variables,
		const linear_process &	lps,
		const process_initializer &	initial_process
	)

inline

Constructor.

Parameters

data	A data specification
action_labels	A sequence of action labels
global_variables	A set of global variables
lps	A linear process
initial_process	A process initializer

Definition at line 185 of file specification.h.

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

lps/include/mcrl2/lps/specification.h

Public Member Functions