mcrl2::lps::specification_base< LinearProcess, InitialProcessExpression > Class Template Reference

#include <specification.h>

Public Types
using	process_type = LinearProcess
	The process type.
using	initial_process_type = InitialProcessExpression
	The initial process type.

Public Member Functions
	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 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 47 of file specification.h.

Member Typedef Documentation

initial_process_type

template<typename LinearProcess , typename InitialProcessExpression >

using mcrl2::lps::specification_base< LinearProcess, InitialProcessExpression >::initial_process_type = InitialProcessExpression

The initial process type.

Definition at line 70 of file specification.h.

process_type

template<typename LinearProcess , typename InitialProcessExpression >

using mcrl2::lps::specification_base< LinearProcess, InitialProcessExpression >::process_type = LinearProcess

The process type.

Definition at line 67 of file specification.h.

Constructor & Destructor Documentation

specification_base() [1/2]

template<typename LinearProcess , typename InitialProcessExpression >

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

default

Constructor.

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 81 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 135 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 127 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 119 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 112 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 149 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 142 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 163 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 156 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 105 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 98 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 54 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 51 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 57 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 63 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 60 of file specification.h.

---

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

• lps/include/mcrl2/lps/specification.h