mcrl2::lps::linear_process_base< ActionSummand > Class Template Reference

#include <linear_process.h>

Public Types
using	action_summand_type = ActionSummand
	The action summand type.

Public Member Functions
	linear_process_base ()=default
	Constructor.
	linear_process_base (const data::variable_list &process_parameters, const deadlock_summand_vector &deadlock_summands, const std::vector< ActionSummand > &action_summands)
	Constructor.
	linear_process_base (const atermpp::aterm &lps, bool stochastic_distributions_allowed=true)
	Constructor.
std::size_t	summand_count () const
	Returns the number of LPS summands.
const std::vector< ActionSummand > &	action_summands () const
	Returns the sequence of action summands.
std::vector< ActionSummand > &	action_summands ()
	Returns the sequence of action summands.
const deadlock_summand_vector &	deadlock_summands () const
	Returns the sequence of deadlock summands.
deadlock_summand_vector &	deadlock_summands ()
	Returns the sequence of deadlock summands.
const data::variable_list &	process_parameters () const
	Returns the sequence of process parameters.
data::variable_list &	process_parameters ()
	Returns the sequence of process parameters.
bool	has_time () const
	Returns true if time is available in at least one of the summands.

Protected Attributes
data::variable_list	m_process_parameters
	The process parameters of the process.
deadlock_summand_vector	m_deadlock_summands
	The deadlock summands of the process.
std::vector< ActionSummand >	m_action_summands
	The action summands of the process.

Detailed Description

template<typename ActionSummand>
class mcrl2::lps::linear_process_base< ActionSummand >

Definition at line 59 of file linear_process.h.

Member Typedef Documentation

action_summand_type

template<typename ActionSummand >

using mcrl2::lps::linear_process_base< ActionSummand >::action_summand_type = ActionSummand

The action summand type.

Definition at line 73 of file linear_process.h.

Constructor & Destructor Documentation

linear_process_base() [1/3]

template<typename ActionSummand >

mcrl2::lps::linear_process_base< ActionSummand >::linear_process_base ( )

default

Constructor.

linear_process_base() [2/3]

template<typename ActionSummand >

mcrl2::lps::linear_process_base< ActionSummand >::linear_process_base ( const data::variable_list &  process_parameters, const deadlock_summand_vector &  deadlock_summands, const std::vector< ActionSummand > &  action_summands  )

inline

Constructor.

Definition at line 79 of file linear_process.h.

linear_process_base() [3/3]

template<typename ActionSummand >

mcrl2::lps::linear_process_base< ActionSummand >::linear_process_base ( const atermpp::aterm &  lps, bool  stochastic_distributions_allowed = true  )

inlineexplicit

Constructor.

Parameters

lps	A term.
stochastic_distributions_allowed	True when stochastic processes are allowed

Definition at line 92 of file linear_process.h.

Member Function Documentation

action_summands() [1/2]

template<typename ActionSummand >

std::vector< ActionSummand > & mcrl2::lps::linear_process_base< ActionSummand >::action_summands ( )

inline

Returns the sequence of action summands.

Returns

The sequence of action summands.

Definition at line 141 of file linear_process.h.

action_summands() [2/2]

template<typename ActionSummand >

const std::vector< ActionSummand > & mcrl2::lps::linear_process_base< ActionSummand >::action_summands ( ) const

inline

Returns the sequence of action summands.

Returns

The sequence of action summands.

Definition at line 134 of file linear_process.h.

deadlock_summands() [1/2]

template<typename ActionSummand >

deadlock_summand_vector & mcrl2::lps::linear_process_base< ActionSummand >::deadlock_summands ( )

inline

Returns the sequence of deadlock summands.

Returns

The sequence of deadlock summands.

Definition at line 155 of file linear_process.h.

deadlock_summands() [2/2]

template<typename ActionSummand >

const deadlock_summand_vector & mcrl2::lps::linear_process_base< ActionSummand >::deadlock_summands ( ) const

inline

Returns the sequence of deadlock summands.

Returns

The sequence of deadlock summands.

Definition at line 148 of file linear_process.h.

has_time()

template<typename ActionSummand >

bool mcrl2::lps::linear_process_base< ActionSummand >::has_time ( ) const

inline

Returns true if time is available in at least one of the summands.

Returns

True if time is available in at least one of the summands.

Definition at line 176 of file linear_process.h.

process_parameters() [1/2]

template<typename ActionSummand >

data::variable_list & mcrl2::lps::linear_process_base< ActionSummand >::process_parameters ( )

inline

Returns the sequence of process parameters.

Returns

The sequence of process parameters.

Definition at line 169 of file linear_process.h.

process_parameters() [2/2]

template<typename ActionSummand >

const data::variable_list & mcrl2::lps::linear_process_base< ActionSummand >::process_parameters ( ) const

inline

Returns the sequence of process parameters.

Returns

The sequence of process parameters.

Definition at line 162 of file linear_process.h.

summand_count()

template<typename ActionSummand >

std::size_t mcrl2::lps::linear_process_base< ActionSummand >::summand_count ( ) const

inline

Returns the number of LPS summands.

Returns

The number of LPS summands.

Definition at line 127 of file linear_process.h.

Member Data Documentation

m_action_summands

template<typename ActionSummand >

std::vector<ActionSummand> mcrl2::lps::linear_process_base< ActionSummand >::m_action_summands

protected

The action summands of the process.

Definition at line 69 of file linear_process.h.

m_deadlock_summands

template<typename ActionSummand >

deadlock_summand_vector mcrl2::lps::linear_process_base< ActionSummand >::m_deadlock_summands

protected

The deadlock summands of the process.

Definition at line 66 of file linear_process.h.

m_process_parameters

template<typename ActionSummand >

data::variable_list mcrl2::lps::linear_process_base< ActionSummand >::m_process_parameters

protected

The process parameters of the process.

Definition at line 63 of file linear_process.h.

---

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

• lps/include/mcrl2/lps/linear_process.h