Linear process specification. More...

#include <stochastic_specification.h>

Inheritance diagram for mcrl2::lps::stochastic_specification:

Public Member Functions
	stochastic_specification ()
	Constructor.

	stochastic_specification (const data::data_specification &data, const process::action_label_list &action_labels, const std::set< data::variable > &global_variables, const stochastic_linear_process &lps, const stochastic_process_initializer &initial_process)
	Constructor.

	stochastic_specification (const specification &other)
	Constructor. This constructor is explicit as implicit conversions of this kind is a source of bugs.

Public Member Functions inherited from mcrl2::lps::specification_base< stochastic_linear_process, stochastic_process_initializer >
	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 stochastic_linear_process &lps, const stochastic_process_initializer &initial_process)
	Constructor.

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

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

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

Protected Types
typedef specification_base< stochastic_linear_process, stochastic_process_initializer >	super

Additional Inherited Members
Public Types inherited from mcrl2::lps::specification_base< stochastic_linear_process, stochastic_process_initializer >
typedef stochastic_linear_process	process_type
	The process type.

typedef stochastic_process_initializer	initial_process_type
	The initial process type.

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

stochastic_linear_process	m_process
	The linear process of the specification.

stochastic_process_initializer	m_initial_process
	The initial state of the specification.

Detailed Description

Linear process specification.

Definition at line 35 of file stochastic_specification.h.

Member Typedef Documentation

◆ super

typedef specification_base<stochastic_linear_process, stochastic_process_initializer> mcrl2::lps::stochastic_specification::super

protected

Definition at line 38 of file stochastic_specification.h.

Constructor & Destructor Documentation

◆ stochastic_specification() [1/3]

mcrl2::lps::stochastic_specification::stochastic_specification ( )

inline

Constructor.

Definition at line 42 of file stochastic_specification.h.

◆ stochastic_specification() [2/3]

mcrl2::lps::stochastic_specification::stochastic_specification	(	const data::data_specification &	data,
		const process::action_label_list &	action_labels,
		const std::set< data::variable > &	global_variables,
		const stochastic_linear_process &	lps,
		const stochastic_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 51 of file stochastic_specification.h.

◆ stochastic_specification() [3/3]

mcrl2::lps::stochastic_specification::stochastic_specification ( const specification & other )

inlineexplicit

Constructor. This constructor is explicit as implicit conversions of this kind is a source of bugs.

Definition at line 62 of file stochastic_specification.h.

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

lps/include/mcrl2/lps/stochastic_specification.h

Public Member Functions

Protected Types