#include <specification.h>

Public Types
typedef LinearProcess	process_type
	The process type.

typedef InitialProcessExpression	initial_process_type
	The initial process type.

Public Member Functions
	specification_base ()
	Constructor.

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

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

LinearProcess &	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 InitialProcessExpression &	initial_process () const
	Returns the initial process.

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

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.

LinearProcess	m_process
	The linear process of the specification.

InitialProcessExpression	m_initial_process
	The initial state of the specification.

Detailed Description

template<typename LinearProcess, typename InitialProcessExpression>
class mcrl2::lps::specification_base< LinearProcess, InitialProcessExpression >

Definition at line 50 of file specification.h.

Member Typedef Documentation

◆ initial_process_type

template<typename LinearProcess , typename InitialProcessExpression >

typedef InitialProcessExpression mcrl2::lps::specification_base< LinearProcess, InitialProcessExpression >::initial_process_type

The initial process type.

Definition at line 73 of file specification.h.

◆ process_type

template<typename LinearProcess , typename InitialProcessExpression >

typedef LinearProcess mcrl2::lps::specification_base< LinearProcess, InitialProcessExpression >::process_type

The process type.

Definition at line 70 of file specification.h.

Constructor & Destructor Documentation

◆ specification_base() [1/2]

template<typename LinearProcess , typename InitialProcessExpression >

mcrl2::lps::specification_base< LinearProcess, InitialProcessExpression >::specification_base ( )

inline

Constructor.

Definition at line 76 of file specification.h.

◆ specification_base() [2/2]

template<typename LinearProcess , typename InitialProcessExpression >

mcrl2::lps::specification_base< LinearProcess, InitialProcessExpression >::specification_base	(	const data::data_specification &	data,
		const process::action_label_list &	action_labels,
		const std::set< data::variable > &	global_variables,
		const LinearProcess &	lps,
		const InitialProcessExpression &	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 85 of file specification.h.

Member Function Documentation

◆ action_labels() [1/2]

template<typename LinearProcess , typename InitialProcessExpression >

process::action_label_list & mcrl2::lps::specification_base< LinearProcess, InitialProcessExpression >::action_labels ( )

inline

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

Returns: A sequence of action labels.

Definition at line 139 of file specification.h.

◆ action_labels() [2/2]

template<typename LinearProcess , typename InitialProcessExpression >

const process::action_label_list & mcrl2::lps::specification_base< LinearProcess, InitialProcessExpression >::action_labels ( ) const

inline

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

Returns: A sequence of action labels.

Definition at line 131 of file specification.h.

◆ data() [1/2]

template<typename LinearProcess , typename InitialProcessExpression >

data::data_specification & mcrl2::lps::specification_base< LinearProcess, InitialProcessExpression >::data ( )

inline

Returns a reference to the data specification.

Returns: The data specification.

Definition at line 123 of file specification.h.

◆ data() [2/2]

template<typename LinearProcess , typename InitialProcessExpression >

const data::data_specification & mcrl2::lps::specification_base< LinearProcess, InitialProcessExpression >::data ( ) const

inline

Returns the data specification.

Returns: The data specification.

Definition at line 116 of file specification.h.

◆ global_variables() [1/2]

template<typename LinearProcess , typename InitialProcessExpression >

std::set< data::variable > & mcrl2::lps::specification_base< LinearProcess, InitialProcessExpression >::global_variables ( )

inline

Returns the declared free variables of the LPS.

Returns: The declared free variables of the LPS.

Definition at line 153 of file specification.h.

◆ global_variables() [2/2]

template<typename LinearProcess , typename InitialProcessExpression >

const std::set< data::variable > & mcrl2::lps::specification_base< LinearProcess, InitialProcessExpression >::global_variables ( ) const

inline

Returns the declared free variables of the LPS.

Returns: The declared free variables of the LPS.

Definition at line 146 of file specification.h.

◆ initial_process() [1/2]

template<typename LinearProcess , typename InitialProcessExpression >

InitialProcessExpression & mcrl2::lps::specification_base< LinearProcess, InitialProcessExpression >::initial_process ( )

inline

Returns a reference to the initial process.

Returns: The initial process.

Definition at line 167 of file specification.h.

◆ initial_process() [2/2]

template<typename LinearProcess , typename InitialProcessExpression >

const InitialProcessExpression & mcrl2::lps::specification_base< LinearProcess, InitialProcessExpression >::initial_process ( ) const

inline

Returns the initial process.

Returns: The initial process.

Definition at line 160 of file specification.h.

◆ process() [1/2]

template<typename LinearProcess , typename InitialProcessExpression >

LinearProcess & mcrl2::lps::specification_base< LinearProcess, InitialProcessExpression >::process ( )

inline

Returns a reference to the linear process of the specification.

Returns: The linear process of the specification.

Definition at line 109 of file specification.h.

◆ process() [2/2]

template<typename LinearProcess , typename InitialProcessExpression >

const LinearProcess & mcrl2::lps::specification_base< LinearProcess, InitialProcessExpression >::process ( ) const

inline

Returns the linear process of the specification.

Returns: The linear process of the specification.

Definition at line 102 of file specification.h.

Member Data Documentation

◆ m_action_labels

template<typename LinearProcess , typename InitialProcessExpression >

process::action_label_list mcrl2::lps::specification_base< LinearProcess, InitialProcessExpression >::m_action_labels

protected

The action specification of the specification.

Definition at line 57 of file specification.h.

◆ m_data

template<typename LinearProcess , typename InitialProcessExpression >

data::data_specification mcrl2::lps::specification_base< LinearProcess, InitialProcessExpression >::m_data

protected

The data specification of the specification.

Definition at line 54 of file specification.h.

◆ m_global_variables

template<typename LinearProcess , typename InitialProcessExpression >

std::set<data::variable> mcrl2::lps::specification_base< LinearProcess, InitialProcessExpression >::m_global_variables

protected

The set of global variables.

Definition at line 60 of file specification.h.

◆ m_initial_process

template<typename LinearProcess , typename InitialProcessExpression >

InitialProcessExpression mcrl2::lps::specification_base< LinearProcess, InitialProcessExpression >::m_initial_process

protected

The initial state of the specification.

Definition at line 66 of file specification.h.

◆ m_process

template<typename LinearProcess , typename InitialProcessExpression >

LinearProcess mcrl2::lps::specification_base< LinearProcess, InitialProcessExpression >::m_process

protected

The linear process of the specification.

Definition at line 63 of file specification.h.

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

lps/include/mcrl2/lps/specification.h

Public Types

Public Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ initial_process_type

◆ process_type

Constructor & Destructor Documentation

◆ specification_base() [1/2]

◆ specification_base() [2/2]

Member Function Documentation

◆ action_labels() [1/2]

◆ action_labels() [2/2]

◆ data() [1/2]

◆ data() [2/2]

◆ global_variables() [1/2]

◆ global_variables() [2/2]

◆ initial_process() [1/2]

◆ initial_process() [2/2]

◆ process() [1/2]

◆ process() [2/2]

Member Data Documentation

◆ m_action_labels

◆ m_data

◆ m_global_variables

◆ m_initial_process

◆ m_process